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

Goal state before:
pp: α : 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₂)
⊢ μ[μ[f | m₂] | m₁] =ᵐ[μ] μ[f | m₁]

Tactic:
by_cases hμm₁ : SigmaFinite (μ.trim (hm₁₂.trans hm₂))
  swap; · simp_rw [condExp_of_not_sigmaFinite (hm₁₂.trans hm₂) hμm₁]; rfl
  by_cases hf : Integrable f μ
  swap; · simp_rw [condExp_of_not_integrable hf, condExp_zero]; rfl
  refine ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' (hm₁₂.trans hm₂)
    (fun s _ _ => integrable_condExp.integrableOn) (fun s _ _ => integrable_condExp.integrableOn) ?_
    stronglyMeasurable_condExp.aestronglyMeasurable
    stronglyMeasurable_condExp.aestronglyMeasurable
  intro s hs _
  rw [setIntegral_condExp (hm₁₂.trans hm₂) integrable_condExp hs]
  rw [setIntegral_condExp (hm₁₂.trans hm₂) hf hs, setIntegral_condExp hm₂ hf (hm₁₂ s hs)]

Goal state after:
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)
inst✝ : CompleteSpace F'
f : ↥(lpMeas F' ℝ m 1 μ)
⊢ (condExpL1CLM F' hm μ) ↑f = ↑f

Tactic:
let g := lpMeasToLpTrimLie F' ℝ 1 μ hm f
  have hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g := by
    simp only [g, LinearIsometryEquiv.symm_apply_apply]
  rw [hfg]
  refine @Lp.induction α F' m _ 1 (μ.trim hm) _ ENNReal.coe_ne_top (fun g : α →₁[μ.trim hm] F' =>
    condExpL1CLM F' hm μ ((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g : α →₁[μ] F') =
    ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g)) ?_ ?_ ?_ g
  · intro c s hs hμs
    rw [@Lp.simpleFunc.coe_indicatorConst _ _ m, lpMeasToLpTrimLie_symm_indicator hs hμs.ne c,
      condExpL1CLM_indicatorConstLp]
    exact condExpInd_of_measurable hs ((le_trim hm).trans_lt hμs).ne c
  · intro f g hf hg _ hf_eq hg_eq
    rw [LinearIsometryEquiv.map_add]
    push_cast
    rw [map_add, hf_eq, hg_eq]
  · refine isClosed_eq ?_ ?_
    · refine (condExpL1CLM F' hm μ).continuous.comp (continuous_induced_dom.comp ?_)
      exact LinearIsometryEquiv.continuous _
    · refine continuous_induced_dom.comp ?_
      exact LinearIsometryEquiv.continuous _

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)
c : 𝕜
f : α → F'
⊢ condExpL1 hm μ (c • f) = c • condExpL1 hm μ f

Tactic:
by
  refine setToFun_smul _ ?_ c f
  exact fun c _ x => condExpInd_smul' c x

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)
⊢ ∫⁻ (ω : Ω) in s, (∂(P.withDensity X).trim hm/∂P.trim hm) ω ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P

Tactic:
← lintegral_indicator (hm s 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 : Ω), s.indicator (∂(P.withDensity X).trim hm/∂P.trim hm) a ∂P = ∫⁻ (ω : Ω) in s, X ω ∂P
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
this✝ : CompleteSpace ↥Y
this : SecondCountableTopology ↥Y
φY : ↥Y → ℝ := φ ∘ ⇑Y.subtypeL
fY : α → ↥Y := fun a ↦ if h : f a ∈ Y then ⟨f a, h⟩ else 0
fX : α → E := ⇑Y.subtypeL ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᵐ[μ] fX
hfY_int : Integrable fY μ
⊢ φ ∘ μ[f | m] ≤ᵐ[μ] μ[φ ∘ f | m]

Tactic:
have lem2 : μ[f | m] =ᵐ[μ] Y.subtypeL ∘ μ[fY | m] := calc
    _ =ᵐ[μ] μ[fX | m] := condExp_congr_ae lem1
    _ =ᵐ[μ] _ := (Y.subtypeL.comp_condExp_comm hfY_int).symm

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst✝ : IsFiniteMeasure μ
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := (Submodule.span ℝ t).topologicalClosure
this✝ : CompleteSpace ↥Y
this : SecondCountableTopology ↥Y
φY : ↥Y → ℝ := φ ∘ ⇑Y.subtypeL
fY : α → ↥Y := fun a ↦ if h : f a ∈ Y then ⟨f a, h⟩ else 0
fX : α → E := ⇑Y.subtypeL ∘ fY
lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y
lem1 : f =ᵐ[μ] fX
hfY_int : Integrable fY μ
lem2 : μ[f | m] =ᵐ[μ] ⇑Y.subtypeL ∘ μ[fY | m]
⊢ φ ∘ μ[f | m] ≤ᵐ[μ] μ[φ ∘ f | m]
Module: Mathlib.LinearAlgebra.AffineSpace.Matrix

Goal state before:
pp: ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : DecidableEq ι
⊢ b.toMatrix ⇑b = 1

Tactic:
ext i j

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
inst✝ : DecidableEq ι
i j : ι
⊢ b.toMatrix (⇑b) i j = 1 i j
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
⊢ r • (t • (x -ᵥ ↑h.some) + (↑h.some -ᵥ c)) +ᵥ c = (1 - r) • (c -ᵥ ↑h.some) +ᵥ x

Tactic:
smul_add,

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
⊢ (r • t • (x -ᵥ ↑h.some) + r • (↑h.some -ᵥ c)) +ᵥ c = (1 - r) • (c -ᵥ ↑h.some) +ᵥ x
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝¹⁷ : CommSemiring R
S : Type u_2
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Algebra R S
M : Type u_3
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
N : Type u_4
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
P : Type u_5
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
Q : Type u_6
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R Q
inst✝⁶ : Module S P
inst✝⁵ : IsScalarTower R S P
inst✝⁴ : Module S Q
inst✝³ : IsScalarTower R S Q
α : M →ₗ[R] P
β : N →ₗ[R] Q
ibcM : IsBaseChange S α
ibcN : IsBaseChange S β
ι : Type u_7
θ : Type u_8
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : Finite θ
b : Basis ι R M
c : Basis θ R N
f : M →ₗ[R] N
⊢ (toMatrix (basis b ibcM) (basis c ibcN)) ((ibcM.linearMapLeftRightHom β) f) = ((toMatrix b c) f).map ⇑(algebraMap R S)

Tactic:
ext i j

