awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J A B : Matrix n n R
hA : Membership.mem (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule J) A
hB : Membership.mem (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule J) B
simp : ∀ (hA : J.IsSkewAdjoint A) (hB : J.IsSkewAdjoint B), J.IsSkewAdjoint ⁅A, B⁆
⊢ Membership.mem (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule J) ⁅A, B⁆

Tactic:
simp only [mem_skewAdjointMatricesSubmodule] at *

Premises used: mem_skewAdjointMatricesSubmodule
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J A B : Matrix n n R
hA : J.IsSkewAdjoint A
hB : J.IsSkewAdjoint B
change : ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆
⊢ J.IsSkewAdjoint ⁅A, B⁆

Tactic:
change ⁅A, B⁆ᵀ * J = J * (-⁅A, B⁆)

Premises used: Bracket.bracket, Neg.neg
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J A B : Matrix n n R
hA : J.IsSkewAdjoint A
hB : J.IsSkewAdjoint B
⊢ Aᵀ * J = J * -A

Tactic:
change Aᵀ * J = J * (-A) at hA

Premises used: Neg.neg
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J A B : Matrix n n R
hB : J.IsSkewAdjoint B
hA : Aᵀ * J = J * -A
⊢ Bᵀ * J = J * -B

Tactic:
change Bᵀ * J = J * (-B) at hB

Premises used: Neg.neg
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
rw : J * -B * -A - J * -A * -B = J * -(A * B - B * A)
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆

Tactic:
rw [Matrix.lie_transpose, LieRing.of_associative_ring_bracket,
    LieRing.of_associative_ring_bracket, sub_mul, mul_assoc, mul_assoc, hA, hB, ← mul_assoc,
    ← mul_assoc, hA, hB]

Premises used: mul_assoc, LieRing.of_associative_ring_bracket, sub_mul, Matrix.lie_transpose
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
noncomm_ring noncomm_ring₁ noncomm_ring₂ noncomm_ring₃ :
  - -(J * (B * A)) + - - -(J * (A * B)) = -(J * (A * B) + -(J * (B * A)))
⊢ J * -B * -A - J * -A * -B = J * -(A * B - B * A)

Tactic:
noncomm_ring
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J A : Matrix n n R
⊢ Membership.mem (γ := LieSubalgebra R (Matrix n n R)) (skewAdjointMatricesLieSubalgebra J) A ↔
    Membership.mem (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule J) A

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J P : Matrix n n R
h : Invertible P
h₁ :
  ∀ (A : Matrix n n R),
    A ∈ LieSubalgebra.map (P.lieConj h).symm.toLieHom (skewAdjointMatricesLieSubalgebra J) ↔
      Membership.mem (γ := LieSubalgebra R (Matrix n n R)) (skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)) A
⊢ LieSubalgebra.map (P.lieConj h).symm.toLieHom (skewAdjointMatricesLieSubalgebra J) =
    skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)

Tactic:
ext A
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J P : Matrix n n R
h : Invertible P
A : Matrix n n R
this :
  Membership.mem (α := Matrix n n R) (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule J)
      ((P.lieConj h : (a : Matrix n n R) → Matrix n n R) A : Matrix n n R) ↔
    Membership.mem (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule (Pᵀ * J * P)) A
simp :
  Membership.mem (α := Matrix n n R) (γ := Submodule R (Matrix n n R))
      (LieSubalgebra.toSubmodule (skewAdjointMatricesLieSubalgebra J))
      (((P.lieConj h).symm.toLinearEquiv.symm : (a : Matrix n n R) → Matrix n n R) A : Matrix n n R) ↔
    Membership.mem (γ := LieSubalgebra R (Matrix n n R)) (skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)) A
⊢ A ∈ LieSubalgebra.map (P.lieConj h).symm.toLieHom (skewAdjointMatricesLieSubalgebra J) ↔
    Membership.mem (γ := LieSubalgebra R (Matrix n n R)) (skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)) A

Tactic:
simp only [Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule]

