From 034199694e3b91536d03bc4a8b0cdbd659cdf50f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 14 Jun 2024 07:38:19 +0000 Subject: [PATCH] =?UTF-8?q?Space=20before=20`=E2=86=90`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanCamCombi/BernoulliSeq.lean | 12 ++++++------ LeanCamCombi/ConvexContinuous.lean | 2 +- LeanCamCombi/ErdosGinzburgZiv.lean | 14 +++++++------- LeanCamCombi/LittlewoodOfford.lean | 2 +- .../Mathlib/Analysis/Convex/Extreme.lean | 16 ++++++++-------- .../Analysis/Convex/SimplicialComplex/Basic.lean | 2 +- LeanCamCombi/Mathlib/Combinatorics/Colex.lean | 8 ++++---- LeanCamCombi/Mathlib/Data/List/DropRight.lean | 2 +- LeanCamCombi/Mathlib/Order/Sublattice.lean | 8 ++++---- LeanCamCombi/Mathlib/Order/SupClosed.lean | 2 +- .../Mathlib/Probability/Independence/Basic.lean | 2 +- .../ProbabilityMassFunction/Constructions.lean | 6 +++--- LeanCamCombi/VanDenBergKesten.lean | 8 ++++---- 13 files changed, 42 insertions(+), 42 deletions(-) diff --git a/LeanCamCombi/BernoulliSeq.lean b/LeanCamCombi/BernoulliSeq.lean index dd46df78da..ffc87136c4 100644 --- a/LeanCamCombi/BernoulliSeq.lean +++ b/LeanCamCombi/BernoulliSeq.lean @@ -43,12 +43,12 @@ namespace IsBernoulliSeq protected lemma ne_zero [Nonempty α] : μ ≠ 0 := Nonempty.elim ‹_› fun a h ↦ (PMF.bernoulli' p hX.le_one).toMeasure_ne_zero $ by - rw [←hX.map a, h, Measure.map_zero] + rw [← hX.map a, h, Measure.map_zero] protected lemma aemeasurable (a : α) : AEMeasurable (fun ω ↦ a ∈ X ω) μ := by classical have : (PMF.bernoulli' p hX.le_one).toMeasure ≠ 0 := NeZero.ne _ - rw [←hX.map a, Measure.map] at this + rw [← hX.map a, Measure.map] at this refine' (Ne.dite_ne_right_iff fun hX' ↦ _).1 this rw [Measure.mapₗ_ne_zero_iff hX'.measurable_mk] haveI : Nonempty α := ⟨a⟩ @@ -65,7 +65,7 @@ protected lemma identDistrib (a j : α) : IdentDistrib (fun ω ↦ a ∈ X ω) ( @[simp] lemma meas_apply (a : α) : μ {ω | a ∈ X ω} = p := by rw [(_ : {ω | a ∈ X ω} = (fun ω ↦ a ∈ X ω) ⁻¹' {True}), - ←Measure.map_apply_of_aemeasurable (hX.aemeasurable a) MeasurableSpace.measurableSet_top] + ← Measure.map_apply_of_aemeasurable (hX.aemeasurable a) MeasurableSpace.measurableSet_top] · simp [hX.map] · ext ω simp @@ -76,11 +76,11 @@ protected lemma meas [Fintype α] (s : Finset α) : μ {ω | {a | a ∈ X ω} = s} = (p : ℝ≥0∞) ^ s.card * (1 - p : ℝ≥0∞) ^ (card α - s.card) := by classical simp_rw [ext_iff, setOf_forall] - rw [hX.iIndepFun.meas_iInter, ←s.prod_mul_prod_compl, Finset.prod_eq_pow_card, + rw [hX.iIndepFun.meas_iInter, ← s.prod_mul_prod_compl, Finset.prod_eq_pow_card, Finset.prod_eq_pow_card, Finset.card_compl] · rintro a hi rw [Finset.mem_compl] at hi - simp only [hi, ←compl_setOf, prob_compl_eq_one_sub₀, mem_setOf_eq, Finset.mem_coe, + simp only [hi, ← compl_setOf, prob_compl_eq_one_sub₀, mem_setOf_eq, Finset.mem_coe, iff_false_iff, hX.nullMeasurableSet, hX.meas_apply] · rintro a hi simp only [hi, mem_setOf_eq, Finset.mem_coe, iff_true_iff, hX.meas_apply] @@ -117,7 +117,7 @@ protected lemma inter (h : IndepFun X Y μ) : IsBernoulliSeq (fun ω ↦ X ω change μ (⋂ i ∈ s, {ω | X ω i} ∩ {ω | Y ω i}) = s.prod fun i ↦ μ ({ω | X ω i} ∩ {ω | Y ω i}) simp_rw [iInter_inter_distrib] rw [h.meas_inter, hX.iIndepFun.meas_biInter, hY.iIndepFun.meas_biInter, - ←Finset.prod_mul_distrib] + ← Finset.prod_mul_distrib] refine' Finset.prod_congr rfl fun i hi ↦ (h.meas_inter _ _).symm sorry -- needs refactor of `Probability.Independence.Basic` sorry -- needs refactor of `Probability.Independence.Basic` diff --git a/LeanCamCombi/ConvexContinuous.lean b/LeanCamCombi/ConvexContinuous.lean index 9169d521f7..fddf3dc94f 100644 --- a/LeanCamCombi/ConvexContinuous.lean +++ b/LeanCamCombi/ConvexContinuous.lean @@ -74,7 +74,7 @@ lemma IsOpen.exists_mem_intrinsicInterior_convexHull_finset -- rw image_subset_iff, -- refine ball_subset_closedBall.trans _, -- simp_rw [closedBall_pi _ zero_le_one, Real.closedBall_eq_segment zero_le_one, - -- ←convexHull_pair, ←convexHull_pi, pi.zero_apply, zero_sub, zero_add, ht, Finset.coe_image, + -- ← convexHull_pair, ← convexHull_pi, pi.zero_apply, zero_sub, zero_add, ht, Finset.coe_image, -- Finset.coe_univ, image_univ], -- refine convexHull_min (fun w hw, subset_convexHull _ _ _) _, -- refine ⟨Finset.univ.filter (fun i ↦ w i = 1), _⟩, diff --git a/LeanCamCombi/ErdosGinzburgZiv.lean b/LeanCamCombi/ErdosGinzburgZiv.lean index 024b6ce717..5395443cc1 100644 --- a/LeanCamCombi/ErdosGinzburgZiv.lean +++ b/LeanCamCombi/ErdosGinzburgZiv.lean @@ -49,7 +49,7 @@ private lemma totalDegree_f₁_add_totalDegree_f₂ : (f₁ s).totalDegree + (f₂ s).totalDegree < 2 * p - 1 := by refine (add_le_add (totalDegree_finset_sum _ _) $ (totalDegree_finset_sum _ _).trans $ Finset.sup_mono_fun fun a _ ↦ totalDegree_smul_le _ _).trans_lt ?_ - simp only [totalDegree_X_pow, ←two_mul] + simp only [totalDegree_X_pow, ← two_mul] refine (mul_le_mul_left' Finset.sup_const_le _).trans_lt ?_ rw [mul_tsub, mul_one] exact tsub_lt_tsub_left_of_le ((Fact.out : p.Prime).two_le.trans $ @@ -78,20 +78,20 @@ private lemma aux (hs : Multiset.card s = 2 * p - 1) : -- Note that we need `Multiset.toEnumFinset` to distinguish duplicated elements of `s`. refine ⟨(s.toEnumFinset.attach.filter $ fun a ↦ x.1 a ≠ 0).1.map (Prod.fst ∘ ((↑) : s.toEnumFinset → ZMod p × ℕ)), le_iff_count.2 $ fun a ↦ ?_, ?_, ?_⟩ - · simp only [←Finset.filter_val, Finset.card_val, Function.comp_apply, count_map] + · simp only [← Finset.filter_val, Finset.card_val, Function.comp_apply, count_map] refine (Finset.card_le_card $ Finset.filter_subset_filter _ $ Finset.filter_subset _ _).trans_eq ?_ refine (Finset.card_filter_attach (fun c : ZMod p × ℕ ↦ a = c.1) _).trans ?_ simp [toEnumFinset_filter_eq] -- From `f₁ x = 0`, we get that `p` divides the number of `a` such that `x a ≠ 0`. - · simp only [card_map, ←Finset.filter_val, Finset.card_val, Function.comp_apply, - count_map, ←Finset.map_val] + · simp only [card_map, ← Finset.filter_val, Finset.card_val, Function.comp_apply, + count_map, ← Finset.map_val] refine Nat.eq_of_dvd_of_lt_two_mul (Finset.card_pos.2 ?_).ne' ?_ $ (Finset.card_filter_le _ _).trans_lt ?_ -- This number is nonzero because `x ≠ 0`. · rw [← Subtype.coe_ne_coe, Function.ne_iff] at hx exact hx.imp (fun a ha ↦ mem_filter.2 ⟨Finset.mem_attach _ _, ha⟩) - · rw [← CharP.cast_eq_zero_iff (ZMod p), ←Finset.sum_boole] + · rw [← CharP.cast_eq_zero_iff (ZMod p), ← Finset.sum_boole] simpa only [f₁, map_sum, ZMod.pow_card_sub_one, map_pow, eval_X] using x.2.1 -- And it is at most `2 * p - 1`, so it must be `p`. · rw [Finset.card_attach, card_toEnumFinset, hs] @@ -128,8 +128,8 @@ lemma exists_submultiset_eq_zero {s : Multiset (ZMod n)} (hs : 2 * n - 1 ≤ Mul rw [card_map] refine (le_tsub_of_add_le_left $ le_trans ?_ hs).trans le_card_sub have : m.map Multiset.card = replicate (2 * a - 1) n := sorry - rw [map_multiset_sum, this, sum_replicate, ←le_tsub_iff_right, tsub_tsub_tsub_cancel_right, - ←mul_tsub, ←mul_tsub_one] + rw [map_multiset_sum, this, sum_replicate, ← le_tsub_iff_right, tsub_tsub_tsub_cancel_right, + ← mul_tsub, ← mul_tsub_one] sorry sorry sorry diff --git a/LeanCamCombi/LittlewoodOfford.lean b/LeanCamCombi/LittlewoodOfford.lean index 8db953b6c0..671f60e199 100644 --- a/LeanCamCombi/LittlewoodOfford.lean +++ b/LeanCamCombi/LittlewoodOfford.lean @@ -40,7 +40,7 @@ lemma card_le_of_forall_dist_sum_le (hr : 0 < r) (h𝒜 : ∀ t ∈ 𝒜, t ⊆ 𝒜.card ≤ s.card.choose (s.card / 2) := by classical obtain ⟨P, hP, _hs, hr⟩ := exists_littlewood_offord_partition hr hf - rw [←hP] + rw [← hP] refine' card_le_card_of_forall_subsingleton (· ∈ ·) (fun t ht ↦ _) fun ℬ hℬ t ht u hu ↦ (hr _ hℬ).eq ht.2 hu.2 (h𝒜r _ ht.1 _ hu.1).not_le diff --git a/LeanCamCombi/Mathlib/Analysis/Convex/Extreme.lean b/LeanCamCombi/Mathlib/Analysis/Convex/Extreme.lean index 5a4de767c3..690877c35e 100644 --- a/LeanCamCombi/Mathlib/Analysis/Convex/Extreme.lean +++ b/LeanCamCombi/Mathlib/Analysis/Convex/Extreme.lean @@ -103,7 +103,7 @@ lemma IsExtreme.subset_frontier (hAB : IsExtreme 𝕜 s t) (hBA : ¬s ⊆ t) : t _, _, _, _⟩).1, { exact (div_pos nat.one_div_pos_of_nat (add_pos nat.one_div_pos_of_nat (by linarith))).le }, { exact le_of_lt (one_div_pos.2 (add_pos nat.one_div_pos_of_nat (by linarith))).le }, - { rw [←add_div, div_self], + { rw [← add_div, div_self], exact (add_pos nat.one_div_pos_of_nat (by linarith)).ne' }, { sorry, }, @@ -112,7 +112,7 @@ lemma IsExtreme.subset_frontier (hAB : IsExtreme 𝕜 s t) (hBA : ¬s ⊆ t) : t { rintro h, apply hyB, suffices h : x = y, - { rw ←h, exact hxB }, + { rw ← h, exact hxB }, suffices h : (1/n.succ : ℝ) • x = (1/n.succ : ℝ) • y, { exact smul_injective (ne_of_gt nat.one_div_pos_of_nat) h }, calc @@ -123,14 +123,14 @@ lemma IsExtreme.subset_frontier (hAB : IsExtreme 𝕜 s t) (hBA : ¬s ⊆ t) : t ... = -(1 • x) + z n + (1/n.succ : ℝ) • y : by refl ... = -(1 • x) + x + (1/n.succ : ℝ) • y : by rw h ... = (1/n.succ : ℝ) • y : by simp } }, - rw ←sub_zero x, + rw ← sub_zero x, apply filter.tendsto.sub, - { nth_rewrite 0 ←one_smul _ x, + { nth_rewrite 0 ← one_smul _ x, apply filter.tendsto.smul_const, - nth_rewrite 0 ←add_zero (1 : ℝ), --weirdly skips the first two `1`. Might break in the future + nth_rewrite 0 ← add_zero (1 : ℝ), --weirdly skips the first two `1`. Might break in the future apply filter.tendsto.const_add, sorry }, - rw ←zero_smul _ y, + rw ← zero_smul _ y, apply filter.tendsto.smul_const,-/ sorry @@ -194,7 +194,7 @@ begin simp }, have hw''₂ : s.sum (λ i, w'' i • i) = 0, { simp only [sub_smul, add_smul, finset.sum_add_distrib, finset.sum_sub_distrib], - simp only [mul_smul, ←finset.smul_sum, hy, hy'], + simp only [mul_smul, ← finset.smul_sum, hy, hy'], simp only [ite_smul, zero_smul, one_smul, finset.sum_ite_eq', if_pos hx, hθ₂, sub_self] }, by_contra t, push_neg at t, suffices hw''₃ : ∀ q ∈ s, w'' q = 0, @@ -225,7 +225,7 @@ begin { rw finset.sum_eq_single x at hy, { rw hw₁ at hy, apply t.1, - rw ←hy, + rw ← hy, simp }, { rintro q hq₁ hq₂, rw both_zero q hq₁ hq₂, diff --git a/LeanCamCombi/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/LeanCamCombi/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean index 4772815b6f..cff38e3eee 100644 --- a/LeanCamCombi/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean +++ b/LeanCamCombi/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean @@ -87,7 +87,7 @@ lemma mem_of_mem_convexHull (hx : x ∈ K.vertices) (hs : s ∈ K) (hxs : x ∈ convexHull 𝕜 (s : Set E)) : x ∈ s := by have h := K.inter_subset_convexHull hx hs ⟨by simp, hxs⟩ by_contra H - rwa [←coe_inter, inter_comm, disjoint_iff_inter_eq_empty.1 (disjoint_singleton_right.2 H), + rwa [← coe_inter, inter_comm, disjoint_iff_inter_eq_empty.1 (disjoint_singleton_right.2 H), coe_empty, convexHull_empty] at h lemma subset_of_convexHull_subset_convexHull (hs : s ∈ K) (ht : t ∈ K) diff --git a/LeanCamCombi/Mathlib/Combinatorics/Colex.lean b/LeanCamCombi/Mathlib/Combinatorics/Colex.lean index c10542f366..d90ae92ee8 100644 --- a/LeanCamCombi/Mathlib/Combinatorics/Colex.lean +++ b/LeanCamCombi/Mathlib/Combinatorics/Colex.lean @@ -12,7 +12,7 @@ lemma cons_le_cons (ha hb) : toColex (s.cons a ha) ≤ toColex (s.cons b hb) ↔ obtain rfl | hab := eq_or_ne a b · simp classical - rw [←toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm, + rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm, singleton_le_singleton] lemma cons_lt_cons (ha hb) : toColex (s.cons a ha) < toColex (s.cons b hb) ↔ a < b := @@ -22,18 +22,18 @@ variable [DecidableEq α] lemma insert_le_insert (ha : a ∉ s) (hb : b ∉ s) : toColex (insert a s) ≤ toColex (insert b s) ↔ a ≤ b := by - rw [←cons_eq_insert _ _ ha, ←cons_eq_insert _ _ hb, cons_le_cons] + rw [← cons_eq_insert _ _ ha, ← cons_eq_insert _ _ hb, cons_le_cons] lemma insert_lt_insert (ha : a ∉ s) (hb : b ∉ s) : toColex (insert a s) < toColex (insert b s) ↔ a < b := by - rw [←cons_eq_insert _ _ ha, ←cons_eq_insert _ _ hb, cons_lt_cons] + rw [← cons_eq_insert _ _ ha, ← cons_eq_insert _ _ hb, cons_lt_cons] lemma erase_le_erase (ha : a ∈ s) (hb : b ∈ s) : toColex (s.erase a) ≤ toColex (s.erase b) ↔ b ≤ a := by obtain rfl | hab := eq_or_ne a b · simp classical - rw [←toColex_sdiff_le_toColex_sdiff', erase_sdiff_erase hab hb, erase_sdiff_erase hab.symm ha, + rw [← toColex_sdiff_le_toColex_sdiff', erase_sdiff_erase hab hb, erase_sdiff_erase hab.symm ha, singleton_le_singleton] lemma erase_lt_erase (ha : a ∈ s) (hb : b ∈ s) : diff --git a/LeanCamCombi/Mathlib/Data/List/DropRight.lean b/LeanCamCombi/Mathlib/Data/List/DropRight.lean index d15f304203..bfc82b33a8 100644 --- a/LeanCamCombi/Mathlib/Data/List/DropRight.lean +++ b/LeanCamCombi/Mathlib/Data/List/DropRight.lean @@ -17,7 +17,7 @@ lemma length_rtake (n : ℕ) (l : List α) : (l.rtake n).length = min n l.length rw [rtake_eq_reverse_take_reverse, reverse_reverse] @[simp] lemma rtake_rtake (n m) (l : List α) : (l.rtake m).rtake n = l.rtake (min n m) := by - rw [rtake_eq_reverse_take_reverse, ←take_reverse, take_take, rtake_eq_reverse_take_reverse] + rw [rtake_eq_reverse_take_reverse, ← take_reverse, take_take, rtake_eq_reverse_take_reverse] @[simp] lemma rdrop_append_rtake (n : ℕ) (l : List α) : l.rdrop n ++ l.rtake n = l := take_append_drop _ _ diff --git a/LeanCamCombi/Mathlib/Order/Sublattice.lean b/LeanCamCombi/Mathlib/Order/Sublattice.lean index 16af967be0..ce809ce7df 100644 --- a/LeanCamCombi/Mathlib/Order/Sublattice.lean +++ b/LeanCamCombi/Mathlib/Order/Sublattice.lean @@ -63,10 +63,10 @@ lemma le_prod_iff {M : Sublattice β} {N : Sublattice (α × β)} : simp [SetLike.le_def, forall_and] @[simp] lemma prod_eq_bot {M : Sublattice β} : L.prod M = ⊥ ↔ L = ⊥ ∨ M = ⊥ := by - simpa only [←coe_inj] using Set.prod_eq_empty_iff + simpa only [← coe_inj] using Set.prod_eq_empty_iff @[simp] lemma prod_eq_top [Nonempty α] [Nonempty β] {M : Sublattice β} : - L.prod M = ⊤ ↔ L = ⊤ ∧ M = ⊤ := by simpa only [←coe_inj] using Set.prod_eq_univ + L.prod M = ⊤ ↔ L = ⊤ ∧ M = ⊤ := by simpa only [← coe_inj] using Set.prod_eq_univ /-- The product of sublattices is isomorphic to their product as lattices. -/ def prodEquiv (L : Sublattice α) (M : Sublattice β) : L.prod M ≃o L × M where @@ -102,7 +102,7 @@ lemma le_pi {s : Set κ} {L : ∀ i, Sublattice (π i)} {M : Sublattice (∀ i, M ≤ pi s L ↔ ∀ i ∈ s, M ≤ comap (Pi.evalLatticeHom π i) (L i) := by simp [SetLike.le_def]; aesop @[simp] lemma pi_univ_eq_bot {L : ∀ i, Sublattice (π i)} : pi univ L = ⊥ ↔ ∃ i, L i = ⊥ := by - simp_rw [←coe_inj]; simp + simp_rw [← coe_inj]; simp end Pi end Sublattice @@ -176,7 +176,7 @@ lemma range_eq_top_of_surjective {β} [Lattice β] (f : LatticeHom α β) (hf : range_eq_top.2 hf lemma _root_.Sublattice.range_subtype (L : Sublattice α) : L.subtype.range = L := by - rw [←map_top, ←SetLike.coe_set_eq, coe_map, Sublattice.coe_subtype]; ext; simp + rw [← map_top, ← SetLike.coe_set_eq, coe_map, Sublattice.coe_subtype]; ext; simp /-- Computable alternative to `LatticeHom.ofInjective`. -/ def ofLeftInverse {f : LatticeHom α β} {g : β →* α} (h : LeftInverse g f) : α ≃o f.range := diff --git a/LeanCamCombi/Mathlib/Order/SupClosed.lean b/LeanCamCombi/Mathlib/Order/SupClosed.lean index b29a4ed8c3..c024d7f8fe 100644 --- a/LeanCamCombi/Mathlib/Order/SupClosed.lean +++ b/LeanCamCombi/Mathlib/Order/SupClosed.lean @@ -47,6 +47,6 @@ open Finset @[simp] lemma latticeClosure_prod (s : Set α) (t : Set β) : latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t := by - simp_rw [←supClosure_infClosure]; simp + simp_rw [← supClosure_infClosure]; simp end DistribLattice diff --git a/LeanCamCombi/Mathlib/Probability/Independence/Basic.lean b/LeanCamCombi/Mathlib/Probability/Independence/Basic.lean index bcdad1abbb..e56898d055 100644 --- a/LeanCamCombi/Mathlib/Probability/Independence/Basic.lean +++ b/LeanCamCombi/Mathlib/Probability/Independence/Basic.lean @@ -9,7 +9,7 @@ variable {Ω ι : Type*} {β : ι → Type*} [MeasurableSpace Ω] {π : ι → Set (Set Ω)} {μ : Measure Ω} {S : Finset ι} {s : ι → Set Ω} {f : ∀ i, Ω → β i} lemma iIndep_comap_iff : iIndep (fun i ↦ MeasurableSpace.comap (· ∈ s i) ⊤) μ ↔ iIndepSet s μ := by - simp_rw [←generateFrom_singleton]; rfl + simp_rw [← generateFrom_singleton]; rfl alias ⟨_, iIndepSet.Indep_comap⟩ := iIndep_comap_iff diff --git a/LeanCamCombi/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean b/LeanCamCombi/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean index 5667592bb0..6c651b6379 100644 --- a/LeanCamCombi/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean +++ b/LeanCamCombi/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean @@ -24,7 +24,7 @@ lemma map_ofFintype (f : α → ℝ≥0∞) (h : ∑ a, f a = 1) (g : α → β) refine' fun b₁ _ b₂ _ hb ↦ disjoint_left.2 fun a ha₁ ha₂ ↦ _ simp only [mem_filter, mem_univ, true_and_iff] at ha₁ ha₂ exact hb (ha₁.symm.trans ha₂) - rw [←sum_disjiUnion _ _ this] + rw [← sum_disjiUnion _ _ this] convert h exact eq_univ_of_forall fun a ↦ mem_disjiUnion.2 ⟨_, mem_univ _, mem_filter.2 ⟨mem_univ _, rfl⟩⟩) := by @@ -46,8 +46,8 @@ section bernoulli /-- A `PMF` which assigns probability `p` to true propositions and `1 - p` to false ones. -/ noncomputable def bernoulli' (p : ℝ≥0) (h : p ≤ 1) : PMF Prop := - (ofFintype fun b ↦ if b then p else 1 - p) $ by simp_rw [←ENNReal.coe_one, ←ENNReal.coe_sub, - ←apply_ite ((↑) : ℝ≥0 → ℝ≥0∞), ←ENNReal.coe_finset_sum, ENNReal.coe_inj]; simp [h] + (ofFintype fun b ↦ if b then p else 1 - p) $ by simp_rw [← ENNReal.coe_one, ← ENNReal.coe_sub, + ← apply_ite ((↑) : ℝ≥0 → ℝ≥0∞), ← ENNReal.coe_finset_sum, ENNReal.coe_inj]; simp [h] variable {p : ℝ≥0} (hp : p ≤ 1) (b : Prop) diff --git a/LeanCamCombi/VanDenBergKesten.lean b/LeanCamCombi/VanDenBergKesten.lean index 3778a26c74..be349361cf 100644 --- a/LeanCamCombi/VanDenBergKesten.lean +++ b/LeanCamCombi/VanDenBergKesten.lean @@ -56,7 +56,7 @@ lemma certificator_subset_disjSups : s □ t ⊆ s ○ t := by rintro x ⟨u, v, huv, hu, hv⟩ refine' ⟨x ⊓ u, hu (inf_right_idem _ _).symm, x ⊓ v, hv (inf_right_idem _ _).symm, huv.disjoint.mono inf_le_right inf_le_right, _⟩ - rw [←inf_sup_left, huv.codisjoint.eq_top, inf_top_eq] + rw [← inf_sup_left, huv.codisjoint.eq_top, inf_top_eq] variable (s t u) @@ -68,7 +68,7 @@ lemma IsUpperSet.certificator_eq_inter (hs : IsUpperSet (s : Set α)) (ht : IsLo refine' certificator_subset_inter.antisymm fun a ha ↦ mem_certificator.2 ⟨a, aᶜ, isCompl_compl, _⟩ rw [mem_inter] at ha - simp only [@eq_comm _ ⊥, ←sdiff_eq, inf_idem, right_eq_inf, _root_.sdiff_self, sdiff_eq_bot_iff] + simp only [@eq_comm _ ⊥, ← sdiff_eq, inf_idem, right_eq_inf, _root_.sdiff_self, sdiff_eq_bot_iff] exact ⟨fun b hab ↦ hs hab ha.1, fun b hab ↦ ht hab ha.2⟩ lemma IsLowerSet.certificator_eq_inter (hs : IsLowerSet (s : Set α)) (ht : IsUpperSet (t : Set α)) : @@ -76,7 +76,7 @@ lemma IsLowerSet.certificator_eq_inter (hs : IsLowerSet (s : Set α)) (ht : IsUp refine' certificator_subset_inter.antisymm fun a ha ↦ mem_certificator.2 ⟨aᶜ, a, isCompl_compl.symm, _⟩ rw [mem_inter] at ha - simp only [@eq_comm _ ⊥, ←sdiff_eq, inf_idem, right_eq_inf, _root_.sdiff_self, sdiff_eq_bot_iff] + simp only [@eq_comm _ ⊥, ← sdiff_eq, inf_idem, right_eq_inf, _root_.sdiff_self, sdiff_eq_bot_iff] exact ⟨fun b hab ↦ hs hab ha.1, fun b hab ↦ ht hab ha.2⟩ lemma IsUpperSet.certificator_eq_disjSups (hs : IsUpperSet (s : Set α)) @@ -84,7 +84,7 @@ lemma IsUpperSet.certificator_eq_disjSups (hs : IsUpperSet (s : Set α)) refine' certificator_subset_disjSups.antisymm fun a ha ↦ mem_certificator.2 _ obtain ⟨x, hx, y, hy, hxy, rfl⟩ := mem_disjSups.1 ha refine' ⟨x, xᶜ, isCompl_compl, _⟩ - simp only [inf_of_le_right, le_sup_left, right_eq_inf, ←sdiff_eq, hxy.sup_sdiff_cancel_left] + simp only [inf_of_le_right, le_sup_left, right_eq_inf, ← sdiff_eq, hxy.sup_sdiff_cancel_left] exact ⟨fun b hab ↦ hs hab hx, fun b hab ↦ ht (hab.trans_le sdiff_le) hy⟩ end BooleanAlgebra