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

Goal state before:
pp: case refine_1
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
⊢ StronglyMeasurable (↑↑(lpMeasSubgroupToLpTrim F p μ hm f) + ↑↑(lpMeasSubgroupToLpTrim F p μ hm g))

pp: case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
⊢ ↑↑(lpMeasSubgroupToLpTrim F p μ hm (f + g)) =ᵐ[μ]
    ↑↑(lpMeasSubgroupToLpTrim F p μ hm f) + ↑↑(lpMeasSubgroupToLpTrim F p μ hm g)

Tactic:
· exact (Lp.stronglyMeasurable _).add (Lp.stronglyMeasurable _)

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

Goal state before:
pp: case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf : ∀ (t : Set α), MeasurableSet t → μ t < ∞ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : μ s ≠ ∞
h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0}
⊢ ∫ (x : α) in {x | 0 ≤ g x} ∩ s, g x ∂μ ≤ ∫ (x : α) in {x | 0 ≤ f x} ∩ s, f x ∂μ

Tactic:
hgf _ (@MeasurableSet.inter α m _ _ h_meas_nonneg_g hs)
        ((measure_mono Set.inter_subset_right).trans_lt (lt_top_iff_ne_top.mpr hμs)),

Goal state after:
case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf : ∀ (t : Set α), MeasurableSet t → μ t < ∞ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : μ s ≠ ∞
h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0}
⊢ ∫ (x : α) in {x | 0 ≤ g x} ∩ s, f x ∂μ ≤ ∫ (x : α) in {x | 0 ≤ f x} ∩ s, f x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf : ∀ (t : Set α), MeasurableSet t → μ t < ∞ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ
hs : MeasurableSet s
hμs : μ s ≠ ∞
⊢ ∫⁻ (x : α) in s, ‖g x‖ₑ ∂μ ≤ ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ

Tactic:
by
  rw [← ofReal_integral_norm_eq_lintegral_enorm hfi, ←
    ofReal_integral_norm_eq_lintegral_enorm hgi, ENNReal.ofReal_le_ofReal_iff]
  · exact integral_norm_le_of_forall_fin_meas_integral_eq hm hf hfi hg hgi hgf hs hμs
  · positivity

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

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
hst : Disjoint s t
x : G
⊢ ↑↑(condExpIndL1Fin hm ⋯ ⋯ x) =ᵐ[μ] ↑↑(condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm ht hμt x)

Tactic:
grw [Lp.coeFn_add, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndL1Fin_ae_eq_condExpIndSMul]

Goal state after:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
hst : Disjoint s t
x : G
⊢ ↑↑(condExpIndSMul hm ⋯ ⋯ x) =ᵐ[μ] ↑↑(condExpIndSMul hm hs hμs x) + ↑↑(condExpIndSMul hm ht hμt x)
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 μ)
hf : ↑↑f =ᵐ[μ.restrict s] 0
⊢ (fun x ↦ ↑‖↑↑f x‖₊) =ᵐ[μ.restrict s] 0

Tactic:
refine hf.mono fun x hx => ?_
    dsimp only
    rw [hx]
    simp

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

Goal state before:
pp: α : Type u_1
F' : Type u_3
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : CompleteSpace F'
c : 𝕜
f : ↥(Lp F' 1 μ)
⊢ (condExpL1CLM F' hm μ) (c • f) = c • (condExpL1CLM F' hm μ) f

Tactic:
refine L1.setToL1_smul (dominatedFinMeasAdditive_condExpInd F' hm μ) ?_ c f

Goal state after:
α : Type u_1
F' : Type u_3
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : CompleteSpace F'
c : 𝕜
f : ↥(Lp F' 1 μ)
⊢ ∀ (c : 𝕜) (s : Set α) (x : F'), (condExpInd F' hm μ s) (c • x) = c • (condExpInd F' hm μ s) x
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
F' : Type u_3
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
inst✝ : CompleteSpace F'
c : 𝕜
f : ↥(Lp F' 1 μ)
⊢ (condExpL1CLM F' hm μ) (c • f) = c • (condExpL1CLM F' hm μ) f

Tactic:
by
  refine L1.setToL1_smul (dominatedFinMeasAdditive_condExpInd F' hm μ) ?_ c f
  exact fun c s x => condExpInd_smul' c x

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

Goal state before:
pp: case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : F'
t : Set α
ht : MeasurableSet t
hμt : μ t < ∞
⊢ ∫ (x_1 : α) in s, ↑↑((condExpInd F' hm μ t) x) x_1 ∂μ = ∫ (x_1 : α) in s, ↑↑(indicatorConstLp 1 ht ⋯ x) x_1 ∂μ

Tactic:
setIntegral_indicatorConstLp (hm _ hs)

Goal state after:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : F'
t : Set α
ht : MeasurableSet t
hμt : μ t < ∞
⊢ ∫ (x_1 : α) in s, ↑↑((condExpInd F' hm μ t) x) x_1 ∂μ = μ.real (t ∩ s) • x
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
⊢ s = s ∩ Set.univ

Tactic:
Set.inter_univ

Goal state after:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝¹ : SigmaFinite (μ.trim hm)
s : Set α
inst✝ : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : ℕ → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
⊢ s = s
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator

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

Tactic:
exact stronglyMeasurable_condExp.aestronglyMeasurable

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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst✝ : SigmaFinite (μ.trim hm₂)
hμm₁ : SigmaFinite (μ.trim ⋯)
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
a✝ : μ s < ∞
⊢ ∫ (x : α) in s, μ[f | m₂] x ∂μ = ∫ (x : α) in s, μ[f | m₁] x ∂μ

Tactic:
setIntegral_condExp (hm₁₂.trans hm₂) hf hs,

Goal state after:
case pos
α : Type u_1
E : Type u_3
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst✝ : SigmaFinite (μ.trim hm₂)
hμm₁ : SigmaFinite (μ.trim ⋯)
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
a✝ : μ s < ∞
⊢ ∫ (x : α) in s, μ[f | m₂] x ∂μ = ∫ (x : α) in s, f x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case neg
α : 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'
hF' : ¬CompleteSpace ↥(Lp F' 1 μ)
⊢ AEStronglyMeasurable (↑↑(condExpL1 hm μ f)) μ

Tactic:
simp only [condExpL1, setToFun, hF', ↓reduceDIte, ZeroMemClass.coe_zero]
    apply stronglyMeasurable_zero.aestronglyMeasurable.congr
    exact (coeFn_zero _ 1 _).symm

Goal state after:
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)
⊢ MeasurableSet (s ∩ Set.univ)

Tactic:
Set.inter_univ

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

Tactic:
rw [Set.inter_comm, ← Measure.restrict_restrict (hm₂ _ ht)]
      calc
        ∫ x : α in t, (μ[s.indicator f | m]) x ∂μ.restrict sᶜ =
            ∫ x : α in t, 0 ∂μ.restrict sᶜ := by
          refine setIntegral_congr_ae (hm₂ _ ht) ?_
          filter_upwards [this] with x hx _ using hx
        _ = 0 := integral_zero _ _

Goal state after:
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 (ν.trim ⋯)
this : SigmaFinite ν
t : Set 𝓨
ht : MeasurableSet t
a✝ : ν (g ⁻¹' t) < ∞
⊢ ∫ (x : 𝓧) in g ⁻¹' t, ((Measure.map g μ).rnDeriv (Measure.map g ν) (g x)).toReal ∂ν =
    ∫ (y : 𝓨) in t, ((Measure.map g μ).rnDeriv (Measure.map g ν) y).toReal ∂Measure.map g ν

Tactic:
setIntegral_map ht _ hg.aemeasurable

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 (ν.trim ⋯)
this : SigmaFinite ν
t : Set 𝓨
ht : MeasurableSet t
a✝ : ν (g ⁻¹' t) < ∞
⊢ ∫ (x : 𝓧) in g ⁻¹' t, ((Measure.map g μ).rnDeriv (Measure.map g ν) (g x)).toReal ∂ν =
    ∫ (x : 𝓧) in g ⁻¹' t, ((Measure.map g μ).rnDeriv (Measure.map g ν) (g x)).toReal ∂ν

𝓧 : 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 (ν.trim ⋯)
this : SigmaFinite ν
t : Set 𝓨
ht : MeasurableSet t
a✝ : ν (g ⁻¹' t) < ∞
⊢ AEStronglyMeasurable (fun y ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) y).toReal) (Measure.map g ν)
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ c * ∫⁻ (a : Ω) in s, P⁻[X | mΩ] a ∂P = ∫⁻ (ω : Ω) in s, c * X ω ∂P

pp: case pos.hf
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ Measurable P⁻[X | mΩ]

Tactic:
lintegral_const_mul'',

Goal state after:
case pos
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ c * ∫⁻ (a : Ω) in s, P⁻[X | mΩ] a ∂P = c * ∫⁻ (a : Ω) in s, X a ∂P

case pos.hf
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ AEMeasurable X (P.restrict s)

case pos.hf
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ≥0∞
hX : AEMeasurable X P
c : ℝ≥0∞
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
⊢ Measurable P⁻[X | mΩ]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym

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

Tactic:
by
  filter_upwards [toReal_rnDeriv_trim hm hμν, Measure.rnDeriv_ne_top (μ.trim hm) (ν.trim hm)]
    with x hx hx_ne_top
  rw [← hx, ENNReal.ofReal_toReal hx_ne_top]

Goal state after:
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✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ b.coords x ᵥ* (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x

Tactic:
← b.toMatrix_vecMul_coords b₂,

Goal state after:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (b.toMatrix ⇑b₂).det
⊢ b₂.coords x ᵥ* b.toMatrix ⇑b₂ ᵥ* (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
p : ↥s
c : P
r : k
h : Nonempty ↥s
q : P
⊢ (∃ y ∈ s, (1 - r) • (c -ᵥ ↑⋯.some) +ᵥ y = q) ↔ ∃ y ∈ s, (1 - r) • (c -ᵥ ↑p) +ᵥ y = q

Tactic:
constructor <;> intro ⟨x, hx, heq⟩

Goal state after:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
p : ↥s
c : P
r : k
h : Nonempty ↥s
q x : P
hx : x ∈ s
heq : (1 - r) • (c -ᵥ ↑⋯.some) +ᵥ x = q
⊢ ∃ y ∈ s, (1 - r) • (c -ᵥ ↑p) +ᵥ y = q

case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
p : ↥s
c : P
r : k
h : Nonempty ↥s
q x : P
hx : x ∈ s
heq : (1 - r) • (c -ᵥ ↑p) +ᵥ x = q
⊢ ∃ y ∈ s, (1 - r) • (c -ᵥ ↑⋯.some) +ᵥ y = q
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' (↑(alternatization a) ⊗ₜ[R'] ↑(alternatization b)) =
    ∑ σa, ∑ σb, Perm.sign σa • Perm.sign σb • domCoprod' (domDomCongr σa a ⊗ₜ[R'] domDomCongr σb b)

Tactic:
MultilinearMap.alternatization_coe

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.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e : V ≃ₗ[R] V
this : ∀ e ∈ dilatransvections R V, e.symm ∈ dilatransvections R V
⊢ e.symm ∈ dilatransvections R V → e ∈ dilatransvections R V

Tactic:
simpa using this e.symm

Goal state after:
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
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
x : A × ↥(S f)
⊢ ((fFold f) m) (((fFold f) m) x) = Q m • x

Tactic:
by
  obtain ⟨a, ⟨g, hg⟩⟩ := x
  ext : 2
  · change f.bilin m m * a = Q m • a
    rw [Algebra.smul_def, f.contract]
  · ext m₁
    change f.bilin _ _ * g m = Q m • g m₁
    refine Submodule.span_induction ?_ ?_ ?_ ?_ hg
    · rintro _ ⟨b, m₃, rfl⟩
      change f.bilin _ _ * (f.bilin _ _ * b) = Q m • (f.bilin _ _ * b)
      rw [← smul_mul_assoc, ← mul_assoc, f.contract_mid]
    · simp
    · rintro x y _hx _hy ihx ihy
      rw [LinearMap.add_apply, LinearMap.add_apply, mul_add, smul_add, ihx, ihy]
    · rintro x hx _c ihx
      rw [LinearMap.smul_apply, LinearMap.smul_apply, mul_smul_comm, ihx, smul_comm]

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

Goal state before:
pp: 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
⊢ LinearMap.det (transvection f v) = 1 + f v

Tactic:
rcases subsingleton_or_nontrivial R with hR | hR
  · subsingleton
  let b := finBasis R V
  set n := finrank R V
  let S := MvPolynomial (Fin n ⊕ Fin n) ℤ
  let γ : S →+* R :=
    (MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) (fun i ↦ b.coord i v)) :
      MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R)
  have : IsDomain S := inferInstance
  let _ : Algebra S R := RingHom.toAlgebra γ
  let _ : Module S V := compHom V γ
  have _ : IsScalarTower S R V := IsScalarTower.of_compHom S R V
  have ibc := IsBaseChange.of_fintype_basis S b
  set ε := Fintype.linearCombination S (fun i ↦ b i)
  set M := Fin n → S
  have hε (i) : ε (Pi.single i 1) = b i := by
    rw [Fintype.linearCombination_apply_single, one_smul]
  let fM : Dual S M :=
    Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
  let vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
  have hf : ibc.toDual fM = f := by
    apply b.ext
    intro i
    rw [← hε, toDual_comp_apply, Fintype.linearCombination_apply_single,
      one_smul, RingHom.algebraMap_toAlgebra, hε]
    apply MvPolynomial.aeval_X
  have hv : ε vM = v := by
    rw [of_fintype_basis_eq]
    ext i
    rw [RingHom.algebraMap_toAlgebra]
    simp only [vM, γ, Function.comp_apply]
    apply MvPolynomial.aeval_X
  rw [← hf, ← hv, ← IsBaseChange.transvection, det_endHom, det_ofDomain]
  rw [map_add, map_one, add_right_inj, toDual_comp_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: case ι
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ↑((toEven Q) (reverse (involute ((ι Q) m)))) = reverse ↑((toEven Q) ((ι Q) m))

Tactic:
simp only [involute_ι, Subalgebra.coe_neg, toEven_ι, reverse.map_mul, reverse_v, reverse_e0,
      reverse_ι, neg_e0_mul_v, map_neg]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case mem
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
i₁' : { n // ↑n = i₁ }
m₁' : CliffordAlgebra Q₁
hm₁ : m₁' ∈ (ι Q₁).range ^ ↑i₁'
⊢ (map f₁) m₁' * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) m₁')

Tactic:
| mem i₁' m₁' hm₁ =>

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: case homogeneous
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm✝ : ↥(⋀[R]^i✝ M)
m : ExteriorAlgebra R M
hm : m ∈ ⋀[R]^i✝ M
⊢ ↑(⋀[R]^i✝ M) ⊆ ↑(Submodule.span R (Set.range fun x ↦ (ιMulti R x.fst) x.snd))

Tactic:
rw [← ιMulti_span_fixedDegree]

Goal state after:
case homogeneous
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm✝ : ↥(⋀[R]^i✝ M)
m : ExteriorAlgebra R M
hm : m ∈ ⋀[R]^i✝ M
⊢ ↑(Submodule.span R (Set.range ⇑(ιMulti R i✝))) ⊆ ↑(Submodule.span R (Set.range fun x ↦ (ιMulti R x.fst) x.snd))