Premises used: LieSubalgebra.mem_map_submodule, Submodule.mem_map_equiv
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J P : Matrix n n R
h : Invertible P
A : Matrix n n R
this :
  Membership.mem (α := Matrix n n R) (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule J)
      ((P.lieConj h : (a : Matrix n n R) → Matrix n n R) A : Matrix n n R) ↔
    Membership.mem (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule (Pᵀ * J * P)) A
⊢ Membership.mem (α := Matrix n n R) (γ := Submodule R (Matrix n n R))
      (LieSubalgebra.toSubmodule (skewAdjointMatricesLieSubalgebra J))
      (((P.lieConj h).symm.toLinearEquiv.symm : (a : Matrix n n R) → Matrix n n R) A : Matrix n n R) ↔
    Membership.mem (γ := LieSubalgebra R (Matrix n n R)) (skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)) A

Tactic:
this

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Set.Mem, Matrix.mulVec, Finset.sum
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J P : Matrix n n R
h : Invertible P
A : Matrix n n R
this :
  Membership.mem (α := Matrix n n R) (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule J)
      ((P.lieConj h : (a : Matrix n n R) → Matrix n n R) A : Matrix n n R) ↔
    Membership.mem (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule (Pᵀ * J * P)) A
⊢ Membership.mem (α := Matrix n n R) (γ := Submodule R (Matrix n n R))
      (LieSubalgebra.toSubmodule (skewAdjointMatricesLieSubalgebra J))
      (((P.lieConj h).symm.toLinearEquiv.symm : (a : Matrix n n R) → Matrix n n R) A : Matrix n n R) ↔
    Membership.mem (γ := LieSubalgebra R (Matrix n n R)) (skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)) A

Tactic:
exact this
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J P : Matrix n n R
h : Invertible P
A : Matrix n n R
h₁ :
  Membership.mem (α := Matrix n n R) (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule J)
      ((P.lieConj h : (a : Matrix n n R) → Matrix n n R) A : Matrix n n R) ↔
    Membership.mem (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule (Pᵀ * J * P)) A
⊢ A ∈ LieSubalgebra.map (P.lieConj h).symm.toLieHom (skewAdjointMatricesLieSubalgebra J) ↔
    Membership.mem (γ := LieSubalgebra R (Matrix n n R)) (skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)) A

Tactic:
suffices P.lieConj h A ∈ skewAdjointMatricesSubmodule J ↔
        A ∈ skewAdjointMatricesSubmodule (Pᵀ * J * P) by
      simp only [Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule]
      exact this
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J P : Matrix n n R
h : Invertible P
A : Matrix n n R
⊢ Membership.mem (α := Matrix n n R) (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule J)
      ((P.lieConj h : (a : Matrix n n R) → Matrix n n R) A : Matrix n n R) ↔
    Membership.mem (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule (Pᵀ * J * P)) A

Tactic:
simp [Matrix.IsSkewAdjoint, J.isAdjointPair_equiv _ _ P (isUnit_of_invertible P)]

Premises used: isUnit_of_invertible, Matrix.isAdjointPair_equiv, Matrix.IsSkewAdjoint
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J P : Matrix n n R
h : Invertible P
A : ↥(skewAdjointMatricesLieSubalgebra J)
⊢ (↑((skewAdjointMatricesLieSubalgebraEquiv J P h :
            (a : ↥(skewAdjointMatricesLieSubalgebra J)) → ↥(skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)))
          A) :
      Matrix n n R) =
    P⁻¹ * (↑A : Matrix n n R) * P

Tactic:
simp [skewAdjointMatricesLieSubalgebraEquiv]

Premises used: skewAdjointMatricesLieSubalgebraEquiv
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J : Matrix n n R
m : Type w
inst_3 : DecidableEq m
inst_4 : Fintype m
e : Matrix n n R ≃ₐ[R] Matrix m m R
h :
  ∀ (A : Matrix n n R),
    Eq (α := Matrix m m R) ((e : (a : Matrix n n R) → Matrix m m R) A)ᵀ ((e : (a : Matrix n n R) → Matrix m m R) Aᵀ)
