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

Goal state before:
pp: α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ∞ → IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
hg_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ∞ → IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, AEStronglyMeasurable.mk f hfm x ∂μ =
    ∫ (x : α), AEStronglyMeasurable.mk g hgm x ∂(μ.restrict s).trim hm

Tactic:
←
      integral_trim hm hgm.stronglyMeasurable_mk,

Goal state after:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ∞ → IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
hg_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ∞ → IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ∫ (x : α) in s, AEStronglyMeasurable.mk f hfm x ∂μ = ∫ (x : α) in s, AEStronglyMeasurable.mk g hgm x ∂μ
Module: Mathlib.InformationTheory.KullbackLeibler.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν = (klDiv μ ν).toReal

Tactic:
toReal_klDiv_eq_integral_klFun hμν

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case neg
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : MeasurableSet s
hμs : ¬μ s = ∞
⊢ ‖condExpIndL1 hm μ s x‖ ≤ μ.real s * ‖x‖

Tactic:
rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs x]

Goal state after:
case neg
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
x : G
hs : MeasurableSet s
hμs : ¬μ s = ∞
⊢ ‖condExpIndL1Fin hm hs hμs x‖ ≤ μ.real s * ‖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
x : α
hx : ↑↑f x = 0 x
⊢ ↑‖↑↑f x‖₊ = 0 x

Tactic:
rw [hx]

Goal state after:
α : 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
x : α
hx : ↑↑f x = 0 x
⊢ ↑‖0 x‖₊ = 0 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 : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : G
x : α
hx : ↑↑(indicatorConstLp 2 ⋯ hμs 1) x = s.indicator (fun x ↦ 1) x
⊢ ↑↑(indicatorConstLp 2 ⋯ hμs 1) x • c = s.indicator (fun x ↦ c) x

Tactic:
rw [hx]

Goal state after:
α : Type u_1
G : Type u_4
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 ≠ ∞
c : G
x : α
hx : ↑↑(indicatorConstLp 2 ⋯ hμs 1) x = s.indicator (fun x ↦ 1) x
⊢ s.indicator (fun x ↦ 1) x • c = s.indicator (fun x ↦ c) 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 ≠ ∞
x : α
hx : ↑↑(indicatorConstLp 2 hs hμs 1) x = s.indicator (fun x ↦ 1) x
⊢ ↑‖↑↑(indicatorConstLp 2 hs hμs 1) x‖₊ = s.indicator (fun x ↦ 1) x

Tactic:
rw [hx]

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 ≠ ∞
x : α
hx : ↑↑(indicatorConstLp 2 hs hμs 1) x = s.indicator (fun x ↦ 1) x
⊢ ↑‖s.indicator (fun x ↦ 1) x‖₊ = s.indicator (fun x ↦ 1) x
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
⊢ μ[f | m] =ᵐ[μ] ↑↑(condExpL1 hm μ f)

Tactic:
rw [condExp_of_sigmaFinite hm]

Goal state after:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
⊢ (if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯
    else 0) =ᵐ[μ]
    ↑↑(condExpL1 hm μ f)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ StronglyMeasurable μ[f | m]

Tactic:
rw [condExp_of_sigmaFinite hm]

Goal state after:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ StronglyMeasurable
    (if Integrable f μ then if StronglyMeasurable f then f else AEStronglyMeasurable.mk ↑↑(condExpL1 hm μ f) ⋯ else 0)
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'
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ ∫⁻ (a : α) in t, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x‖₊ ∂μ =
    (∫⁻ (a : α) in t, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a‖₊ ∂μ) * ↑‖x‖₊

Tactic:
by
      simp_rw [nnnorm_smul, ENNReal.coe_mul]
      rw [lintegral_mul_const]
      exact (Lp.stronglyMeasurable _).enorm (ε := ℝ)

Goal state after:
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
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : G
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ ∫⁻ (a : α) in t, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x‖₊ ∂μ =
    (∫⁻ (a : α) in t, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a‖₊ ∂μ) * ↑‖x‖₊

Tactic:
by
      simp_rw [nnnorm_smul, ENNReal.coe_mul]
      rw [lintegral_mul_const]
      exact (Lp.stronglyMeasurable _).enorm (ε := ℝ)

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

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

Tactic:
condExp_of_not_sigmaFinite hm hμm,

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

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
g : 𝓧 → 𝓨
hμν : μ ≪ ν
hg : Measurable g
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
a : 𝓧
ha1 : ((∂Measure.map g μ/∂Measure.map g ν) (g a)).toReal = ν[fun a ↦ ((∂μ/∂ν) a).toReal | MeasurableSpace.comap g m𝓨] a
ha2 :
  f (ν[fun x ↦ ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] a) ≤
    ν[fun x ↦ f ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] a
