mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

Goal state before:
pp: α : 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 < ∞
⊢ μ[s.indicator f | m] =ᵐ[μ.restrict sᶜ] 0

Tactic:
refine condExp_ae_eq_restrict_zero hs_m.compl ?_

Goal state after:
α : 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 < ∞
⊢ s.indicator f =ᵐ[μ.restrict sᶜ] 0
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 t, μ[s.indicator f | m] x ∂μ = ∫ (x : α) in t, μ[s.indicator f | m₂] x ∂μ

Tactic:
[

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 t, μ[s.indicator f | m] x ∂μ = ∫ (x : α) in t, μ[s.indicator f | m₂] x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner

Goal state before:
pp: case pos.refine_2
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ≥0∞
hf_meas : AEMeasurable f μ
hf : ∫⁻ (x : 𝓧), f x ∂μ ≠ ∞
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
⊢ ∀ (s : Set 𝓧), MeasurableSet s → μ s < ∞ → IntegrableOn (fun x ↦ (μ⁻[f | m] x).toReal) s μ

Tactic:
refine fun s hs hsμ ↦ Integrable.integrableOn ?_
    rwa [integrable_toReal_iff (by fun_prop) (condLExp_ne_top hf), lintegral_condLExp]

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

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᵐ[P] Y
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[X | mΩ] ≤ᵐ[P] P⁻[Y | mΩ]

Tactic:
[

Goal state after:
case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᵐ[P] Y
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[X | mΩ] ≤ᵐ[P] P⁻[Y | mΩ]
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᵐ[P] Y
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ P⁻[X | mΩ] ≤ᵐ[P] P⁻[Y | mΩ]

Tactic:
[

Goal state after:
case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᵐ[P] Y
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ P⁻[X | mΩ] ≤ᵐ[P] P⁻[Y | mΩ]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

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

Tactic:
[

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

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᵐ[P] Y
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ P⁻[X | mΩ] ≤ᵐ[P] P⁻[Y | mΩ]

Tactic:
condLExp_of_not_sigmaFinite hm hσ,

Goal state after:
case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hXY : X ≤ᵐ[P] Y
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ 0 ≤ᵐ[P] 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᵐ[μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] ≤ᵐ[μ] μ[g | m]

Tactic:
[

Goal state after:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᵐ[μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] ≤ᵐ[μ] μ[g | m]
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[X | mΩ] + P⁻[Y | mΩ] ≤ᵐ[P] P⁻[X + Y | mΩ]

Tactic:
[

Goal state after:
case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[X | mΩ] + P⁻[Y | mΩ] ≤ᵐ[P] P⁻[X + Y | mΩ]
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ P⁻[X | mΩ] + P⁻[Y | mΩ] ≤ᵐ[P] P⁻[X + Y | mΩ]

Tactic:
[

Goal state after:
case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ P⁻[X | mΩ] + P⁻[Y | mΩ] ≤ᵐ[P] P⁻[X + Y | mΩ]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ
hf : Integrable f μ
h'f : 0 ≤ᵐ[μ] f
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
A : μ[fun x ↦ (ENNReal.ofReal (f x)).toReal | m] =ᵐ[μ] μ[f | m]
B : 0 ≤ᵐ[μ] μ[f | m]
g : 𝓧 → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (f x)
this : ∫⁻ (x : 𝓧), g x ∂μ = ∫⁻ (x : 𝓧), ‖f x‖ₑ ∂μ
⊢ ∫⁻ (x : 𝓧), g x ∂μ ≠ ∞

Tactic:
this

Goal state after:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
f : 𝓧 → ℝ
hf : Integrable f μ
h'f : 0 ≤ᵐ[μ] f
hm : m ≤ m𝓧
hμ : SigmaFinite (μ.trim hm)
A : μ[fun x ↦ (ENNReal.ofReal (f x)).toReal | m] =ᵐ[μ] μ[f | m]
B : 0 ≤ᵐ[μ] μ[f | m]
g : 𝓧 → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (f x)
this : ∫⁻ (x : 𝓧), g x ∂μ = ∫⁻ (x : 𝓧), ‖f x‖ₑ ∂μ
⊢ ∫⁻ (x : 𝓧), ‖f x‖ₑ ∂μ ≠ ∞
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[X + Y | mΩ] =ᵐ[P] P⁻[X | mΩ] + P⁻[Y | mΩ]

Tactic:
[

Goal state after:
case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[X + Y | mΩ] =ᵐ[P] P⁻[X | mΩ] + P⁻[Y | mΩ]
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ P⁻[X + Y | mΩ] =ᵐ[P] P⁻[X | mΩ] + P⁻[Y | mΩ]

Tactic:
[

Goal state after:
case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hX : AEMeasurable X P
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ P⁻[X + Y | mΩ] =ᵐ[P] P⁻[X | mΩ] + P⁻[Y | mΩ]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst✝ : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
⊢ (fun x ↦ ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal) =ᵐ[ν.trim hm] ν[fun x ↦ (μ.rnDeriv ν x).toReal | m]

Tactic:
[

Goal state after:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst✝ : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
⊢ (fun x ↦ ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal) =ᵐ[ν.trim hm] ν[fun x ↦ (μ.rnDeriv ν x).toReal | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst✝ : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
this : SigmaFinite (Measure.map id ν)
h :
  (fun a ↦ ((Measure.map id μ).rnDeriv (Measure.map id ν) (id a)).toReal) =ᵐ[ν.trim ⋯]
    ν[fun a ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap id m]
⊢ (fun x ↦ ((Measure.map id μ).rnDeriv (Measure.map id ν) x).toReal) =ᵐ[Measure.map id ν]
    ν[fun x ↦ (μ.rnDeriv ν x).toReal | m]

Tactic:
[

Goal state after:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst✝ : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
this : SigmaFinite (Measure.map id ν)
h :
  (fun a ↦ ((Measure.map id μ).rnDeriv (Measure.map id ν) (id a)).toReal) =ᵐ[ν.trim ⋯]
    ν[fun a ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap id m]
⊢ (fun x ↦ ((Measure.map id μ).rnDeriv (Measure.map id ν) x).toReal) =ᵐ[Measure.map id ν]
    ν[fun x ↦ (μ.rnDeriv ν x).toReal | m]
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X Y : Ω → ℝ≥0∞
hY : AEMeasurable Y P
⊢ P⁻[X + Y | mΩ] =ᵐ[P] P⁻[X | mΩ] + P⁻[Y | mΩ]

Tactic:
by
  rw [add_comm, add_comm P⁻[X|mΩ]]
  exact condLExp_add_left X hY

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

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
⊢ c • P⁻[X | mΩ] ≤ᵐ[P] P⁻[c • X | mΩ]

Tactic:
[

Goal state after:
case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : ¬mΩ ≤ mΩ₀
⊢ c • P⁻[X | mΩ] ≤ᵐ[P] P⁻[c • X | mΩ]
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ c • P⁻[X | mΩ] ≤ᵐ[P] P⁻[c • X | mΩ]

Tactic:
[

Goal state after:
case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ c • P⁻[X | mΩ] ≤ᵐ[P] P⁻[c • X | mΩ]
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝ : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[∑' (i : ι), X i | mΩ] =ᵐ[P] ∑' (i : ι), P⁻[X i | mΩ]

Tactic:
[

Goal state after:
case neg
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝ : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : ¬mΩ ≤ mΩ₀
⊢ P⁻[∑' (i : ι), X i | mΩ] =ᵐ[P] ∑' (i : ι), P⁻[X i | mΩ]
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝ : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ P⁻[∑' (i : ι), X i | mΩ] =ᵐ[P] ∑' (i : ι), P⁻[X i | mΩ]

Tactic:
[

Goal state after:
case neg
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝ : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : mΩ ≤ mΩ₀
hσ : ¬SigmaFinite (P.trim hm)
⊢ P⁻[∑' (i : ι), X i | mΩ] =ᵐ[P] ∑' (i : ι), P⁻[X i | mΩ]
Module: Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hm : m ≤ m𝓧
⊢ klDiv (μ.trim hm) (ν.trim hm) ≤ klDiv μ ν

Tactic:
[

Goal state after:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hm : m ≤ m𝓧
⊢ klDiv (μ.trim hm) (ν.trim hm) ≤ klDiv μ ν
Module: Mathlib.Lean.Thunk

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq α
a b : Thunk α
this : a = b ↔ a.get = b.get
⊢ Decidable (a = b)

Tactic:
this

Goal state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
a b : Thunk α
this : a = b ↔ a.get = b.get
⊢ Decidable (a.get = b.get)
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: case intro
ι : 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
ι' : Type u_1
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val✝ : Fintype ι'
w₁ w₂ : ι' → k
hw₁ : ∑ i, w₁ i = 1
hw₂ : ∑ i, w₂ i = 1
⊢ (Finset.affineCombination k Finset.univ p) w₁ = (Finset.affineCombination k Finset.univ p) w₂ → w₁ = w₂

Tactic:
hweq

Goal state after:
case intro
ι : 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
ι' : Type u_1
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val✝ : Fintype ι'
w₁ w₂ : ι' → k
hw₁ : ∑ i, w₁ i = 1
hw₂ : ∑ i, w₂ i = 1
hweq : (Finset.affineCombination k Finset.univ p) w₁ = (Finset.affineCombination k Finset.univ p) w₂
⊢ w₁ = w₂
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
ι' : Type u_1
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val✝ : Fintype ι'
w₁ w₂ : ι' → k
hw₁ : ∑ i, w₁ i = 1
hw₂ : ∑ i, w₂ i = 1
hweq : (Finset.affineCombination k Finset.univ p) w₁ = (Finset.affineCombination k Finset.univ p) w₂
j : ι
⊢ (b.coord j) ((Finset.affineCombination k Finset.univ p) w₁) =
    (b.coord j) ((Finset.affineCombination k Finset.univ p) w₂)

Tactic:
hweq

Goal state after:
ι : 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
ι' : Type u_1
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : b.toMatrix p * A = 1
val✝ : Fintype ι'
w₁ w₂ : ι' → k
hw₁ : ∑ i, w₁ i = 1
hw₂ : ∑ i, w₂ i = 1
hweq : (Finset.affineCombination k Finset.univ p) w₁ = (Finset.affineCombination k Finset.univ p) w₂
j : ι
⊢ (b.coord j) ((Finset.affineCombination k Finset.univ p) w₂) =
    (b.coord j) ((Finset.affineCombination k Finset.univ p) w₂)
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
ι' : Type u_1
inst✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
i : ι
⊢ ∑ j, A i j * ∑ l, b.toMatrix p j l = ∑ j, ∑ l, A i j * b.toMatrix p j l

Tactic:
[

Goal state after:
ι : 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
ι' : Type u_1
inst✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
i : ι
⊢ ∑ j, A i j * ∑ l, b.toMatrix p j l = ∑ j, ∑ l, A i j * b.toMatrix p j l
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
ι' : Type u_1
inst✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
i : ι
hAi : ∑ j, A i j = 1
j : ι
⊢ (if j = i then 1 else 0) = (A * b.toMatrix p) i j

Tactic:
[

Goal state after:
ι : 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
ι' : Type u_1
inst✝³ : Finite ι
inst✝² : Fintype ι'
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val✝ : Fintype ι
i : ι
hAi : ∑ j, A i j = 1
j : ι
⊢ (if j = i then 1 else 0) = (A * b.toMatrix p) i j
Module: Mathlib.LinearAlgebra.BilinearForm.Isometry

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
B₄ : LinearMap.BilinForm R M₄
g : B₂ →bᵢ B₃
f : B₁ →bᵢ B₂
x y : M₁
⊢ (B₃ (g (f x))) (g (f y)) = (B₁ x) y

Tactic:
by rw [← f.map_app, ← g.map_app]

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

Goal state before:
pp: case inr.mp.refine_2
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 x : P
hmem : x ∈ s
heq : (1 - r) • (c -ᵥ ↑h.some) +ᵥ x = p
⊢ (x -ᵥ ↑h.some + r • (↑h.some -ᵥ c)) +ᵥ c = (c -ᵥ ↑h.some + r • (↑h.some -ᵥ c)) +ᵥ x

Tactic:
[

Goal state after:
case inr.mp.refine_2
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 x : P
hmem : x ∈ s
heq : (1 - r) • (c -ᵥ ↑h.some) +ᵥ x = p
⊢ (x -ᵥ ↑h.some + r • (↑h.some -ᵥ c)) +ᵥ c = (c -ᵥ ↑h.some + r • (↑h.some -ᵥ c)) +ᵥ x
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
i' j' : ιa
hv : v (σ (Sum.inl i')) = v (σ (Sum.inl j'))
hij : σ (Sum.inl i') ≠ σ (Sum.inl j')
hσ✝ : swap (σ (Sum.inl i')) (σ (Sum.inl j')) • Quotient.mk'' σ = Quotient.mk'' σ
hσ : (Perm.sumCongrHom ιa ιb) (sl, sr) = ((fun x ↦ swap (σ (Sum.inl i')) (σ (Sum.inl j')) • x) σ)⁻¹ * σ
⊢ (Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)) v = 0

Tactic:
suffices (a fun i ↦ v (σ (Sum.inl i))) = 0 by simp_all
    exact AlternatingMap.map_eq_zero_of_eq _ _ hv fun hij' => hij (hij' ▸ rfl)

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
⊢ (↑(alternatization a)).domCoprod ↑(alternatization b) =
    ∑ σa, ∑ σb, Perm.sign σa • Perm.sign σb • (domDomCongr σa a).domCoprod (domDomCongr σb b)

Tactic:
[

Goal state after:
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
⊢ (↑(alternatization a)).domCoprod ↑(alternatization b) =
    ∑ σa, ∑ σb, Perm.sign σa • Perm.sign σb • (domDomCongr σa a).domCoprod (domDomCongr σb b)
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
⊢ domCoprod' ((∑ σ, Perm.sign σ • domDomCongr σ a) ⊗ₜ[R'] ∑ σ, Perm.sign σ • domDomCongr σ b) =
    ∑ σa, ∑ σb, Perm.sign σa • Perm.sign σb • domCoprod' (domDomCongr σa a ⊗ₜ[R'] domDomCongr σb b)

Tactic:
[

Goal state after:
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
⊢ domCoprod' ((∑ σ, Perm.sign σ • domDomCongr σ a) ⊗ₜ[R'] ∑ σ, Perm.sign σ • domDomCongr σ b) =
    ∑ σa, ∑ σb, Perm.sign σa • Perm.sign σb • domCoprod' (domDomCongr σa a ⊗ₜ[R'] domDomCongr σb b)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case pos
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
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hp : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
⊢ (∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1) ∧ w i = 1 - x ↔
    ∃ x_1 ∈ (s.faceOpposite i).closedInterior, (homothety (s.points i) x) x_1 = (affineCombination k univ s.points) w

Tactic:
[

Goal state after:
case pos
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
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hp : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
⊢ (∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1) ∧ w i = 1 - x ↔
    ∃ x_1 ∈ (s.faceOpposite i).closedInterior, (homothety (s.points i) x) x_1 = (affineCombination k univ s.points) w