mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case zero
R : Type u_3
V : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
A : Type u_5
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
W : Type u_6
inst✝³ : AddCommMonoid W
inst✝² : Module R W
inst✝¹ : Module A W
inst✝ : IsScalarTower R A W
ε : V →ₗ[R] W
ibc : IsBaseChange A ε
f : Dual R V
v : V
⊢ (ibc.endHom (LinearMap.transvection f v)) 0 = (LinearMap.transvection (ibc.toDual f) (ε v)) 0

Tactic:
simp

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

Goal state before:
pp: case ι
R : Type u_1
inst✝ : CommRing R
y : CliffordAlgebra 0
x : Unit
⊢ (ι 0) x * y = y * (ι 0) x

Tactic:
simp

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
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 : x = y
⊢ (Finsupp.single y 1) y = 1 y y

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x✝ : Unit
⊢ (involute.toLinearMap ∘ₗ ι 0) x✝ = ((AlgHom.id R (CliffordAlgebra 0)).toLinearMap ∘ₗ ι 0) x✝

Tactic:
simp

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

Goal state before:
pp: r : ℝ
⊢ ↑r * ↑r * (Complex.I * Complex.I) = ↑(-(r * r))

Tactic:
simp

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

Goal state before:
pp: ⊢ ↑⟨(ι Q) 1, ofComplex._proof_1⟩ * ↑⟨(ι Q) 1, ofComplex._proof_1⟩ = -1

Tactic:
simp

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
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 x ((Finsupp.single y 1) y)) x = Matrix.single x y 1 x y

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (algebraMap R (CliffordAlgebra (Q c₁ c₂))) (c₁ * ((1, 0).1 * (1, 0).1) + c₂ * ((1, 0).2 * (1, 0).2)) =
    (algebraMap R (CliffordAlgebra (Q c₁ c₂))) c₁ + 0 • (ι (Q c₁ c₂)) (1, 0)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (algebraMap R (CliffordAlgebra (Q c₁ c₂))) (c₁ * ((0, 1).1 * (0, 1).1) + c₂ * ((0, 1).2 * (0, 1).2)) =
    (algebraMap R (CliffordAlgebra (Q c₁ c₂))) c₂

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (algebraMap R (CliffordAlgebra (Q c₁ c₂))) ((Q c₁ c₂) ((0, 1) + (1, 0)) - (Q c₁ c₂) (0, 1) - (Q c₁ c₂) (1, 0)) = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v₁ v₂ : R × R
⊢ { re := 0, imI := (v₁ + v₂).1, imJ := (v₁ + v₂).2, imK := 0 } =
    { re := 0, imI := v₁.1, imJ := v₁.2, imK := 0 } + { re := 0, imI := v₂.1, imJ := v₂.2, imK := 0 }

Tactic:
simp

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

Goal state before:
pp: case algebraMap
R : Type u_1
inst✝ : CommRing R
c₁ c₂ r : R
⊢ toQuaternion (involute (reverse ((algebraMap R (CliffordAlgebra (Q c₁ c₂))) r))) =
    star (toQuaternion ((algebraMap R (CliffordAlgebra (Q c₁ c₂))) r))

Tactic:
simp

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

Goal state before:
pp: case ι
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
x : R × R
⊢ toQuaternion (involute (reverse ((ι (Q c₁ c₂)) x))) = star (toQuaternion ((ι (Q c₁ c₂)) x))

Tactic:
simp

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

Goal state before:
pp: case hl
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (((ofQuaternion.comp toQuaternion).toLinearMap ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inl R R R) 1 =
    (((AlgHom.id R (CliffordAlgebra (Q c₁ c₂))).toLinearMap ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inl R R R) 1

Tactic:
simp

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

Goal state before:
pp: case hr
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (((ofQuaternion.comp toQuaternion).toLinearMap ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inr R R R) 1 =
    (((AlgHom.id R (CliffordAlgebra (Q c₁ c₂))).toLinearMap ∘ₗ ι (Q c₁ c₂)) ∘ₗ LinearMap.inr R R R) 1

Tactic:
simp

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

Goal state before:
pp: case hi
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (toQuaternion.comp ofQuaternion) (Basis.self R).i = (AlgHom.id R ℍ[R,c₁,c₂]) (Basis.self R).i

Tactic:
simp

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

Goal state before:
pp: case hj
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (toQuaternion.comp ofQuaternion) (Basis.self R).j = (AlgHom.id R ℍ[R,c₁,c₂]) (Basis.self R).j

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ (((CliffordAlgebra.lift 0) ⟨inrHom R R, ⋯⟩).comp (DualNumber.lift ⟨(Algebra.ofId R (CliffordAlgebra 0), (ι 0) 1), ⋯⟩))
      ε =
    (AlgHom.id R R[ε]) ε

Tactic:
simp

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

Goal state before:
pp: 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))
⊢ Function.update 1 i (1 + f v) i = 1 + f v

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ (((DualNumber.lift ⟨(Algebra.ofId R (CliffordAlgebra 0), (ι 0) 1), ⋯⟩).comp
            ((CliffordAlgebra.lift 0) ⟨inrHom R R, ⋯⟩)).toLinearMap ∘ₗ
        ι 0)
      1 =
    ((AlgHom.id R (CliffordAlgebra 0)).toLinearMap ∘ₗ ι 0) 1

Tactic:
simp

Goal state after:
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))
⊢ ∀ b ∈ Finset.univ, b ≠ i → Function.update 1 i (1 + f v) b = 1

Tactic:
intro j

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 : ↑ι
⊢ j ∈ Finset.univ → j ≠ i → Function.update 1 i (1 + f v) j = 1
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))
⊢ i ∉ Finset.univ → Function.update 1 i (1 + f v) i = 1

Tactic:
simp

Goal state after:
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
⊢ (algebraMap R (CliffordAlgebra (Q' Q))) ((Q' Q) (0, 1)) = -1

Tactic:
simp

Goal state after:
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
m : M
⊢ (algebraMap R (CliffordAlgebra (Q' Q))) ((Q' Q) ((LinearMap.inl R M R) m)) =
    (algebraMap R (CliffordAlgebra (Q' Q))) (Q m)

Tactic:
simp

Goal state after:
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
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this : Fintype ↑ι
x y : ↑ι
⊢ (Finsupp.single y 1) x + f (b y) * (Finsupp.single i 1) x = if x = y then if x = i then 1 + f (b i) else 1 else 0

Tactic:
hf

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
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this : Fintype ↑ι
x y : ↑ι
⊢ (Finsupp.single y 1) x + (f v • b.coord i) (b y) * (Finsupp.single i 1) x =
    if x = y then if x = i then 1 + (f v • b.coord i) (b i) else 1 else 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

Goal state before:
pp: case snd.refine_2
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
⊢ (f.bilin m₁) m * 0 m = Q m • 0 m₁

Tactic:
simp

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

Tactic:
let : Field K := inferInstance

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

Goal state before:
pp: 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
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
hf : ibc.toDual fM = f
⊢ LinearMap.det (transvection f v) = 1 + f v

Tactic:
have hv : ε vM = v := by
    rw [of_fintype_basis_eq]
    ext i
    rw [RingHom.algebraMap_toAlgebra]
    simp only [vM, γ, Function.comp_apply]
    apply MvPolynomial.aeval_X

Goal state after:
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
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
hf : ibc.toDual fM = f
hv : ε vM = v
⊢ LinearMap.det (transvection f v) = 1 + f v
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' Q) m₂ •
        (((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
          ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2))

Tactic:
intro m₁ m₂ m₃

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 - (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) * ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion

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
inst✝¹ : Invertible 2
m : M
inst✝ : Invertible ((ι Q) m)
⊢ ↑(equivExterior Q) 1 = 1

Tactic:
simp

Goal state after:
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 ℬ
inst✝ : Module ι (Additive ℤˣ)
⊢ 0 ᵍ⊗ₜ[R] 1 = 0

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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 ℬ
inst✝ : Module ι (Additive ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
⊢ r • x = r • (auxEquiv R 𝒜 ℬ).symm ((auxEquiv R 𝒜 ℬ) x)

Tactic:
simp

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

Goal state before:
pp: case ha
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
x✝ : M₁
⊢ ((((ofProd Q₁ Q₂).comp (toProd Q₁ Q₂)).comp
            (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))).toLinearMap ∘ₗ
        ι Q₁)
      x✝ =
    (((AlgHom.id R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)).comp
            (GradedTensorProduct.includeLeft (evenOdd Q₁) (evenOdd Q₂))).toLinearMap ∘ₗ
        ι Q₁)
      x✝

Tactic:
simp

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

Goal state before:
pp: case hb
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
x✝ : M₂
⊢ ((((ofProd Q₁ Q₂).comp (toProd Q₁ Q₂)).comp
            (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))).toLinearMap ∘ₗ
        ι Q₂)
      x✝ =
    (((AlgHom.id R (evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂)).comp
            (GradedTensorProduct.includeRight (evenOdd Q₁) (evenOdd Q₂))).toLinearMap ∘ₗ
        ι Q₂)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)

Tactic:
refine Fin.consInduction ?_ ?_ x <;> clear x

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x ↦ a.elim0)) (List.finRange 0)).prod =
    GradedMonoid.mk 0 ((PiTensorProduct.tprod R) Fin.elim0)

