mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: case mk.mk
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
toLinearEquiv✝¹ : M₁ ≃ₗ[R] M₂
map_app'✝¹ : ∀ (m : M₁), Q₂ ((↑toLinearEquiv✝¹).toFun m) = Q₁ m
toLinearEquiv✝ : M₁ ≃ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), Q₂ ((↑toLinearEquiv✝).toFun m) = Q₁ m
⊢ ⇑{ toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ }.toLinearEquiv =
      ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.toLinearEquiv →
    ⇑{ toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ }.symm =
        ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.symm →
      { toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ } =
        { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }

Tactic:
;

Goal state after:
case mk.mk
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
toLinearEquiv✝¹ : M₁ ≃ₗ[R] M₂
map_app'✝¹ : ∀ (m : M₁), Q₂ ((↑toLinearEquiv✝¹).toFun m) = Q₁ m
toLinearEquiv✝ : M₁ ≃ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), Q₂ ((↑toLinearEquiv✝).toFun m) = Q₁ m
⊢ ⇑{ toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ }.toLinearEquiv =
      ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.toLinearEquiv →
    ⇑{ toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ }.symm =
        ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.symm →
      { toLinearEquiv := toLinearEquiv✝¹, map_app' := map_app'✝¹ } =
        { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
m : M₂
⊢ Q₁ ((↑f.symm).toFun m) = Q₂ m

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
m : M₂
⊢ Q₁ ((↑f.symm).toFun m) = Q₂ m
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
m : M₂
⊢ Q₂ (f ((↑f.symm).toFun m)) = Q₂ m

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
m : M₂
⊢ Q₂ (f ((↑f.symm).toFun m)) = Q₂ m
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: case e_6
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
m : M₂
⊢ f ((↑f.symm).toFun m) = m

Tactic:
;

Goal state after:
case e_6
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
m : M₂
⊢ f ((↑f.symm).toFun m) = m
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
g : Q₂.IsometryEquiv Q₃
m : M₁
⊢ Q₃ ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun m) = Q₁ m

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
g : Q₂.IsometryEquiv Q₃
m : M₁
⊢ Q₃ ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun m) = Q₁ m
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
g : Q₂.IsometryEquiv Q₃
m : M₁
⊢ Q₃ ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun m) = Q₃ (g (f m))

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
g : Q₂.IsometryEquiv Q₃
m : M₁
⊢ Q₃ ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun m) = Q₃ (g (f m))
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case inl
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
x✝¹ x✝ : SpecialLinearGroup n R
A : Matrix n n R
hA : A.det = 1
B : Matrix n n R
hB : B.det = 1
i j : n
hn : IsEmpty n
⊢ ↑⟨A, hA⟩ i j = ↑⟨B, hB⟩ i j

pp: case inr
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
x✝¹ x✝ : SpecialLinearGroup n R
A : Matrix n n R
hA : A.det = 1
B : Matrix n n R
hB : B.det = 1
i j : n
hn : Nonempty n
⊢ ↑⟨A, hA⟩ i j = ↑⟨B, hB⟩ i j

Tactic:
;

Goal state after:
case inl
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
x✝¹ x✝ : SpecialLinearGroup n R
A : Matrix n n R
hA : A.det = 1
B : Matrix n n R
hB : B.det = 1
i j : n
hn : IsEmpty n
⊢ ↑⟨A, hA⟩ i j = ↑⟨B, hB⟩ i j

case inr
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
x✝¹ x✝ : SpecialLinearGroup n R
A : Matrix n n R
hA : A.det = 1
B : Matrix n n R
hB : B.det = 1
i j : n
hn : Nonempty n
⊢ ↑⟨A, hA⟩ i j = ↑⟨B, hB⟩ i j
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case inl
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
x✝¹ x✝ : SpecialLinearGroup n R
A : Matrix n n R
hA : A.det = 1
B : Matrix n n R
hB : B.det = 1
i j : n
hn : IsEmpty n
⊢ False

Tactic:
;

Goal state after:
case inl
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
x✝¹ x✝ : SpecialLinearGroup n R
A : Matrix n n R
hA : A.det = 1
B : Matrix n n R
hB : B.det = 1
i j : n
hn : IsEmpty n
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case inl
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
hn : IsEmpty n
⊢ A ∈ center (SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A

pp: case inr
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
⊢ A ∈ center (SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A

Tactic:
;

Goal state after:
case inl
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
hn : IsEmpty n
⊢ A ∈ center (SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A

case inr
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
i : n
⊢ A ∈ center (SpecialLinearGroup n R) ↔ ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
i j : Fin 2
⊢ m i j = !![m 0 0, m 0 1; m 1 0, m 1 1] i j

Tactic:
;

Goal state after:
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
i j : Fin 2
⊢ m i j = !![m 0 0, m 0 1; m 1 0, m 1 1] i j
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
i✝ j✝ : ι
⊢ ↑(transvection hij 0) i✝ j✝ = ↑1 i✝ j✝

Tactic:
;

Goal state after:
ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
i✝ j✝ : ι
⊢ ↑(transvection hij 0) i✝ j✝ = ↑1 i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
k : Fin 2
⊢ (diag2 a ha • Pi.single 0 1) k = (a • Pi.single 0 1) k

Tactic:
;

Goal state after:
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
k : Fin 2
⊢ (diag2 a ha • Pi.single 0 1) k = (a • Pi.single 0 1) k
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
k : Fin 2
⊢ (diag2 a ha • Pi.single 1 1) k = (a⁻¹ • Pi.single 1 1) k

Tactic:
;

Goal state after:
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
k : Fin 2
⊢ (diag2 a ha • Pi.single 1 1) k = (a⁻¹ • Pi.single 1 1) k
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

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 ∈ ⊤
⊢ x ∈ Algebra.adjoin R (Set.range ⇑(ι Q))

Tactic:
;

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 ∈ ⊤
⊢ x ∈ Algebra.adjoin R (Set.range ⇑(ι Q))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

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
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ f a * f b + f b * f a = f a * f a + f b * f a + (f a * f b + f b * f b) - f a * f a - f b * f b

Tactic:
;

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
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ f a * f b + f b * f a = f a * f a + f b * f a + (f a * f b + f b * f b) - f a * f a - f b * f b
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case neg
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
hi2 : i2 ∈ ↑{i | i ≠ i₀}
hi12 : i1 ≠ i2
i j : ι
h✝¹ : ¬i2 = i₀
h✝ : ¬i1 = i₀
⊢ (if i = j then
      if i = i2 then if i = i1 then D i1 * D i2 else if i = i₀ then (D i1)⁻¹ * D i2 else D i2
      else if i = i₀ then if i = i1 then D i1 * (D i2)⁻¹ else (D i1)⁻¹ * (D i2)⁻¹ else if i = i1 then D i1 else 1
    else 0) =
    if i = j then
      if i = i1 then if i = i2 then D i2 * D i1 else if i = i₀ then (D i2)⁻¹ * D i1 else D i1
      else if i = i₀ then if i = i2 then D i2 * (D i1)⁻¹ else (D i2)⁻¹ * (D i1)⁻¹ else if i = i2 then D i2 else 1
    else 0

Tactic:
;

Goal state after:
case neg
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
i1 : ι
hi1 : i1 ∈ ↑{i | i ≠ i₀}
i2 : ι
hi2 : i2 ∈ ↑{i | i ≠ i₀}
hi12 : i1 ≠ i2
i j : ι
h✝¹ : ¬i2 = i₀
h✝ : ¬i1 = i₀
⊢ (if i = j then
      if i = i2 then if i = i1 then D i1 * D i2 else if i = i₀ then (D i1)⁻¹ * D i2 else D i2
      else if i = i₀ then if i = i1 then D i1 * (D i2)⁻¹ else (D i1)⁻¹ * (D i2)⁻¹ else if i = i1 then D i1 else 1
    else 0) =
    if i = j then
      if i = i1 then if i = i2 then D i2 * D i1 else if i = i₀ then (D i2)⁻¹ * D i1 else D i1
      else if i = i₀ then if i = i2 then D i2 * (D i1)⁻¹ else (D i2)⁻¹ * (D i1)⁻¹ else if i = i2 then D i2 else 1
    else 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M₁ : Type u_4
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
Q₁ : QuadraticForm R M₁
m : M₁
⊢ ((map (QuadraticMap.Isometry.id Q₁)).toLinearMap ∘ₗ ι Q₁) m =
    ((AlgHom.id R (CliffordAlgebra Q₁)).toLinearMap ∘ₗ ι Q₁) m

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : CommRing R
M₁ : Type u_4
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
Q₁ : QuadraticForm R M₁
m : M₁
⊢ ((map (QuadraticMap.Isometry.id Q₁)).toLinearMap ∘ₗ ι Q₁) m =
    ((AlgHom.id R (CliffordAlgebra Q₁)).toLinearMap ∘ₗ ι Q₁) m
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ mk 0 GOne.one = 1

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ mk 0 GOne.one = 1
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
h : Std.Associative fun x y ↦ x * y
x y z : R
⊢ associator x y z = 0 x y z

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
h : Std.Associative fun x y ↦ x * y
x y z : R
⊢ associator x y z = 0 x y z
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x✝¹ x✝ : R
⊢ ((mul.comp (mulLeft 0)) x✝¹) x✝ = (0 x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x✝¹ x✝ : R
⊢ ((mul.comp (mulLeft 0)) x✝¹) x✝ = (0 x✝¹) x✝
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y x✝¹ x✝ : R
⊢ ((mul.comp (mulLeft (x + y))) x✝¹) x✝ = ((mul.comp (mulLeft x) + mul.comp (mulLeft y)) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y x✝¹ x✝ : R
⊢ ((mul.comp (mulLeft (x + y))) x✝¹) x✝ = ((mul.comp (mulLeft x) + mul.comp (mulLeft y)) x✝¹) x✝
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x✝¹ x✝ : R
⊢ ((mul.compr₂ (mulLeft 0)) x✝¹) x✝ = (0 x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x✝¹ x✝ : R
⊢ ((mul.compr₂ (mulLeft 0)) x✝¹) x✝ = (0 x✝¹) x✝
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y x✝¹ x✝ : R
⊢ ((mul.compr₂ (mulLeft (x + y))) x✝¹) x✝ = ((mul.compr₂ (mulLeft x) + mul.compr₂ (mulLeft y)) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y x✝¹ x✝ : R
⊢ ((mul.compr₂ (mulLeft (x + y))) x✝¹) x✝ = ((mul.compr₂ (mulLeft x) + mul.compr₂ (mulLeft y)) x✝¹) x✝
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : Std.Associative fun x y ↦ x * y
x y z : R
⊢ ((mulLeft₃ x) y) z = ((mulRight₃ x) y) z

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : Std.Associative fun x y ↦ x * y
x y z : R
⊢ ((mulLeft₃ x) y) z = ((mulRight₃ x) y) z
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
i✝ j✝ : Fin 2
⊢ ↑(diag2n hij c hc) i✝ j✝ = ↑(diag2 c⁻¹ ⋯) i✝ j✝

Tactic:
;

Goal state after:
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
i✝ j✝ : Fin 2
⊢ ↑(diag2n hij c hc) i✝ j✝ = ↑(diag2 c⁻¹ ⋯) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
i✝ j✝ : Fin 2
⊢ (if i✝ = j✝ then if i✝ = 1 then c else if i✝ = 0 then c⁻¹ else 1 else 0) =
    if i✝ = j✝ then if i✝ = 0 then c⁻¹ else if i✝ = 1 then c else 1 else 0

Tactic:
;

Goal state after:
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
i✝ j✝ : Fin 2
⊢ (if i✝ = j✝ then if i✝ = 1 then c else if i✝ = 0 then c⁻¹ else 1 else 0) =
    if i✝ = j✝ then if i✝ = 0 then c⁻¹ else if i✝ = 1 then c else 1 else 0
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i), ((mulHom A) One.one) ((of A i) y) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) y)

Tactic:
;

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i), ((mulHom A) One.one) ((of A i) y) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) y)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i), ((mulHom A).flip One.one) ((of A i) y) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) y)