h₁ :
  ∀ (A : Matrix m m R),
    Membership.mem (γ := LieSubalgebra R (Matrix m m R))
        (LieSubalgebra.map (LieEquiv.toLieHom e.toLieEquiv) (skewAdjointMatricesLieSubalgebra J)) A ↔
      Membership.mem (γ := LieSubalgebra R (Matrix m m R))
        (skewAdjointMatricesLieSubalgebra ((e : (a : Matrix n n R) → Matrix m m R) J)) A
⊢ Eq (α := LieSubalgebra R (Matrix m m R))
    (LieSubalgebra.map (LieEquiv.toLieHom e.toLieEquiv) (skewAdjointMatricesLieSubalgebra J))
    (skewAdjointMatricesLieSubalgebra ((e : (a : Matrix n n R) → Matrix m m R) J))

Tactic:
ext A
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J : Matrix n n R
m : Type w
inst_3 : DecidableEq m
inst_4 : Fintype m
e : Matrix n n R ≃ₐ[R] Matrix m m R
h :
  ∀ (A : Matrix n n R),
    Eq (α := Matrix m m R) ((e : (a : Matrix n n R) → Matrix m m R) A)ᵀ ((e : (a : Matrix n n R) → Matrix m m R) Aᵀ)
A : Matrix m m R
this :
  J.IsSkewAdjoint ((e.symm : (a : Matrix m m R) → Matrix n n R) A) ↔
    Matrix.IsSkewAdjoint ((e : (a : Matrix n n R) → Matrix m m R) J) A
⊢ Membership.mem (γ := LieSubalgebra R (Matrix m m R))
      (LieSubalgebra.map (LieEquiv.toLieHom e.toLieEquiv) (skewAdjointMatricesLieSubalgebra J)) A ↔
    Membership.mem (γ := LieSubalgebra R (Matrix m m R))
      (skewAdjointMatricesLieSubalgebra ((e : (a : Matrix n n R) → Matrix m m R) J)) A

Tactic:
simpa [-LieSubalgebra.mem_map, LieSubalgebra.mem_map_submodule]

Premises used: LieSubalgebra.mem_map_submodule, LieSubalgebra.mem_map
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J : Matrix n n R
m : Type w
inst_3 : DecidableEq m
inst_4 : Fintype m
e : Matrix n n R ≃ₐ[R] Matrix m m R
h :
  ∀ (A : Matrix n n R),
    Eq (α := Matrix m m R) ((e : (a : Matrix n n R) → Matrix m m R) A)ᵀ ((e : (a : Matrix n n R) → Matrix m m R) Aᵀ)
A : Matrix m m R
h₁ :
  J.IsSkewAdjoint ((e.symm : (a : Matrix m m R) → Matrix n n R) A) ↔
    Matrix.IsSkewAdjoint ((e : (a : Matrix n n R) → Matrix m m R) J) A
⊢ Membership.mem (γ := LieSubalgebra R (Matrix m m R))
      (LieSubalgebra.map (LieEquiv.toLieHom e.toLieEquiv) (skewAdjointMatricesLieSubalgebra J)) A ↔
    Membership.mem (γ := LieSubalgebra R (Matrix m m R))
      (skewAdjointMatricesLieSubalgebra ((e : (a : Matrix n n R) → Matrix m m R) J)) A

Tactic:
suffices J.IsSkewAdjoint (e.symm A) ↔ (e J).IsSkewAdjoint A by
      simpa [-LieSubalgebra.mem_map, LieSubalgebra.mem_map_submodule]
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J : Matrix n n R
m : Type w
inst_3 : DecidableEq m
inst_4 : Fintype m
e : Matrix n n R ≃ₐ[R] Matrix m m R
h :
  ∀ (A : Matrix n n R),
    Eq (α := Matrix m m R) ((e : (a : Matrix n n R) → Matrix m m R) A)ᵀ ((e : (a : Matrix n n R) → Matrix m m R) Aᵀ)
