mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ GradedMonoid.GOne.one = 1

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ GradedMonoid.GOne.one = 1
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
head : α
tail : List α
⊢ GradedMonoid.GMul.mul (fA head) (map fA tail).prod = fA head * (map fA tail).prod

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
head : α
tail : List α
⊢ GradedMonoid.GMul.mul (fA head) (map fA tail).prod = fA head * (map fA tail).prod
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
⊢ 1 ∈ A 0

Tactic:
]

Goal state after:
ι : 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
⊢ 1 ∈ A 0
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 * diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b) =
    SpecialLinearGroup.transvection ⋯ c

Tactic:
]

Goal state after:
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 * diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b) =
    SpecialLinearGroup.transvection ⋯ c
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
n : ℕ
⊢ r * r ^ n ∈ A (i + n • i)

Tactic:
]

Goal state after:
ι : 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
n : ℕ
⊢ r * r ^ n ∈ A (i + n • i)
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 ∈ [], r j ∈ A (i j)
⊢ 1 ∈ A 0

Tactic:
]

Goal state after:
ι : 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 ∈ [], r j ∈ A (i j)
⊢ 1 ∈ A 0
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
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
⊢ r head * (List.map r tail).prod ∈ A (i head + (List.map i tail).sum)

Tactic:
]

Goal state after:
ι : 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
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
⊢ r head * (List.map r tail).prod ∈ A (i head + (List.map i tail).sum)
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.map r (List.finRange n)).prod ∈ A (List.map i (List.finRange n)).sum

Tactic:
]

Goal state after:
ι : 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.map r (List.finRange n)).prod ∈ A (List.map i (List.finRange n)).sum
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 α
⊢ 1 = 1

Tactic:
]

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 α
head : α
tail : List α
⊢ ↑(fA head) * (List.map (fun a ↦ ↑(fA a)) tail).prod = ↑(fA head) * (List.map (fun a ↦ ↑(fA a)) tail).prod

Tactic:
]

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 * ∏ x ∈ F', g x ∈ A (i j + ∑ x ∈ F', i x)

Tactic:
]

Goal state after:
ι : 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 * ∏ x ∈ F', g x ∈ A (i j + ∑ x ∈ F', i x)
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
⊢ ⁅diag2 a ha, SpecialLinearGroup.transvection ⋯ (c / (a ^ 2 - 1))⁆ ∈ commutator SL(2, F)

Tactic:
]

Goal state after:
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c : F
⊢ ⁅diag2 a ha, SpecialLinearGroup.transvection ⋯ (c / (a ^ 2 - 1))⁆ ∈ commutator SL(2, F)
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 * diag2 a⁻¹⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b) =
    SpecialLinearGroup.transvection ⋯ c'

Tactic:
]

Goal state after:
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 * diag2 a⁻¹⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b) =
    SpecialLinearGroup.transvection ⋯ c'
Module: Mathlib.Algebra.Ring.Associator

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

Tactic:
]

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
this :
  ∀ (b c' : F),
    c' = b * (a ^ 2 - 1) → ⁅diag2 a⁻¹ ⋯, SpecialLinearGroup.transvection ⋯ b⁆ = SpecialLinearGroup.transvection ⋯ c'
⊢ ⁅diag2 a⁻¹ ⋯, SpecialLinearGroup.transvection ⋯ (c / (a ^ 2 - 1))⁆ ∈ commutator SL(2, F)

Tactic:
]

Goal state after:
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
hasq : a ^ 2 ≠ 1
c : F
this :
  ∀ (b c' : F),
    c' = b * (a ^ 2 - 1) → ⁅diag2 a⁻¹ ⋯, SpecialLinearGroup.transvection ⋯ b⁆ = SpecialLinearGroup.transvection ⋯ c'
⊢ ⁅diag2 a⁻¹ ⋯, SpecialLinearGroup.transvection ⋯ (c / (a ^ 2 - 1))⁆ ∈ commutator SL(2, F)
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_1, ∑ j_1, σ₂ (Pi.single j 1 j_1) •> σ₁ (Pi.single i 1 i_1) •> f i_1 j_1 = f i j

Tactic:
]

Goal state after:
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_1, ∑ j_1, σ₂ (Pi.single j 1 j_1) •> σ₁ (Pi.single i 1 i_1) •> f i_1 j_1 = f i j
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
⊢ ∑ i_1, ∑ j_1, σ₂ (Pi.single j 1 j_1) •> σ₁ (Pi.single i 1 i_1) •> f i_1 j_1 =
    ∑ i', ∑ j', (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j'

Tactic:
]

Goal state after:
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
⊢ ∑ i_1, ∑ j_1, σ₂ (Pi.single j 1 j_1) •> σ₁ (Pi.single i 1 i_1) •> f i_1 j_1 =
    ∑ i', ∑ j', (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j'
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «0»
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) ⟨0, ⋯⟩ ≠ 1
⊢ P
    (SpecialLinearGroup.transvection ⋯ c * SpecialLinearGroup.transvection ⋯ (-c⁻¹) *
            SpecialLinearGroup.transvection ⋯ c *
          SpecialLinearGroup.transvection ⋯ (-1) *
        SpecialLinearGroup.transvection ⋯ 1 *
      SpecialLinearGroup.transvection ⋯ (-1))

Tactic:
]

Goal state after:
case «0»
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) ⟨0, ⋯⟩ ≠ 1
⊢ P
    (SpecialLinearGroup.transvection ⋯ c * SpecialLinearGroup.transvection ⋯ (-c⁻¹) *
            SpecialLinearGroup.transvection ⋯ c *
          SpecialLinearGroup.transvection ⋯ (-1) *
        SpecialLinearGroup.transvection ⋯ 1 *
      SpecialLinearGroup.transvection ⋯ (-1))
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₂
⊢ ∑ i, ∑ j, σ₂ (y j) •> σ₁ (x i) •> M i j = ∑ i, ∑ j, σ₁ (x i) •> σ₂ (y j) •> M i j

Tactic:
]

Goal state after:
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₂
⊢ ∑ i, ∑ j, σ₂ (y j) •> σ₁ (x i) •> M i j = ∑ i, ∑ j, σ₁ (x i) •> σ₂ (y j) •> M i j
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
⊢ σ₁ (x x✝³) •> σ₂ (y x✝¹) •> M x✝³ x✝¹ = σ₁ (x x✝³) •> σ₂ (y x✝¹) •> M x✝³ x✝¹

Tactic:
]

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
⊢ x x✝³ •> y x✝¹ •> M x✝³ x✝¹ = x x✝³ •> y x✝¹ •> M x✝³ x✝¹

Tactic:
]

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:
Matrix.toLinearMap₂'_apply,

Goal state after:
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
⊢ ∑ i, ∑ j, v i •> w j •> M i j = v ⬝ᵥ M *ᵥ w
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
x✝¹ : n
x✝ : x✝¹ ∈ univ
⊢ ∑ j, v x✝¹ •> w j •> M x✝¹ j = ∑ i, v x✝¹ * (M x✝¹ i * w i)

Tactic:
]

Goal state after:
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
x✝¹ : n
x✝ : x✝¹ ∈ univ
⊢ ∑ j, v x✝¹ •> w j •> M x✝¹ j = ∑ i, v x✝¹ * (M x✝¹ i * w i)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «1»
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
⊢ P
    (SpecialLinearGroup.transvection ⋯ c⁻¹ * SpecialLinearGroup.transvection ⋯ (-c⁻¹⁻¹) *
            SpecialLinearGroup.transvection ⋯ c⁻¹ *
          SpecialLinearGroup.transvection ⋯ (-1) *
        SpecialLinearGroup.transvection ⋯ 1 *
      SpecialLinearGroup.transvection ⋯ (-1))

Tactic:
]

Goal state after:
case «1»
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
⊢ P
    (SpecialLinearGroup.transvection ⋯ c⁻¹ * SpecialLinearGroup.transvection ⋯ (-c⁻¹⁻¹) *
            SpecialLinearGroup.transvection ⋯ c⁻¹ *
          SpecialLinearGroup.transvection ⋯ (-1) *
        SpecialLinearGroup.transvection ⋯ 1 *
      SpecialLinearGroup.transvection ⋯ (-1))
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
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ v x✝³ * M x✝³ x✝¹ * w x✝¹ = v x✝³ * M x✝³ x✝¹ * w x✝¹

Tactic:
]

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

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ (B (l (Pi.single i 1))) (r (Pi.single j 1)) =
    ∑ y,
      ∑ x,
        of (fun i j ↦ l (Pi.single j 1) i) y i * (B (Pi.single y 1)) (Pi.single x 1) *
          of (fun i j ↦ r (Pi.single j 1) i) x j

Tactic:
]

Goal state after:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ (B (l (Pi.single i 1))) (r (Pi.single j 1)) =
    ∑ y,
      ∑ x,
        of (fun i j ↦ l (Pi.single j 1) i) y i * (B (Pi.single y 1)) (Pi.single x 1) *
          of (fun i j ↦ r (Pi.single j 1) i) x j
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ (∑ i_1,
      ((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj ↦
        ((Pi.basisFun R n).repr (l (Pi.single i 1))) i_1 •> yj •> (B ((Pi.basisFun R n) i_1)) ((Pi.basisFun R m) j)) =
    ∑ y,
      ∑ x,
        of (fun i j ↦ l (Pi.single j 1) i) y i * (B (Pi.single y 1)) (Pi.single x 1) *
          of (fun i j ↦ r (Pi.single j 1) i) x j

pp: case h
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ ∀ (i : n),
    (((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj ↦
        0 •> yj •> (B ((Pi.basisFun R n) i)) ((Pi.basisFun R m) j)) =
      0

Tactic:
]

Goal state after:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ (∑ i_1,
      ((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj ↦
        ((Pi.basisFun R n).repr (l (Pi.single i 1))) i_1 •> yj •> (B ((Pi.basisFun R n) i_1)) ((Pi.basisFun R m) j)) =
    ∑ y,
      ∑ x,
        of (fun i j ↦ l (Pi.single j 1) i) y i * (B (Pi.single y 1)) (Pi.single x 1) *
          of (fun i j ↦ r (Pi.single j 1) i) x j

case h
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
⊢ ∀ (i : n),
    (((Pi.basisFun R m).repr (r (Pi.single j 1))).sum fun j yj ↦
        0 •> yj •> (B ((Pi.basisFun R n) i)) ((Pi.basisFun R m) j)) =
      0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case zero
⊢ !![1, 0; 0, 1] = !![1, 0; 0, 1]

Tactic:
]

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

Goal state before:
pp: n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ ∑ i_1,
      ((Pi.basisFun R n).repr (l (Pi.single i 1))) i' •>
        ((Pi.basisFun R m).repr (r (Pi.single j 1))) i_1 •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) i_1) =
    ∑ x,
      of (fun i j ↦ l (Pi.single j 1) i) i' i * (B (Pi.single i' 1)) (Pi.single x 1) *
        of (fun i j ↦ r (Pi.single j 1) i) x j

pp: case h
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ ∀ (i_1 : m),
    ((Pi.basisFun R n).repr (l (Pi.single i 1))) i' •> 0 •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) i_1) = 0

Tactic:
]

Goal state after:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ ∑ i_1,
      ((Pi.basisFun R n).repr (l (Pi.single i 1))) i' •>
        ((Pi.basisFun R m).repr (r (Pi.single j 1))) i_1 •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) i_1) =
    ∑ x,
      of (fun i j ↦ l (Pi.single j 1) i) i' i * (B (Pi.single i' 1)) (Pi.single x 1) *
        of (fun i j ↦ r (Pi.single j 1) i) x j

case h
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
i' : n
⊢ ∀ (i_1 : m),
    ((Pi.basisFun R n).repr (l (Pi.single i 1))) i' •> 0 •> (B ((Pi.basisFun R n) i')) ((Pi.basisFun R m) i_1) = 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case succ
n : ℕ
h : ↑(T ^ ↑n) = !![1, ↑n; 0, 1]
⊢ ↑n + 1 = ↑n + 1

Tactic:
]

Goal state after: