mathlib-initiative/mathlib-tactics huggingface dataset:
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 α
mE : MeasurableSpace E
inst✝¹ : BorelSpace E
hm : m ≤ mα
inst✝ : SigmaFinite (μ.trim hm)
hφ_cvx : ConcaveOn ℝ univ φ
hφ_cont : UpperSemicontinuous φ
hφ_meas : StronglyMeasurable φ
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
⊢ μ[φ ∘ f | m] ≤ᵐ[μ.trim hm] φ ∘ μ[f | m]

Tactic:
by
  rw [StronglyMeasurable.ae_le_trim_iff hm (by fun_prop) (by fun_prop)]
  exact hφ_cvx.condExp_map_le_univ hm hφ_cont hf_int hφ_int

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
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
l m : ι
⊢ b₂.coords (b₂ l) m = 1 l m

Tactic:
coords_apply,

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✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
l m : ι
⊢ (b₂.coord m) (b₂ l) = 1 l m
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
inst✝¹ : Free R M
inst✝ : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
β : N →ₗ[R] Q
k : IsBaseChange S β
f : M →ₗ[R] N
p : P
⊢ ((⋯.equiv ≪≫ₗ liftBaseChangeEquiv S ≪≫ₗ LinearEquiv.congrLeft Q S j.equiv) (1 ⊗ₜ[R] f)) p =
    ((j.linearMapLeftRightHom β) f) p

Tactic:
simp [IsBaseChange.equiv_tmul, LinearEquiv.congrLeft, linearMapLeftRightHom_apply]

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

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
⊢ Mᵢ [⋀^ιa]→ₗ[R'] N₁ →ₗ[R'] Mᵢ [⋀^ιb]→ₗ[R'] N₂ →ₗ[R'] Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂

