Space before ←

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`

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), _⟩,

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

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

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₂,

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)

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) :

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 _ _

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 :=

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

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
 

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)
 

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,23 +68,23 @@ 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 α)) :
     s □ t = s ∩ t := by
   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 α))
     (ht : IsUpperSet (t : Set α)) : s □ t = s ○ t := by
   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