Tactic:
;

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i), ((mulHom A).flip One.one) ((of A i) y) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) y)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: case nil
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
⊢ (of A ([].dProdIndex fι)) GradedMonoid.GOne.one = 1

Tactic:
;

Goal state after:
case nil
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
⊢ (of A ([].dProdIndex fι)) GradedMonoid.GOne.one = 1
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case mk
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q Q' y : QuadraticMap R M N
toFun✝ : M → N
toFun_smul✝ : ∀ (a : R) (x : M), toFun✝ (a • x) = (a * a) • toFun✝ x
exists_companion'✝ : ∃ B, ∀ (x y : M), toFun✝ (x + y) = toFun✝ x + toFun✝ y + (B x) y
h : { toFun := toFun✝, toFun_smul := toFun_smul✝, exists_companion' := exists_companion'✝ }.toFun = y.toFun
⊢ { toFun := toFun✝, toFun_smul := toFun_smul✝, exists_companion' := exists_companion'✝ } = y

Tactic:
;

Goal state after:
case mk
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q Q' y : QuadraticMap R M N
toFun✝ : M → N
toFun_smul✝ : ∀ (a : R) (x : M), toFun✝ (a • x) = (a * a) • toFun✝ x
exists_companion'✝ : ∃ B, ∀ (x y : M), toFun✝ (x + y) = toFun✝ x + toFun✝ y + (B x) y
h : { toFun := toFun✝, toFun_smul := toFun_smul✝, exists_companion' := exists_companion'✝ }.toFun = y.toFun
⊢ { toFun := toFun✝, toFun_smul := toFun_smul✝, exists_companion' := exists_companion'✝ } = y