chore(Probability): remove 15/24 backward.isDefEq.respectTransparency options (#42733)

Remove 15 of the 24 `set_option backward.isDefEq.respectTransparency` (and `.types`) occurrences in `Mathlib/Probability`.

See #42734 for 5 more.
See #42735 for 1 more. 
See #42738 for 2 more in `Mathlib/Probability`.
See #42739 for the last one.

Author: FrankieNC

Mathlib/Probability/Distributions/Binomial.lean

@@ -127,14 +127,13 @@ lemma binomial_real_self (n : ℕ) (p : I) :
 lemma map_cast_binomial_real_self [MeasurableSingletonClass R] [CharZero R] (n : ℕ) (p : I) :
     Bin(R, n, p).real {(n : R)} = p ^ n := by simp [map_cast_binomial_real_singleton]
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp]
 lemma binomial_one_eq_bernoulliMeasure (p : I) :
     Bin(1, p) = Ber(1, 0, p) := by
   refine ext_of_measureReal_singleton fun k ↦ ?_
   match k with
   | 0 | 1 => simp
-  | k + 2 => simp [binomial_real_singleton]
+  | k + 2 => simp [binomial_real_singleton, Nat.choose_eq_zero_of_lt]
 
 lemma binomial_eq_sum_dirac (n : ℕ) (p : I) :
     Bin(n, p) =

Mathlib/Probability/Distributions/Fernique.lean