Goal state after:
R : Type u_1
inst✝¹⁷ : CommSemiring R
S : Type u_2
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Algebra R S
M : Type u_3
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
N : Type u_4
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
P : Type u_5
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
Q : Type u_6
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R Q
inst✝⁶ : Module S P
inst✝⁵ : IsScalarTower R S P
inst✝⁴ : Module S Q
inst✝³ : IsScalarTower R S Q
α : M →ₗ[R] P
β : N →ₗ[R] Q
ibcM : IsBaseChange S α
ibcN : IsBaseChange S β
ι : Type u_7
θ : Type u_8
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : Finite θ
b : Basis ι R M
c : Basis θ R N
f : M →ₗ[R] N
i : θ
j : ι
⊢ (toMatrix (basis b ibcM) (basis c ibcN)) ((ibcM.linearMapLeftRightHom β) f) i j =
    ((toMatrix b c) f).map (⇑(algebraMap R S)) i j
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:
by
  simp_rw [← MultilinearMap.domCoprod'_apply, MultilinearMap.alternatization_coe]
  simp_rw [TensorProduct.sum_tmul, TensorProduct.tmul_sum, _root_.map_sum,
    ← TensorProduct.smul_tmul', TensorProduct.tmul_smul]
  rfl

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
α : M →ₗ[R] P
ibcM : IsBaseChange S α
ι : Type u_7
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : M →ₗ[R] M
⊢ (toMatrix (basis b ibcM) (basis b ibcM)) (ibcM.endHom f) = ((toMatrix b b) f).map ⇑(algebraMap R S)

Tactic:
ext i j

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
α : M →ₗ[R] P
ibcM : IsBaseChange S α
ι : Type u_7
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : M →ₗ[R] M
i j : ι
⊢ (toMatrix (basis b ibcM) (basis b ibcM)) (ibcM.endHom f) i j = ((toMatrix b b) f).map (⇑(algebraMap R S)) i j
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f g : Dual R V
v x : V
hf : f v = 0
⊢ (transvection f v) ((transvection g v) x) = (transvection (f + g) v) x

Tactic:
simp [transvection, map_add, hf, add_smul, add_assoc]

Goal state after:
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
⊢ transvections R V ⊆ dilatransvections R V

Tactic:
rintro e ⟨f, v, hfv, rfl⟩

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
hfv : f v = 0
⊢ transvection hfv ∈ dilatransvections R V
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing A
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : AddCommGroup M₂
inst✝¹³ : AddCommGroup N₁
inst✝¹² : AddCommGroup N₂
inst✝¹¹ : Algebra R A
inst✝¹⁰ : Module R M₁
inst✝⁹ : Module A M₁
inst✝⁸ : Module R N₁
inst✝⁷ : Module A N₁
inst✝⁶ : SMulCommClass R A M₁
inst✝⁵ : IsScalarTower R A M₁
inst✝⁴ : IsScalarTower R A N₁
inst✝³ : Module R M₂
inst✝² : Module R N₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticMap A M₁ N₁
Q₂ : QuadraticMap R M₂ N₂
this : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
⊢ associated (Q₁.tmul Q₂) = (associated Q₁).tmul (associated Q₂)

Tactic:
QuadraticMap.tmul,

Goal state after:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing A
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : AddCommGroup M₂
inst✝¹³ : AddCommGroup N₁
inst✝¹² : AddCommGroup N₂
inst✝¹¹ : Algebra R A
inst✝¹⁰ : Module R M₁
inst✝⁹ : Module A M₁
inst✝⁸ : Module R N₁
inst✝⁷ : Module A N₁
inst✝⁶ : SMulCommClass R A M₁
inst✝⁵ : IsScalarTower R A M₁
inst✝⁴ : IsScalarTower R A N₁
inst✝³ : Module R M₂
inst✝² : Module R N₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticMap A M₁ N₁
Q₂ : QuadraticMap R M₂ N₂
this : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
⊢ associated ((tensorDistrib R A) (Q₁ ⊗ₜ[R] Q₂)) = (associated Q₁).tmul (associated Q₂)
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 : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x : CliffordAlgebra Q
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0 + foldr' Q (contractLeftAux Q d₂) ⋯ 0) x

Tactic:
LinearMap.add_apply

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
x : CliffordAlgebra Q
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x
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 : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x = ((RingHom.id R) c • foldr' Q (contractLeftAux Q d) ⋯ 0) x

Tactic:
LinearMap.smul_apply,

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x = (RingHom.id R) c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝
hy : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) y✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) y✝ =
    c • ((foldr' Q (contractLeftAux Q d) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d) ⋯ 0) y✝)

Tactic:
smul_add,

Goal state after:
case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝
hy : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) y✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) y✝ =
    c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝ + c • (foldr' Q (contractLeftAux Q d) ⋯ 0) y✝
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝
⊢ (c • d) m✝ • x✝ - (ι Q) m✝ * c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝ =
    c • (d m✝ • x✝ - (ι Q) m✝ * (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝)

Tactic:
LinearMap.smul_apply,

Goal state after:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) x✝ = c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝
⊢ (c • d m✝) • x✝ - (ι Q) m✝ * c • (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝ =
    c • (d m✝ • x✝ - (ι Q) m✝ * (foldr' Q (contractLeftAux Q d) ⋯ 0) x✝)
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
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
x y : ↑ι
h : i = x ∧ j = y
⊢ (Finsupp.single i ((Finsupp.single y 1) j)) x = Matrix.single i j 1 x y

Tactic:
rw [h.1, h.2]; simp

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

Goal state before:
pp: case algebraMap
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
r✝ : R
⊢ 0 = -0

Tactic:
neg_zero

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' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ (changeForm h) ((contractLeft d) x) = (contractLeft d) ((changeForm h) x)

Tactic:
induction x using CliffordAlgebra.left_induction with
  | algebraMap => simp only [contractLeft_algebraMap, changeForm_algebraMap, map_zero]
  | add _ _ hx hy => rw [map_add, map_add, map_add, map_add, hx, hy]
  | ι_mul _ _ hx =>
    simp only [contractLeft_ι_mul, changeForm_ι_mul, map_sub, map_smul]
    rw [← hx, contractLeft_comm, ← sub_add, sub_neg_eq_add, ← hx]

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

Goal state before:
pp: case snd.refine_3
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
m₁ : M
x y : M →ₗ[R] A
_hx : x ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
_hy : y ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
ihx : (f.bilin m₁) m * x m = Q m • x m₁
ihy : (f.bilin m₁) m * y m = Q m • y m₁
⊢ (f.bilin m₁) m * x m + (f.bilin m₁) m * y m = Q m • (x m₁ + y m₁)

Tactic:
smul_add,

Goal state after:
case snd.refine_3
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
m₁ : M
x y : M →ₗ[R] A
_hx : x ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
_hy : y ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
ihx : (f.bilin m₁) m * x m = Q m • x m₁
ihy : (f.bilin m₁) m * y m = Q m • y m₁
⊢ (f.bilin m₁) m * x m + (f.bilin m₁) m * y m = Q m • x m₁ + Q m • y m₁
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

Goal state before:
pp: case snd.refine_4
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
m₁ : M
x : R
hx : M →ₗ[R] A
_c : hx ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
ihx : (f.bilin m₁) m * hx m = Q m • hx m₁
⊢ (f.bilin m₁) m * (x • hx) m = Q m • (x • hx) m₁

Tactic:
LinearMap.smul_apply,

Goal state after:
case snd.refine_4
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
m₁ : M
x : R
hx : M →ₗ[R] A
_c : hx ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
ihx : (f.bilin m₁) m * hx m = Q m • hx m₁
⊢ (f.bilin m₁) m * x • hx m = Q m • (x • hx) m₁
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

Goal state before:
pp: case snd.refine_4
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
m₁ : M
x : R
hx : M →ₗ[R] A
_c : hx ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
ihx : (f.bilin m₁) m * hx m = Q m • hx m₁
⊢ (f.bilin m₁) m * x • hx m = Q m • (x • hx) m₁

Tactic:
LinearMap.smul_apply,

Goal state after:
case snd.refine_4
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
m₁ : M
x : R
hx : M →ₗ[R] A
_c : hx ∈ Submodule.span R {f' | ∃ x m₂, f' = (LinearMap.lcomp R A (f.bilin.flip m₂)) (LinearMap.mulRight R x)}
ihx : (f.bilin m₁) m * hx m = Q m • hx m₁
⊢ (f.bilin m₁) m * x • hx m = Q m • x • hx m₁
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
hx : x ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
inst✝ : Invertible 2
m : M
⊢ ConjAct.toConjAct x • (ι Q) m ∈ (ι Q).range

Tactic:
ConjAct.units_smul_def,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
hx : x ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
inst✝ : Invertible 2
m : M
⊢ ↑(ConjAct.ofConjAct (ConjAct.toConjAct x)) * (ι Q) m * ↑(ConjAct.ofConjAct (ConjAct.toConjAct x))⁻¹ ∈ (ι Q).range