staging

PFR/ForMathlib/Uniform.lean

@@ -202,7 +202,8 @@ lemma IsUniform.of_identDistrib {Ω' : Type*} [MeasurableSpace Ω'] (h : IsUnifo
 
 /-- $\mathbb{P}(U_H \in H') \neq 0$ if $H'$ intersects $H$ and the measure is non-zero. -/
 lemma IsUniform.measure_preimage_ne_zero {H : Finset S} [NeZero μ] (h : IsUniform H X μ)
-    (hX : Measurable X) (H' : Set S) [Nonempty (H' ∩ H.toSet).Elem] : μ (X ⁻¹' H') ≠ 0 := by
+    (hX : Measurable X) {H' : Set S} (h' : (H' ∩ H).Nonempty) : μ (X ⁻¹' H') ≠ 0 := by
+  have : Nonempty (H' ∩ H : Set S) := h'.to_subtype
   simp_rw [h.measure_preimage hX H', ne_eq, ENNReal.div_eq_zero_iff, ENNReal.natCast_ne_top,
     or_false, mul_eq_zero, NeZero.ne, false_or, Nat.cast_eq_zero, ← Nat.pos_iff_ne_zero,
     Nat.card_pos]

PFR/ImprovedPFR.lean

@@ -29,6 +29,7 @@ variable (h_indep : iIndepFun (fun _i => hG) ![Z₁, Z₂, Z₃, Z₄])
 
 local notation3 "Sum" => Z₁ + Z₂ + Z₃ + Z₄
 
+include hY hZ₁ hZ₂ hZ₃ hZ₄ h_indep in
 lemma gen_ineq_aux1 :
     d[Y # Z₁ + Z₂ | ⟨Z₁ + Z₃, Sum⟩] ≤ d[Y # Z₁]
       + (d[Z₁ # Z₂] + d[Z₁ # Z₃] + d[Z₂ # Z₄] - d[Z₁ | Z₁ + Z₂ # Z₃ | Z₃ + Z₄]) / 2
@@ -69,6 +70,7 @@ lemma gen_ineq_aux1 :
       linarith
   _ = _ := by linarith
 
+include hY hZ₁ hZ₂ hZ₃ hZ₄ h_indep in
 lemma gen_ineq_aux2 :
     d[Y # Z₁ + Z₂ | ⟨Z₁ + Z₃, Sum⟩] ≤ d[Y # Z₁]
       + (d[Z₁ # Z₃] + d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄]) / 2
@@ -190,6 +192,7 @@ lemma gen_ineq_aux2 :
     linarith
   _ = _ := by ring
 
+include hY hZ₁ hZ₂ hZ₃ hZ₄ h_indep in
 /-- Let `Z₁, Z₂, Z₃, Z₄` be independent `G`-valued random variables, and let `Y` be another
 `G`-valued random variable.  Set `S := Z₁ + Z₂ + Z₃ + Z₄`. Then
 `(d[Z₁ # Z₂] + 2 * d[Z₁ # Z₃] + d[Z₂ # Z₄]) / 4`
@@ -204,6 +207,7 @@ lemma gen_ineq_00 : d[Y # Z₁ + Z₂ | ⟨Z₁ + Z₃, Sum⟩] - d[Y # Z₁] 
   have I2 := gen_ineq_aux2 Y hY Z₁ Z₂ Z₃ Z₄ hZ₁ hZ₂ hZ₃ hZ₄ h_indep
   linarith
 
+include hY hZ₁ hZ₂ hZ₃ hZ₄ h_indep in
 /-- Other version of `gen_ineq_00`, in which we switch to the complement in the second term. -/
 lemma gen_ineq_01 : d[Y # Z₁ + Z₂ | ⟨Z₂ + Z₄, Sum⟩] - d[Y # Z₁] ≤
     (d[Z₁ # Z₂] + 2 * d[Z₁ # Z₃] + d[Z₂ # Z₄]) / 4
@@ -220,6 +224,7 @@ lemma gen_ineq_01 : d[Y # Z₁ + Z₂ | ⟨Z₂ + Z₄, Sum⟩] - d[Y # Z₁] 
   simp only [e, Pi.add_apply, Equiv.coe_fn_mk, Function.comp_apply]
   abel
 
+include hY hZ₁ hZ₂ hZ₃ hZ₄ h_indep in
 /-- Other version of `gen_ineq_00`, in which we switch to the complement in the first term. -/
 lemma gen_ineq_10 : d[Y # Z₃ + Z₄ | ⟨Z₁ + Z₃, Sum⟩] - d[Y # Z₁] ≤
     (d[Z₁ # Z₂] + 2 * d[Z₁ # Z₃] + d[Z₂ # Z₄]) / 4
@@ -249,7 +254,7 @@ section MainEstimates
 open MeasureTheory ProbabilityTheory
 
 variable {G : Type*} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G]
-  [MeasurableSingletonClass G] [ElementaryAddCommGroup G 2] [MeasurableAdd₂ G]
+  [MeasurableSingletonClass G] [ElementaryAddCommGroup G 2]
 
 variable {Ω₀₁ Ω₀₂ : Type*} [MeasureSpace Ω₀₁] [MeasureSpace Ω₀₂]
   [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] [IsProbabilityMeasure (ℙ : Measure Ω₀₂)]
@@ -312,6 +317,7 @@ local notation3:max "ψ[" A " # " B "]" => d[A # B] + p.η * (c[A # B])
 local notation3:max "ψ[" A "; " μ " # " B " ; " μ' "]" =>
   d[A ; μ # B ; μ'] + p.η * c[A ; μ # B ; μ']
 
+include hT hT₁ hT₂ hT₃ h_min in
 /-- For any $T_1, T_2, T_3$ adding up to $0$, then $k$ is at most
 $$ \delta + \eta (d[X^0_1;T_1|T_3]-d[X^0_1;X_1]) + \eta (d[X^0_2;T_2|T_3]-d[X^0_2;X_2])$$
 where $\delta = I[T₁ : T₂ ; μ] + I[T₂ : T₃ ; μ] + I[T₃ : T₁ ; μ]$. -/
@@ -365,6 +371,7 @@ lemma construct_good_prelim' : k ≤ δ + p.η * c[T₁ | T₃ # T₂ | T₃] :=
 
 open ElementaryAddCommGroup
 
+include hT hT₁ hT₂ hT₃ h_min in
 /-- In fact $k$ is at most
  $$ \delta + \frac{\eta}{6}  \sum_{i=1}^2 \sum_{1 \leq j,l \leq 3; j \neq l}
      (d[X^0_i;T_j|T_l] - d[X^0_i; X_i]).$$
@@ -394,6 +401,7 @@ lemma construct_good_improved' :
   simp only [I1, I2, I3] at Z123 Z132 Z213 Z231 Z312 Z321
   linarith
 
+include h_min in
 /-- Rephrase `construct_good_improved'` with an explicit probability measure, as we will
 apply it to (varying) conditional measures. -/
 lemma construct_good_improved'' {Ω' : Type*} [MeasurableSpace Ω'] (μ : Measure Ω')
@@ -412,6 +420,7 @@ lemma construct_good_improved'' {Ω' : Type*} [MeasurableSpace Ω'] (μ : Measur
 
 end aux
 
+include hX₁ hX₂ hX₁' hX₂' h_min in
 /--   $k$ is at most
 $$ \leq I(U : V \, | \, S) + I(V : W \, | \,S) + I(W : U \, | \, S) + \frac{\eta}{6}
 \sum_{i=1}^2 \sum_{A,B \in \{U,V,W\}: A \neq B} (d[X^0_i;A|B,S] - d[X^0_i; X_i]).$$
@@ -446,6 +455,7 @@ lemma averaged_construct_good : k ≤ (I[U : V | S] + I[V : W | S] + I[W : U | S
 
 variable (p)
 
+include hX₁ hX₂ hX₁' hX₂' h_indep h₁ h₂ in
 lemma dist_diff_bound_1 :
       (d[p.X₀₁ # U | ⟨V, S⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # U | ⟨W, S⟩] - d[p.X₀₁ # X₁])
     + (d[p.X₀₁ # V | ⟨U, S⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # V | ⟨W, S⟩] - d[p.X₀₁ # X₁])
@@ -465,11 +475,11 @@ lemma dist_diff_bound_1 :
   have C5 : W + X₂' + X₂ = S := by abel
   have C7 : X₂ + X₁' = V := by abel
   have C8 : X₁ + X₁' = W := by abel
-  have C9 : d[X₁ # X₂'] = d[X₁ # X₂] := (IdentDistrib.refl hX₁.aemeasurable).rdist_eq  h₂.symm
+  have C9 : d[X₁ # X₂'] = d[X₁ # X₂] := (IdentDistrib.refl hX₁.aemeasurable).rdist_eq h₂.symm
   have C10 : d[X₂ # X₁'] = d[X₁' # X₂] := rdist_symm
-  have C11 : d[X₁ # X₁'] = d[X₁ # X₁] := (IdentDistrib.refl hX₁.aemeasurable).rdist_eq  h₁.symm
+  have C11 : d[X₁ # X₁'] = d[X₁ # X₁] := (IdentDistrib.refl hX₁.aemeasurable).rdist_eq h₁.symm
   have C12 : d[X₁' # X₂'] = d[X₁ # X₂] := h₁.symm.rdist_eq  h₂.symm
-  have C13 : d[X₂ # X₂'] = d[X₂ # X₂] := (IdentDistrib.refl hX₂.aemeasurable).rdist_eq  h₂.symm
+  have C13 : d[X₂ # X₂'] = d[X₂ # X₂] := (IdentDistrib.refl hX₂.aemeasurable).rdist_eq h₂.symm
   have C14 : d[X₁' # X₂] = d[X₁ # X₂] := h₁.symm.rdist_eq  (IdentDistrib.refl hX₂.aemeasurable)
   have C15 : H[X₁' + X₂'] = H[U] := by
     apply ProbabilityTheory.IdentDistrib.entropy_eq
@@ -537,6 +547,7 @@ lemma dist_diff_bound_1 :
     C20, C21, C22, C23, C24, C25, C26, C27, C28, C29, C30] at I1 I2 I3 I4 I5 I6 ⊢
   linarith only [I1, I2, I3, I4, I5, I6]
 
+include hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep in
 lemma dist_diff_bound_2 :
       ((d[p.X₀₂ # U | ⟨V, S⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # U | ⟨W, S⟩] - d[p.X₀₂ # X₂])
     + (d[p.X₀₂ # V | ⟨U, S⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # V | ⟨W, S⟩] - d[p.X₀₂ # X₂])
@@ -645,6 +656,7 @@ lemma dist_diff_bound_2 :
     at I1 I2 I3 I4 I5 I6 ⊢
   linarith only [I1, I2, I3, I4, I5, I6]
 
+include hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep h_min in
 lemma averaged_final : k ≤ (6 * p.η * k - (1 - 5 * p.η) / (1 - p.η) * (2 * p.η * k - I₁))
     + p.η / 6 * (8 * k + 2 * (d[X₁ # X₁] + d[X₂ # X₂])) := by
   apply (averaged_construct_good hX₁ hX₂ hX₁' hX₂' h_min).trans
@@ -654,6 +666,7 @@ lemma averaged_final : k ≤ (6 * p.η * k - (1 - 5 * p.η) / (1 - p.η) * (2 *
   linarith [dist_diff_bound_1 p hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep,
     dist_diff_bound_2 p hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep]
 
+include hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep h_min in
 /-- Suppose $0 < \eta < 1/8$.  Let $X_1, X_2$ be tau-minimizers.  Then $d[X_1;X_2] = 0$. The proof
 of this lemma uses copies `X₁', X₂'` already in the context. For a version that does not assume
 these are given and constructs them instead, use `tau_strictly_decreases'`.
@@ -678,6 +691,7 @@ theorem tau_strictly_decreases_aux' (hp : 8 * p.η < 1) : d[X₁ # X₂] = 0 :=
   apply le_antisymm _ (rdist_nonneg hX₁ hX₂)
   nlinarith
 
+include hX₁ hX₂ h_min in
 theorem tau_strictly_decreases' (hp : 8 * p.η < 1) : d[X₁ # X₂] = 0 := by
   let ⟨A, mA, μ, Y₁, Y₂, Y₁', Y₂', hμ, h_indep, hY₁, hY₂, hY₁', hY₂', h_id1, h_id2, h_id1', h_id2'⟩
     := independent_copies4_nondep hX₁ hX₂ hX₁ hX₂ ℙ ℙ ℙ ℙ
@@ -964,7 +978,7 @@ lemma PFR_conjecture_improv_aux (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤
     apply Au.trans
     rw [add_sub_assoc]
     apply add_subset_add_left
-    apply (sub_subset_sub (inter_subset_right _ _) (inter_subset_right _ _)).trans
+    apply (sub_subset_sub inter_subset_right inter_subset_right).trans
     rintro - ⟨-, ⟨y, hy, xy, hxy, rfl⟩, -, ⟨z, hz, xz, hxz, rfl⟩, rfl⟩
     simp only [mem_singleton_iff] at hxy hxz
     simpa [hxy, hxz, -ElementaryAddCommGroup.sub_eq_add] using H.sub_mem hy hz

PFR/Main.lean

@@ -1,6 +1,7 @@
 import Mathlib.Combinatorics.Additive.RuzsaCovering
 import Mathlib.GroupTheory.Complement
 import Mathlib.GroupTheory.OrderOfElement
+import Mathlib.Data.Finset.Pointwise.Card
 import PFR.Mathlib.Algebra.Group.Subgroup.Pointwise
 import PFR.ForMathlib.Entropy.RuzsaSetDist
 import PFR.Tactic.RPowSimp
@@ -120,12 +121,13 @@ lemma PFR_conjecture_pos_aux' {G : Type*} [AddCommGroup G] {A : Set G} [Finite A
     simpa [Nat.cast_pos, I, and_false, or_false] using mul_pos_iff.1 (card_AA_pos.trans_le hA)
   exact ⟨KA_pos.2, card_AA_pos, KA_pos.1⟩
 
-variable {G : Type*} [AddCommGroup G] [MeasurableSpace G]
-  [MeasurableSingletonClass G] {A : Set G} [Finite A] {K : ℝ} [Countable G]
+variable {G : Type*} [AddCommGroup G] {A : Set G} [Finite A] {K : ℝ} [Countable G]
 
 /-- A uniform distribution on a set with doubling constant `K` has self Rusza distance
 at most `log K`. -/
-theorem rdist_le_of_isUniform_of_card_add_le (h₀A : A.Nonempty) (hA : Nat.card (A - A) ≤ K * Nat.card A)
+theorem rdist_le_of_isUniform_of_card_add_le [MeasurableSpace G]
+    [MeasurableSingletonClass G]
+    (h₀A : A.Nonempty) (hA : Nat.card (A - A) ≤ K * Nat.card A)
     {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)] {U₀ : Ω → G}
     (U₀unif : IsUniform A U₀) (U₀meas : Measurable U₀) : d[U₀ # U₀] ≤ log K := by
   obtain ⟨A_pos, AA_pos, K_pos⟩ : (0 : ℝ) < Nat.card A ∧ (0 : ℝ) < Nat.card (A - A) ∧ 0 < K :=
@@ -138,21 +140,21 @@ theorem rdist_le_of_isUniform_of_card_add_le (h₀A : A.Nonempty) (hA : Nat.card
       convert entropy_le_log_card_of_mem (A := (A-A).toFinite.toFinset) ?_ ?_ with x
       · simp
         exact Iff.rfl
-      . measurability
+      · measurability
       filter_upwards [Uunif.ae_mem, U'unif.ae_mem] with ω h1 h2
       simp
       exact Set.sub_mem_sub h1 h2
     have J : log (Nat.card (A - A)) ≤ log K + log (Nat.card A) := by
       apply (log_le_log AA_pos hA).trans (le_of_eq _)
       rw [log_mul K_pos.ne' A_pos.ne']
---    have : H[U + U'] = H[U - U'] := by congr; simp
     rw [UU'_indep.rdist_eq hU hU', IsUniform.entropy_eq' Uunif hU, IsUniform.entropy_eq' U'unif hU']
     linarith
   rwa [idU.rdist_eq idU'] at IU
 
 variable [ElementaryAddCommGroup G 2] [Fintype G]
 
-lemma sumset_eq_sub : A + A = A - A := by
+lemma sumset_eq_sub {G : Type*} [AddCommGroup G] [ElementaryAddCommGroup G 2] (A : Set G) :
+    A + A = A - A := by
   rw [← Set.image2_add, ← Set.image2_sub]
   congr! 1 with a _ b _
   show a + b = a - b

PFR/Mathlib/Probability/Independence/Kernel.lean

@@ -175,7 +175,6 @@ lemma iIndepFun.finsets [IsMarkovKernel κ] {J : Type*} [Fintype J]
   rw [h1 i]
 
 
-
 /-- If `f` is a family of mutually independent random variables, `(S j)ⱼ` are pairwise disjoint
 finite index sets, and `φ j` is a function that maps the tuple formed by `f i` for `i ∈ S j` to a
 measurable space `γ j`, then the family of random variables formed by `φ j (f i)_{i ∈ S j}` and

PFR/MoreRuzsaDist.lean

@@ -871,11 +871,11 @@ lemma condMultiDist_eq {m : ℕ} {Ω : Type*} (hΩ : MeasureSpace Ω) (hprob: Is
           rw [<-Finset.mul_sum, <-mul_assoc, mul_comm _ (f y), mul_assoc, <-mul_sub, inv_mul_eq_div]
         _ = _ := by
           congr
-          . rw [condEntropy_eq_sum_fintype]
-            . apply Finset.sum_congr rfl
+          · rw [condEntropy_eq_sum_fintype]
+            · apply Finset.sum_congr rfl
               intro y _
               congr
-              . calc
+              · calc
                   _ = (∏ i, (ℙ (E i (y i)))).toReal := Eq.symm ENNReal.toReal_prod
                   _ = (ℙ (⋂ i, (E i (y i)))).toReal := by
                     congr
@@ -888,7 +888,7 @@ lemma condMultiDist_eq {m : ℕ} {Ω : Type*} (hΩ : MeasureSpace Ω) (hprob: Is
                     ext x
                     simp [E]
                     exact Iff.symm funext_iff
-              . exact Finset.sum_fn Finset.univ fun c ↦ X c
+              · exact Finset.sum_fn Finset.univ fun c ↦ X c
               ext x
               simp [E']
               exact Iff.symm funext_iff
@@ -917,12 +917,12 @@ lemma condMultiDist_eq {m : ℕ} {Ω : Type*} (hΩ : MeasureSpace Ω) (hprob: Is
                   apply Finset.prod_congr rfl
                   intro i' _
                   by_cases h : i' = i
-                  . simp [h, E]
+                  · simp [h, E]
                     rw [condEntropy_eq_sum_fintype]
                     exact hY i
-                  simp [h, E]
-                  apply (sum_measure_preimage_singleton' _ _).symm
-                  exact hY i'
+                  · simp [h, E]
+                    apply (sum_measure_preimage_singleton' _ _).symm
+                    exact hY i'
 
 end multiDistance
 

PFR/WeakPFR.lean

@@ -205,10 +205,10 @@ lemma torsion_free_doubling [FiniteRange X] [FiniteRange Y]
 /-- If `G` is a torsion-free group and `X, Y` are `G`-valued random variables and
 `φ : G → 𝔽₂^d` is a homomorphism then `H[φ ∘ X ; μ] ≤ 10 * d[X; μ # Y ; μ']`. -/
 lemma torsion_dist_shrinking {H : Type u} [FiniteRange X] [FiniteRange Y] (hX : Measurable X)
-  (hY : Measurable Y) [AddCommGroup H] [ElementaryAddCommGroup H 2]
-  [MeasurableSpace H] [MeasurableSingletonClass H] [Countable H]
-  (hG : AddMonoid.IsTorsionFree G) (φ : G →+ H) :
-  H[φ ∘ X ; μ] ≤ 10 * d[X; μ # Y ; μ'] := by
+    (hY : Measurable Y) [AddCommGroup H] [ElementaryAddCommGroup H 2]
+    [MeasurableSpace H] [MeasurableSingletonClass H] [Countable H]
+    (hG : AddMonoid.IsTorsionFree G) (φ : G →+ H) :
+    H[φ ∘ X ; μ] ≤ 10 * d[X; μ # Y ; μ'] := by
   have :=
     calc d[φ ∘ X ; μ # φ ∘ (Y + Y); μ'] ≤ d[X; μ # (Y + Y) ; μ'] := rdist_of_hom_le φ hX (Measurable.add hY hY)
     _ ≤ 5 * d[X; μ # Y ; μ'] := torsion_free_doubling X Y μ μ' hX hY hG
@@ -220,8 +220,7 @@ lemma torsion_dist_shrinking {H : Type u} [FiniteRange X] [FiniteRange Y] (hX :
 end Torsion
 
 instance {G : Type u} [AddCommGroup G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G]
-  (H : AddSubgroup G)
-    : MeasurableSingletonClass (G ⧸ H) :=
+    (H : AddSubgroup G) : MeasurableSingletonClass (G ⧸ H) :=
   ⟨λ _ ↦ by { rw [measurableSet_quotient]; simp [measurableSet_discrete] }⟩
 
 section F2_projection
@@ -240,10 +239,10 @@ There is a non-trivial subgroup $H\leq G$ such that
 where $\psi:G\to G/H$ is the natural projection homomorphism.
 -/
 lemma app_ent_PFR' [MeasureSpace Ω] [MeasureSpace Ω'] (X : Ω → G) (Y : Ω' → G)
-  [IsProbabilityMeasure (ℙ : Measure Ω)] [IsProbabilityMeasure (ℙ : Measure Ω')]
-  {α : ℝ} (hent : 20 * d[X # Y] < α * (H[X] + H[Y])) (hX : Measurable X) (hY : Measurable Y) :
-  ∃ H : AddSubgroup G, log (Nat.card H) < (1 + α) / 2 * (H[X] + H[Y]) ∧
-  H[(QuotientAddGroup.mk' H) ∘ X] + H[(QuotientAddGroup.mk' H) ∘ Y] < α * (H[X] + H[Y]) := by
+    [IsProbabilityMeasure (ℙ : Measure Ω)] [IsProbabilityMeasure (ℙ : Measure Ω')]
+    {α : ℝ} (hent : 20 * d[X # Y] < α * (H[X] + H[Y])) (hX : Measurable X) (hY : Measurable Y) :
+    ∃ H : AddSubgroup G, log (Nat.card H) < (1 + α) / 2 * (H[X] + H[Y]) ∧
+    H[(QuotientAddGroup.mk' H) ∘ X] + H[(QuotientAddGroup.mk' H) ∘ Y] < α * (H[X] + H[Y]) := by
   let p : refPackage Ω Ω' G := {
     X₀₁ := X
     X₀₂ := Y
@@ -498,6 +497,20 @@ lemma single_fibres {G H Ω Ω': Type u}
       haveI : Nonempty (A_ x) := h_Ax ⟨x, hx⟩
       haveI : Nonempty (B_ y) := h_By ⟨y, hy⟩
       let μx := (ℙ : Measure Ω)[|(φ.toFun ∘ UA) ⁻¹' {x}]
+      have hμx : IsProbabilityMeasure μx := by
+        apply ProbabilityTheory.cond_isProbabilityMeasure
+        rw [Set.preimage_comp]
+        apply hUA_coe.measure_preimage_ne_zero hUA'
+
+
+        sorry
+      sorry
+    _ ≤ _ := sorry
+  sorry
+
+
+#exit
+
       let μy := (ℙ : Measure Ω')[|(φ.toFun ∘ UB) ⁻¹' {y}]
       have h_μ_p : IsProbabilityMeasure μx ∧ IsProbabilityMeasure μy := by
         constructor <;> apply ProbabilityTheory.cond_isProbabilityMeasure <;> rw [Set.preimage_comp]
@@ -516,6 +529,9 @@ lemma single_fibres {G H Ω Ω': Type u}
     _ ≤ d[UA # UB] - d[φ.toFun ∘ UA # φ.toFun ∘ UB] := by
       rewrite [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe]
       linarith only [rdist_le_sum_fibre φ hUA' hUB' (μ := ℙ) (μ' := ℙ)]
+
+#exit
+
   let M := H[φ.toFun ∘ UA] + H[φ.toFun ∘ UB]
   have hM : M = ∑ x in X, ∑ y in Y, Real.negMulLog (p x y) := by
     have h_compl {x y} (h_notin : (x, y) ∉ X ×ˢ Y) : Real.negMulLog (p x y) = 0 := by