A : Matrix m m R
⊢ J.IsSkewAdjoint ((e.symm : (a : Matrix m m R) → Matrix n n R) A) ↔
    Matrix.IsSkewAdjoint ((e : (a : Matrix n n R) → Matrix m m R) J) A

Tactic:
simp only [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair, ← h,
      ← Function.Injective.eq_iff e.injective, map_mul, AlgEquiv.apply_symm_apply, map_neg]

Premises used: Function.Injective.eq_iff, AlgEquiv.apply_symm_apply, map_neg, map_mul, Matrix.IsSkewAdjoint, AlgEquiv.injective, Matrix.IsAdjointPair
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
J : Matrix n n R
m : Type w
inst_3 : DecidableEq m
inst_4 : Fintype m
e : Matrix n n R ≃ₐ[R] Matrix m m R
h :
  ∀ (A : Matrix n n R),
    Eq (α := Matrix m m R) ((e : (a : Matrix n n R) → Matrix m m R) A)ᵀ ((e : (a : Matrix n n R) → Matrix m m R) Aᵀ)
A : ↥(skewAdjointMatricesLieSubalgebra J)
⊢ Eq (α := Matrix m m R)
    ((↑((skewAdjointMatricesLieSubalgebraEquivTranspose J e h :
              (a : ↥(skewAdjointMatricesLieSubalgebra J)) →
                ↥(skewAdjointMatricesLieSubalgebra ((e : (a : Matrix n n R) → Matrix m m R) J)))
            A) :
        Matrix m m R) :
      Matrix m m R)
    ((e : (a : Matrix n n R) → Matrix m m R) (↑A : Matrix n n R) : Matrix m m R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
u : Rˣ
J A : Matrix n n R
simp : Aᵀ * u • J = u • J * -A ↔ Aᵀ * J = J * -A
⊢ Membership.mem (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule (u • J)) A ↔
    Membership.mem (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule J) A

Tactic:
simp only [mem_skewAdjointMatricesSubmodule, Matrix.IsSkewAdjoint, Matrix.IsAdjointPair]

Premises used: mem_skewAdjointMatricesSubmodule, Matrix.IsSkewAdjoint, Matrix.IsAdjointPair
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
u : Rˣ
J A : Matrix n n R
mp : Aᵀ * u • J = u • J * -A → Aᵀ * J = J * -A
mpr : Aᵀ * J = J * -A → Aᵀ * u • J = u • J * -A
⊢ Aᵀ * u • J = u • J * -A ↔ Aᵀ * J = J * -A

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
u : Rˣ
J A : Matrix n n R
h : Aᵀ * u • J = u • J * -A
⊢ Aᵀ * J = J * -A

Tactic:
simpa using congr_arg (fun B => u⁻¹ • B) h

Premises used: congr_arg, Inv.inv, HSMul.hSMul
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
u : Rˣ
J A : Matrix n n R
h : Aᵀ * J = J * -A
⊢ Aᵀ * u • J = u • J * -A

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
L : Type u_2
inst : LieRing L
h e f : L
ht : IsSl2Triple h e f
⊢ -h ≠ 0

Tactic:
simpa using ht.h_ne_zero

Premises used: IsSl2Triple.h_ne_zero
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
L : Type u_2
inst : LieRing L
h e f : L
ht : IsSl2Triple h e f
rw : -⁅f, e⁆ = h
rw₁ : ⁅e, f⁆ = h
rw₂ rw₃ : h = h
⊢ ⁅f, e⁆ = -h

Tactic:
rw [← neg_eq_iff_eq_neg, lie_skew, ht.lie_e_f]

Premises used: neg_eq_iff_eq_neg, lie_skew, IsSl2Triple.lie_e_f
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
L : Type u_2
inst : LieRing L
h e f : L
ht : IsSl2Triple h e f
rw : -⁅h, f⁆ = HSMul.hSMul (α := ℕ) 2 f
rw₁ : ⁅h, f⁆ = -HSMul.hSMul (α := ℕ) 2 f
rw₂ rw₃ : -HSMul.hSMul (α := ℕ) 2 f = -HSMul.hSMul (α := ℕ) 2 f
⊢ ⁅-h, f⁆ = HSMul.hSMul (α := ℕ) 2 f

Tactic:
rw [neg_lie, neg_eq_iff_eq_neg, ht.lie_h_f_nsmul]

Premises used: neg_eq_iff_eq_neg, neg_lie, IsSl2Triple.lie_h_f_nsmul
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
L : Type u_2
inst : LieRing L
h e f : L
ht : IsSl2Triple h e f
rw : -⁅h, e⁆ = -HSMul.hSMul (α := ℕ) 2 e
rw₁ : ⁅h, e⁆ = HSMul.hSMul (α := ℕ) 2 e
rw₂ rw₃ : HSMul.hSMul (α := ℕ) 2 e = HSMul.hSMul (α := ℕ) 2 e
⊢ ⁅-h, e⁆ = -HSMul.hSMul (α := ℕ) 2 e

Tactic:
rw [neg_lie, neg_inj, ht.lie_h_e_nsmul]

Premises used: neg_lie, neg_inj, IsSl2Triple.lie_h_e_nsmul
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
L : Type u_2
inst : LieRing L
h e f : L
⊢ IsSl2Triple (-h) f e ↔ IsSl2Triple h e f

Tactic:
⟨fun t ↦ neg_neg h ▸ t.symm, symm⟩

Premises used: Eq.rec, neg_neg, IsSl2Triple.symm, Iff.intro
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h e f : L
t : IsSl2Triple h e f
⊢ ⁅h, e⁆ = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 e

Tactic:
simp [t.lie_h_e_nsmul, two_smul]

Premises used: two_smul, IsSl2Triple.lie_h_e_nsmul
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h e f : L
t : IsSl2Triple h e f
⊢ ⁅h, f⁆ = -HSMul.hSMul.{u_1, u_2, u_2} (α := R) 2 f

Tactic:
simp [t.lie_h_f_nsmul, two_smul]

Premises used: two_smul, IsSl2Triple.lie_h_f_nsmul
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
L : Type u_2
inst : LieRing L
h e f : L
t : IsSl2Triple h e f
⊢ h ≠ 0

Tactic:
have := t.h_ne_zero
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
L : Type u_2
inst : LieRing L
h e f : L
t : IsSl2Triple h e f
this : h ≠ 0
contrapose : ∀ (this : e = 0), h = 0
⊢ e ≠ 0

Tactic:
contrapose this
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
L : Type u_2
inst : LieRing L
h e f : L
t : IsSl2Triple h e f
this : e = 0
⊢ h = 0

Tactic:
simpa [this] using t.lie_e_f.symm

Premises used: Eq.symm, IsSl2Triple.lie_e_f
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
L : Type u_2
inst : LieRing L
h e f : L
t : IsSl2Triple h e f
this : h ≠ 0
contrapose : ∀ (this : f = 0), h = 0
⊢ f ≠ 0

Tactic:
contrapose this
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
L : Type u_2
inst : LieRing L
h e f : L
t : IsSl2Triple h e f
this : f = 0
⊢ h = 0

Tactic:
simpa [this] using t.lie_e_f.symm

Premises used: Eq.symm, IsSl2Triple.lie_e_f
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
inst_7 : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
this : HSMul.hSMul (α := ℕ) 2 ⁅e, m⁆ = 0
⊢ ⁅e, m⁆ = 0

Tactic:
simpa using this
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
inst_7 : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
suffices : HSMul.hSMul (α := ℕ) 2 ⁅e, m⁆ = 0
⊢ ⁅e, m⁆ = 0

Tactic:
suffices 2 • ⁅e, m⁆ = 0 by simpa using this
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
inst_7 : IsAddTorsionFree M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
rw : ⁅HSMul.hSMul (α := ℕ) 2 e, m⁆ = 0
rw₁ : ⁅⁅h, e⁆, m⁆ = 0
rw₂ : ⁅h, ⁅e, m⁆⁆ - ⁅e, ⁅h, m⁆⁆ = 0
rw₃ : ⁅h, ⁅e, m⁆⁆ - ⁅e, μ • m⁆ = 0
rw₄ : ⁅h, ⁅e, m⁆⁆ - μ • ⁅e, m⁆ = 0
rw₅ : ⁅h, ρ • m⁆ - μ • ρ • m = 0
rw₆ : ρ • ⁅h, m⁆ - μ • ρ • m = 0
rw₇ : ρ • μ • m - μ • ρ • m = 0
rw₈ : (ρ * μ) • m - μ • ρ • m = 0
rw₉ : (ρ * μ) • m - (μ * ρ) • m = 0
rw₁₀ : (μ * ρ) • m - (μ * ρ) • m = 0
rw₁₁ rw₁₂ : Eq.{u_3 + 1} (α := M) 0 0
⊢ HSMul.hSMul (α := ℕ) 2 ⁅e, m⁆ = 0

Tactic:
rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm',
      smul_smul, smul_smul, mul_comm ρ μ, sub_self]

