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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
hf : Function.Surjective ⇑f
x✝³ x✝² : CliffordAlgebra Q₂
x✝¹ : ∃ a, (map f) a = x✝³
x✝ : ∃ a, (map f) a = x✝²
x : CliffordAlgebra Q₁
hx : (map f) x = x✝³
y : CliffordAlgebra Q₁
hy : (map f) y = x✝²
⊢ (map f) (x * y) = x✝³ * x✝²

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
hf : Function.Surjective ⇑f
x✝³ x✝² : CliffordAlgebra Q₂
x✝¹ : ∃ a, (map f) a = x✝³
x✝ : ∃ a, (map f) a = x✝²
x : CliffordAlgebra Q₁
hx : (map f) x = x✝³
y : CliffordAlgebra Q₁
hy : (map f) y = x✝²
⊢ (map f) (x + y) = x✝³ + x✝²

Tactic:
by

Goal state after:
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_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
⊢ map (e.toIsometry.comp e.symm.toIsometry) = AlgHom.id R (CliffordAlgebra Q₂)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial ι
P : SpecialLinearGroup ι F → Prop
M : SpecialLinearGroup ι F
hdiag : ∀ (i j : ι) (hij : i ≠ j) {c : F} (hc : c ≠ 0), P (diag2n hij c hc)
htransvec : ∀ (i j : ι) (hij : i ≠ j) (a : F), P (transvection hij a)
hmul : ∀ (A B : SpecialLinearGroup ι F), P A → P B → P (A * B)
i₀ j₀ : ι
hij₀ : i₀ ≠ j₀
hP1 : P 1
D : ι → F
hD : (diagonal D).det = 1
⊢ P ⟨diagonal D, hD⟩

Tactic:
by

Goal state after:
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_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticMap.IsometryEquiv Q₁ Q₂
⊢ map (e.symm.toIsometry.comp e.toIsometry) = AlgHom.id R (CliffordAlgebra Q₁)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e₁₂ : QuadraticMap.IsometryEquiv Q₁ Q₂
e₂₃ : QuadraticMap.IsometryEquiv Q₂ Q₃
⊢ (equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃) = equivOfIsometry (e₁₂.trans e₂₃)

Tactic:
by

Goal state after:
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₁
⊢ equivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁) = AlgEquiv.refl

Tactic:
by

Goal state after:
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
m : M
⊢ toClifford ((ι R) m) = (CliffordAlgebra.ι Q) m

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial ι
P : SpecialLinearGroup ι F → Prop
M : SpecialLinearGroup ι F
hdiag : ∀ (i j : ι) (hij : i ≠ j) {c : F} (hc : c ≠ 0), P (diag2n hij c hc)
htransvec : ∀ (i j : ι) (hij : i ≠ j) (a : F), P (transvection hij a)
hmul : ∀ (A B : SpecialLinearGroup ι F), P A → P B → P (A * B)
i₀ j₀ : ι
hij₀ : i₀ ≠ j₀
hP1 : P 1
hdiagonal : ∀ (D : ι → F) (hD : (diagonal D).det = 1), P ⟨diagonal D, hD⟩
L : List (TransvectionStruct ι F)
⊢ P (List.map TransvectionStruct.toSpecialLinearGroup L).prod

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : AddMonoid ι
l : List α
fι : α → ι
⊢ l.dProdIndex fι = (map fι l).sum

Tactic:
by

Goal state after:
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 (l.dProdIndex fι) (l.dProd fι fA) = (List.map (fun a ↦ mk (fι a) (fA a)) l).prod

Tactic:
match l with
  | [] => simp only [List.dProdIndex_nil, List.dProd_nil, List.map_nil, List.prod_nil]; rfl
  | head::tail =>
    simp [← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]

Goal state after:
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 (l.dProdIndex fι) (l.dProd fι fA) = (List.map (fun a ↦ mk (fι a) (fA a)) l).prod

Tactic:
by

Goal state after:
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 : α → GradedMonoid A
⊢ (List.map f l).prod = mk (l.dProdIndex fun i ↦ (f i).fst) (l.dProd (fun i ↦ (f i).fst) fun i ↦ (f i).snd)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
n : ℕ
f : Fin n → GradedMonoid A
⊢ (List.ofFn f).prod =
    mk ((List.finRange n).dProdIndex fun i ↦ (f i).fst) ((List.finRange n).dProd (fun i ↦ (f i).fst) fun i ↦ (f i).snd)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial ι
P : SpecialLinearGroup ι F → Prop
M : SpecialLinearGroup ι F
hdiag : ∀ (i j : ι) (hij : i ≠ j) {c : F} (hc : c ≠ 0), P (diag2n hij c hc)
htransvec : ∀ (i j : ι) (hij : i ≠ j) (a : F), P (transvection hij a)
hmul : ∀ (A B : SpecialLinearGroup ι F), P A → P B → P (A * B)
⊢ P M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ l.dProd fι fA = (map fA l).prod

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ r ^ n ∈ A (n • i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ j ∈ l, r j ∈ A (i j)
⊢ (List.map r l).prod ∈ A (List.map i l).sum

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ (List.ofFn r).prod ∈ A (List.ofFn i).sum

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
⊢ ↑(l.dProd fι fA) = (List.map (fun a ↦ ↑(fA a)) l).prod

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
⊢ ⁅diag2 a ha, SpecialLinearGroup.transvection ⋯ b⁆ = SpecialLinearGroup.transvection ⋯ c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : CommMonoid R
inst✝¹ : AddCommMonoid ι
A : ι → S
inst✝ : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
j : κ
F' : Finset κ
hF2 : j ∉ F'
h3 : (∀ k ∈ F', g k ∈ A (i k)) → ∏ k ∈ F', g k ∈ A (∑ k ∈ F', i k)
hF : ∀ k ∈ insert j F', g k ∈ A (i k)
⊢ g j ∈ A (i j)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c : F
⊢ SpecialLinearGroup.transvection ⋯ c ∈ commutator SL(2, F)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : CommMonoid R
inst✝¹ : AddCommMonoid ι
A : ι → S
inst✝ : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
hF : ∀ k ∈ F, g k ∈ A (i k)
⊢ ∏ k ∈ F, g k ∈ A (∑ k ∈ F, i k)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Associator

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
a b c d : R
⊢ a * associator b c d - associator (a * b) c d + associator a (b * c) d - associator a b (c * d) +
      associator a b c * d =
    0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x y z : Rᵐᵒᵖ
⊢ associator x y z = -op (associator (unop z) (unop y) (unop x))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Associator

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Associator

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Associator

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Associator

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Associator

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Associator

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Associator

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

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c b c' : F
hc : c' = b * (a ^ 2 - 1)
⊢ ⁅diag2 a⁻¹ ⋯, SpecialLinearGroup.transvection ⋯ b⁆ = SpecialLinearGroup.transvection ⋯ c'

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
j : Fin 2
c : F
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ j = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
N₂ : Type u_10
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
ι : Type u_15
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring S₁
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring S₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module S₁ N₂
inst✝³ : Module S₂ N₂
inst✝² : SMulCommClass S₂ S₁ N₂
inst✝¹ : Fintype n
inst✝ : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
f : Matrix n m N₂
x✝² x✝¹ : n → R₁
x✝ : m → R₂
⊢ ∑ i, ∑ j, σ₂ (x✝ j) •> σ₁ ((x✝² + x✝¹) i) •> f i j =
    ∑ i, ∑ j, σ₂ (x✝ j) •> σ₁ (x✝² i) •> f i j + ∑ i, ∑ j, σ₂ (x✝ j) •> σ₁ (x✝¹ i) •> f i j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
j : Fin 2
c : F
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ j = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
N₂ : Type u_10
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
ι : Type u_15
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring S₁
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring S₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module S₁ N₂
inst✝³ : Module S₂ N₂
inst✝² : SMulCommClass S₂ S₁ N₂
inst✝¹ : Fintype n
inst✝ : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
f : Matrix n m N₂
c : R₁
v : n → R₁
w : m → R₂
⊢ ∑ i, ∑ j, σ₂ (w j) •> σ₁ ((c •> v) i) •> f i j = σ₁ c •> ∑ i, ∑ j, σ₂ (w j) •> σ₁ (v i) •> f i j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
N₂ : Type u_10
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
ι : Type u_15
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring S₁
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring S₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module S₁ N₂
inst✝³ : Module S₂ N₂
inst✝² : SMulCommClass S₂ S₁ N₂
inst✝¹ : Fintype n
inst✝ : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
f : Matrix n m N₂
x✝² : n → R₁
x✝¹ x✝ : m → R₂
⊢ ∑ i, ∑ j, σ₂ ((x✝¹ + x✝) j) •> σ₁ (x✝² i) •> f i j =
    ∑ i, ∑ j, σ₂ (x✝¹ j) •> σ₁ (x✝² i) •> f i j + ∑ i, ∑ j, σ₂ (x✝ j) •> σ₁ (x✝² i) •> f i j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
N₂ : Type u_10
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
ι : Type u_15
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring S₁
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring S₂
inst✝⁵ : AddCommMonoid N₂
inst✝⁴ : Module S₁ N₂
inst✝³ : Module S₂ N₂
inst✝² : SMulCommClass S₂ S₁ N₂
inst✝¹ : Fintype n
inst✝ : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
f : Matrix n m N₂
x✝ : R₂
v : n → R₁
w : m → R₂
⊢ ∑ i, ∑ j, σ₂ ((x✝ •> w) j) •> σ₁ (v i) •> f i j = σ₂ x✝ •> ∑ i, ∑ j, σ₂ (w j) •> σ₁ (v i) •> f i j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
i j : Fin 2
h : i ≠ j
c : F
⊢ SpecialLinearGroup.transvection h c ∈ commutator SL(2, F)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹¹ : Semiring R₁
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : Module S₁ N₂
inst✝⁵ : Module S₂ N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
i : n
j : m
⊢ ∑ i', ∑ j', (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j' = f i j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹¹ : Semiring R₁
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : Module S₁ N₂
inst✝⁵ : Module S₂ N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
i : n
j : m
this : ∑ i', ∑ j', (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j' = f i j
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ σ₂ (Pi.single j 1 x✝¹) •> σ₁ (Pi.single i 1 x✝³) •> f x✝³ x✝¹ =
    (if i = x✝³ then 1 else 0) •> (if j = x✝¹ then 1 else 0) •> f x✝³ x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹¹ : Semiring R₁
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : Module S₁ N₂
inst✝⁵ : Module S₂ N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
i : n
j : m
⊢ ((toLinearMap₂'Aux σ₁ σ₂ f) (Pi.single i 1)) (Pi.single j 1) = f i j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ diag2 a ha =
    SpecialLinearGroup.transvection ⋯ a * SpecialLinearGroup.transvection ⋯ (-a⁻¹) *
            SpecialLinearGroup.transvection ⋯ a *
          SpecialLinearGroup.transvection ⋯ (-1) *
        SpecialLinearGroup.transvection ⋯ 1 *
      SpecialLinearGroup.transvection ⋯ (-1)

Tactic:
ext i j
  fin_cases i <;> fin_cases j <;>
  simp [diag2_coe', transvection_coe, mul_add, add_mul, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring S₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring S₂
inst✝¹⁰ : AddCommMonoid N₂
inst✝⁹ : Module R N₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂
⊢ toLinearMap₂'Aux σ₁ σ₂ ((toMatrix₂Aux R (fun i ↦ Pi.single i 1) fun j ↦ Pi.single j 1) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ diag2 a ha =
    SpecialLinearGroup.transvection ⋯ a * SpecialLinearGroup.transvection ⋯ (-a⁻¹) *
            SpecialLinearGroup.transvection ⋯ a *
          SpecialLinearGroup.transvection ⋯ (-1) *
        SpecialLinearGroup.transvection ⋯ 1 *
      SpecialLinearGroup.transvection ⋯ (-1)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring S₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring S₂
inst✝¹⁰ : AddCommMonoid N₂
inst✝⁹ : Module R N₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
⊢ (toMatrix₂Aux R (fun i ↦ Pi.single i 1) fun j ↦ Pi.single j 1) (toLinearMap₂'Aux σ₁ σ₂ f) = f

Tactic:
by

Goal state after:
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)
j : Fin 2
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ j = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid N₂
inst✝¹³ : Module R N₂
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring S₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
M : Matrix n m N₂
x : n → R₁
y : m → R₂
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ σ₂ (y x✝¹) •> σ₁ (x x✝³) •> M x✝³ x✝¹ = σ₁ (x x✝³) •> σ₂ (y x✝¹) •> M x✝³ x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid N₂
inst✝¹³ : Module R N₂
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring S₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
M : Matrix n m N₂
x : n → R₁
y : m → R₂
⊢ (((toLinearMapₛₗ₂' R σ₁ σ₂) M) x) y = ∑ i, ∑ j, σ₁ (x i) •> σ₂ (y j) •> M i j

Tactic:
by

Goal state after:
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)
j : Fin 2
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ j = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
S₁ : Type u_3
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid N₂
inst✝¹¹ : Module R N₂
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring S₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
M : Matrix n m N₂
x : n → S₁
y : m → S₂
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ (RingHom.id S₂) (y x✝¹) •> (RingHom.id S₁) (x x✝³) •> M x✝³ x✝¹ = x x✝³ •> y x✝¹ •> M x✝³ x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
inst✝⁴ : Fintype n
inst✝³ : Fintype m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq m
T : Type u_16
inst✝ : CommSemiring T
M : Matrix n m T
v : n → T
w : m → T
⊢ (((toLinearMap₂' T) M) v) w = v ⬝ᵥ M *ᵥ w

Tactic:
by

Goal state after:
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)
⊢ P A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ⊢ !![0, -1; 1, 0].det = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ⊢ !![1, 1; 0, 1].det = 1

Tactic:
by

Goal state after: