Merge branch 'LagrangeDerivative' into ChebyshevExtremal

Author: YuvalFilmus

Mathlib/Algebra/Polynomial/Derivative.lean

@@ -652,55 +652,36 @@ theorem iterate_derivative_eq_zero_of_degree_lt {k : ℕ} {P : R[X]} (h : P.degr
 
 theorem iterate_derivative_prod_X_sub_C {k : ℕ} {S : Finset R} (hk : k ≤ #S) :
     derivative^[k] (∏ a ∈ S, (X - C a)) =
-    k.factorial * ∑ T ∈ S.powerset with #T = #S - k, ∏ a ∈ T, (X - C a):= by
+    k.factorial * ∑ T ∈ S.powersetCard (#S - k), ∏ a ∈ T, (X - C a):= by
   classical
   induction k
-  case zero =>
-    suffices {T ∈ S.powerset | #T = #S} = {S} by simp [this]
-    refine eq_singleton_iff_unique_mem.mpr ⟨by simp, fun T hT => ?_⟩
-    simp only [mem_filter, mem_powerset] at hT
-    exact Finset.eq_of_subset_of_card_le hT.1 (ge_of_eq hT.2)
+  case zero => simp
   case succ k ind =>
-    replace ind := ind (Nat.le_of_succ_le hk)
+    specialize ind (Nat.le_of_succ_le hk)
     nth_rewrite 1 [add_comm]
     rw [Function.iterate_add_apply, Function.iterate_one, ind, ← nsmul_eq_mul, derivative_smul,
       nsmul_eq_mul, derivative_sum, Nat.factorial_succ, mul_comm (k + 1), Nat.cast_mul, mul_assoc]
     congr 1
-    set r₁ : Set ((Finset R) × R) :=
-      { p : (Finset R) × R | p.1 ∈ S.powerset ∧ #(p.1) = #S - k ∧ p.2 ∈ p.1 } with hr₁
-    have : Fintype r₁ := by
-      refine Set.Finite.fintype (Set.finite_image_fst_and_snd_iff.mp ⟨?_, ?_⟩)
-      · exact Set.Finite.subset (Finite.of_fintype S.powerset) (by grind)
-      · exact Set.Finite.subset (Finite.of_fintype S) (by grind)
-    set r₂ : Set ((Finset R) × R) :=
-      {p : (Finset R) × R | p.1 ∈ S.powerset ∧ #(p.1) = #S - (k + 1) ∧ p.2 ∈ S \ p.1} with hr₂
-    have : Fintype r₂ := by
-      refine Set.Finite.fintype (Set.finite_image_fst_and_snd_iff.mp ⟨?_, ?_⟩)
-      · exact Set.Finite.subset (Finite.of_fintype S.powerset) (by grind)
-      · exact Set.Finite.subset (Finite.of_fintype S) (by grind)
     calc
-      ∑ T ∈ S.powerset with #T = #S - k, derivative (∏ a ∈ T, (X - C a)) =
-      ∑ T ∈ S.powerset with #T = #S - k, ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
+      ∑ T ∈ S.powersetCard (#S - k), derivative (∏ a ∈ T, (X - C a)) =
+      ∑ T ∈ S.powersetCard (#S - k), ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
         congr! with T hT
         simp_rw [derivative_prod_finset, derivative_X_sub_C, mul_one]
-      _ = ∑ p ∈ r₁.toFinset, ∏ a ∈ p.1.erase p.2, (X - C a) := by
+      _ = ∑ (T ∈ S.powersetCard (#S - k)) (i ∈ S) with i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
         rw [← sum_finset_product']
         grind
-      _ = ∑ p ∈ r₂.toFinset, ∏ a ∈ p.1, (X - C a) := by
-        apply sum_bij' (fun p hp => ⟨p.1.erase p.2, p.2⟩) (fun p hp => ⟨insert p.2 p.1, p.2⟩)
-        · intro r hr; congr 1; grind
-        · intro r hr; congr 1; grind
-        · simp
-        · grind
-        · grind
-      _ = ∑ T ∈ S.powerset with #T = #S - (k + 1), ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) := by
+      _ = ∑ (T ∈ S.powersetCard (#S - (k + 1))) (i ∈ S) with i ∉ T, ∏ a ∈ T, (X - C a) := by
+        apply sum_bij' (fun ⟨T, i⟩ _ => ⟨T.erase i, i⟩) (fun ⟨T, i⟩ _ => ⟨insert i T, i⟩)
+        · intro r hr; dsimp at hr ⊢; congr 1; grind
+        · intro r hr; dsimp at hr ⊢; congr 1; grind
+        all_goals grind
+      _ = ∑ T ∈ S.powersetCard (#S - (k + 1)), ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) := by
         rw [← sum_finset_product']
         grind
-      _ = (k + 1) * ∑ T ∈ S.powerset with #T = #S - (k + 1), ∏ a ∈ T, (X - C a) := by
+      _ = (k + 1) * ∑ T ∈ S.powersetCard (#S - (k + 1)), ∏ a ∈ T, (X - C a) := by
         rw [mul_sum]
         congr! 1 with T hT
-        have : #(S \ T) = k + 1 := by grind
-        simp [sum_const, this]
+        simp [sum_const, show #(S \ T) = k + 1 by grind]
       _ = _ := by grind
 
 end CommRing

Mathlib/Data/Finset/Powerset.lean

@@ -75,39 +75,16 @@ theorem powerset_eq_singleton_empty : s.powerset = {∅} ↔ s = ∅ := by
 
 theorem image_injOn_powerset_of_injOn {β : Type*} [DecidableEq β] {f : α → β} (H : Set.InjOn f s) :
     Set.InjOn (fun (x : Finset α) => x.image f) s.powerset := by
-  intro x hx y hy h
-  rw [mem_coe, mem_powerset] at hx hy
-  dsimp at h
-  ext a
-  by_cases a ∈ s
-  case pos ha =>
-    have {z : Finset α} (hz : z ⊆ s) : a ∈ z ↔ f a ∈ z.image f := by
-      refine ⟨fun b => mem_image_of_mem f b, fun h => ?_⟩
-      obtain ⟨b, hb₁, hb₂⟩ := mem_image.mp h
-      suffices b = a by rwa [this] at hb₁
-      exact (H.eq_iff (hz hb₁) ha).mp hb₂
-    rw [this hx, this hy, h]
-  case neg ha => tauto
+  have {z a} (_ : z ⊆ s) (_ : a ∈ s) : a ∈ z ↔ f a ∈ z.image f := by grind [H.eq_iff]
+  exact fun _ _ _ _ _ => by grind
 
 theorem image_surjOn_powerset {β : Type*} [DecidableEq β] {f : α → β} :
-    Set.SurjOn (fun (x : Finset α) => x.image f) s.powerset (s.image f).powerset := by
-  intro t ht
-  rw [mem_coe, mem_powerset] at ht
-  simp_rw [Set.mem_image, mem_coe, mem_powerset]
-  use { x ∈ s | f x ∈ t}
-  grind
+    Set.SurjOn (fun (x : Finset α) => x.image f) s.powerset (s.image f).powerset :=
+  fun t ht => ⟨{ x ∈ s | f x ∈ t}, by grind⟩
 
 theorem powerset_image {β : Type*} [DecidableEq β] {f : α → β} :
-    (s.image f).powerset = s.powerset.image (fun x => x.image f) := by
-  ext a
-  rw [mem_powerset, mem_image]
-  refine ⟨fun ha => ?_, fun ha => ?_⟩
-  · use { x ∈ s | f x ∈ a }
-    grind
-  · obtain ⟨b, hb₁, hb₂⟩ := ha
-    rw [mem_powerset] at hb₁
-    rw [← hb₂]
-    exact image_subset_image hb₁
+    (s.image f).powerset = s.powerset.image (fun x => x.image f) :=
+  ext fun a => ⟨fun _ => mem_image.mpr ⟨{ x ∈ s | f x ∈ a}, by grind⟩, by grind⟩
 
 /-- **Number of Subsets of a Set** -/
 @[simp]

Mathlib/LinearAlgebra/Lagrange.lean

@@ -460,7 +460,7 @@ theorem iterate_derivative_interpolate
     (hvs : Set.InjOn v s) {k : ℕ} (hk : k ≤ #s - 1) :
     derivative^[k] (interpolate s v r) = k.factorial *
       ∑ i ∈ s, C (r i / ∏ j ∈ s.erase i, ((v i) - (v j))) *
-      ∑ t ∈ (s.erase i).powerset with #t = #s - (k + 1),
+      ∑ t ∈ (s.erase i).powersetCard (#s - (k + 1)),
       ∏ a ∈ t, (X - C (v a)) := by
   classical
   simp_rw [interpolate_eq_sum, iterate_derivative_sum, iterate_derivative_C_mul, mul_sum (s := s),
@@ -471,88 +471,71 @@ theorem iterate_derivative_interpolate
     derivative^[k] (∏ j ∈ s.erase i, (X - C (v j))) =
     derivative^[k] (∏ vj ∈ (s.erase i).image v, (X - C vj)) := by
       rw [Finset.prod_image hvs']
-    _ = k.factorial * ∑ t ∈ ((s.erase i).image v).powerset with #t = #s - (k + 1),
+    _ = k.factorial * ∑ t ∈ ((s.erase i).image v).powersetCard (#s - (k + 1)),
       ∏ va ∈ t, (X - C va) := by
       have hcard : #((s.erase i).image v) = #s - 1 := by
         rw [card_image_of_injOn hvs', card_erase_of_mem hi]
-      have : k ≤ #((s.erase i).image v) := by rwa [hcard]
-      rw [iterate_derivative_prod_X_sub_C this]
-      congr! 5
+      rw [iterate_derivative_prod_X_sub_C (by rwa [hcard])]
+      congr! 3
       omega
-    _ = k.factorial * ∑ t ∈ (s.erase i).powerset with #t = #s - (k + 1),
+    _ = k.factorial * ∑ t ∈ (s.erase i).powersetCard (#s - (k + 1)),
       ∏ a ∈ t, (X - C (v a)) := by
-      rw [powerset_image, sum_nbij (fun (t : Finset ι) => t.image v)]
+      rw [powersetCard_eq_filter, powerset_image, sum_nbij (fun (t : Finset ι) => t.image v)]
       case hi =>
         intro a ha
-        rw [mem_filter, mem_powerset] at ha
+        rw [mem_powersetCard] at ha
         rw [mem_filter, mem_image]
-        constructor
-        · use a; simp [ha.1]
-        · rw [card_image_of_injOn (hvs'.mono (coe_subset.mpr ha.1))]
-          exact ha.2
-      case i_inj =>
-        refine (image_injOn_powerset_of_injOn hvs').mono (coe_subset.mpr ?_)
-        simp
+        refine ⟨⟨a, by simp [ha.1]⟩, ?_⟩
+        rw [card_image_of_injOn (hvs'.mono (by grind))]
+        exact ha.2
+      case i_inj => exact (image_injOn_powerset_of_injOn hvs').mono (by grind)
       case i_surj =>
         intro t ht
         rw [mem_coe, mem_filter, mem_image] at ht
         obtain ⟨a, ha⟩ := ht.1
-        simp_rw [Set.mem_image, mem_coe, mem_filter]
-        use a
-        refine ⟨⟨ha.1, ?_⟩, ha.2⟩
-        rw [← ht.2, ← ha.2, card_image_of_injOn (hvs'.mono (coe_subset.mpr (mem_powerset.mp ha.1)))]
+        simp_rw [Set.mem_image, mem_coe, mem_powersetCard]
+        refine ⟨a, ⟨⟨mem_powerset.mp ha.1, ?_⟩, ha.2⟩⟩
+        rw [← ht.2, ← ha.2, card_image_of_injOn (hvs'.mono (by grind))]
       case h =>
         intro a ha
-        rw [mem_filter, mem_powerset] at ha
-        rw [prod_image (hvs'.mono (coe_subset.mpr ha.1))]
-
-omit [DecidableEq ι] in
-private theorem degree_eq_of_card_eq {P : Polynomial F} (hP : #s = P.degree + 1) :
-    P.degree = ↑(s.card - 1) := by
-  cases h : P.degree
-  case bot => simp_all
-  case coe d =>
-    rw [Nat.cast_withBot] at hP ⊢
-    suffices #s = d + 1 by grind
-    rw [h] at hP
-    simp [← WithBot.coe_inj, hP]
-
-omit [DecidableEq ι] in
-private theorem natDegree_eq_of_card_eq {P : Polynomial F} (hP : #s = P.degree + 1) :
-    P.natDegree = s.card - 1 := natDegree_eq_of_degree_eq_some (degree_eq_of_card_eq hP)
-
-omit [DecidableEq ι] in
-private theorem degree_lt_of_card_eq {P : Polynomial F} (hP : #s = P.degree + 1) :
-    P.degree < s.card := by
-  have := degree_eq_of_card_eq hP
-  have := natDegree_eq_of_card_eq hP
-  have s_card : s.card > 0 := by by_contra! h; simp_all
-  grind [Nat.cast_lt]
+        convert (prod_image (hvs'.mono (coe_subset.mpr (mem_powersetCard.mp ha).1))).symm
+        rfl
 
 theorem eval_iterate_derivative_eq_sum
     (hvs : Set.InjOn v s) {P : Polynomial F} (hP : #s = P.degree + 1)
     {k : ℕ} (hk : k ≤ P.degree) (x : F) :
     (derivative^[k] P).eval x = k.factorial *
       ∑ i ∈ s, (P.eval (v i) / ∏ j ∈ s.erase i, ((v i) - (v j))) *
-      ∑ t ∈ (s.erase i).powerset with #t = #s - (k + 1),
+      ∑ t ∈ (s.erase i).powersetCard (#s - (k + 1)),
       ∏ a ∈ t, (x - v a) := by
-  rw (occs := [1]) [eq_interpolate hvs (degree_lt_of_card_eq hP)]
-  rw [iterate_derivative_interpolate, ← nsmul_eq_mul, eval_smul, nsmul_eq_mul, eval_finset_sum]
-  · congr! 2 with i hi
-    simp_rw [eval_C_mul, eval_finset_sum, eval_prod, eval_sub, eval_X, eval_C]
-  · exact hvs
-  · rw [degree_eq_of_card_eq hP] at hk
-    exact WithBot.coe_le_coe.mp hk
+  lift P.degree to ℕ using (by contrapose! hP; rw [hP]; simp) with deg hdeg
+  rw [← WithBot.coe_one, ← WithBot.coe_add] at hP
+  replace hP := WithBot.coe_eq_coe.mp hP
+  have hdegree : P.degree = ↑(#s - 1) := hdeg.symm.trans (WithBot.coe_eq_coe.mpr (by grind))
+  rw (occs := [1]) [eq_interpolate hvs (f := P)]
+  · rw [iterate_derivative_interpolate, ← nsmul_eq_mul, eval_smul, nsmul_eq_mul, eval_finset_sum]
+    · congr! 2 with i hi
+      simp_rw [eval_C_mul, eval_finset_sum, eval_prod, eval_sub, eval_X, eval_C]
+    · exact hvs
+    · exact WithBot.coe_le_coe.mp (le_of_le_of_eq hk (by rwa [hdeg]))
+  · exact lt_of_eq_of_lt hdeg.symm (WithBot.coe_lt_coe.mpr <|
+      lt_of_lt_of_eq (lt_add_one deg) hP.symm)
 
 theorem leadingCoeff_eq_sum
     (hvs : Set.InjOn v s) {P : Polynomial F} (hP : #s = P.degree + 1) :
     P.leadingCoeff = ∑ i ∈ s, (P.eval (v i)) / ∏ j ∈ s.erase i, ((v i) - (v j)) := by
-  rw [leadingCoeff, natDegree_eq_of_card_eq hP]
-  rw (occs := [1]) [eq_interpolate hvs (degree_lt_of_card_eq hP)]
-  rw [interpolate_apply, finset_sum_coeff]
-  congr! with i hi
-  rw [coeff_C_mul, ← natDegree_basis hvs hi, ← leadingCoeff, leadingCoeff_basis hvs hi]
-  field_simp
+  lift P.degree to ℕ using (by contrapose! hP; rw [hP]; simp) with deg hdeg
+  rw [← WithBot.coe_one, ← WithBot.coe_add] at hP
+  replace hP := WithBot.coe_eq_coe.mp hP
+  have hdegree : P.degree = ↑(#s - 1) := hdeg.symm.trans (WithBot.coe_eq_coe.mpr (by grind))
+  rw [leadingCoeff, natDegree_eq_of_degree_eq_some hdegree]
+  rw (occs := [1]) [eq_interpolate (f := P) hvs]
+  · rw [interpolate_apply, finset_sum_coeff]
+    congr! with i hi
+    rw [coeff_C_mul, ← natDegree_basis hvs hi, ← leadingCoeff, leadingCoeff_basis hvs hi]
+    field_simp
+  · exact lt_of_eq_of_lt hdeg.symm (WithBot.coe_lt_coe.mpr <|
+      lt_of_lt_of_eq (lt_add_one deg) hP.symm)
 
 end Interpolate