bump to nightly-2024-02-01-06

mathlib commit leanprover-community/mathlib@65a1391

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -401,6 +401,45 @@ theorem ballot_neg (p q : ℕ) (qp : q < p) :
 theorem ballot_problem' :
     ∀ q p, q < p → (condCount (countedSequence p q) staysPositive).toReal = (p - q) / (p + q) := by
   classical
+  apply Nat.diag_induction
+  · intro p
+    rw [ballot_same]
+    simp
+  · intro p
+    rw [ballot_edge]
+    simp only [ENNReal.one_toReal, Nat.cast_add, Nat.cast_one, Nat.cast_zero, sub_zero, add_zero]
+    rw [div_self]
+    exact Nat.cast_add_one_ne_zero p
+  · intro q p qp h₁ h₂
+    haveI :=
+      cond_count_is_probability_measure (counted_sequence_finite p (q + 1))
+        (counted_sequence_nonempty _ _)
+    haveI :=
+      cond_count_is_probability_measure (counted_sequence_finite (p + 1) q)
+        (counted_sequence_nonempty _ _)
+    have h₃ : p + 1 + (q + 1) > 0 := Nat.add_pos_left (Nat.succ_pos _) _
+    rw [← cond_count_add_compl_eq {l : List ℤ | l.headI = 1} _ (counted_sequence_finite _ _),
+      first_vote_pos _ _ h₃, first_vote_neg _ _ h₃, ballot_pos, ballot_neg _ _ qp]
+    rw [ENNReal.toReal_add, ENNReal.toReal_mul, ENNReal.toReal_mul, ← Nat.cast_add,
+      ENNReal.toReal_div, ENNReal.toReal_div, ENNReal.toReal_nat, ENNReal.toReal_nat,
+      ENNReal.toReal_nat, h₁, h₂]
+    · have h₄ : ↑(p + 1) + ↑(q + 1) ≠ (0 : ℝ) :=
+        by
+        apply ne_of_gt
+        assumption_mod_cast
+      have h₅ : ↑(p + 1) + ↑q ≠ (0 : ℝ) := by
+        apply ne_of_gt
+        norm_cast
+        linarith
+      have h₆ : ↑p + ↑(q + 1) ≠ (0 : ℝ) := by
+        apply ne_of_gt
+        norm_cast
+        linarith
+      field_simp [h₄, h₅, h₆] at *
+      ring
+    all_goals
+      refine' (ENNReal.mul_lt_top (measure_lt_top _ _).Ne _).Ne
+      simp [Ne.def, ENNReal.div_eq_top]
 #align ballot.ballot_problem' Ballot.ballot_problem'
 
 /-- The ballot problem. -/

Archive/Wiedijk100Theorems/CubingACube.lean

@@ -503,6 +503,48 @@ theorem valley_mi : Valley cs (cs (mi h v)).shiftUp :=
   · intro p; apply h.shift_up_bottom_subset_bottoms mi_xm_ne_one
   · rintro i' hi' ⟨p2, hp2, h2p2⟩; simp only [head_shift_up] at hi' 
     classical