⊢ f ((∂Measure.map g μ/∂Measure.map g ν) (g a)).toReal =
    f (ν[fun x ↦ ((∂μ/∂ν) x).toReal | MeasurableSpace.comap g m𝓨] a)

Tactic:
rw [ha1]

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

Goal state before:
pp: 𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
f : ℝ → ℝ
hm : m ≤ m𝓧
hμν : μ ≪ ν
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
a : 𝓧
ha1 : ((∂μ.trim hm/∂ν.trim hm) a).toReal = ν[fun x ↦ ((∂μ/∂ν) x).toReal | m] a
ha2 : f (ν[fun x ↦ ((∂μ/∂ν) x).toReal | m] a) ≤ ν[fun x ↦ f ((∂μ/∂ν) x).toReal | m] a
⊢ f ((∂μ.trim hm/∂ν.trim hm) a).toReal = f (ν[fun x ↦ ((∂μ/∂ν) x).toReal | m] a)

Tactic:
rw [ha1]

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✝⁵ : 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 : ι
⊢ (b.coord j) (b i) = (b.coord j) ((Finset.affineCombination k Finset.univ p) (A i))

Tactic:
rw [b.coord_apply, Finset.univ.map_affineCombination _ _ hAi,
      Finset.univ.affineCombination_eq_linear_combination _ _ hAi]

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) = ∑ i_1, A i i_1 • (⇑(b.coord j) ∘ p) i_1
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

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

Tactic:
let b' : AffineBasis ι k P := ⟨p, h_tot, h_ind⟩

Goal state after:
case mpr
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι → P
h_tot : AffineIndependent k p
h_ind : affineSpan k (range p) = ⊤
b' : AffineBasis ι k P := { toFun := p, ind' := h_tot, tot' := h_ind }
⊢ IsUnit (b.toMatrix p)
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₂)
⊢ b.coords x ᵥ* (b.toMatrix ⇑b₂)⁻¹ = b₂.coords x

Tactic:
Matrix.isUnit_iff_isUnit_det

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

Tactic:
Matrix.isUnit_iff_isUnit_det

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.toMatrix ⇑b₂).det • b₂.coords x = (b.toMatrix ⇑b₂)ᵀ.cramer (b.coords x)
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 ∈ transvections R V, e.symm ∈ transvections R V
⊢ e.symm ∈ transvections R V ↔ e ∈ transvections R V

Tactic:
refine ⟨fun h ↦ ?_, this e⟩

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e : V ≃ₗ[R] V
this : ∀ e ∈ transvections R V, e.symm ∈ transvections R V
h : e.symm ∈ transvections R V
⊢ e ∈ transvections R V
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
⊢ ∀ e ∈ transvections R V, e.symm ∈ transvections R V

Tactic:
rintro _ ⟨f, v, hv, rfl⟩

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e : V ≃ₗ[R] V
f : Dual R V
v : V
hv : f v = 0
⊢ (transvection hv).symm ∈ transvections R V
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := ⋯
s t : R
hst : s = 0 → ¬t = 0
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
hx : x = b i + r • b j
h1 : s = -(t * (b.coord i) (f (b i)))
h2 : t = 0 ∨ r * (b.coord j) (f (b j)) = (b.coord i) (f (b i)) * r
⊢ ¬t = 0

Tactic:
contrapose hst

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
i j : ι
hij : i ≠ j
r : R
x : V := b.repr.symm ((Finsupp.single i 1).update j r)
s t : R
h : ∀ (i : ι), s * (b.repr x) i + t * (b.repr (f x)) i = 0
hx : x = b i + r • b j
h1 : s = -(t * (b.coord i) (f (b i)))
h2 : t = 0 ∨ r * (b.coord j) (f (b j)) = (b.coord i) (f (b i)) * r
hst : t = 0
⊢ ¬(s = 0 → ¬t = 0)
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case mpr
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
he : Module.rank K ↥(↑e - LinearMap.id).range ≤ 1
⊢ ∃ f v, ↑e = LinearMap.transvection f v

Tactic:
set u := (e : V →ₗ[K] V) - LinearMap.id with hu

Goal state after:
case mpr
V : Type u_2
inst✝² : AddCommGroup V
K : Type u_3
inst✝¹ : DivisionRing K
inst✝ : Module K V
e : V ≃ₗ[K] V
u : V →ₗ[K] V := ↑e - LinearMap.id
he : Module.rank K ↥u.range ≤ 1
hu : u = ↑e - LinearMap.id
⊢ ∃ f v, ↑e = LinearMap.transvection f v
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: 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
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
⊢ ((toMatrix b b) (transvection f v)).det = 1 + f v

Tactic:
suffices toMatrix b b (LinearMap.transvection f v) = Matrix.transvection i j 1 by
      rw [this, Matrix.det_transvection_of_ne i j hi 1, hfv, add_zero]

Goal state after:
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
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
⊢ (toMatrix b b) (transvection f v) = Matrix.transvection i j 1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { toFun := fun v ↦ { re := 0, imI := v.1, imJ := v.2, imK := 0 }, map_add' := ⋯, map_smul' := ⋯ } v *
      { toFun := fun v ↦ { re := 0, imI := v.1, imJ := v.2, imK := 0 }, map_add' := ⋯, map_smul' := ⋯ } v =
    (algebraMap R ℍ[R,c₁,c₂]) ((Q c₁ c₂) v)

Tactic:
by
      dsimp
      ext
      all_goals dsimp; ring

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

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
x : CliffordAlgebra Q'
⊢ (Q' m - (Q' m - Q m)) • x = Q m • x

Tactic:
sub_sub_cancel

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
x : CliffordAlgebra Q'
⊢ Q m • x = Q m • x
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✝² + x✝¹) * (CliffordAlgebra.ι Q) x✝, ⋯⟩ =
    ⟨(CliffordAlgebra.ι Q) x✝² * (CliffordAlgebra.ι Q) x✝, ⋯⟩ +
      ⟨(CliffordAlgebra.ι Q) x✝¹ * (CliffordAlgebra.ι Q) x✝, ⋯⟩

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

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₂ : M
⊢ (aux f) (((ι Q).bilin m₁) m₂) = (f.bilin m₁) m₂

Tactic:
CliffordAlgebra.even.lift.aux_apply

Goal state after:
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₂ : M
⊢ (((foldr Q (fFold f) ⋯) (1, 0)) ↑(((ι Q).bilin m₁) m₂)).1 = (f.bilin m₁) m₂
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  ((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
f_apply :
  ∀ (x y : M × R),
    (f x) y =
      ((ι Q) x.1 + (algebraMap R (CliffordAlgebra Q)) x.2) * ((ι Q) y.1 - (algebraMap R (CliffordAlgebra Q)) y.2)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute ((algebraMap R (CliffordAlgebra Q)) r) x
hm :
  ∀ (m : M × R),
    (ι Q) m.1 * (ι Q) m.1 - (algebraMap R (CliffordAlgebra Q)) m.2 * (algebraMap R (CliffordAlgebra Q)) m.2 =
      (algebraMap R (CliffordAlgebra Q)) ((Q' Q) m)
m₁ m₂ m₃ : M × R
⊢ ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
        (((ι Q) m₂.1 - (algebraMap R (CliffordAlgebra Q)) m₂.2) *
          ((ι Q) m₂.1 + (algebraMap R (CliffordAlgebra Q)) m₂.2)) *
      ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2) =
    ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
      (Q' Q) m₂ • ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2)

Tactic:
← (hc _ _).symm.mul_self_sub_mul_self_eq',

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  ((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
f_apply :
  ∀ (x y : M × R),
    (f x) y =
      ((ι Q) x.1 + (algebraMap R (CliffordAlgebra Q)) x.2) * ((ι Q) y.1 - (algebraMap R (CliffordAlgebra Q)) y.2)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute ((algebraMap R (CliffordAlgebra Q)) r) x
hm :
  ∀ (m : M × R),
    (ι Q) m.1 * (ι Q) m.1 - (algebraMap R (CliffordAlgebra Q)) m.2 * (algebraMap R (CliffordAlgebra Q)) m.2 =
      (algebraMap R (CliffordAlgebra Q)) ((Q' Q) m)
m₁ m₂ m₃ : M × R
⊢ ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
        ((ι Q) m₂.1 * (ι Q) m₂.1 - (algebraMap R (CliffordAlgebra Q)) m₂.2 * (algebraMap R (CliffordAlgebra Q)) m₂.2) *
      ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2) =
    ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
      (Q' Q) m₂ • ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2)
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝¹ : GradedAlgebra 𝒜
inst✝ : GradedAlgebra ℬ
⊢ 1 ⊗ₜ[R] 1 = 1

Tactic:
Algebra.TensorProduct.one_def

Goal state after:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝¹ : GradedAlgebra 𝒜
inst✝ : GradedAlgebra ℬ
⊢ 1 ⊗ₜ[R] 1 = 1 ⊗ₜ[R] 1