Tactic:
refine
      LinearMap.mk₂ R' domCoprod (fun m₁ m₂ n => ?_) (fun c m n => ?_) (fun m n₁ n₂ => ?_)
        fun c m n => ?_ <;>
    · ext
      simp only [domCoprod_apply, add_apply, smul_apply, ← Finset.sum_add_distrib,
        Finset.smul_sum, _root_.sum_apply, domCoprod.summand]
      congr
      ext σ
      induction σ using Quotient.inductionOn'
      simp only [Quotient.liftOn'_mk'', coe_add, coe_smul, _root_.smul_apply,
        ← MultilinearMap.domCoprod'_apply]
      simp only [TensorProduct.add_tmul, ← TensorProduct.smul_tmul', TensorProduct.tmul_add,
        TensorProduct.tmul_smul, map_add, map_smul]
      first | rw [← smul_add] | rw [smul_comm]
      rfl

Goal state after:
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f : V →ₗ[R] V
v : V
⊢ v ∈ f.fixedSubmodule ↔ f v = v

Tactic:
by
  simp [fixedSubmodule]

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
f : Dual R V
v : V
hv : f v = 0
hv' : f (-v) = 0
⊢ (transvection hv).symm = transvection hv'

Tactic:
by
  ext;
  simp [symm_apply_eq, comp_of_left_eq_apply hv']

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
f : Dual R V
v : V
h : IsUnit (1 + f v)
x : V
⊢ (dilatransvection h) x = x + f x • v

Tactic:
simp [dilatransvection, LinearMap.transvection.apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case inr
R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : StrongRankCondition R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
hV : Nontrivial V
⊢ ∃ a, f = a • 1

Tactic:
let ι := Free.ChooseBasisIndex R V

Goal state after:
case inr
R : Type u_1
V : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : StrongRankCondition R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
hV : Nontrivial V
ι : Type u_2 := Free.ChooseBasisIndex R V
⊢ ∃ a, f = a • 1
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ associated (Q₁.tmul Q₂) = (BilinForm.tensorDistrib R A) (associated Q₁ ⊗ₜ[R] associated Q₂)

Tactic:
BilinForm.tensorDistrib,

Goal state after:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ associated (Q₁.tmul Q₂) =
    (↑(AlgebraTensorModule.rid R A A).congrRight₂ ∘ₗ BilinMap.tensorDistrib R A) (associated Q₁ ⊗ₜ[R] associated Q₂)
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (m : M₂), Q₁ (1 ⊗ₜ[R] m) = Q₂ (1 ⊗ₜ[R] m)
a : A
m : M₂
⊢ Q₁ ((a * 1) ⊗ₜ[R] m) = Q₂ ((a * 1) ⊗ₜ[R] m)

Tactic:
← smul_eq_mul,

Goal state after:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Algebra R A
inst✝³ : Module R N₁
inst✝² : Module A N₁
inst✝¹ : IsScalarTower R A N₁
inst✝ : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h : ∀ (m : M₂), Q₁ (1 ⊗ₜ[R] m) = Q₂ (1 ⊗ₜ[R] m)
a : A
m : M₂
⊢ Q₁ ((a • 1) ⊗ₜ[R] m) = Q₂ ((a • 1) ⊗ₜ[R] m)
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' d₁ d₂ : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
hy :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝ +
      ((foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝)

Tactic:
hx,

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' d₁ d₂ : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) x✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝
hy :
  (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝
⊢ (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝ +
      (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) y✝ =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) x✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) x✝ +
      ((foldr' Q (contractLeftAux Q d₁) ⋯ 0) y✝ + (foldr' Q (contractLeftAux Q d₂) ⋯ 0) y✝)
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✝ + c • (foldr' Q (contractLeftAux Q d) ⋯ 0) y✝

Tactic:
hx,

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✝
⊢ c • (foldr' Q (contractLeftAux Q 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 add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d) x✝) = 0
hy : (contractLeft d) ((contractLeft d) y✝) = 0
⊢ (contractLeft d) ((contractLeft d) x✝) + (contractLeft d) ((contractLeft d) y✝) = 0

Tactic:
hx,

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 : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d) x✝) = 0
hy : (contractLeft d) ((contractLeft d) y✝) = 0
⊢ 0 + (contractLeft d) ((contractLeft d) y✝) = 0
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 : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (contractLeft d) ((contractLeft d) x✝) = 0
⊢ (contractLeft d) (d m✝ • x✝) - (d m✝ • (contractLeft d) x✝ - (ι Q) m✝ * (contractLeft d) ((contractLeft d) x✝)) = 0

Tactic:
hx,

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 : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (contractLeft d) ((contractLeft d) x✝) = 0
⊢ (contractLeft d) (d m✝ • x✝) - (d m✝ • (contractLeft d) x✝ - (ι Q) m✝ * 0) = 0
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
x✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
hy : (contractLeft d) ((contractLeft d') y✝) = -(contractLeft d') ((contractLeft d) y✝)
⊢ (contractLeft d) ((contractLeft d') x✝) + (contractLeft d) ((contractLeft d') y✝) =
    -((contractLeft d') ((contractLeft d) x✝) + (contractLeft d') ((contractLeft d) y✝))

Tactic:
hx,

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
x✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
hy : (contractLeft d) ((contractLeft d') y✝) = -(contractLeft d') ((contractLeft d) y✝)
⊢ -(contractLeft d') ((contractLeft d) x✝) + (contractLeft d) ((contractLeft d') y✝) =
    -((contractLeft d') ((contractLeft d) x✝) + (contractLeft d') ((contractLeft d) 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
x✝ : CliffordAlgebra Q
m✝ : M
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
⊢ d' m✝ • (contractLeft d) x✝ + (ι Q) m✝ * (contractLeft d) ((contractLeft d') x✝) - d m✝ • (contractLeft d') x✝ =
    d' m✝ • (contractLeft d) x✝ - (ι Q) m✝ * (contractLeft d') ((contractLeft d) x✝) - d m✝ • (contractLeft d') x✝

Tactic:
hx,

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
x✝ : CliffordAlgebra Q
m✝ : M
hx : (contractLeft d) ((contractLeft d') x✝) = -(contractLeft d') ((contractLeft d) x✝)
⊢ d' m✝ • (contractLeft d) x✝ + (ι Q) m✝ * -(contractLeft d') ((contractLeft d) x✝) - d m✝ • (contractLeft d') x✝ =
    d' m✝ • (contractLeft d) x✝ - (ι Q) m✝ * (contractLeft d') ((contractLeft d) x✝) - d m✝ • (contractLeft d') 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 Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h) ((contractLeft d) x✝) = (contractLeft d) ((changeForm h) x✝)
hy : (changeForm h) ((contractLeft d) y✝) = (contractLeft d) ((changeForm h) y✝)
⊢ (changeForm h) ((contractLeft d) x✝) + (changeForm h) ((contractLeft d) y✝) =
    (contractLeft d) ((changeForm h) x✝) + (contractLeft d) ((changeForm h) y✝)

Tactic:
hx,

Goal state after:
case add
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✝ y✝ : CliffordAlgebra Q
hx : (changeForm h) ((contractLeft d) x✝) = (contractLeft d) ((changeForm h) x✝)
hy : (changeForm h) ((contractLeft d) y✝) = (contractLeft d) ((changeForm h) y✝)
⊢ (contractLeft d) ((changeForm h) x✝) + (changeForm h) ((contractLeft d) y✝) =
    (contractLeft d) ((changeForm h) x✝) + (contractLeft d) ((changeForm h) y✝)
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
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm ⋯) x✝ = x✝
hy : (changeForm ⋯) y✝ = y✝
⊢ (changeForm ⋯) x✝ + (changeForm ⋯) y✝ = x✝ + y✝

Tactic:
hx,

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
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm ⋯) x✝ = x✝
hy : (changeForm ⋯) y✝ = y✝
⊢ x✝ + (changeForm ⋯) y✝ = x✝ + 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
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm ⋯) x✝ = x✝
⊢ (ι Q) m✝ * (changeForm ⋯) x✝ - (contractLeft (0 m✝)) ((changeForm ⋯) x✝) = (ι Q) m✝ * x✝

Tactic:
hx,

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
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm ⋯) x✝ = x✝
⊢ (ι Q) m✝ * x✝ - (contractLeft (0 m✝)) x✝ = (ι Q) m✝ * x✝
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

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
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
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)

Tactic:
rw [ι_sq_scalar, ← map_mul, ← map_sub, sub_eq_add_neg, Q'_apply, sub_eq_add_neg]

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
inst✝ : IsDomain R
f : Dual R V
v : V
K : Type u_3 := FractionRing R
this✝ : Field K := inferInstance
this : (algebraMap R K) (LinearMap.det (transvection f v)) = 1 + ((Dual.baseChange K) f) (1 ⊗ₜ[R] v)
⊢ (algebraMap R K) (LinearMap.det (transvection f v)) = (algebraMap R K) (1 + f v)

Tactic:
← algebraMap.coe_one (R := R) (A := K)

Goal state after:
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
inst✝ : IsDomain R
f : Dual R V
v : V
K : Type u_3 := FractionRing R
this✝ : Field K := inferInstance
this : (algebraMap R K) (LinearMap.det (transvection f v)) = ↑1 + ((Dual.baseChange K) f) (↑1 ⊗ₜ[R] v)
⊢ (algebraMap R K) (LinearMap.det (transvection f v)) = (algebraMap R K) (1 + f v)
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 Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
hy : (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) y✝
⊢ (changeForm h') ((changeForm h) x✝) + (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) x✝ + (changeForm ⋯) y✝

Tactic:
hx,

Goal state after:
case add
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
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ y✝ : CliffordAlgebra Q
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
hy : (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) y✝
⊢ (changeForm ⋯) x✝ + (changeForm h') ((changeForm h) y✝) = (changeForm ⋯) x✝ + (changeForm ⋯) 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 Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (ι Q'') m✝ * (changeForm h') ((changeForm h) x✝) - (contractLeft (B' m✝)) ((changeForm h') ((changeForm h) x✝)) -
      (changeForm h') ((contractLeft (B m✝)) ((changeForm h) x✝)) =
    (ι Q'') m✝ * (changeForm ⋯) x✝ - (contractLeft ((B + B') m✝)) ((changeForm ⋯) x✝)

Tactic:
hx,

Goal state after:
case ι_mul
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
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (ι Q'') m✝ * (changeForm ⋯) x✝ - (contractLeft (B' m✝)) ((changeForm ⋯) x✝) -
      (changeForm h') ((contractLeft (B m✝)) ((changeForm h) x✝)) =
    (ι Q'') m✝ * (changeForm ⋯) x✝ - (contractLeft ((B + B') m✝)) ((changeForm ⋯) x✝)
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 Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (ι Q'') m✝ * (changeForm ⋯) x✝ -
      ((contractLeft (B' m✝)) ((changeForm ⋯) x✝) + (contractLeft (B m✝)) ((changeForm h') ((changeForm h) x✝))) =
    (ι Q'') m✝ * (changeForm ⋯) x✝ -
      ((contractLeft (B m✝)) ((changeForm ⋯) x✝) + (contractLeft (B' m✝)) ((changeForm ⋯) x✝))

Tactic:
hx,

Goal state after:
case ι_mul
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
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (ι Q'') m✝ * (changeForm ⋯) x✝ -
      ((contractLeft (B' m✝)) ((changeForm ⋯) x✝) + (contractLeft (B m✝)) ((changeForm ⋯) x✝)) =
    (ι Q'') m✝ * (changeForm ⋯) x✝ -
      ((contractLeft (B m✝)) ((changeForm ⋯) x✝) + (contractLeft (B' m✝)) ((changeForm ⋯) x✝))
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: case e'_3
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 ℬ
inst✝ : Module ι (Additive ℤˣ)
i₂ : ι
a₁ : A
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ b₂ = ↑GradedMonoid.GOne.one * b₂

Tactic:
SetLike.coe_gOne,

Goal state after:
case e'_3
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 ℬ
inst✝ : Module ι (Additive ℤˣ)
i₂ : ι
a₁ : A
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ b₂ = 1 * b₂
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: case e'_3
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 ℬ
inst✝ : Module ι (Additive ℤˣ)
j₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
b₂ : B
⊢ a₁ = a₁ * ↑GradedMonoid.GOne.one

Tactic:
SetLike.coe_gOne,

Goal state after:
case e'_3
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 ℬ
inst✝ : Module ι (Additive ℤˣ)
j₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
b₂ : B
⊢ a₁ = a₁ * 1