@@ -377,7 +377,6 @@ lemma lintegral_closedBall_sdiff_exp_logRatio_mul_sq_le [IsProbabilityMeasure μ
 alias lintegral_closedBall_diff_exp_logRatio_mul_sq_le :=
   lintegral_closedBall_sdiff_exp_logRatio_mul_sq_le
 
-set_option backward.isDefEq.respectTransparency.types false in
 open Metric in
 lemma lintegral_exp_mul_sq_norm_le_mul [IsProbabilityMeasure μ]
     (h_rot : (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) = μ.prod μ)
@@ -421,7 +420,7 @@ lemma lintegral_exp_mul_sq_norm_le_mul [IsProbabilityMeasure μ]
     rw [← setLIntegral_univ]
     refine setLIntegral_congr ?_
     rw [← ae_iff_prob_eq_one ?_] at ha
-    · rw [eventuallyEq_comm, ae_eq_univ]
+    · refine (ae_eq_univ.2 ?_).symm
       change μ {x | ¬ x ∈ closedBall 0 a} = 0
       rw [← ae_iff]
       filter_upwards [ha] with x hx using by simp [hx]

Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Basic.lean

@@ -52,14 +52,12 @@ lemma aemeasurable (hX : IsGaussianProcess X P) (t : T) : AEMeasurable (X t) P :
   AEMeasurable.of_map_ne_zero
     (hX.hasGaussianLaw {t}).isGaussian_map.toIsProbabilityMeasure.ne_zero |>.eval ⟨t, by simp⟩
 
-set_option backward.isDefEq.respectTransparency false in
 /-- A modification of a Gaussian process is a Gaussian process. -/
 lemma congr (hX : IsGaussianProcess X P) (hXY : ∀ t, X t =ᵐ[P] Y t) :
     IsGaussianProcess Y P where
   hasGaussianLaw I := by
-    constructor
-    rw [map_restrict_eq_of_forall_ae_eq fun t ↦ (hXY t).symm]
-    exact (hX.hasGaussianLaw I).isGaussian_map
+    refine (hX.hasGaussianLaw I).congr ?_
+    filter_upwards [ae_all_iff.2 fun i : I ↦ hXY i] with ω h using funext h
 
 end Basic
 

Mathlib/Probability/Distributions/Gaussian/Real.lean

@@ -325,7 +325,6 @@ lemma gaussianReal_map_const_add (y : ℝ) :
   simp_rw [add_comm y]
   exact gaussianReal_map_add_const y
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- The map of a Gaussian distribution by multiplication by a constant is a Gaussian. -/
 lemma gaussianReal_map_const_mul (c : ℝ) :
     (gaussianReal μ v).map (c * ·) = gaussianReal (c * μ) (.mk (c ^ 2) (sq_nonneg _) * v) := by
@@ -345,8 +344,7 @@ lemma gaussianReal_map_const_mul (c : ℝ) :
   · simp only [ne_eq, mul_eq_zero, hv, or_false]
     rw [← NNReal.coe_inj]
     simp [hc]
-  simp only [e, Homeomorph.mulLeft₀,
-    Equiv.mulLeft₀_symm_apply, Homeomorph.toMeasurableEquiv_coe, Homeomorph.homeomorph_mk_coe_symm,
+  simp only [e, Homeomorph.toMeasurableEquiv_coe, Homeomorph.mulLeft₀_symm_apply,
     gaussianPDFReal_inv_mul hc]
   congr with x
   suffices |c⁻¹| * |c| = 1 by rw [← mul_assoc, this, one_mul]

Mathlib/Probability/Distributions/Uniform.lean

@@ -236,13 +236,10 @@ theorem uniformOfFinset_apply_of_mem (ha : a ∈ s) : uniformOfFinset s hs a = (
 
 theorem uniformOfFinset_apply_of_notMem (ha : a ∉ s) : uniformOfFinset s hs a = 0 := by simp [ha]
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp]
-theorem support_uniformOfFinset : (uniformOfFinset s hs).support = s :=
-  Set.ext
-    (by
-      let ⟨a, ha⟩ := hs
-      simp [mem_support_iff])
+theorem support_uniformOfFinset : (uniformOfFinset s hs).support = s := by
+  ext a
+  simp [mem_support_iff]
 
 theorem mem_support_uniformOfFinset_iff (a : α) : a ∈ (uniformOfFinset s hs).support ↔ a ∈ s := by
   simp

Mathlib/Probability/IdentDistrib.lean

@@ -295,7 +295,6 @@ section UniformIntegrable
 variable {E : Type*} [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E]
   {μ : Measure α} [IsFiniteMeasure μ]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- This lemma is superseded by `MemLp.uniformIntegrable_of_identDistrib` which only requires
 `AEStronglyMeasurable`. -/
 theorem MemLp.uniformIntegrable_of_identDistrib_aux {ι : Type*} {f : ι → α → E} {j : ι} {p : ℝ≥0∞}
@@ -304,21 +303,21 @@ theorem MemLp.uniformIntegrable_of_identDistrib_aux {ι : Type*} {f : ι → α
   refine uniformIntegrable_of' hp hp' hfmeas fun ε hε => ?_
   by_cases hι : Nonempty ι
   swap; · exact ⟨0, fun i => False.elim (hι <| Nonempty.intro i)⟩
-  obtain ⟨C, hC₁, hC₂⟩ := hℒp.eLpNorm_indicator_norm_ge_pos_le (hfmeas _) hε
-  refine ⟨⟨C, hC₁.le⟩, fun i => le_trans (le_of_eq ?_) hC₂⟩
-  have : {x | (⟨C, hC₁.le⟩ : ℝ≥0) ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖} := by
+  obtain ⟨C, -, hC₂⟩ := hℒp.eLpNorm_indicator_norm_ge_pos_le (hfmeas _) hε
+  refine ⟨C.toNNReal, fun i ↦ le_trans (le_of_eq ?_) hC₂⟩
+  have : {x | C.toNNReal ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖} := by
     ext x
-    simp_rw [← norm_toNNReal]
-    exact Real.le_toNNReal_iff_coe_le (norm_nonneg _)
+    simp_rw [Set.mem_ofPred_eq, Real.toNNReal_le_iff_le_coe, coe_nnnorm]
   rw [this, ← eLpNorm_norm, ← eLpNorm_norm (Set.indicator _ _)]
   simp_rw [norm_indicator_eq_indicator_norm, coe_nnnorm]
-  let F : E → ℝ := (fun x : E => if (⟨C, hC₁.le⟩ : ℝ≥0) ≤ ‖x‖₊ then ‖x‖ else 0)
+  let F : E → ℝ := (fun x : E ↦ if C.toNNReal ≤ ‖x‖₊ then ‖x‖ else 0)
   have F_meas : Measurable F := by
     apply measurable_norm.indicator (measurableSet_le measurable_const measurable_nnnorm)
   have : ∀ k, (fun x ↦ Set.indicator {x | C ≤ ‖f k x‖} (fun a ↦ ‖f k a‖) x) = F ∘ f k := by
     intro k
     ext x
-    simp only [Set.indicator, Set.mem_ofPred_eq]; norm_cast
+    simp only [F, Set.indicator, Set.mem_ofPred_eq, Function.comp_apply,
+      Real.toNNReal_le_iff_le_coe, coe_nnnorm]
   rw [this, this, ← eLpNorm_map_measure F_meas.aestronglyMeasurable (hf i).aemeasurable_fst,
     (hf i).map_eq, eLpNorm_map_measure F_meas.aestronglyMeasurable (hf j).aemeasurable_fst]
 

Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean

@@ -191,7 +191,6 @@ lemma tendsto_defaultRatCDF_atBot : Tendsto defaultRatCDF atBot (𝓝 0) := by
   refine ⟨-1, fun q hq => (ite_eq_left (hq.trans_lt ?_)).symm⟩
   linarith
 
-set_option backward.isDefEq.respectTransparency false in
 lemma iInf_rat_gt_defaultRatCDF (t : ℚ) :
     ⨅ r : Ioi t, defaultRatCDF r = defaultRatCDF t := by
   simp only [defaultRatCDF]
@@ -205,8 +204,7 @@ lemma iInf_rat_gt_defaultRatCDF (t : ℚ) :
   · refine le_antisymm ?_ (le_ciInf fun x ↦ ?_)
     · obtain ⟨q, htq, hq_neg⟩ : ∃ q, t < q ∧ q < 0 := ⟨t / 2, by linarith, by linarith⟩
       refine (ciInf_le h_bdd ⟨q, htq⟩).trans ?_
-      rw [ite_eq_left]
-      rwa [Subtype.coe_mk]
+      exact (ite_eq_left hq_neg).le
     · split_ifs
       exacts [le_rfl, zero_le_one]
   · refine le_antisymm ?_ ?_

Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean

@@ -159,10 +159,11 @@ instance instIsMarkovKernelCondKernelUnitReal (κ : Kernel Unit (α × ℝ)) [Is
   rw [condKernelUnitReal]
   infer_instance
 
-set_option backward.isDefEq.respectTransparency false in
 instance condKernelUnitReal.instIsCondKernel (κ : Kernel Unit (α × ℝ)) [IsFiniteKernel κ] :
     κ.IsCondKernel κ.condKernelUnitReal where
-  disintegrate := by rw [condKernelUnitReal, compProd_toKernel]; ext; simp
+  disintegrate := by
+    rw [condKernelUnitReal]
+    exact compProd_toKernel (isCondKernelCDF_condCDF (κ ()))
 
 end Real
 

Mathlib/Probability/Martingale/BorelCantelli.lean

@@ -75,25 +75,25 @@ protected lemma Submartingale.stoppedAbove [IsFiniteMeasure μ] (hf : Submarting
 
 variable {r : ℝ} {R : ℝ≥0}
 
-set_option backward.isDefEq.respectTransparency false in
 theorem stoppedAbove_le (hr : 0 ≤ r) (hf0 : f 0 = 0)
     (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) (i : ℕ) :
     ∀ᵐ ω ∂μ, stoppedAbove f r i ω ≤ r + R := by
   filter_upwards [hbdd] with ω hbddω
-  rw [stoppedAbove, stoppedProcess, ENat.some_eq_natCast]
-  by_cases h_zero : (min (i : ℕ∞) (leastGE f r ω)).untopA = 0
+  rw [stoppedAbove, stoppedProcess]
+  by_cases h_zero : (min (WithTop.some i) (leastGE f r ω)).untopA = 0
   · simp only [h_zero, hf0, Pi.zero_apply]
     positivity
   obtain ⟨k, hk⟩ := Nat.exists_eq_add_one_of_ne_zero h_zero
   rw [hk, add_comm r, ← sub_le_iff_le_add]
   have := notMem_of_lt_hittingAfter (?_ : k < leastGE f r ω)
   · simp only [bot_eq_zero, zero_le, Set.mem_Ici, not_le, forall_const] at this
     exact (sub_lt_sub_left this _).le.trans ((le_abs_self _).trans (hbddω _))
-  · suffices (k : ℕ∞) < min (i : ℕ∞) (leastGE f r ω) from this.trans_le (min_le_right _ _)
-    have h_top : min (i : ℕ∞) (leastGE f r ω) ≠ ⊤ :=
+  · suffices WithTop.some k < min (WithTop.some i) (leastGE f r ω) from
+      this.trans_le (min_le_right _ _)
+    have h_top : min (WithTop.some i) (leastGE f r ω) ≠ ⊤ :=
       ne_top_of_le_ne_top (by simp) (min_le_left _ _)
-    lift min (i : ℕ∞) (leastGE f r ω) to ℕ using h_top with p
-    simp only [untopD_coe_enat, Nat.cast_lt, gt_iff_lt] at *
+    lift min (WithTop.some i) (leastGE f r ω) to ℕ using h_top with p
+    simp only [WithTop.untopD_coe, WithTop.coe_lt_coe, gt_iff_lt] at *
     lia
 
 theorem Submartingale.eLpNorm_stoppedAbove_le [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ)

Mathlib/Probability/Moments/ComplexMGF.lean

@@ -313,7 +313,6 @@ section ext
 
 variable {Ω' : Type*} {mΩ' : MeasurableSpace Ω'} {Y : Ω' → ℝ} {μ' : Measure Ω'}
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- If the complex moment-generating functions of two random variables `X` and `Y` with respect to
 the finite measures `μ`, `μ'`, respectively, coincide, then `μ.map X = μ'.map Y`. In other words,
 complex moment-generating functions separate the distributions of random variables. -/
@@ -323,8 +322,9 @@ theorem _root_.MeasureTheory.Measure.ext_of_complexMGF_eq [IsFiniteMeasure μ]
     μ.map X = μ'.map Y := by
   have inner_ne_zero (x : ℝ) (h : x ≠ 0) : innerₗ ℝ x ≠ 0 :=
     DFunLike.ne_iff.mpr ⟨x, inner_self_ne_zero.mpr h⟩
+  have h_cont : Continuous fun p : ℝ × ℝ ↦ innerₗ ℝ p.1 p.2 := continuous_inner
   apply MeasureTheory.ext_of_integral_char_eq continuous_probChar probChar_ne_one inner_ne_zero
-    continuous_inner (fun w ↦ ?_)
+    h_cont (fun w ↦ ?_)
   rw [funext_iff] at h
   specialize h (Multiplicative.toAdd w * I)
   simp_rw [complexMGF, mul_assoc, mul_comm I, ← mul_assoc] at h