mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f : β × γ → E
hf : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ (fun x ↦ ∫ (y : γ), f (x, y) ∂η (a, x)) =ᵐ[κ a] fun x ↦ ∫ (y : γ), AEStronglyMeasurable.mk f hf (x, y) ∂η (a, x)

Tactic:
filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with _ hx using integral_congr_ae hx

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: case e'_3
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure 𝓧 := (ν univ)⁻¹ • μ
ν' : Measure 𝓧 := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᵐ[ν] μ.rnDeriv ν
h_eq : ∫ (x : 𝓧), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν.real univ)⁻¹ * ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
h : ν.real univ * f (μ'.real univ) ≤ ∫ (x : 𝓧), f (μ.rnDeriv ν x).toReal ∂ν
⊢ μ.real univ / ν.real univ = μ'.real univ

Tactic:
· simp only [div_eq_inv_mul, Measure.smul_apply, smul_eq_mul, ENNReal.toReal_mul,
      ENNReal.toReal_inv, μ', measureReal_def]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
s : Set 𝓧
hs : MeasurableSet s
hsμ : μ s < ∞
⊢ ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨) in univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a ∂μ = ∫⁻ (a : 𝓧) in s, (κ a) univ ∂μ

Tactic:
← Measure.setLIntegral_compProd (by fun_prop) hs .univ,

Goal state after:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
s : Set 𝓧
hs : MeasurableSet s
hsμ : μ s < ∞
⊢ ∫⁻ (x : 𝓧 × 𝓨) in s ×ˢ univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) x ∂μ ⊗ₘ η = ∫⁻ (a : 𝓧) in s, (κ a) univ ∂μ
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᵐ[ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ log c⁻¹.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal

Tactic:
ENNReal.toReal_inv,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᵐ[ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ log c.toReal⁻¹ + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f : γ → E
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn f s ((η ∘ₖ κ) a)
⊢ ∫ (x : β), ∫ (y : γ), f y ∂(η.restrict hs) x ∂κ a = ∫ (x : β), ∫ (y : γ) in s, f y ∂η x ∂κ a

Tactic:
simp_rw [restrict_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
H : ∀ᵐ (a : X) ∂μ, ∑' (n : ι), ‖f n a‖ₑ < ∞
⊢ ∀ᵐ (a : X) ∂μ, Summable fun n ↦ ‖f n a‖

Tactic:
filter_upwards [H] with x hx using tsum_enorm_ne_top_iff_summable_norm.1 hx.ne

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
f : ↥(Lp ℝ 2 μ)
⊢ ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖↑↑f x‖₊ ∂μ

Tactic:
by
  let h_meas := lpMeas.aestronglyMeasurable (condExpL2 ℝ ℝ hm f)
  let g := h_meas.choose
  have hg_meas : StronglyMeasurable[m] g := h_meas.choose_spec.1
  have hg_eq : g =ᵐ[μ] condExpL2 ℝ ℝ hm f := h_meas.choose_spec.2.symm
  have hg_eq_restrict : g =ᵐ[μ.restrict s] condExpL2 ℝ ℝ hm f := ae_restrict_of_ae hg_eq
  have hg_nnnorm_eq : (fun x => (‖g x‖₊ : ℝ≥0∞)) =ᵐ[μ.restrict s] fun x =>
      (‖(condExpL2 ℝ ℝ hm f : α → ℝ) x‖₊ : ℝ≥0∞) := by
    refine hg_eq_restrict.mono fun x hx => ?_
    dsimp only
    simp_rw [hx]
  rw [lintegral_congr_ae hg_nnnorm_eq.symm]
  refine lintegral_enorm_le_of_forall_fin_meas_integral_eq
    hm (Lp.stronglyMeasurable f) ?_ ?_ ?_ ?_ hs hμs
  · exact integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs
  · exact hg_meas
  · rw [IntegrableOn, integrable_congr hg_eq_restrict]
    exact integrableOn_condExpL2_of_measure_ne_top hm hμs f
  · intro t ht hμt
    rw [← integral_condExpL2_eq_of_fin_meas_real (hm := hm) f ht hμt.ne]
    exact setIntegral_congr_ae (hm t ht) (hg_eq.mono fun x hx _ => hx)

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hf_int : Integrable f μ
hs : MeasurableSet s
hm : m ≤ m0
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[s.indicator f | m] =ᵐ[μ] s.indicator μ[f | m]

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm, Set.indicator_zero']; rfl

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hm_not : ¬mΩ ≤ mΩ₀
⊢ P⁻[X | mΩ] = 0

Tactic:
by
  rw [condLExp, dif_neg hm_not]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : f ≤ᵐ[μ] 0
hfint : Integrable f μ
⊢ μ[f | m] ≤ᵐ[μ] 0

pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : f ≤ᵐ[μ] 0
hfint : ¬Integrable f μ
⊢ μ[f | m] ≤ᵐ[μ] 0

Tactic:
· rw [(condExp_zero.symm : (0 : α → E) = μ[0 | m])]
    exact condExp_mono hfint (integrable_zero _ _ _) hf

Goal state after:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : f ≤ᵐ[μ] 0
hfint : ¬Integrable f μ
⊢ μ[f | m] ≤ᵐ[μ] 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (Measure.map g ν)
this : SigmaFinite ν
h_ne_top1 : ∀ᵐ (x : 𝓧) ∂ν, (Measure.map g μ).rnDeriv (Measure.map g ν) (g x) ≠ ∞
h_ne_top2 : ∀ᵐ (x : 𝓧) ∂ν, ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x ≠ ∞
h_condExp :
  (fun x ↦ (ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x).toReal) =ᵐ[ν]
    ν[fun x ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨]
x : 𝓧
hx :
  ((Measure.map g μ).rnDeriv (Measure.map g ν) (g x)).toReal =
    ν[fun a ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨] x
⊢ (ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x).toReal =
      ν[fun x ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨] x →
    (Measure.map g μ).rnDeriv (Measure.map g ν) (g x) ≠ ∞ →
      ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x ≠ ∞ →
        (Measure.map g μ).rnDeriv (Measure.map g ν) (g x) = ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x

Tactic:
h_condExp

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (Measure.map g ν)
this : SigmaFinite ν
h_ne_top1 : ∀ᵐ (x : 𝓧) ∂ν, (Measure.map g μ).rnDeriv (Measure.map g ν) (g x) ≠ ∞
h_ne_top2 : ∀ᵐ (x : 𝓧) ∂ν, ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x ≠ ∞
h_condExp✝ :
  (fun x ↦ (ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x).toReal) =ᵐ[ν]
    ν[fun x ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨]
x : 𝓧
hx :
  ((Measure.map g μ).rnDeriv (Measure.map g ν) (g x)).toReal =
    ν[fun a ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨] x
h_condExp :
  (ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x).toReal =
    ν[fun x ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨] x
⊢ (Measure.map g μ).rnDeriv (Measure.map g ν) (g x) ≠ ∞ →
    ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x ≠ ∞ →
      (Measure.map g μ).rnDeriv (Measure.map g ν) (g x) = ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨] x
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
this✝ : CompleteSpace ↥Y
this : SecondCountableTopology ↥Y
φY : ↥Y → ℝ := φ ∘ ⇑Y.subtypeL
fY : α → ↥Y := fun a ↦ if h : f a ∈ Y then ⟨f a, h⟩ else 0
fX : α → E := ⇑Y.subtypeL ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᵐ[μ] fX
hfY_int : Integrable fY μ
lem2 : μ[f | m] =ᵐ[μ] ⇑Y.subtypeL ∘ μ[fY | m]
lem3 : φ ∘ f =ᵐ[μ] φY ∘ fY
x : ↥Y
⊢ x ∈ ⇑Y.subtypeL ⁻¹' s → Y.subtypeL x ∈ s

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
          (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
          goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem
          in the new canonicalizer; a minimization would help. The original proof was: `grind` -/

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
this✝ : CompleteSpace ↥Y
this : SecondCountableTopology ↥Y
φY : ↥Y → ℝ := φ ∘ ⇑Y.subtypeL
fY : α → ↥Y := fun a ↦ if h : f a ∈ Y then ⟨f a, h⟩ else 0
fX : α → E := ⇑Y.subtypeL ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᵐ[μ] fX
hfY_int : Integrable fY μ
lem2 : μ[f | m] =ᵐ[μ] ⇑Y.subtypeL ∘ μ[fY | m]
lem3 : φ ∘ f =ᵐ[μ] φY ∘ fY
x : ↥Y
⊢ x ∈ ⇑Y.subtypeL ⁻¹' s → Y.subtypeL x ∈ s
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ φ ∘ μ[f | m] ≤ᵐ[μ] μ[φ ∘ f | m]

Tactic:
borelize E
  obtain ⟨t, ht, htt⟩ := hf_int.aestronglyMeasurable.isSeparable_ae_range
  let Y := (Submodule.span ℝ t).topologicalClosure
  have : CompleteSpace Y := (Submodule.isClosed_topologicalClosure _).completeSpace_coe
  have : SecondCountableTopology Y := ht.span.closure.secondCountableTopology
  let φY := φ ∘ Y.subtypeL
  classical
  let fY : α → Y := fun a => if h : f a ∈ Y then ⟨f a, h⟩ else 0
  let fX : α → E := Y.subtypeL ∘ fY
  have lem0 : ∀ᵐ a ∂μ, f a ∈ Y := by
    filter_upwards [htt] with a ha using
      (Submodule.closure_subset_topologicalClosure_span t) (subset_closure ha)
  have lem1 : f =ᵐ[μ] fX := by
    filter_upwards [lem0] with a ha
    simp_all [fX, fY]
  have hfY_int : Integrable fY μ := by
    refine (hf_int.congr lem1).mono ?_ (by simp [fX])
    obtain ⟨g, hg1, hg2, hg3⟩ := hf_int.1.exists_stronglyMeasurable_range_subset
      ((Submodule.isClosed_topologicalClosure _).measurableSet) Nonempty.of_subtype lem0
    refine ⟨codRestrict g Y hg2, (hg1.measurable.codRestrict hg2).stronglyMeasurable, ?_⟩
    filter_upwards [hg3] with a ha
    have : g a ∈ Y := hg2 a
    simp_all [fY, codRestrict]
  have lem2 : μ[f | m] =ᵐ[μ] Y.subtypeL ∘ μ[fY | m] := calc
    _ =ᵐ[μ] μ[fX | m] := condExp_congr_ae lem1
    _ =ᵐ[μ] _ := (Y.subtypeL.comp_condExp_comm hfY_int).symm
  have lem3 : φ ∘ f =ᵐ[μ] φY ∘ fY := by filter_upwards [lem1] with a ha; simp [φY, ha, fX]
  calc
    φ ∘ μ[f | m]
      =ᵐ[μ] φY ∘ μ[fY | m] := by filter_upwards [lem2] with a ha; simp [φY, ha]
    _ ≤ᵐ[μ] μ[φY ∘ fY | m] := by
      refine (hφ_cvx.comp_linearMap Y.subtype).map_condExp_le_of_hereditarilyLindelofSpace
        (s := Y.subtypeL ⁻¹' s) hm ?_ ?_ ?_ hfY_int (Integrable.congr hφ_int lem3)
      · exact hφ_cont.comp (by fun_prop) fun x => by
          #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
          (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
          goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem
          in the new canonicalizer; a minimization would help. The original proof was: `grind` -/
          simp
      · filter_upwards [lem0, hf] with a ha hb
        simp_all [fY]
      · exact hs.preimage Y.subtypeL.continuous
    _ =ᵐ[μ] μ[φ ∘ f | m] := condExp_congr_ae lem3.symm

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: case mpr
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι → P
⊢ AffineIndependent k p ∧ affineSpan k (range p) = ⊤ → IsUnit (b.toMatrix p)

Tactic:
· rintro ⟨h_tot, h_ind⟩
    let b' : AffineBasis ι k P := ⟨p, h_tot, h_ind⟩
    change IsUnit (b.toMatrix b')
    exact b.isUnit_toMatrix b'

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
⊢ map (↑(AffineEquiv.constVAdd k P ((1 - r) • (c -ᵥ ↑h.some)))) s = map (homothety c r) s

Tactic:
ext p

Goal state after:
case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p : P
⊢ p ∈ map (↑(AffineEquiv.constVAdd k P ((1 - r) • (c -ᵥ ↑h.some)))) s ↔ p ∈ map (homothety c r) s
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝¹² : CommSemiring R
S : Type u_2
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
M : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
⊢ Function.Bijective ⇑(linearMapRightBaseChangeHom S M ε)

Tactic:
set ι := Free.ChooseBasisIndex R M

Goal state after:
R : Type u_1
inst✝¹² : CommSemiring R
S : Type u_2
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
M : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
⊢ Function.Bijective ⇑(linearMapRightBaseChangeHom S M ε)
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝¹² : CommSemiring R
S : Type u_2
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
M : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this : Fintype (Free.ChooseBasisIndex R M)
⊢ Function.Bijective ⇑(linearMapRightBaseChangeHom S M ε)

Tactic:
let e := (b.repr.congrLeft N R).trans (Finsupp.llift N R R ι).symm

Goal state after:
R : Type u_1
inst✝¹² : CommSemiring R
S : Type u_2
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
M : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ (Finsupp.llift N R R ι).symm
⊢ Function.Bijective ⇑(linearMapRightBaseChangeHom S M ε)
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommSemiring R
S : Type u_2
inst✝¹⁵ : CommSemiring S
inst✝¹⁴ : Algebra R S
M : Type u_3
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type u_4
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type u_5
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
Q : Type u_6
inst✝⁷ : AddCommMonoid Q
inst✝⁶ : Module R Q
inst✝⁵ : Module S P
inst✝⁴ : IsScalarTower R S P
inst✝³ : Module S Q
inst✝² : IsScalarTower R S Q
inst✝¹ : Free R M
inst✝ : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
β : N →ₗ[R] Q
k : IsBaseChange S β
f : M →ₗ[R] N
⊢ (⋯.equiv ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft Q S j.equiv) (1 ⊗ₜ[R] f) = (j.linearMapLeftRightHom β) f

Tactic:
ext p

Goal state after:
R : Type u_1
inst✝¹⁶ : CommSemiring R
S : Type u_2
inst✝¹⁵ : CommSemiring S
inst✝¹⁴ : Algebra R S
M : Type u_3
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type u_4
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type u_5
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
Q : Type u_6
inst✝⁷ : AddCommMonoid Q
inst✝⁶ : Module R Q
inst✝⁵ : Module S P
inst✝⁴ : IsScalarTower R S P
inst✝³ : Module S Q
inst✝² : IsScalarTower R S Q
inst✝¹ : Free R M
inst✝ : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
β : N →ₗ[R] Q
k : IsBaseChange S β
f : M →ₗ[R] N
p : P
⊢ ((⋯.equiv ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft Q S j.equiv) (1 ⊗ₜ[R] f)) p =
    ((j.linearMapLeftRightHom β) f) p
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
⊢ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) x) =
    ⇑(homothety (s.points i) x) '' (s.faceOpposite i).closedInterior

Tactic:
ext p

Goal state after:
case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
p : P
⊢ p ∈ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) x) ↔
    p ∈ ⇑(homothety (s.points i) x) '' (s.faceOpposite i).closedInterior
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : Module S P
inst✝ : IsScalarTower R S P
α : M →ₗ[R] P
j : IsBaseChange S α
⊢ j.endHom 1 = 1

Tactic:
ext p

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : Module S P
inst✝ : IsScalarTower R S P
α : M →ₗ[R] P
j : IsBaseChange S α
p : P
⊢ (j.endHom 1) p = 1 p
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
⊢ (⋯.equiv ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft P S j.equiv) (1 ⊗ₜ[R] f) = j.endHom f

Tactic:
ext p

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
p : P
⊢ ((⋯.equiv ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft P S j.equiv) (1 ⊗ₜ[R] f)) p = (j.endHom f) p