+    by_contra h2i'
+    rw [tail_shift_up] at h2p2 
+    simp only [not_subset, tail_shift_up] at h2i' 
+    rcases h2i' with ⟨p1, hp1, h2p1⟩
+    have : ∃ p3, p3 ∈ (cs i').tail.to_set ∧ p3 ∉ (cs i).tail.to_set ∧ p3 ∈ c.tail.to_set :=
+      by
+      simp only [to_set, Classical.not_forall, mem_set_of_eq] at h2p1 ; cases' h2p1 with j hj
+      rcases Ico_lemma (mi_not_on_boundary' j).1 (by simp [hw]) (mi_not_on_boundary' j).2
+          (le_trans (hp2 j).1 <| le_of_lt (h2p2 j).2) (le_trans (h2p2 j).1 <| le_of_lt (hp2 j).2)
+          ⟨hj, hp1 j⟩ with
+        ⟨w, hw, h2w, h3w⟩
+      refine' ⟨fun j' => if j' = j then w else p2 j', _, _, _⟩
+      · intro j'; by_cases h : j' = j
+        · simp only [if_pos h]; convert h3w
+        · simp only [if_neg h]; exact hp2 j'
+      · simp only [to_set, Classical.not_forall, mem_set_of_eq]; use j; rw [if_pos rfl]; convert h2w
+      · intro j'; by_cases h : j' = j
+        · simp only [if_pos h, side_tail]; convert hw
+        · simp only [if_neg h]; apply hi.2; apply h2p2
+    rcases this with ⟨p3, h1p3, h2p3, h3p3⟩
+    let p := @cons n (fun _ => ℝ) (c.b 0) p3
+    have hp : p ∈ c.bottom := by refine' ⟨rfl, _⟩; rwa [tail_cons]
+    rcases v.1 hp with ⟨_, ⟨i'', rfl⟩, hi''⟩
+    have h2i'' : i'' ∈ bcubes cs c := by
+      use hi''.1.symm; apply v.2.1 i'' hi''.1.symm
+      use tail p; constructor; exact hi''.2; rw [tail_cons]; exact h3p3
+    have h3i'' : (cs i).w < (cs i'').w := by apply mi_strict_minimal _ h2i''; rintro rfl;
+      apply h2p3; convert hi''.2; rw [tail_cons]
+    let p' := @cons n (fun _ => ℝ) (cs i).xm p3
+    have hp' : p' ∈ (cs i').to_set := by simpa [to_set, forall_fin_succ, p', hi'.symm] using h1p3
+    have h2p' : p' ∈ (cs i'').to_set :=
+      by
+      simp only [to_set, forall_fin_succ, p', cons_succ, cons_zero, mem_set_of_eq]
+      refine' ⟨_, by simpa [to_set, p] using hi''.2⟩
+      have : (cs i).b 0 = (cs i'').b 0 := by rw [hi.1, h2i''.1]
+      simp [side, hw', xm, this, h3i'']
+    apply not_disjoint_iff.mpr ⟨p', hp', h2p'⟩
+    apply h.1
+    rintro rfl
+    apply (cs i).b_ne_xm
+    rw [← hi', ← hi''.1, hi.1]
+    rfl
   · intro i' hi' h2i'
     dsimp only [shift_up] at h2i' 
     replace h2i' := h.injective h2i'.symm

Mathbin/Algebra/Algebra/Subalgebra/Basic.lean

@@ -1865,7 +1865,30 @@ end Centralizer
 theorem mem_of_finset_sum_eq_one_of_pow_smul_mem {S : Type _} [CommRing S] [Algebra R S]
     (S' : Subalgebra R S) {ι : Type _} (ι' : Finset ι) (s : ι → S) (l : ι → S)
     (e : ∑ i in ι', l i * s i = 1) (hs : ∀ i, s i ∈ S') (hl : ∀ i, l i ∈ S') (x : S)
-    (H : ∀ i, ∃ n : ℕ, (s i ^ n : S) • x ∈ S') : x ∈ S' := by classical
+    (H : ∀ i, ∃ n : ℕ, (s i ^ n : S) • x ∈ S') : x ∈ S' := by
+  classical
+  suffices x ∈ (Algebra.ofId S' S).range.toSubmodule by obtain ⟨x, rfl⟩ := this; exact x.2
+  choose n hn using H
+  let s' : ι → S' := fun x => ⟨s x, hs x⟩
+  have : Ideal.span (s' '' ι') = ⊤ :=
+    by
+    rw [Ideal.eq_top_iff_one, Ideal.span, Finsupp.mem_span_iff_total]
+    refine'
+      ⟨(Finsupp.ofSupportFinite (fun i : ι' => (⟨l i, hl i⟩ : S')) (Set.toFinite _)).mapDomain
+          fun i => ⟨s' i, i, i.2, rfl⟩,
+        S'.to_submodule.injective_subtype _⟩
+    rw [Finsupp.total_mapDomain, Finsupp.total_apply, Finsupp.sum_fintype, map_sum,
+      Submodule.subtype_apply, Subalgebra.coe_one]
+    · exact finset.sum_attach.trans e
+    · exact fun _ => zero_smul _ _
+  let N := ι'.sup n
+  have hs' := Ideal.span_pow_eq_top _ this N
+  apply (Algebra.ofId S' S).range.toSubmodule.mem_of_span_top_of_smul_mem _ hs'
+  rintro ⟨_, _, ⟨i, hi, rfl⟩, rfl⟩
+  change s i ^ N • x ∈ _
+  rw [← tsub_add_cancel_of_le (show n i ≤ N from Finset.le_sup hi), pow_add, mul_smul]
+  refine' Submodule.smul_mem _ (⟨_, pow_mem (hs i) _⟩ : S') _
+  exact ⟨⟨_, hn i⟩, rfl⟩
 #align subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem
 -/
 

Mathbin/Algebra/BigOperators/Associated.lean

@@ -101,7 +101,13 @@ theorem Multiset.prod_primes_dvd [CancelCommMonoidWithZero α]
 
 #print Finset.prod_primes_dvd /-
 theorem Finset.prod_primes_dvd [CancelCommMonoidWithZero α] [Unique αˣ] {s : Finset α} (n : α)
-    (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) : ∏ p in s, p ∣ n := by classical
+    (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) : ∏ p in s, p ∣ n := by
+  classical exact
+    Multiset.prod_primes_dvd n (by simpa only [Multiset.map_id', Finset.mem_def] using h)
+      (by simpa only [Multiset.map_id', Finset.mem_def] using div)
+      (by
+        simp only [Multiset.map_id', associated_eq_eq, Multiset.countP_eq_card_filter, ←
+          Multiset.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup])
 #align finset.prod_primes_dvd Finset.prod_primes_dvd
 -/
 

Mathbin/Algebra/BigOperators/Basic.lean

@@ -483,7 +483,8 @@ variable [Fintype α] [CommMonoid β]
 @[to_additive]
 theorem IsCompl.prod_mul_prod {s t : Finset α} (h : IsCompl s t) (f : α → β) :
     (∏ i in s, f i) * ∏ i in t, f i = ∏ i, f i :=
-  (Finset.prod_disjUnion h.Disjoint).symm.trans <| by classical
+  (Finset.prod_disjUnion h.Disjoint).symm.trans <| by
+    classical rw [Finset.disjUnion_eq_union, ← Finset.sup_eq_union, h.sup_eq_top] <;> rfl
 #align is_compl.prod_mul_prod IsCompl.prod_mul_prod
 #align is_compl.sum_add_sum IsCompl.sum_add_sum
 -/
@@ -768,7 +769,15 @@ variable. -/
       "Generalization of `finset.sum_comm` to the case when the inner `finset`s depend on\nthe outer variable."]
 theorem prod_comm' {s : Finset γ} {t : γ → Finset α} {t' : Finset α} {s' : α → Finset γ}
     (h : ∀ x y, x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t') {f : γ → α → β} :
-    ∏ x in s, ∏ y in t x, f x y = ∏ y in t', ∏ x in s' y, f x y := by classical
+    ∏ x in s, ∏ y in t x, f x y = ∏ y in t', ∏ x in s' y, f x y := by
+  classical
+  have :
+    ∀ z : γ × α,
+      (z ∈ s.bUnion fun x => (t x).map <| Function.Embedding.sectr x _) ↔ z.1 ∈ s ∧ z.2 ∈ t z.1 :=
+    by rintro ⟨x, y⟩; simp
+  exact
+    (prod_finset_product' _ _ _ this).symm.trans
+      (prod_finset_product_right' _ _ _ fun ⟨x, y⟩ => (this _).trans ((h x y).trans and_comm))
 #align finset.prod_comm' Finset.prod_comm'
 #align finset.sum_comm' Finset.sum_comm'
 -/
@@ -827,7 +836,10 @@ theorem prod_subset (h : s₁ ⊆ s₂) (hf : ∀ x ∈ s₂, x ∉ s₁ → f x
 @[to_additive]
 theorem prod_filter_of_ne {p : α → Prop} [DecidablePred p] (hp : ∀ x ∈ s, f x ≠ 1 → p x) :
     ∏ x in s.filterₓ p, f x = ∏ x in s, f x :=
-  prod_subset (filter_subset _ _) fun x => by classical
+  prod_subset (filter_subset _ _) fun x => by
+    classical
+    rw [not_imp_comm, mem_filter]
+    exact fun h₁ h₂ => ⟨h₁, hp _ h₁ h₂⟩
 #align finset.prod_filter_of_ne Finset.prod_filter_of_ne
 #align finset.sum_filter_of_ne Finset.sum_filter_of_ne
 -/
@@ -1268,7 +1280,24 @@ theorem prod_bij_ne_one {s : Finset α} {t : Finset γ} {f : α → β} {g : γ
     (i : ∀ a ∈ s, f a ≠ 1 → γ) (hi : ∀ a h₁ h₂, i a h₁ h₂ ∈ t)
     (i_inj : ∀ a₁ a₂ h₁₁ h₁₂ h₂₁ h₂₂, i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂)
     (i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a h₁ h₂, b = i a h₁ h₂) (h : ∀ a h₁ h₂, f a = g (i a h₁ h₂)) :
-    ∏ x in s, f x = ∏ x in t, g x := by classical
+    ∏ x in s, f x = ∏ x in t, g x := by
+  classical exact
+    calc
+      ∏ x in s, f x = ∏ x in s.filter fun x => f x ≠ 1, f x := prod_filter_ne_one.symm
+      _ = ∏ x in t.filter fun x => g x ≠ 1, g x :=
+        (prod_bij (fun a ha => i a (mem_filter.mp ha).1 (mem_filter.mp ha).2)
+          (fun a ha =>
+            (mem_filter.mp ha).elim fun h₁ h₂ =>
+              mem_filter.mpr ⟨hi a h₁ h₂, fun hg => h₂ (hg ▸ h a h₁ h₂)⟩)
+          (fun a ha => (mem_filter.mp ha).elim <| h a)
+          (fun a₁ a₂ ha₁ ha₂ =>
+            (mem_filter.mp ha₁).elim fun ha₁₁ ha₁₂ =>
+              (mem_filter.mp ha₂).elim fun ha₂₁ ha₂₂ => i_inj a₁ a₂ _ _ _ _)
+          fun b hb =>
+          (mem_filter.mp hb).elim fun h₁ h₂ =>
+            let ⟨a, ha₁, ha₂, Eq⟩ := i_surj b h₁ h₂
+            ⟨a, mem_filter.mpr ⟨ha₁, ha₂⟩, Eq⟩)
+      _ = ∏ x in t, g x := prod_filter_ne_one
 #align finset.prod_bij_ne_one Finset.prod_bij_ne_one
 #align finset.sum_bij_ne_zero Finset.sum_bij_ne_zero
 -/
@@ -1305,7 +1334,11 @@ theorem nonempty_of_prod_ne_one (h : ∏ x in s, f x ≠ 1) : s.Nonempty :=
 
 #print Finset.exists_ne_one_of_prod_ne_one /-
 @[to_additive]
-theorem exists_ne_one_of_prod_ne_one (h : ∏ x in s, f x ≠ 1) : ∃ a ∈ s, f a ≠ 1 := by classical
+theorem exists_ne_one_of_prod_ne_one (h : ∏ x in s, f x ≠ 1) : ∃ a ∈ s, f a ≠ 1 := by
+  classical
+  rw [← prod_filter_ne_one] at h 
+  rcases nonempty_of_prod_ne_one h with ⟨x, hx⟩
+  exact ⟨x, (mem_filter.1 hx).1, (mem_filter.1 hx).2⟩
 #align finset.exists_ne_one_of_prod_ne_one Finset.exists_ne_one_of_prod_ne_one
 #align finset.exists_ne_zero_of_sum_ne_zero Finset.exists_ne_zero_of_sum_ne_zero
 -/
@@ -1755,6 +1788,8 @@ theorem Fintype.prod_eq_prod_compl_mul [DecidableEq α] [Fintype α] (a : α) (f
 #print Finset.dvd_prod_of_mem /-
 theorem dvd_prod_of_mem (f : α → β) {a : α} {s : Finset α} (ha : a ∈ s) : f a ∣ ∏ i in s, f i := by
   classical
+  rw [Finset.prod_eq_mul_prod_diff_singleton ha]
+  exact dvd_mul_right _ _
 #align finset.dvd_prod_of_mem Finset.dvd_prod_of_mem
 -/
 
@@ -1908,6 +1943,13 @@ theorem eq_one_of_prod_eq_one {s : Finset α} {f : α → β} {a : α} (hp : ∏
   by
   intro x hx
   classical
+  by_cases h : x = a
+  · rw [h]
+    rw [h] at hx 
+    rw [← prod_subset (singleton_subset_iff.2 hx) fun t ht ha => h1 t ht (not_mem_singleton.1 ha),
+      prod_singleton] at hp 
+    exact hp
+  · exact h1 x hx h
 #align finset.eq_one_of_prod_eq_one Finset.eq_one_of_prod_eq_one
 #align finset.eq_zero_of_sum_eq_zero Finset.eq_zero_of_sum_eq_zero
 -/
@@ -1920,7 +1962,13 @@ theorem prod_pow_boole [DecidableEq α] (s : Finset α) (f : α → β) (a : α)
 
 #print Finset.prod_dvd_prod_of_dvd /-
 theorem prod_dvd_prod_of_dvd {S : Finset α} (g1 g2 : α → β) (h : ∀ a ∈ S, g1 a ∣ g2 a) :
-    S.Prod g1 ∣ S.Prod g2 := by classical
+    S.Prod g1 ∣ S.Prod g2 := by
+  classical
+  apply Finset.induction_on' S
+  · simp
+  intro a T haS _ haT IH
+  repeat' rw [Finset.prod_insert haT]
+  exact mul_dvd_mul (h a haS) IH
 #align finset.prod_dvd_prod_of_dvd Finset.prod_dvd_prod_of_dvd
 -/
 
@@ -1938,7 +1986,10 @@ end CommMonoid
   is the sum of the products of `g` and `h`. -/
 theorem prod_add_prod_eq [CommSemiring β] {s : Finset α} {i : α} {f g h : α → β} (hi : i ∈ s)
     (h1 : g i + h i = f i) (h2 : ∀ j ∈ s, j ≠ i → g j = f j) (h3 : ∀ j ∈ s, j ≠ i → h j = f j) :
-    ∏ i in s, g i + ∏ i in s, h i = ∏ i in s, f i := by classical
+    ∏ i in s, g i + ∏ i in s, h i = ∏ i in s, f i := by
+  classical
+  simp_rw [prod_eq_mul_prod_diff_singleton hi, ← h1, right_distrib]
+  congr 2 <;> apply prod_congr rfl <;> simpa
 #align finset.prod_add_prod_eq Finset.prod_add_prod_eq
 -/
 
@@ -2134,7 +2185,11 @@ theorem card_eq_sum_card_image [DecidableEq β] (f : α → β) (s : Finset α)
 
 #print Finset.mem_sum /-
 theorem mem_sum {f : α → Multiset β} (s : Finset α) (b : β) :
-    b ∈ ∑ x in s, f x ↔ ∃ a ∈ s, b ∈ f a := by classical
+    b ∈ ∑ x in s, f x ↔ ∃ a ∈ s, b ∈ f a := by
+  classical
+  refine' s.induction_on (by simp) _
+  · intro a t hi ih
+    simp [sum_insert hi, ih, or_and_right, exists_or]
 #align finset.mem_sum Finset.mem_sum
 -/
 
@@ -2166,7 +2221,12 @@ theorem prod_boole {s : Finset α} {p : α → Prop} [DecidablePred p] :
 variable [Nontrivial β] [NoZeroDivisors β]
 
 #print Finset.prod_eq_zero_iff /-
-theorem prod_eq_zero_iff : ∏ x in s, f x = 0 ↔ ∃ a ∈ s, f a = 0 := by classical
+theorem prod_eq_zero_iff : ∏ x in s, f x = 0 ↔ ∃ a ∈ s, f a = 0 := by
+  classical
+  apply Finset.induction_on s
+  exact ⟨Not.elim one_ne_zero, fun ⟨_, H, _⟩ => H.elim⟩
+  intro a s ha ih
+  rw [prod_insert ha, mul_eq_zero, bex_def, exists_mem_insert, ih, ← bex_def]
 #align finset.prod_eq_zero_iff Finset.prod_eq_zero_iff
 -/
 
@@ -2286,7 +2346,13 @@ theorem prod_subsingleton {α β : Type _} [CommMonoid β] [Subsingleton α] [Fi
 @[to_additive]
 theorem prod_subtype_mul_prod_subtype {α β : Type _} [Fintype α] [CommMonoid β] (p : α → Prop)
     (f : α → β) [DecidablePred p] :
-    (∏ i : { x // p x }, f i) * ∏ i : { x // ¬p x }, f i = ∏ i, f i := by classical
+    (∏ i : { x // p x }, f i) * ∏ i : { x // ¬p x }, f i = ∏ i, f i := by
+  classical
+  let s := {x | p x}.toFinset
+  rw [← Finset.prod_subtype s, ← Finset.prod_subtype (sᶜ)]
+  · exact Finset.prod_mul_prod_compl _ _
+  · simp
+  · simp
 #align fintype.prod_subtype_mul_prod_subtype Fintype.prod_subtype_mul_prod_subtype
 #align fintype.sum_subtype_add_sum_subtype Fintype.sum_subtype_add_sum_subtype
 -/
@@ -2471,7 +2537,11 @@ theorem toFinset_prod_dvd_prod [CommMonoid α] (S : Multiset α) : S.toFinset.Pr
 #print Multiset.prod_sum /-
 @[to_additive]
 theorem prod_sum {α : Type _} {ι : Type _} [CommMonoid α] (f : ι → Multiset α) (s : Finset ι) :
-    (∑ x in s, f x).Prod = ∏ x in s, (f x).Prod := by classical
+    (∑ x in s, f x).Prod = ∏ x in s, (f x).Prod := by
+  classical
+  induction' s using Finset.induction_on with a t hat ih
+  · rw [Finset.sum_empty, Finset.prod_empty, Multiset.prod_zero]
+  · rw [Finset.sum_insert hat, Finset.prod_insert hat, Multiset.prod_add, ih]
 #align multiset.prod_sum Multiset.prod_sum
 #align multiset.sum_sum Multiset.sum_sum
 -/
@@ -2589,13 +2659,19 @@ theorem Units.coe_prod {M : Type _} [CommMonoid M] (f : α → Mˣ) (s : Finset
 theorem Units.mk0_prod [CommGroupWithZero β] (s : Finset α) (f : α → β) (h) :
     Units.mk0 (∏ b in s, f b) h =
       ∏ b in s.attach, Units.mk0 (f b) fun hh => h (Finset.prod_eq_zero b.2 hh) :=
-  by classical
+  by classical induction s using Finset.induction_on <;> simp [*]
 #align units.mk0_prod Units.mk0_prod
 -/
 
 #print nat_abs_sum_le /-
 theorem nat_abs_sum_le {ι : Type _} (s : Finset ι) (f : ι → ℤ) :
-    (∑ i in s, f i).natAbs ≤ ∑ i in s, (f i).natAbs := by classical
+    (∑ i in s, f i).natAbs ≤ ∑ i in s, (f i).natAbs := by
+  classical
+  apply Finset.induction_on s
+  · simp only [Finset.sum_empty, Int.natAbs_zero]
+  · intro i s his IH
+    simp only [his, Finset.sum_insert, not_false_iff]
+    exact (Int.natAbs_add_le _ _).trans (add_le_add le_rfl IH)
 #align nat_abs_sum_le nat_abs_sum_le
 -/