Premises used: sub_self, lie_smul, smul_smul, mul_comm, IsSl2Triple.lie_h_e_nsmul, nsmul_lie, lie_lie
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
t : IsSl2Triple h e f
x y : L
hx :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R {e, f, h})))) x
hy :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R {e, f, h})))) y
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) x

Tactic:
simp only [carrier_eq_coe, SetLike.mem_coe] at hx hy ⊢

Premises used: SetLike.mem_coe, Submodule.carrier_eq_coe
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
t : IsSl2Triple h e f
x y : L
hx :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R {e, f, h})))) x
hy :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R {e, f, h})))) y
hx₁ : Membership.mem (γ := Submodule R L) (span R {e, f, h}) x
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) y

Tactic:
simp only [carrier_eq_coe, SetLike.mem_coe] at hx hy ⊢

Premises used: SetLike.mem_coe, Submodule.carrier_eq_coe
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
t : IsSl2Triple h e f
x y : L
hy : Membership.mem (γ := Submodule R L) (span R {e, f, h}) y
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) (Bracket.bracket (L := L) 0 y)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
t : IsSl2Triple h e f
x y : L
hy : Membership.mem (γ := Submodule R L) (span R {e, f, h}) y
u v : L
hu : Membership.mem (γ := Submodule R L) (span R {e, f, h}) u
hv : Membership.mem (γ := Submodule R L) (span R {e, f, h}) v
hu' : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, y⁆
hv' : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅v, y⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u + v, y⁆

Tactic:
simpa only [add_lie] using add_mem hu' hv'

Premises used: AddMemClass.add_mem, add_lie
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
t_1 : IsSl2Triple h e f
x y : L
hy : Membership.mem (γ := Submodule R L) (span R {e, f, h}) y
t : R
u : L
hu : Membership.mem (γ := Submodule R L) (span R {e, f, h}) u
hu' : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, y⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅t • u, y⁆

Tactic:
simpa only [smul_lie] using smul_mem _ t hu'

Premises used: smul_lie, Submodule.smul_mem
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
t : IsSl2Triple h e f
x y u : L
hu : Membership.mem (γ := Set L) {e, f, h} u
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u, 0⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Sl2
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h e f : L
t : IsSl2Triple h e f
x y u_1 : L
hu_1 : Membership.mem (γ := Set L) {e, f, h} u_1
u v : L
hu : Membership.mem (γ := Submodule R L) (span R {e, f, h}) u
hv : Membership.mem (γ := Submodule R L) (span R {e, f, h}) v
hu' : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u_1, u⁆
hv' : Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u_1, v⁆
⊢ Membership.mem (γ := Submodule R L) (span R {e, f, h}) ⁅u_1, u + v⁆

Tactic:
simpa only [lie_add] using add_mem hu' hv'

Premises used: AddMemClass.add_mem, lie_add