mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
α : Fin (p + 1) → Fin n
i j : Fin n
⊢ (-1) ^ ↑0 * A.submatrix (Fin.cons i α) (Fin.cons j α) 0 0 *
        ((A.submatrix (Fin.cons i α) (Fin.cons j α)).submatrix (Fin.succAbove 0) Fin.succ).det +
      ∑ i_1,
        (-1) ^ ↑i_1.succ * A.submatrix (Fin.cons i α) (Fin.cons j α) i_1.succ 0 *
          ((A.submatrix (Fin.cons i α) (Fin.cons j α)).submatrix i_1.succ.succAbove Fin.succ).det =
    A i j * pminor A α + ∑ s, (-1) ^ (↑s + 1) * A (α s) j * (A.submatrix (Fin.cons i (s.removeNth α)) α).det

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
α : Fin (p + 1) → Fin n
i j : Fin n
⊢ (-1) ^ ↑0 * A.submatrix (Fin.cons i α) (Fin.cons j α) 0 0 *
        ((A.submatrix (Fin.cons i α) (Fin.cons j α)).submatrix (Fin.succAbove 0) Fin.succ).det +
      ∑ i_1,
        (-1) ^ ↑i_1.succ * A.submatrix (Fin.cons i α) (Fin.cons j α) i_1.succ 0 *
          ((A.submatrix (Fin.cons i α) (Fin.cons j α)).submatrix i_1.succ.succAbove Fin.succ).det =
    A i j * pminor A α + ∑ s, (-1) ^ (↑s + 1) * A (α s) j * (A.submatrix (Fin.cons i (s.removeNth α)) α).det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
α : Fin (p + 1) → Fin n
i j : Fin n
⊢ pminor A α * A i j + ∑ x, (-1) ^ (↑x + 1 + ↑x) * bminor A i (α x) (x.removeNth α) * A (α x) j =
    pminor A α * A i j + ∑ s, -(bminor A i (α s) (s.removeNth α) * A (α s) j)

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
α : Fin (p + 1) → Fin n
i j : Fin n
⊢ pminor A α * A i j + ∑ x, (-1) ^ (↑x + 1 + ↑x) * bminor A i (α x) (x.removeNth α) * A (α x) j =
    pminor A α * A i j + ∑ s, -(bminor A i (α s) (s.removeNth α) * A (α s) j)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: n : ℕ
i : Fin n
a✝ : Fin 0 → Fin n
⊢ a✝ ∈ S 0 i ↔ a✝ ∈ {![]}

Tactic:
;

Goal state after:
n : ℕ
i : Fin n
a✝ : Fin 0 → Fin n
⊢ a✝ ∈ S 0 i ↔ a✝ ∈ {![]}
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: p : ℕ
a✝ : Fin p → Fin (p + 1)
⊢ a✝ ∈ S p 0 ↔ a✝ ∈ {Fin.succ}

Tactic:
;

Goal state after:
p : ℕ
a✝ : Fin p → Fin (p + 1)
⊢ a✝ ∈ S p 0 ↔ a✝ ∈ {Fin.succ}
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∀ x ∈ S (p + 1) i, bminor A i j x = pminor A x * A i j - ∑ t, bminor A i (x t) (t.removeNth x) * A (x t) j

Tactic:
simp [det_bordered_expand]

Goal state after:
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ e (((k ∙ z).projectionOnto ↑A ⋯) x) • ⁅z, v⁆ = e (π₂ x) • ↑(((toEnd k L ↥W) z) ⟨v, hv⟩)

Tactic:
;

Goal state after:
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ e (((k ∙ z).projectionOnto ↑A ⋯) x) • ⁅z, v⁆ = e (π₂ x) • ↑(((toEnd k L ↥W) z) ⟨v, hv⟩)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∑ k > i, ∑ α ∈ S p i, bminor A i k α * A k j =
    ∑ α' ∈ S (p + 1) i, ∑ t, bminor A i (α' t) (t.removeNth α') * A (α' t) j

Tactic:
rw [Finset.sum_comm, ← Finset.sum_product', ← Finset.sum_product']

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∑ x ∈ S p i ×ˢ Finset.Ioi i, bminor A i x.2 x.1 * A x.2 j =
    ∑ x ∈ S (p + 1) i ×ˢ Finset.univ, bminor A i (x.1 x.2) (x.2.removeNth x.1) * A (x.1 x.2) j
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ e (π₂ x) • ↑(c • ⟨v, hv⟩) = e (π₂ x) • c • v

Tactic:
;

Goal state after:
k : Type u_1
inst✝¹⁰ : Field k
L : Type u_2
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra k L
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : LieRingModule L V
inst✝⁴ : LieModule k L V
inst✝³ : CharZero k
inst✝² : Module.Finite k V
inst✝¹ : IsTriangularizable k L V
A : LieIdeal k L
hA✝ : IsCoatom ↑A
χ₀ : Module.Dual k ↥A
inst✝ : Nontrivial ↥(weightSpace V ⇑χ₀)
z : L
hz : z ∉ ↑A
e : ↥(k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z ⋯).symm
he : ∀ (x : ↥(k ∙ z)), e x • z = ↑x
hA : IsCompl (↑A) (k ∙ z)
π₁ : L →ₗ[k] ↥A := (↑A).projectionOnto (k ∙ z) hA
π₂ : L →ₗ[k] ↥(k ∙ z) := (k ∙ z).projectionOnto (LieIdeal.toLieSubalgebra k L A).toSubmodule ⋯
W : LieSubmodule k L V := weightSpaceOfIsLieTower k V ⇑χ₀
c : k
hc : ((toEnd k L ↥W) z).HasEigenvalue c
v : V
hv : v ∈ W
hvc : ((toEnd k L ↥W) z).HasEigenvector c ⟨v, hv⟩
hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v
x : L
hπ : ↑(π₁ x) + ↑(π₂ x) = x
⊢ e (π₂ x) • ↑(c • ⟨v, hv⟩) = e (π₂ x) • c • v
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
k : ℕ
A : Matrix (Fin (k + 1)) (Fin (k + 1)) R
this : ∑ α ∈ S k 0, bminor A 0 0 α = A.det
⊢ A.det = (-1) ^ (k + k) * ∑ α ∈ S k 0, bminor A 0 0 α

Tactic:
;

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
k : ℕ
A : Matrix (Fin (k + 1)) (Fin (k + 1)) R
this : ∑ α ∈ S k 0, bminor A 0 0 α = A.det
⊢ A.det = (-1) ^ (k + k) * ∑ α ∈ S k 0, bminor A 0 0 α
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A₁
inst✝¹⁶ : LieRing L₁
inst✝¹⁵ : Module A₁ L₁
inst✝¹⁴ : LieRingModule L₁ A₁
inst✝¹³ : CommRing A₂
inst✝¹² : LieRing L₂
inst✝¹¹ : Module A₂ L₂
inst✝¹⁰ : LieRingModule L₂ A₂
inst✝⁹ : CommRing A₃
inst✝⁸ : LieRing L₃
inst✝⁷ : Module A₃ L₃
inst✝⁶ : LieRingModule L₃ A₃
inst✝⁵ : Algebra R A₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : Algebra R A₂
inst✝² : LieAlgebra R L₂
inst✝¹ : Algebra R A₃
inst✝ : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x✝² : Derivation R A₁ A₁
x✝¹ x✝ : A₁
⊢ x✝ * x✝² x✝¹ = x✝² x✝¹ * x✝

Tactic:
;

Goal state after:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A₁
inst✝¹⁶ : LieRing L₁
inst✝¹⁵ : Module A₁ L₁
inst✝¹⁴ : LieRingModule L₁ A₁
inst✝¹³ : CommRing A₂
inst✝¹² : LieRing L₂
inst✝¹¹ : Module A₂ L₂
inst✝¹⁰ : LieRingModule L₂ A₂
inst✝⁹ : CommRing A₃
inst✝⁸ : LieRing L₃
inst✝⁷ : Module A₃ L₃
inst✝⁶ : LieRingModule L₃ A₃
inst✝⁵ : Algebra R A₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : Algebra R A₂
inst✝² : LieAlgebra R L₂
inst✝¹ : Algebra R A₃
inst✝ : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x✝² : Derivation R A₁ A₁
x✝¹ x✝ : A₁
⊢ x✝ * x✝² x✝¹ = x✝² x✝¹ * x✝
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A₁
inst✝¹⁶ : LieRing L₁
inst✝¹⁵ : Module A₁ L₁
inst✝¹⁴ : LieRingModule L₁ A₁
inst✝¹³ : CommRing A₂
inst✝¹² : LieRing L₂
inst✝¹¹ : Module A₂ L₂
inst✝¹⁰ : LieRingModule L₂ A₂
inst✝⁹ : CommRing A₃
inst✝⁸ : LieRing L₃
inst✝⁷ : Module A₃ L₃
inst✝⁶ : LieRingModule L₃ A₃
inst✝⁵ : Algebra R A₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : Algebra R A₂
inst✝² : LieAlgebra R L₂
inst✝¹ : Algebra R A₃
inst✝ : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x✝² x✝¹ : Derivation R A₁ A₁
x✝ a✝ : A₁
⊢ ⁅x✝², x✝ • x✝¹⁆ a✝ = (x✝ • ⁅x✝², x✝¹⁆ + ⁅x✝², x✝⁆ • x✝¹) a✝

Tactic:
;

Goal state after:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A₁
inst✝¹⁶ : LieRing L₁
inst✝¹⁵ : Module A₁ L₁
inst✝¹⁴ : LieRingModule L₁ A₁
inst✝¹³ : CommRing A₂
inst✝¹² : LieRing L₂
inst✝¹¹ : Module A₂ L₂
inst✝¹⁰ : LieRingModule L₂ A₂
inst✝⁹ : CommRing A₃
inst✝⁸ : LieRing L₃
inst✝⁷ : Module A₃ L₃
inst✝⁶ : LieRingModule L₃ A₃
inst✝⁵ : Algebra R A₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : Algebra R A₂
inst✝² : LieAlgebra R L₂
inst✝¹ : Algebra R A₃
inst✝ : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x✝² x✝¹ : Derivation R A₁ A₁
x✝ a✝ : A₁
⊢ ⁅x✝², x✝ • x✝¹⁆ a✝ = (x✝ • ⁅x✝², x✝¹⁆ + ⁅x✝², x✝⁆ • x✝¹) a✝
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A₁
inst✝¹⁶ : LieRing L₁
inst✝¹⁵ : Module A₁ L₁
inst✝¹⁴ : LieRingModule L₁ A₁
inst✝¹³ : CommRing A₂
inst✝¹² : LieRing L₂
inst✝¹¹ : Module A₂ L₂
inst✝¹⁰ : LieRingModule L₂ A₂
inst✝⁹ : CommRing A₃
inst✝⁸ : LieRing L₃
inst✝⁷ : Module A₃ L₃
inst✝⁶ : LieRingModule L₃ A₃
inst✝⁵ : Algebra R A₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : Algebra R A₂
inst✝² : LieAlgebra R L₂
inst✝¹ : Algebra R A₃
inst✝ : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x✝² x✝¹ : Derivation R A₁ A₁
x✝ a✝ : A₁
⊢ x✝ * x✝² (x✝¹ a✝) + x✝¹ a✝ * x✝² x✝ - x✝ * x✝¹ (x✝² a✝) = x✝ * (x✝² (x✝¹ a✝) - x✝¹ (x✝² a✝)) + x✝² x✝ * x✝¹ a✝

Tactic:
;

Goal state after:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing A₁
inst✝¹⁶ : LieRing L₁
inst✝¹⁵ : Module A₁ L₁
inst✝¹⁴ : LieRingModule L₁ A₁
inst✝¹³ : CommRing A₂
inst✝¹² : LieRing L₂
inst✝¹¹ : Module A₂ L₂
inst✝¹⁰ : LieRingModule L₂ A₂
inst✝⁹ : CommRing A₃
inst✝⁸ : LieRing L₃
inst✝⁷ : Module A₃ L₃
inst✝⁶ : LieRingModule L₃ A₃
inst✝⁵ : Algebra R A₁
inst✝⁴ : LieAlgebra R L₁
inst✝³ : Algebra R A₂
inst✝² : LieAlgebra R L₂
inst✝¹ : Algebra R A₃
inst✝ : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x✝² x✝¹ : Derivation R A₁ A₁
x✝ a✝ : A₁
⊢ x✝ * x✝² (x✝¹ a✝) + x✝¹ a✝ * x✝² x✝ - x✝ * x✝¹ (x✝² a✝) = x✝ * (x✝² (x✝¹ a✝) - x✝¹ (x✝² a✝)) + x✝² x✝ * x✝¹ a✝
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ x✝ : L₁
a✝ : A₁
⊢ (Derivation.mk' ((LieModule.toEnd R L₁ A₁) (x✝¹ + x✝)) ⋯) a✝ =
    (Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝¹) ⋯ + Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝) ⋯) a✝

Tactic:
;

Goal state after:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ x✝ : L₁
a✝ : A₁
⊢ (Derivation.mk' ((LieModule.toEnd R L₁ A₁) (x✝¹ + x✝)) ⋯) a✝ =
    (Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝¹) ⋯ + Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝) ⋯) a✝
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ : R
x✝ : L₁
a✝ : A₁
⊢ (Derivation.mk' ((LieModule.toEnd R L₁ A₁) (x✝¹ • x✝)) ⋯) a✝ =
    ((RingHom.id R) x✝¹ • Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝) ⋯) a✝

Tactic:
;

Goal state after:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ : R
x✝ : L₁
a✝ : A₁
⊢ (Derivation.mk' ((LieModule.toEnd R L₁ A₁) (x✝¹ • x✝)) ⋯) a✝ =
    ((RingHom.id R) x✝¹ • Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝) ⋯) a✝
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ x✝ : L₁
a✝ : A₁
⊢ (Derivation.mk' ((LieModule.toEnd R L₁ A₁) ⁅x✝¹, x✝⁆) ⋯) a✝ =
    ⁅Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝¹) ⋯, Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝) ⋯⁆ a✝

Tactic:
;

Goal state after:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ x✝ : L₁
a✝ : A₁
⊢ (Derivation.mk' ((LieModule.toEnd R L₁ A₁) ⁅x✝¹, x✝⁆) ⋯) a✝ =
    ⁅Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝¹) ⋯, Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝) ⋯⁆ a✝
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ : A₁
x✝ : L₁
a✝ : A₁
⊢ ({ toFun := fun x ↦ Derivation.mk' ((LieModule.toEnd R L₁ A₁) x) ⋯, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }
        (x✝¹ • x✝))
      a✝ =
    ((AlgHom.id R A₁) x✝¹ •
        { toFun := fun x ↦ Derivation.mk' ((LieModule.toEnd R L₁ A₁) x) ⋯, map_add' := ⋯, map_smul' := ⋯,
            map_lie' := ⋯ }
          x✝)
      a✝

Tactic:
;

Goal state after:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ : A₁
x✝ : L₁
a✝ : A₁
⊢ ({ toFun := fun x ↦ Derivation.mk' ((LieModule.toEnd R L₁ A₁) x) ⋯, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }
        (x✝¹ • x✝))
      a✝ =
    ((AlgHom.id R A₁) x✝¹ •
        { toFun := fun x ↦ Derivation.mk' ((LieModule.toEnd R L₁ A₁) x) ⋯, map_add' := ⋯, map_smul' := ⋯,
            map_lie' := ⋯ }
          x✝)
      a✝
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
x✝ : Fin n
⊢ (A n).diag x✝ = 2 x✝

Tactic:
;

Goal state after:
n : ℕ
x✝ : Fin n
⊢ (A n).diag x✝ = 2 x✝
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
i j : Fin n
h : i ≠ j
⊢ (if i = j then 2 else if ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i then -1 else 0) ≤ 0

Tactic:
;

Goal state after:
n : ℕ
i j : Fin n
h : i ≠ j
⊢ (if i = j then 2 else if ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i then -1 else 0) ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
i j : Fin n
h : i ≠ j
⊢ (if i = j then 2 else if ↑i + 1 = ↑j then if ↑j = n - 1 then -2 else -1 else if ↑j + 1 = ↑i then -1 else 0) ≤ 0

Tactic:
;

Goal state after:
n : ℕ
i j : Fin n
h : i ≠ j
⊢ (if i = j then 2 else if ↑i + 1 = ↑j then if ↑j = n - 1 then -2 else -1 else if ↑j + 1 = ↑i then -1 else 0) ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
i j : Fin n
h : i ≠ j
⊢ (if i = j then 2 else if ↑i + 1 = ↑j then -1 else if ↑j + 1 = ↑i then if ↑i = n - 1 then -2 else -1 else 0) ≤ 0

Tactic:
;

Goal state after:
n : ℕ
i j : Fin n
h : i ≠ j
⊢ (if i = j then 2 else if ↑i + 1 = ↑j then -1 else if ↑j + 1 = ↑i then if ↑i = n - 1 then -2 else -1 else 0) ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
i j : Fin n
h : i ≠ j
⊢ (if i = j then 2
    else
      if n ≤ 2 then 0
      else
        if ↑i + 1 = ↑j ∧ ↑j + 2 < n then -1
        else
          if ↑j + 1 = ↑i ∧ ↑i + 2 < n then -1
          else
            if ↑i + 3 = n ∧ (↑j + 2 = n ∨ ↑j + 1 = n) then -1
            else if ↑j + 3 = n ∧ (↑i + 2 = n ∨ ↑i + 1 = n) then -1 else 0) ≤
    0

Tactic:
;

Goal state after:
n : ℕ
i j : Fin n
h : i ≠ j
⊢ (if i = j then 2
    else
      if n ≤ 2 then 0
      else
        if ↑i + 1 = ↑j ∧ ↑j + 2 < n then -1
        else
          if ↑j + 1 = ↑i ∧ ↑i + 2 < n then -1
          else
            if ↑i + 3 = n ∧ (↑j + 2 = n ∨ ↑j + 1 = n) then -1
            else if ↑j + 3 = n ∧ (↑i + 2 = n ∨ ↑i + 1 = n) then -1 else 0) ≤
    0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
i✝ j✝ : Fin n
⊢ (A n)ᵀ i✝ j✝ = A n i✝ j✝

Tactic:
;

Goal state after:
n : ℕ
i✝ j✝ : Fin n
⊢ (A n)ᵀ i✝ j✝ = A n i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
i✝ j✝ : Fin n
⊢ (if j✝ = i✝ then 2 else if ↑j✝ + 1 = ↑i✝ ∨ ↑i✝ + 1 = ↑j✝ then -1 else 0) =
    if i✝ = j✝ then 2 else if ↑i✝ + 1 = ↑j✝ ∨ ↑j✝ + 1 = ↑i✝ then -1 else 0

Tactic:
;

Goal state after:
n : ℕ
i✝ j✝ : Fin n
⊢ (if j✝ = i✝ then 2 else if ↑j✝ + 1 = ↑i✝ ∨ ↑i✝ + 1 = ↑j✝ then -1 else 0) =
    if i✝ = j✝ then 2 else if ↑i✝ + 1 = ↑j✝ ∨ ↑j✝ + 1 = ↑i✝ then -1 else 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
i✝ j✝ : Fin n
⊢ (B n)ᵀ i✝ j✝ = C n i✝ j✝

Tactic:
;

Goal state after:
n : ℕ
i✝ j✝ : Fin n
⊢ (B n)ᵀ i✝ j✝ = C n i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
i✝ j✝ : Fin n
⊢ (if j✝ = i✝ then 2 else if ↑j✝ + 1 = ↑i✝ then if ↑i✝ = n - 1 then -2 else -1 else if ↑i✝ + 1 = ↑j✝ then -1 else 0) =
    if i✝ = j✝ then 2 else if ↑i✝ + 1 = ↑j✝ then -1 else if ↑j✝ + 1 = ↑i✝ then if ↑i✝ = n - 1 then -2 else -1 else 0

Tactic:
;

Goal state after:
n : ℕ
i✝ j✝ : Fin n
⊢ (if j✝ = i✝ then 2 else if ↑j✝ + 1 = ↑i✝ then if ↑i✝ = n - 1 then -2 else -1 else if ↑i✝ + 1 = ↑j✝ then -1 else 0) =
    if i✝ = j✝ then 2 else if ↑i✝ + 1 = ↑j✝ then -1 else if ↑j✝ + 1 = ↑i✝ then if ↑i✝ = n - 1 then -2 else -1 else 0
Module: Mathlib.LinearAlgebra.Matrix.Cartan

Goal state before:
pp: n : ℕ
i✝ j✝ : Fin n
⊢ (D n)ᵀ i✝ j✝ = D n i✝ j✝

Tactic:
;

Goal state after:
n : ℕ
i✝ j✝ : Fin n
⊢ (D n)ᵀ i✝ j✝ = D n i✝ j✝