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
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)
⊢ ∫ (x : β), ∫ (y : γ), f (x, y) ∂(η.restrict ht) (a, x) ∂(κ.restrict hs) a =
    ∫ (x : β) in s, ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a

Tactic:
Kernel.restrict_apply

Goal state after:
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
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)
⊢ Integrable f (((κ ⊗ₖ η).restrict ⋯) a)

Tactic:
Kernel.restrict_apply

Goal state after:
α : 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
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ((κ ⊗ₖ η) a)
⊢ Integrable f (((κ ⊗ₖ η) a).restrict (s ×ˢ t))
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
⊢ llr μ (↑c • ν) =ᵐ[μ] fun x ↦ llr μ ν x - log ↑c

Tactic:
filter_upwards [llr_smul_right hμν (c : ℝ≥0∞) (by simpa) (by simp)] with x hx

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : c ≠ 0
x : α
hx : llr μ (↑c • ν) x = llr μ ν x - log (↑c).toReal
⊢ llr μ (↑c • ν) x = llr μ ν x - log ↑c
Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Goal state before:
pp: case inl
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
hμ : μ = 0
⊢ llr (μ.tilted f) ν =ᵐ[μ] fun x ↦ f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x

Tactic:
| inl hμ =>

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
mα : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedSpace ℝ E
hp : Fact (1 ≤ p)
inst✝¹ : CompleteSpace ↥(Lp E p μ)
inst✝ : Nontrivial ↥(Lp E p μ)
⊢ ∃ f, f ≠ 0

Tactic:
by
    have : Nontrivial (Lp ℝ p μ) := nontrivial_Lp_real_of_nontrivial_Lp E p μ
    exact exists_ne 0

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : c ≠ 0
⊢ (klDiv μ (c • ν)).toReal = (klDiv μ ν).toReal + (↑c - 1) * ν.real univ - log ↑c * μ.real univ

Tactic:
by
  rw [toReal_klDiv_smul_right_eq_smul_left hμν h_int c, toReal_klDiv_smul_left hμν h_int c⁻¹]
  simp only [NNReal.coe_inv, log_inv, mul_neg, neg_mul, ← sub_eq_add_neg]
  field_simp

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

Goal state before:
pp: α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ ↑↑(lpMeasSubgroupToLpTrim F p μ hm (-f)) =ᵐ[μ.trim hm] -↑↑(lpMeasSubgroupToLpTrim F p μ hm f)

Tactic:
refine (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm (Lp.stronglyMeasurable _).neg
    ?_

Goal state after:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ ↑↑(lpMeasSubgroupToLpTrim F p μ hm (-f)) =ᵐ[μ] -↑↑(lpMeasSubgroupToLpTrim F p μ hm f)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Goal state before:
pp: case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f✝ : ↥(Lp F p μ)
hf✝ : AEStronglyMeasurable (↑↑f✝) μ
f' : ↥(lpMeas F ℝ m p μ) := ⟨f✝, hf✝⟩
g✝ : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'
hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g✝
f g : α → F
hf : MemLp f p (μ.trim hm)
hg : MemLp g p (μ.trim hm)
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf))
hgP : P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp g hg))
⊢ P
    (↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf)) +
      ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp g hg)))

Tactic:
have h_eq :
      ∀ (f : α → F) (hf : MemLp f p (μ.trim hm)),
        ((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf) : Lp F p μ) =
          (memLp_of_memLp_trim hm hf).toLp f :=
      lpMeasToLpTrimLie_symm_toLp hm

Goal state after:
case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f✝ : ↥(Lp F p μ)
hf✝ : AEStronglyMeasurable (↑↑f✝) μ
f' : ↥(lpMeas F ℝ m p μ) := ⟨f✝, hf✝⟩
g✝ : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'
hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g✝
f g : α → F
hf : MemLp f p (μ.trim hm)
hg : MemLp g p (μ.trim hm)
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf))
hgP : P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp g hg))
h_eq :
  ∀ (f : α → F) (hf : MemLp f p (μ.trim hm)), ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf)) = MemLp.toLp f ⋯
⊢ P
    (↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf)) +
      ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp g hg)))
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E'
h_comp :
  ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) =ᵐ[μ] fun a ↦
    (toSpanSingleton ℝ x) (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a)
⊢ (fun a ↦ ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x) =ᵐ[μ]
    ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))

Tactic:
refine EventuallyEq.trans ?_ h_comp.symm

Goal state after:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E'
h_comp :
  ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) =ᵐ[μ] fun a ↦
    (toSpanSingleton ℝ x) (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a)
⊢ (fun a ↦ ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x) =ᵐ[μ] fun a ↦
    (toSpanSingleton ℝ x) (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a)
Module: Mathlib.InformationTheory.KullbackLeibler.ChainRule

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ ∀ᵐ (p : 𝓧 × 𝓨) ∂ν ⊗ₘ η,
    ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal =
      ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)

Tactic:
filter_upwards [rnDeriv_compProd h_ac ν] with p hp

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst✝³ : IsFiniteMeasure μ
inst✝² : IsFiniteMeasure ν
inst✝¹ : IsMarkovKernel κ
inst✝ : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
⊢ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal =
    ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
inst✝ : SigmaFinite (μ.trim hm)
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      (μ.trim hm) s_1 < ∞ →
        IntegrableOn (AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h) s_1 (μ.trim hm)

Tactic:
rintro t - -

Goal state after:
case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
inst✝ : SigmaFinite (μ.trim hm)
h : AEStronglyMeasurable (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
t : Set α
⊢ IntegrableOn (AEStronglyMeasurable.mk (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) h) t (μ.trim hm)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case hfm
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
f : α → F'
inst✝ : CompleteSpace F'
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ AEStronglyMeasurable (↑↑(Integrable.toL1 f hfi)) μ

Tactic:
exact hfm.congr hfi.coeFn_toL1.symm

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

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
⊢ ∫⁻ (ω : Ω), P⁻[X | mΩ] ω ∂P = ∫⁻ (ω : Ω), X ω ∂P

Tactic:
simpa [← setLIntegral_univ] using setLIntegral_condLExp _ _ _ .univ

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

Goal state before:
pp: case pos.refine_1
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
this : ∫ (x : α) in t, μ[s.indicator f | m] x ∂μ = ∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ
hst_m : MeasurableSet (s ∩ t)
⊢ ∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ = ∫ (x : α) in t, μ[s.indicator f | m₂] x ∂μ

Tactic:
setIntegral_condExp hm₂ (hf_int.indicator (hm _ hs_m)) ht,

Goal state after:
case pos.refine_1
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : α → E
s : Set α
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : SigmaFinite (μ.trim hm₂)
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) ↔ MeasurableSet (s ∩ t)
hs_m₂ : MeasurableSet s
hf_int : Integrable f μ
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
this : ∫ (x : α) in t, μ[s.indicator f | m] x ∂μ = ∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ
hst_m : MeasurableSet (s ∩ t)
⊢ ∫ (x : α) in s ∩ t, μ[s.indicator f | m] x ∂μ = ∫ (x : α) in t, s.indicator f x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case inr
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hP : NeZero P
⊢ P⁻[X | ⊥] =ᵐ[P] fun x ↦ (P Set.univ)⁻¹ • ∫⁻ (ω : Ω), X ω ∂P

Tactic:
exact ae_of_all P <| congr_fun (condLExp_bot' P X)

Goal state after:
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
h_int : Integrable (llr μ ν) μ
⊢ Integrable (llr (Measure.map g μ) (Measure.map g ν)) (Measure.map g μ)

Tactic:
← integrable_klFun_rnDeriv_iff (hμν.map hg)

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun x ↦ klFun ((∂Measure.map g μ/∂Measure.map g ν) x).toReal) (Measure.map g ν)
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
h_int : Integrable (llr μ ν) μ
⊢ (if Measure.map g μ ≪ Measure.map g ν ∧ Integrable (llr (Measure.map g μ) (Measure.map g ν)) (Measure.map g μ) then
      ENNReal.ofReal (∫ (x : 𝓨), klFun ((∂Measure.map g μ/∂Measure.map g ν) x).toReal ∂Measure.map g ν)
    else ∞) =
    ENNReal.ofReal (∫ (x : 𝓧), klFun (ν[fun x ↦ ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] x) ∂ν)

Tactic:
if_pos ⟨hμν.map hg, integrable_llr_map hμν hg h_int⟩

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
h_int : Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (∫ (x : 𝓨), klFun ((∂Measure.map g μ/∂Measure.map g ν) x).toReal ∂Measure.map g ν) =
    ENNReal.ofReal (∫ (x : 𝓧), klFun (ν[fun x ↦ ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] x) ∂ν)
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: ι : 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 ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
⊢ b.toMatrix ⇑b₂ * b₂.toMatrix ⇑b = 1

Tactic:
by
  ext l m
  change (b.coords (b₂ l) ᵥ* b₂.toMatrix b) m = _
  rw [toMatrix_vecMul_coords, coords_apply, ← toMatrix_apply, toMatrix_self]

Goal state after:
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
ε : N →ₗ[R] P
s : S
x : S ⊗[R] (M →ₗ[R] N)
⊢ (TensorProduct.lift { toFun := fun s ↦ s • compRight R ε, map_add' := ⋯, map_smul' := ⋯ }).toFun (s • x) =
    (RingHom.id S) s •
      (TensorProduct.lift { toFun := fun s ↦ s • compRight R ε, map_add' := ⋯, map_smul' := ⋯ }).toFun x

Tactic:
by
    simp only [AddHom.toFun_eq_coe, coe_toAddHom, RingHom.id_apply]
    induction x using TensorProduct.induction_on with
    | zero => simp
    | add x y hx hy => simp [smul_add, hx, hy]
    | tmul t f => simp [TensorProduct.smul_tmul', mul_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ polarBilin (Q₁.tmul Q₂) = ⅟2 • BilinForm.tmul (polarBilin Q₁) (polarBilin Q₂)

Tactic:
simp_rw [← two_nsmul_associated A, ← two_nsmul_associated R, BilinForm.tmul, tmul_smul,
    ← smul_tmul', map_nsmul, associated_tmul]

Goal state after:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ 2 • BilinForm.tmul (associated Q₁) (associated Q₂) =
    ⅟2 • 2 • 2 • (BilinForm.tensorDistrib R A) ((associatedHom A) Q₁ ⊗ₜ[R] (associatedHom R) Q₂)
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ polarBilin (QuadraticForm.tmul QuadraticMap.sq Q) = BilinForm.baseChange A (polarBilin Q)

Tactic:
BilinForm.baseChange,

Goal state after:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ polarBilin (QuadraticForm.tmul QuadraticMap.sq Q) = BilinForm.tmul (LinearMap.mul A A) (polarBilin Q)
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case neg
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
eq_top : (↑e).fixedSubmodule ⊔ K ∙ w = ⊤
v : V := (f w)⁻¹ • (e w - w)
⊢ f v = 0

Tactic:
suffices e w - w ∈ LinearMap.ker f by
      simp only [LinearMap.mem_ker, map_sub] at this
      simp only [v, LinearMap.map_smul, map_sub, this, smul_zero]

Goal state after:
case neg
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
eq_top : (↑e).fixedSubmodule ⊔ K ∙ w = ⊤
v : V := (f w)⁻¹ • (e w - w)
⊢ e w - w ∈ ker f
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case neg.hx
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : f v = 0
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
x y : ↑ι
⊢ (Finsupp.single y 1) x = 1 x y

pp: case neg.hy
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : f v = 0
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
x y : ↑ι
⊢ (Finsupp.single i ((Finsupp.single y 1) j)) x = Matrix.single i j 1 x y

Tactic:
· by_cases h : x = y
      · rw [h]; simp
      · rw [Finsupp.single_eq_of_ne h, Matrix.one_apply_ne h]

Goal state after:
case neg.hy
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : f v = 0
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
x y : ↑ι
⊢ (Finsupp.single i ((Finsupp.single y 1) j)) x = Matrix.single i j 1 x y
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type u_3
B : Type u_4
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x✝² x✝¹ x✝ : M
⊢ ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) (x✝¹ + x✝), ⋯⟩ =
    ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝¹, ⋯⟩ +
      ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝, ⋯⟩

Tactic:
by simp only [map_add, mul_add]; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
hf : ibc.toDual fM = f
hv : ε vM = v
⊢ (algebraMap S R) (LinearMap.det (transvection fM vM)) = 1 + (ibc.toDual fM) (ε vM)

Tactic:
det_ofDomain

Goal state after:
case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
hf : ibc.toDual fM = f
hv : ε vM = v
⊢ (algebraMap S R) (1 + fM vM) = 1 + (ibc.toDual fM) (ε vM)