mathlib-initiative/mathlib-tactics huggingface dataset:
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 α
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
⊢ ↑↑↑(f + g) =ᵐ[μ] ↑↑(lpMeasSubgroupToLpTrim F p μ hm f) + ↑↑(lpMeasSubgroupToLpTrim F p μ hm g)

Tactic:
lpMeasSubgroupToLpTrim_ae_eq,

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 μ)
⊢ ↑↑↑(f + g) =ᵐ[μ] ↑↑↑f + ↑↑(lpMeasSubgroupToLpTrim F p μ hm g)
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 α
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
⊢ ↑↑↑(f + g) =ᵐ[μ] ↑↑↑f + ↑↑(lpMeasSubgroupToLpTrim F p μ hm g)

Tactic:
lpMeasSubgroupToLpTrim_ae_eq,

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 μ)
⊢ ↑↑↑(f + g) =ᵐ[μ] ↑↑↑f + ↑↑↑g
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)) =ᵐ[μ] -↑↑(lpMeasSubgroupToLpTrim F p μ hm f)

Tactic:
lpMeasSubgroupToLpTrim_ae_eq,

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 μ)
⊢ ↑↑↑(-f) =ᵐ[μ] -↑↑(lpMeasSubgroupToLpTrim F p μ hm f)
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 μ)
⊢ ↑↑↑(-f) =ᵐ[μ] -↑↑(lpMeasSubgroupToLpTrim F p μ hm f)

Tactic:
lpMeasSubgroupToLpTrim_ae_eq,

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 μ)
⊢ ↑↑↑(-f) =ᵐ[μ] -↑↑↑f
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
this : Fact (m ≤ m0)
⊢ ↑((lpMeas E 𝕜 m 2 μ).orthogonalProjectionOnto (indicatorConstLp 2 ⋯ hμs c)) = indicatorConstLp 2 ⋯ hμs c

Tactic:
have h_mem : indicatorConstLp 2 (hm s hs) hμs c ∈ lpMeas E 𝕜 m 2 μ :=
    mem_lpMeas_indicatorConstLp hm hs hμs

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
this : Fact (m ≤ m0)
h_mem : indicatorConstLp 2 ⋯ hμs c ∈ lpMeas E 𝕜 m 2 μ
⊢ ↑((lpMeas E 𝕜 m 2 μ).orthogonalProjectionOnto (indicatorConstLp 2 ⋯ hμs c)) = indicatorConstLp 2 ⋯ hμs c
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'p : p < ∞
s : Set X
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ ∀ᵐ (x : X) ∂μ, x ∈ s → ∑' (n : ι), ‖f n x‖ₑ < ∞

Tactic:
rw [← ae_restrict_iff' hs]

Goal state after:
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'p : p < ∞
s : Set X
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ∑' (n : ι), ‖f n x‖ₑ < ∞
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
⊢ condExpInd G hm μ (s ∪ t) = condExpInd G hm μ s + condExpInd G hm μ t

Tactic:
ext1 x

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
⊢ (condExpInd G hm μ (s ∪ t)) x = (condExpInd G hm μ s + condExpInd G hm μ t) x
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
ht : MeasurableSet t
hμt : μ t ≠ ∞
h_eq : ∫⁻ (x : α) in t, ↑‖↑↑(indicatorConstLp 2 hs hμs 1) x‖₊ ∂μ = ∫⁻ (x : α) in t, s.indicator (fun x ↦ 1) x ∂μ
⊢ ∫⁻ (x : α) in t, s.indicator (fun x ↦ 1) x ∂μ = μ (s ∩ t)

Tactic:
lintegral_indicator hs,

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ∞
ht : MeasurableSet t
hμt : μ t ≠ ∞
h_eq : ∫⁻ (x : α) in t, ↑‖↑↑(indicatorConstLp 2 hs hμs 1) x‖₊ ∂μ = ∫⁻ (x : α) in t, s.indicator (fun x ↦ 1) x ∂μ
⊢ ∫⁻ (a : α) in s, 1 ∂μ.restrict t = μ (s ∩ t)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
⊢ μ[f | ⊥] = fun x ↦ (μ.real Set.univ)⁻¹ • ∫ (x : α), f x ∂μ

Tactic:
by_cases hμ_finite : IsFiniteMeasure μ

Goal state after:
case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
⊢ μ[f | ⊥] = fun x ↦ (μ.real Set.univ)⁻¹ • ∫ (x : α), f x ∂μ

case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : ¬IsFiniteMeasure μ
⊢ μ[f | ⊥] = fun x ↦ (μ.real Set.univ)⁻¹ • ∫ (x : α), f x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : G
⊢ Integrable (↑↑(condExpIndSMul hm hs hμs x)) μ

Tactic:
by
  refine integrable_of_forall_fin_meas_le' hm (μ s * ‖x‖₊)
    (ENNReal.mul_lt_top hμs.lt_top ENNReal.coe_lt_top) ?_ ?_
  · exact Lp.aestronglyMeasurable _
  · refine fun t ht hμt => (setLIntegral_nnnorm_condExpIndSMul_le hm hs hμs x ht hμt).trans ?_
    gcongr
    apply Set.inter_subset_left

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

Goal state before:
pp: case pos.refine_3
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
hf_int : Integrable f μ
T : E →L[ℝ] F
hm : m ≤ m₀
hμ : SigmaFinite (μ.trim hm)
s : Set α
ms : MeasurableSet s
hs : μ s < ∞
⊢ ∫ (x : α) in s, (⇑T ∘ μ[f | m]) x ∂μ = ∫ (x : α) in s, (⇑T ∘ f) x ∂μ

Tactic:
calc
          ∫ x in s, (T ∘ μ[f | m]) x ∂μ = T (∫ x in s, μ[f | m] x ∂μ) :=
            T.integral_comp_comm integrable_condExp.restrict
          _ = T (∫ x in s, f x ∂μ) := congrArg T (setIntegral_condExp hm hf_int ms)
          _ = ∫ x in s, (T ∘ f) x ∂μ := (T.integral_comp_comm hf_int.restrict).symm

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

Goal state before:
pp: case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
hX : ¬Measurable X
h : (P.withDensity X).trim hm ≪ P.trim hm
this : SFinite ((P.withDensity X).trim hm)
⊢ ∫⁻ (a : Ω), s.indicator (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P

Tactic:
lintegral_indicator hs,

Goal state after:
case neg
Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
hm : mΩ ≤ mΩ₀
P : Measure Ω
hσ : SigmaFinite (P.trim hm)
X : Ω → ℝ≥0∞
s : Set Ω
hs : MeasurableSet s
hX : ¬Measurable X
h : (P.withDensity X).trim hm ≪ P.trim hm
this : SFinite ((P.withDensity X).trim hm)
⊢ ∫⁻ (a : Ω) in s, (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P.trim hm = ∫⁻ (ω : Ω) in s, X ω ∂P
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: Ω : Type u_1
mΩ₀ mΩ : MeasurableSpace Ω
P : Measure Ω
f : Ω → ℝ≥0∞
hf : ∫⁻ (x : Ω), f x ∂P ≠ ∞
⊢ ∀ᵐ (x : Ω) ∂P, P⁻[f | mΩ] x < ∞

Tactic:
by
  by_cases hm : mΩ ≤ mΩ₀
  swap; · simp [condLExp_of_not_le hm]
  by_cases hσ : SigmaFinite (P.trim hm)
  · exact ae_lt_top' (by fun_prop) (by rwa [lintegral_condLExp])
  · simp [condLExp_of_not_sigmaFinite hm hσ]

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
inst✝ : SigmaFinite (Measure.map g ν)
⊢ (fun a ↦ (Measure.map g μ).rnDeriv (Measure.map g ν) (g a)) =ᵐ[ν.trim ⋯] ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨]

Tactic:
StronglyMeasurable.ae_eq_trim_iff

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
⊢ (fun a ↦ (Measure.map g μ).rnDeriv (Measure.map g ν) (g a)) =ᵐ[ν] ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g m𝓨]

case hf
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
⊢ StronglyMeasurable fun a ↦ (Measure.map g μ).rnDeriv (Measure.map g ν) (g a)

case hg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
⊢ StronglyMeasurable ν⁻[μ.rnDeriv ν | MeasurableSpace.comap g 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Ω₀
⊢ P⁻[X + Y | mΩ] =ᵐ[P] P⁻[X | mΩ] + P⁻[Y | mΩ]

pp: case pos
Ω : 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:
· simp_rw [condLExp_of_not_le hm]; simp

Goal state after:
case pos
Ω : 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.ConditionalExpectation.RadonNikodym

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
⊢ (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal) =ᵐ[ν.trim ⋯]
    ν[fun a ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]

Tactic:
StronglyMeasurable.ae_eq_trim_iff

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
⊢ (fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal) =ᵐ[ν]
    ν[fun a ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]

case hf
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
⊢ StronglyMeasurable fun a ↦ ((Measure.map g μ).rnDeriv (Measure.map g ν) (g a)).toReal

case hg
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst✝ : SigmaFinite (Measure.map g ν)
⊢ StronglyMeasurable ν[fun a ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

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

Tactic:
refine ⟨t • (x -ᵥ h.some.val) +ᵥ h.some.val, ?_, ?_⟩

Goal state after:
case inr.mp.refine_1
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
⊢ t • (x -ᵥ ↑h.some) +ᵥ ↑h.some ∈ s

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
⊢ r • ((t • (x -ᵥ ↑h.some) +ᵥ ↑h.some) -ᵥ c) +ᵥ c = (1 - r) • (c -ᵥ ↑h.some) +ᵥ 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ᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
⊢ (∑ σ, domCoprod.summand a b σ) v = 0

Tactic:
by
      rw [_root_.sum_apply]
      exact
        Finset.sum_involution (fun σ _ => Equiv.swap i j • σ)
          (fun σ _ => domCoprod.summand_add_swap_smul_eq_zero a b σ hv hij)
          (fun σ _ => mt <| domCoprod.summand_eq_zero_of_smul_invariant a b σ hv hij)
          (fun σ _ => Finset.mem_univ _) fun σ _ =>
          Equiv.swap_smul_involutive i j σ

Goal state after:
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✝⁵ : PartialOrder k
inst✝⁴ : IsOrderedAddMonoid k
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Module k V
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x < 0 ∨ 1 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hleft : (affineCombination k univ s.points) w ∈ s.closedInterior
hright : (affineCombination k univ s.points) w ∈ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) x)
⊢ False

Tactic:
rw [SetLike.mem_coe, s.independent.affineCombination_mem_shift_iff i hw] at hright

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring k
inst✝⁵ : PartialOrder k
inst✝⁴ : IsOrderedAddMonoid k
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Module k V
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x < 0 ∨ 1 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hleft : (affineCombination k univ s.points) w ∈ s.closedInterior
hright : w i = 1 - x
⊢ False
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_6
inst✝¹⁰ : CommRing R
S : Type u_7
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_8
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
P : Type u_9
inst✝⁵ : AddCommGroup 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
⊢ LinearMap.det (j.endHom f) = (algebraMap R S) (LinearMap.det f)

Tactic:
rcases subsingleton_or_nontrivial R with hR | hR

Goal state after:
case inl
R : Type u_6
inst✝¹⁰ : CommRing R
S : Type u_7
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_8
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
P : Type u_9
inst✝⁵ : AddCommGroup 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
hR : Subsingleton R
⊢ LinearMap.det (j.endHom f) = (algebraMap R S) (LinearMap.det f)

case inr
R : Type u_6
inst✝¹⁰ : CommRing R
S : Type u_7
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_8
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
P : Type u_9
inst✝⁵ : AddCommGroup 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
hR : Nontrivial R
⊢ LinearMap.det (j.endHom f) = (algebraMap R S) (LinearMap.det f)
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, e y = y
x✝ : v ∈ map (↑e) W
w : V
hv' : e w = v
hv : w ∈ W
⊢ e w ∈ W

Tactic:
he w hv

Goal state after:
case refine_1
R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
v : V
he : ∀ y ∈ W, e y = y
x✝ : v ∈ map (↑e) W
w : V
hv' : e w = v
hv : w ∈ W
⊢ w ∈ W
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₂
⊢ alternatization ((↑a).domCoprod ↑b) = ((Fintype.card ιa).factorial * (Fintype.card ιb).factorial) • a.domCoprod b

Tactic:
rw [MultilinearMap.domCoprod_alternization, coe_alternatization, coe_alternatization, mul_smul,
    ← AlternatingMap.domCoprod'_apply, ← AlternatingMap.domCoprod'_apply,
    ← TensorProduct.smul_tmul', TensorProduct.tmul_smul,
    LinearMap.map_smul_of_tower AlternatingMap.domCoprod',
    LinearMap.map_smul_of_tower AlternatingMap.domCoprod']

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

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

Tactic:
by_cases hv : v = 0

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

case neg
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
⊢ LinearMap.det (transvection f v) = 1 + f v
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case h₀
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
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this✝ : Fintype ↑ι
this : (toMatrix b b) (transvection f v) = Matrix.diagonal (Function.update 1 i (1 + f v))
j : ↑ι
a✝ : j ∈ Finset.univ
⊢ j ≠ i → Function.update 1 i (1 + f v) j = 1

Tactic:
hj

Goal state after:
case h₀
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
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this✝ : Fintype ↑ι
this : (toMatrix b b) (transvection f v) = Matrix.diagonal (Function.update 1 i (1 + f v))
j : ↑ι
a✝ : j ∈ Finset.univ
hj : j ≠ i
⊢ Function.update 1 i (1 + f v) j = 1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

Goal state before:
pp: case fst
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
a : A
g : M →ₗ[R] A
hg : g ∈ S f
⊢ (((fFold f) m) (((fFold f) m) (a, ⟨g, hg⟩))).1 = (Q m • (a, ⟨g, hg⟩)).1

Tactic:
change f.bilin m m * a = Q m • a

Goal state after:
case fst
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
a : A
g : M →ₗ[R] A
hg : g ∈ S f
⊢ (f.bilin m) m * a = Q m • a
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

Goal state after:
case inl
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 : Subsingleton R
⊢ LinearMap.det (transvection f v) = 1 + f v

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
⊢ LinearMap.det (transvection f v) = 1 + f v
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
⊢ DirectSum ι ℬ ⊗[R] (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) →ₗ[R]
    (⨁ (i : ι), 𝒜 i) ⊗[R] ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)

Tactic:
refine (assoc R _ _ _).toLinearMap ∘ₗ .rTensor _ ?_ ∘ₗ (assoc R _ _ _).symm.toLinearMap

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
⊢ DirectSum ι ℬ ⊗[R] DirectSum ι 𝒜 →ₗ[R] (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i