case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ ∀ {n : ℕ} (x₀ : M) (x : Fin n → M),
    (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ x a)) (List.finRange n)).prod =
        GradedMonoid.mk n ((PiTensorProduct.tprod R) x) →
      (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ Fin.cons x₀ x a))
            (List.finRange (n + 1))).prod =
        GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
inst✝ : AddCommGroup G
n : ℕ
⊢ ∀ (x : G), n • x ∈ ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: G : Type u_1
H✝ : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b.repr
x : G
⊢ ((LinearMap.lsmul ℤ G) ↑n) x ∈ (mod ∘ₗ f).ker

Tactic:
ext b

Goal state after:
G : Type u_1
H✝ : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b✝ : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b✝.repr
x : G
b : ι
⊢ ((mod ∘ₗ f) (((LinearMap.lsmul ℤ G) ↑n) x)) b = 0 b
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
c : Fin n → R
i : ι
h : ∃ j, f j = i
⊢ h.choose ∉ Finset.univ → (c h.choose • if i = f h.choose then a h.choose else 0) = 0

Tactic:
simp

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

Goal state before:
pp: case e'_8
I : Type u
inst✝³ : DecidableEq I
i : I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
a₁ a₂ : A i
⊢ (ι R) ((lof R I A i) a₁) * (ι R) ((lof R I A i) a₂) =
    (tprod R (⨁ (i : I), A i) 2) fun x ↦
      match x with
      | 0 => (lof R I A i) a₁
      | 1 => (lof R I A i) a₂

Tactic:
simp

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

Goal state before:
pp: case id
I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps✝ maps : {i : I} → A i →ₐ[R] B
i✝ : I
⊢ (RingCon.ker ((TensorAlgebra.lift R) (toModule R I B fun x ↦ maps.toLinearMap)).toRingHom)
    ((TensorAlgebra.ι R) ((DirectSum.lof R I A i✝) 1)) 1

Tactic:
simp

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

Goal state before:
pp: case prod
I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps✝ maps : {i : I} → A i →ₐ[R] B
i✝ : I
a₁✝ a₂✝ : A i✝
⊢ (RingCon.ker ((TensorAlgebra.lift R) (toModule R I B fun x ↦ maps.toLinearMap)).toRingHom)
    ((tprod R (⨁ (i : I), A i) 2) fun x ↦
      match x with
      | 0 => (DirectSum.lof R I A i✝) a₁✝
      | 1 => (DirectSum.lof R I A i✝) a₂✝)
    ((TensorAlgebra.ι R) ((DirectSum.lof R I A i✝) (a₁✝ * a₂✝)))

Tactic:
simp

Goal state after: