Fix warnings

FormalBook/Ch28/BrouwerCovering.lean

@@ -21,7 +21,7 @@ private def acLoop : Path acBase acBase where
     show QuotientAddGroup.mk (1 : ℝ) = QuotientAddGroup.mk 0
     rw [QuotientAddGroup.eq]; simp
 
-private def acCov : IsCoveringMap (QuotientAddGroup.mk : ℝ → AddCircle (1 : ℝ)) :=
+private theorem acCov : IsCoveringMap (QuotientAddGroup.mk : ℝ → AddCircle (1 : ℝ)) :=
   AddCircle.isCoveringMap_coe 1
 
 private theorem acLoop_lift_eq :
@@ -245,7 +245,7 @@ private theorem retraction_from_fp_free {f : ℂ → ℂ}
 private theorem brouwer_complex
     (f : ℂ → ℂ) (hf : Continuous f) (hB : ∀ x, ‖x‖ ≤ 1 → ‖f x‖ ≤ 1) :
     ∃ x, ‖x‖ ≤ 1 ∧ f x = x := by
-  by_contra h; push_neg at h
+  by_contra h; push Not at h
   have hfp : ∀ x, ‖x‖ ≤ 1 → f x ≠ x := fun x hx hfx => (h x hx hfx).elim
   exact no_retraction_complex (retraction_from_fp_free hf hB hfp)
 

FormalBook/Ch28/SpernerBrouwer.lean

@@ -135,7 +135,7 @@ vertex extraction) below; `sperner_coloring_rainbow_triangles` is proved modulo
 
 /-- The standard 2-simplex equals Mathlib's `stdSimplex`. -/
 private theorem stdSimplex2_eq : stdSimplex2 = stdSimplex ℝ (Fin 3) := by
-  ext x; simp only [stdSimplex2, stdSimplex, Set.mem_setOf_eq]
+  ext x; simp only [stdSimplex2, stdSimplex, Set.mem_ofPred_eq]
 
 /-- The standard 2-simplex is compact. -/
 private theorem stdSimplex2_isCompact : IsCompact stdSimplex2 := by
@@ -146,14 +146,14 @@ private theorem stdSimplex2_isCompact : IsCompact stdSimplex2 := by
 private theorem spernerColor_exists {f : (Fin 3 → ℝ) → (Fin 3 → ℝ)}
     {v : Fin 3 → ℝ} (hv : v ∈ stdSimplex2) (hfv : f v ∈ stdSimplex2)
     (hne : f v ≠ v) : ∃ i : Fin 3, f v i < v i := by
-  by_contra h; push_neg at h
+  by_contra h; push Not at h
   have hsum_v := hv.2; have hsum_fv := hfv.2
   have : ∀ i, f v i = v i := by
     intro i
     have hle_sum : ∑ j, v j ≤ ∑ j, f v j := Finset.sum_le_sum (fun j _ => h j)
     rw [hsum_v, hsum_fv] at hle_sum
     have hge : f v i ≤ v i := by
-      by_contra hlt; push_neg at hlt
+      by_contra hlt; push Not at hlt
       have : ∑ j, v j < ∑ j, f v j :=
         Finset.sum_lt_sum (fun j _ => h j) ⟨i, Finset.mem_univ _, hlt⟩
       linarith
@@ -167,7 +167,7 @@ private theorem spernerColor_boundary {f : (Fin 3 → ℝ) → (Fin 3 → ℝ)}
     (hne : f v ≠ v) : spernerColor f v ≠ j := by
   have hex := spernerColor_exists hv hfv hne
   intro heq
-  unfold spernerColor at heq; rw [dif_pos hex] at heq
+  unfold spernerColor at heq; rw [dite_eq_left hex] at heq
   have hchoose := hex.choose_spec
   rw [heq] at hchoose
   rw [hvj] at hchoose; linarith [hfv.1 j]
@@ -201,7 +201,7 @@ private instance subdivVertDecEq (k : ℕ) : DecidableEq (SubdivVert k) :=
 
 /-- The coordinate map: send a subdivision vertex to its barycentric point in Δ². -/
 @[nolint unusedArguments]
-private noncomputable def subdivCoord (k : ℕ) (hk : 0 < k) (v : SubdivVert k) : Fin 3 → ℝ :=
+private noncomputable def subdivCoord (k : ℕ) (_hk : 0 < k) (v : SubdivVert k) : Fin 3 → ℝ :=
   fun i => (v.1 i : ℝ) / (k : ℝ)
 
 private theorem subdivCoord_mem (k : ℕ) (hk : 0 < k) (v : SubdivVert k) :
@@ -290,7 +290,7 @@ private noncomputable def subdivTriangulation (k : ℕ) (_hk : 0 < k) :
   have mkVert_coord0 : ∀ a b (h : a + b ≤ k), (mkVert a b h).1 0 = a := by
     intro a b h; simp [mkVert, Matrix.cons_val_zero]
   have mkVert_coord1 : ∀ a b (h : a + b ≤ k), (mkVert a b h).1 1 = b := by
-    intro a b h; simp [mkVert, Matrix.cons_val_one, Matrix.head_cons]
+    intro a b h; simp [mkVert, Matrix.cons_val_one]
   have hcard : ∀ t ∈ allTris, t.card = 3 := by
     intro t ht
     simp only [allTris, Finset.mem_biUnion, Finset.mem_univ, true_and] at ht
@@ -316,7 +316,7 @@ private noncomputable def subdivTriangulation (k : ℕ) (_hk : 0 < k) :
         rw [Finset.card_insert_of_notMem, Finset.card_insert_of_notMem, Finset.card_singleton]
         · simp; exact he12
         · simp only [Finset.mem_insert, Finset.mem_singleton]
-          push_neg; exact ⟨he01, he02⟩
+          push Not; exact ⟨he01, he02⟩
       · -- Down triangle: (i+1,j), (i,j+1), (i+1,j+1)
         have h01 : mkVert (i+1) j (by omega) ≠ mkVert i (j+1) (by omega) := by
           intro h; have := congr_arg (fun v => v.1 0) h; simp [mkVert_coord0] at this
@@ -333,7 +333,7 @@ private noncomputable def subdivTriangulation (k : ℕ) (_hk : 0 < k) :
         rw [Finset.card_insert_of_notMem, Finset.card_insert_of_notMem, Finset.card_singleton]
         · simp; exact he12
         · simp only [Finset.mem_insert, Finset.mem_singleton]
-          push_neg; exact ⟨he01, he02⟩
+          push Not; exact ⟨he01, he02⟩
     · simp at hcond
   refine ⟨m, ⟨allTris, hcard⟩, decode, ?_⟩
   -- Adjacency: any two vertices in the same triangle differ by ≤ 1 in each coordinate
@@ -357,11 +357,11 @@ private noncomputable def subdivTriangulation (k : ℕ) (_hk : 0 < k) :
     · -- Up triangle: mkVert ii jj, mkVert (ii+1) jj, mkVert ii (jj+1)
       rcases hda with ha' | ha' | ha' <;> rcases hdb with hb' | hb' | hb' <;>
         (simp only [Set.mem_Icc]; rw [ha', hb']; fin_cases idx <;>
-          simp [mkVert, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons] <;> omega)
+          simp [mkVert, Matrix.cons_val_zero, Matrix.cons_val_one] <;> omega)
     · -- Down triangle: mkVert (ii+1) jj, mkVert ii (jj+1), mkVert (ii+1) (jj+1)
       rcases hda with ha' | ha' | ha' <;> rcases hdb with hb' | hb' | hb' <;>
         (simp only [Set.mem_Icc]; rw [ha', hb']; fin_cases idx <;>
-          simp [mkVert, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons] <;> omega)
+          simp [mkVert, Matrix.cons_val_zero, Matrix.cons_val_one] <;> omega)
   · simp at hcond
 
 /-! ### Boundary parity for Sperner coloring
@@ -413,7 +413,7 @@ private lemma transitions_parity_nat : ∀ (m : ℕ) (f : Fin (m + 1) → Bool),
     have hlast_cs : f (Fin.last m).castSucc = f ⟨m, by omega⟩ :=
       congrArg f (by simp [Fin.last, Fin.castSucc])
     have hlast_succ : f (Fin.last m).succ = f ⟨m + 1, by omega⟩ :=
-      congrArg f (by simp [Fin.last, Fin.val_succ])
+      congrArg f (by simp [Fin.last])
     rw [hlast_cs, hlast_succ]
     rcases Bool.eq_false_or_eq_true (f 0) with h0 | h0 <;>
     rcases Bool.eq_false_or_eq_true (f (⟨m, by omega⟩ : Fin (m + 2))) with hm | hm <;>
@@ -433,14 +433,14 @@ private lemma odd_transitions (n : ℕ) (s : Fin (n + 1) → Bool)
 
 @[nolint unusedArguments]
 private theorem subdivSperner_odd_sum
-    (f : (Fin 3 → ℝ) → (Fin 3 → ℝ)) (hfS : ∀ x ∈ stdSimplex2, f x ∈ stdSimplex2)
-    (hne : ∀ x ∈ stdSimplex2, f x ≠ x)
-    (k : ℕ) (hk : 0 < k)
+    (f : (Fin 3 → ℝ) → (Fin 3 → ℝ)) (_hfS : ∀ x ∈ stdSimplex2, f x ∈ stdSimplex2)
+    (_hne : ∀ x ∈ stdSimplex2, f x ≠ x)
+    (k : ℕ) (_hk : 0 < k)
     (m : ℕ) (T : Triangulation m) (decode : Fin m → SubdivVert k)
-    (hadj : ∀ t ∈ T.triangles, ∀ a ∈ t, ∀ b ∈ t,
+    (_hadj : ∀ t ∈ T.triangles, ∀ a ∈ t, ∀ b ∈ t,
       ∀ i, ((decode a).1 i : ℤ) - ((decode b).1 i : ℤ) ∈ Set.Icc (-1 : ℤ) 1)
     (col : Fin m → Fin 3)
-    (hcol_boundary : ∀ v j, (decode v).1 j = 0 → col v ≠ j)
+    (_hcol_boundary : ∀ v j, (decode v).1 j = 0 → col v ≠ j)
     (h_odd_sum_hyp : Odd (∑ t ∈ T.triangles,
       (t.filter (fun v => col v = 1)).card * (t.filter (fun v => col v = 2)).card)) :
     ∃ count12 : Finset (Fin m) → ℕ,
@@ -528,7 +528,7 @@ private theorem rainbow_triangle_gives_vertices
     (hne : ∀ x ∈ stdSimplex2, f x ≠ x)
     (k : ℕ) (hk : 0 < k) (m : ℕ) (T : Triangulation m) (decode : Fin m → SubdivVert k)
     (col : Fin m → Fin 3) (t : Finset (Fin m)) (ht : t ∈ T.triangles)
-    (hcard : t.card = 3) (hrainbow : isRainbow col t)
+    (_hcard : t.card = 3) (hrainbow : isRainbow col t)
     (hcol_def : ∀ v, col v = spernerColor f (subdivCoord k hk (decode v)))
     (hadj : ∀ t ∈ T.triangles, ∀ a ∈ t, ∀ b ∈ t,
       ∀ i, ((decode a).1 i : ℤ) - ((decode b).1 i : ℤ) ∈ Set.Icc (-1 : ℤ) 1) :
@@ -555,21 +555,20 @@ private theorem rainbow_triangle_gives_vertices
   · -- f (v i) i < (v i) i
     intro i
     have hcol_i : col (vert i) = i := by
-      fin_cases i <;> simp only [vert, Matrix.cons_val_zero, Matrix.cons_val_one,
-        Matrix.head_cons] <;> assumption
+      fin_cases i <;> simp [vert] <;> assumption
     rw [hcol_def] at hcol_i
     unfold spernerColor at hcol_i
     split_ifs at hcol_i with hex
     · have := hex.choose_spec; rw [hcol_i] at this; exact this
     · -- ¬∃ j, f v j < v j means f(v) ≥ v componentwise, and ∑ = 1 forces f(v) = v.
       -- But hne says f(v) ≠ v, contradiction.
-      push_neg at hex
+      push Not at hex
       have hv_mem := subdivCoord_mem k hk (decode (vert i))
       have hfv_mem := hfS _ hv_mem
       have heq : f (subdivCoord k hk (decode (vert i))) = subdivCoord k hk (decode (vert i)) := by
         ext j
         exact le_antisymm (by
-          by_contra hlt; push_neg at hlt
+          by_contra hlt; push Not at hlt
           have : ∑ l, f (subdivCoord k hk (decode (vert i))) l >
                  ∑ l, subdivCoord k hk (decode (vert i)) l :=
             Finset.sum_lt_sum (fun l _ => hex l)
@@ -585,11 +584,9 @@ private theorem rainbow_triangle_gives_vertices
     apply subdivCoord_dist
     intro idx
     have hvi : vert i ∈ t := by
-      fin_cases i <;> simp [vert, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons] <;>
-        assumption
+      fin_cases i <;> simp [vert] <;> assumption
     have hvj : vert j ∈ t := by
-      fin_cases j <;> simp [vert, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons] <;>
-        assumption
+      fin_cases j <;> simp [vert] <;> assumption
     exact hadj t ht (vert i) hvi (vert j) hvj idx
 
 /-- **Geometric Sperner:** For each k ≥ 1, the Sperner coloring of the k-th regular
@@ -736,7 +733,7 @@ private theorem brouwer_fixed_point_simplex2_sperner
     ∃ x ∈ stdSimplex2, f x = x := by
   -- Use contradiction: assume no fixed point, then spernerColor is always well-defined
   by_contra hno
-  push_neg at hno
+  push Not at hno
   have hne : ∀ x ∈ stdSimplex2, f x ≠ x := by
     intro x hx heq; exact hno x hx heq
   -- For each k ≥ 1, get rainbow triangle vertices
@@ -752,7 +749,7 @@ private theorem brouwer_fixed_point_simplex2_sperner
   suffices hle : ∀ i, f xstar i ≤ xstar i by
     have heq : f xstar = xstar := by
       ext i; exact le_antisymm (hle i) (by
-        by_contra hlt; push_neg at hlt
+        by_contra hlt; push Not at hlt
         have : ∑ j, f xstar j < ∑ j, xstar j :=
           Finset.sum_lt_sum (fun j _ => hle j) ⟨i, Finset.mem_univ _, hlt⟩
         linarith [hfxstar_mem.2, hxstar_mem.2])

FormalBook/Ch30/EKRAuxiliary.lean

@@ -98,7 +98,7 @@ lemma arc_lemma {n k : ℕ} (h2k : 2 * k ≤ n) (S : Finset (Fin n))
   · obtain ⟨i₀, hi₀⟩ := hne; exact absurd (hS i₀ hi₀ i₀ hi₀) (by simp [circularArc])
   have hkn : k ≤ n := by omega
   obtain ⟨i₀, hi₀⟩ := hne
-  haveI : NeZero n := ⟨by omega⟩
+  have : NeZero n := ⟨by omega⟩
   let f : Fin n → ℕ := fun s =>
     let d := (s - i₀).val
     if d < k then d else d - (n - k)

FormalBook/Chapter_01.lean

@@ -197,7 +197,7 @@ noncomputable def invRealHom : ℕ →*₀ ℝ :=
 
 lemma S1_eq_smoothNumbers (x : ℝ) : S₁ x = Nat.smoothNumbers (⌊x⌋₊ + 1) := by
   ext n
-  simp only [S₁, Nat.smoothNumbers, Set.mem_setOf_eq]
+  simp only [S₁, Nat.smoothNumbers, Set.mem_ofPred_eq]
   constructor
   · intro hn
     have hn0 : n ≠ 0 := by
@@ -367,7 +367,7 @@ theorem euler_product_rearrangement (x: ℝ) (n: ℕ) (hxge : x ≥ n) (hxlt : x
         intro he0; subst he0; exact he (Finset.mem_singleton_self 0)
       have pnin : (p : ℕ)^e ∉ S₁ x := by
         intro h
-        simp only [S₁, Set.mem_setOf_eq] at h
+        simp only [S₁, Set.mem_ofPred_eq] at h
         have h_dvd : (p : ℕ) ∣ (p : ℕ)^e := dvd_pow_self _ enz
         have hle : (p : ℝ) ≤ x := h (p : ℕ) pprime h_dvd
         have : (p : ℕ) ≤ ⌊x⌋ := Int.le_floor.mpr hle
@@ -465,7 +465,7 @@ theorem sum_le_infinite_sum (x: ℝ) (n: ℕ) (hxge : x ≥ n) (hxlt : x < n + 1
 
   . have: i ∈ Set.Icc 1 n ∨ i ∉ Set.Icc 1 n := by exact Decidable.em (i ∈ Set.Icc 1 n)
     rcases this with (case | case)
-    . simp [case]
+    . simp
       have: i ∈ S₁ x := by {
         unfold S₁
         have i_lt_n: i ≤ n := by simp_all only [ge_iff_le, Set.mem_Icc]
@@ -478,18 +478,18 @@ theorem sum_le_infinite_sum (x: ℝ) (n: ℕ) (hxge : x ≥ n) (hxlt : x < n + 1
 
           bound
         }
-        rewrite [Set.mem_setOf]
+        rewrite [Set.mem_ofPred]
         assumption
       }
-      simp_all only [ge_iff_le, Set.mem_Icc, Set.indicator_of_mem, le_refl]
+      simp_all only [ge_iff_le, Set.mem_Icc]
       sorry
-    . simp [case]
+    . simp
       clear case
       have: i ∈ (S₁ x) ∨ i ∉ S₁ x := by exact Decidable.em (i ∈ S₁ x)
       rcases this with (case | case)
-      . simp_all only [ge_iff_le, Set.indicator_of_mem, inv_nonneg, cast_nonneg]
+      . simp_all only [ge_iff_le]
         sorry
-      . simp_all only [ge_iff_le, not_false_eq_true, Set.indicator_of_notMem, le_refl]
+      . simp_all only [ge_iff_le]
         sorry
 }
 
@@ -534,7 +534,7 @@ theorem geom_series_simp (n : ℕ) (x : ℝ) (hxge : x ≥ n) (hxlt : x < n + 1)
     clear this
     apply Finset.prod_image
     intros i hi j hj hij
-    have := Nat.nth_injective (Nat.infinite_setOf_prime) hij
+    have := Nat.nth_injective (Nat.infinite_setOfPred_prime) hij
     assumption
   }
   rewrite [this]
@@ -588,7 +588,7 @@ lemma prime_counting_lemma (x : ℝ) :
       have h_term_le : ∀ k ∈ Finset.Icc 1 (primeCountingReal x), ((Nat.nth Nat.Prime k : ℝ) / ((Nat.nth Nat.Prime k) - 1)) ≤ ((k + 1) : ℝ) / (k : ℝ) := by
         intro k hk; rw [ div_le_div_iff₀ ] <;> norm_num;
         · norm_cast;
-          rw [ Int.subNatNat_eq_coe ] ; push_cast ; nlinarith [ Nat.Prime.one_lt ( Nat.prime_nth_prime k ), show Nat.nth Nat.Prime k ≥ k + 1 from Nat.recOn k ( Nat.Prime.pos ( Nat.prime_nth_prime 0 ) ) fun n ihn => Nat.succ_le_of_lt ( Nat.lt_of_le_of_lt ihn ( Nat.nth_strictMono ( Nat.infinite_setOf_prime ) ( Nat.lt_succ_self _ ) ) ) ];
+          rw [ Int.subNatNat_eq_coe ] ; push_cast ; nlinarith [ Nat.Prime.one_lt ( Nat.prime_nth_prime k ), show Nat.nth Nat.Prime k ≥ k + 1 from Nat.recOn k ( Nat.Prime.pos ( Nat.prime_nth_prime 0 ) ) fun n ihn => Nat.succ_le_of_lt ( Nat.lt_of_le_of_lt ihn ( Nat.nth_strictMono ( Nat.infinite_setOfPred_prime ) ( Nat.lt_succ_self _ ) ) ) ];
         · exact Nat.Prime.one_lt ( Nat.prime_nth_prime k );
         · linarith [ Finset.mem_Icc.mp hk ];
       exact Finset.prod_le_prod ( fun _ _ => div_nonneg ( Nat.cast_nonneg _ ) ( sub_nonneg.mpr ( Nat.one_le_cast.mpr ( Nat.Prime.pos ( Nat.prime_nth_prime _ ) ) ) ) ) h_term_le
@@ -685,7 +685,7 @@ theorem infinity_of_primes₅ : { p : ℕ | p.Prime }.Infinite := by
       obtain ⟨b₂, hb₂, hNab₂⟩ := hO₂ a haO₂
       refine ⟨b₁*b₂, mul_pos hb₁ hb₂,
         Set.subset_inter (subset_trans ?_ hNab₁) (subset_trans ?_ hNab₂)⟩
-      <;> simp only [N, Set.setOf_subset_setOf, forall_exists_index, forall_apply_eq_imp_iff,
+      <;> simp only [N, Set.ofPred_subset_ofPred, forall_exists_index, forall_apply_eq_imp_iff,
         add_right_inj]
       · refine fun k ↦ ⟨b₂*k, by ring⟩
       · refine fun k ↦ ⟨b₁*k, by ring⟩
@@ -706,7 +706,7 @@ theorem infinity_of_primes₅ : { p : ℕ | p.Prime }.Infinite := by
 
   have IsClosed_N (a b : ℤ) (hb : 0 < b) : IsClosed (N a b):= by
     refine isOpen_compl_iff.1 (Or.inr fun n hn ↦ ⟨b, hb, fun k hk ↦ ?_⟩)
-    simp only [N, Set.mem_compl_iff, Set.mem_setOf_eq, not_exists] at *
+    simp only [N, Set.mem_compl_iff, Set.mem_ofPred_eq, not_exists] at *
     intro b₁ hb₁
     obtain ⟨m, hm⟩ := hk
     apply hn (b₁ - m)
@@ -726,7 +726,7 @@ theorem infinity_of_primes₅ : { p : ℕ | p.Prime }.Infinite := by
       rw [Int.ofNat_dvd_left]
       exact (Nat.minFac_dvd (Int.natAbs n))
     ext n
-    simp only [Set.mem_setOf_eq, N, zero_add, Set.mem_iUnion, exists_prop, Int.reduceNeg,
+    simp only [Set.mem_ofPred_eq, N, zero_add, Set.mem_iUnion, exists_prop, Int.reduceNeg,
       Set.mem_compl_iff, Set.mem_insert_iff, Set.mem_singleton_iff, not_or]
     constructor
     · intro ⟨p, hp, ⟨k, hk⟩⟩

FormalBook/Chapter_04.lean

@@ -136,7 +136,7 @@ variable (k : ℕ)
 
 /-- The linear involution `(x, y, z) ↦ (y, x, -z)`. -/
 def linearInvo : Function.End (S k) := fun ⟨⟨x, y, z⟩, h⟩ => ⟨⟨y, x, -z⟩, by
-  simp only [S, Set.mem_setOf_eq] at h ⊢
+  simp only [S, Set.mem_ofPred_eq] at h ⊢
   exact ⟨by linarith [h], h.2.2, h.2.1⟩ ⟩
 
 theorem linearInvo_sq : linearInvo k ^ 2 = (1 : Function.End (S k)) := by
@@ -149,7 +149,7 @@ theorem linearInvo_sq : linearInvo k ^ 2 = (1 : Function.End (S k)) := by
   ext <;> simp
 
 theorem linearInvo_no_fixedPoints : IsEmpty (fixedPoints (linearInvo k)) := by
-  simp only [isEmpty_subtype, mem_fixedPoints, Subtype.forall, Prod.forall]
+  simp only [isEmpty_subtype, Subtype.forall, Prod.forall]
   intro x y z h hfixed
   have hfixed' : (linearInvo k ⟨⟨x, y, z⟩, h⟩).1.2.2 = z := by rw [hfixed]
   have : -z = z := hfixed'
@@ -188,7 +188,7 @@ def secondInvo : Function.End (U k) := fun ⟨⟨⟨x, y, z⟩, hS⟩, h⟩ =>
   · rw [← hS.1]; ring
   refine ⟨h, hS.2.2⟩
   ⟩, by
-    simp only [U, gt_iff_lt, secondInvo_fun, Set.mem_setOf_eq]
+    simp only [U, gt_iff_lt, secondInvo_fun, Set.mem_ofPred_eq]
     ring_nf
     exact hS.2.1⟩
 
@@ -307,6 +307,6 @@ def toTriple := fun (xyz : ℤ × ℤ × ℤ) ↦
 
 -- The second winged derived from the windeg shape of are 73 using `secondInvo`:
 
-#eval secondInvo_fun xyz
+-- #eval secondInvo_fun xyz
 
 #widget WindmillWidget with ({triple? := (toTriple <| secondInvo_fun xyz)} : WindmillWidgetProps)