awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal k L) (center k L) x ↔
      Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
x : L
hx :
  Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
    (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
h :
  Eq.{u_1 + 1} (α := k)
    ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
      k)
    (0 : k)
obtain :
  ∀ (t : k)
    (ht :
      HSMul.hSMul (β := End k M) t LinearMap.id =
        ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x),
    x = 0
⊢ x = 0

Tactic:
obtain ⟨t, ht⟩ := Submodule.mem_span_singleton.mp hx

Premises used: Submodule.mem_span_singleton, Iff.mp
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
this_1 : finrank k M ≠ 0
_i : HasCentralRadical k L
h' :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal k L) (center k L) x ↔
      Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
x : L
hx :
  Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
    (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
h :
  Eq.{u_1 + 1} (α := k)
    ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
      k)
    (0 : k)
t : k
ht :
  HSMul.hSMul (β := End k M) t LinearMap.id =
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x
this : t = 0
⊢ x = 0

Tactic:
simp [← toEnd_eq_zero_iff (R := k) (L := L) (M := M), ← ht, this]

Premises used: LieModule.toEnd_eq_zero_iff
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal k L) (center k L) x ↔
      Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
x : L
hx :
  Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
    (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
h :
  Eq.{u_1 + 1} (α := k)
    ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
      k)
    (0 : k)
t : k
ht :
  HSMul.hSMul (β := End k M) t LinearMap.id =
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x
suffices : t = 0
⊢ x = 0

Tactic:
suffices t = 0 by simp [← toEnd_eq_zero_iff (R := k) (L := L) (M := M), ← ht, this]
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal k L) (center k L) x ↔
      Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
x : L
hx :
  Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
    (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
h :
  Eq.{u_1 + 1} (α := k)
    ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
      k)
    (0 : k)
t : k
ht :
  HSMul.hSMul (β := End k M) t LinearMap.id =
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x
⊢ t = 0

Tactic:
simpa [this, ← ht] using h
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
R : Type u_4
inst_3 : CommRing R
inst_4 : LieAlgebra R L
inst_5 : Module R M
inst_6 : LieModule R L M
s : Set L
hs :
  ∀ x ∈ s,
    Eq.{u_4 + 1} (α := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) x : End R M) :
        R)
      (0 : R)
x u : L
hu : u ∈ s
⊢ Eq.{u_4 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) u : End R M) :
      R)
    (0 : R)

Tactic:
simpa using hs u hu
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
R : Type u_4
inst_3 : CommRing R
inst_4 : LieAlgebra R L
inst_5 : Module R M
inst_6 : LieModule R L M
s : Set L
hs :
  ∀ x ∈ s,
    Eq.{u_4 + 1} (α := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) x : End R M) :
        R)
      (0 : R)
x : L
⊢ Eq.{u_4 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R) (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) 0) :
      R)
    (0 : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
R : Type u_4
inst_3 : CommRing R
inst_4 : LieAlgebra R L
inst_5 : Module R M
inst_6 : LieModule R L M
s : Set L
hs :
  ∀ x ∈ s,
    Eq.{u_4 + 1} (α := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) x : End R M) :
        R)
      (0 : R)
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) u
hy : Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) v
hu :
  Eq.{u_4 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) u : End R M) :
      R)
    (0 : R)
hv :
  Eq.{u_4 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) v : End R M) :
      R)
    (0 : R)
⊢ Eq.{u_4 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) (u + v) : End R M) :
      R)
    (0 : R)

Tactic:
simp [hu, hv]
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
R : Type u_4
inst_3 : CommRing R
inst_4 : LieAlgebra R L
inst_5 : Module R M
inst_6 : LieModule R L M
s : Set L
hs :
  ∀ x ∈ s,
    Eq.{u_4 + 1} (α := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) x : End R M) :
        R)
      (0 : R)
x : L
t : R
u : L
hx : Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) u
hu :
  Eq.{u_4 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) u : End R M) :
      R)
    (0 : R)
⊢ Eq.{u_4 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) (t • u) : End R M) :
      R)
    (0 : R)

Tactic:
simp [hu]
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
R : Type u_4
inst_3 : CommRing R
inst_4 : LieAlgebra R L
inst_5 : Module R M
inst_6 : LieModule R L M
s : Set L
hs :
  ∀ x ∈ s,
    Eq.{u_4 + 1} (α := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) x : End R M) :
        R)
      (0 : R)
x u v : L
hx : Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) u
hy : Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) v
h :
  Eq.{u_4 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) u : End R M) :
      R)
    (0 : R)
h_1 :
  Eq.{u_4 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) v : End R M) :
      R)
    (0 : R)
⊢ Eq.{u_4 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((toEnd R L M : LieHom.{u_4, u_2, u_3} R L (End R M)) : (a : L) → End R M) ⁅u, v⁆ : End R M) :
      R)
    (0 : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SerreConstruction
Goal:
R : Type u
B : Type v
inst : CommRing R
CM : Matrix B B ℤ
i : B
h : CM i i = 2
⊢ Int.toNat (-2) = 0

Tactic:
have h' : (-2 : ℤ).toNat = 0 := rfl
-- Module: Mathlib.Algebra.Lie.SerreConstruction
Goal:
R : Type u
B : Type v
inst : CommRing R
CM : Matrix B B ℤ
i : B
h : CM i i = 2
h' : Int.toNat (-2) = 0
⊢ Eq (α := FreeLieAlgebra.{u, v} R (Generators B)) (adE R CM (i, i)) 0

Tactic:
simp [adE, h, h']

Premises used: CartanMatrix.Relations.adE
-- Module: Mathlib.Algebra.Lie.SerreConstruction
Goal:
R : Type u
B : Type v
inst : CommRing R
CM : Matrix B B ℤ
i : B
h : CM i i = 2
h' : Int.toNat (-2) = 0
⊢ Eq (α := FreeLieAlgebra.{u, v} R (Generators B)) (adF R CM (i, i)) 0

Tactic:
simp [adF, h, h']

Premises used: CartanMatrix.Relations.adF
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
f g : Module.End R M
hf : Membership.mem (γ := Submodule R (Module.End R M)) (skewAdjointSubmodule (M₂ := R) B) f
hg : Membership.mem (γ := Submodule R (Module.End R M)) (skewAdjointSubmodule (M₂ := R) B) g
rw :
  ∀ (hf : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑f : (a : M) → M))
    (hg : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑g : (a : M) → M)),
    IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑⁅f, g⁆ : (a : M) → M)
⊢ Membership.mem (γ := Submodule R (Module.End R M)) (skewAdjointSubmodule (M₂ := R) B) ⁅f, g⁆

Tactic:
rw [mem_skewAdjointSubmodule] at *

Premises used: LinearMap.mem_skewAdjointSubmodule
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑f : (a : M) → M)
hg : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑g : (a : M) → M)
rw : IsAdjointPair B B (⇑(f * g) : (a : M) → M) (⇑(-g * -f) : (a : M) → M)
⊢ IsAdjointPair B B (⇑(f * g) : (a : M) → M) (⇑(g * f) : (a : M) → M)

Tactic:
rw [← neg_mul_neg g f]

Premises used: neg_mul_neg
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑f : (a : M) → M)
hg : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑g : (a : M) → M)
⊢ IsAdjointPair B B (⇑(f * g) : (a : M) → M) (⇑(-g * -f) : (a : M) → M)

Tactic:
hg.comp hf

Premises used: LinearMap.IsAdjointPair.comp
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑f : (a : M) → M)
hg : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑g : (a : M) → M)
⊢ IsAdjointPair B B (⇑(f * g) : (a : M) → M) (⇑(-g * -f) : (a : M) → M)

Tactic:
exact hg.comp hf

Premises used: LinearMap.IsAdjointPair.comp
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑f : (a : M) → M)
hg : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑g : (a : M) → M)
⊢ IsAdjointPair B B (⇑(f * g) : (a : M) → M) (⇑(g * f) : (a : M) → M)

Tactic:
have hfg : IsAdjointPair B B (f * g) (g * f) := by rw [← neg_mul_neg g f]; exact hg.comp hf
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑f : (a : M) → M)
hg : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑g : (a : M) → M)
hfg : IsAdjointPair B B (⇑(f * g) : (a : M) → M) (⇑(g * f) : (a : M) → M)
rw : IsAdjointPair B B (⇑(g * f) : (a : M) → M) (⇑(-f * -g) : (a : M) → M)
⊢ IsAdjointPair B B (⇑(g * f) : (a : M) → M) (⇑(f * g) : (a : M) → M)

Tactic:
rw [← neg_mul_neg f g]

Premises used: neg_mul_neg
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑f : (a : M) → M)
hg : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑g : (a : M) → M)
hfg : IsAdjointPair B B (⇑(f * g) : (a : M) → M) (⇑(g * f) : (a : M) → M)
⊢ IsAdjointPair B B (⇑(g * f) : (a : M) → M) (⇑(-f * -g) : (a : M) → M)

Tactic:
hf.comp hg

Premises used: LinearMap.IsAdjointPair.comp
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑f : (a : M) → M)
hg : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑g : (a : M) → M)
hfg : IsAdjointPair B B (⇑(f * g) : (a : M) → M) (⇑(g * f) : (a : M) → M)
⊢ IsAdjointPair B B (⇑(g * f) : (a : M) → M) (⇑(-f * -g) : (a : M) → M)

Tactic:
exact hf.comp hg

Premises used: LinearMap.IsAdjointPair.comp
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑f : (a : M) → M)
hg : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑g : (a : M) → M)
hfg : IsAdjointPair B B (⇑(f * g) : (a : M) → M) (⇑(g * f) : (a : M) → M)
⊢ IsAdjointPair B B (⇑(g * f) : (a : M) → M) (⇑(f * g) : (a : M) → M)

Tactic:
have hgf : IsAdjointPair B B (g * f) (f * g) := by rw [← neg_mul_neg f g]; exact hf.comp hg
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑f : (a : M) → M)
hg : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑g : (a : M) → M)
hfg : IsAdjointPair B B (⇑(f * g) : (a : M) → M) (⇑(g * f) : (a : M) → M)
hgf : IsAdjointPair B B (⇑(g * f) : (a : M) → M) (⇑(f * g) : (a : M) → M)
change : IsAdjointPair B B (⇑(f * g - g * f) : (a : M) → M) (⇑(-(f * g - g * f)) : (a : M) → M)
⊢ IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑⁅f, g⁆ : (a : M) → M)

Tactic:
change IsAdjointPair B B (f * g - g * f) (-(f * g - g * f))

Premises used: HMul.hMul, LinearMap.IsAdjointPair, HSub.hSub, DFunLike.coe, Neg.neg
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑f : (a : M) → M)
hg : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑g : (a : M) → M)
hfg : IsAdjointPair B B (⇑(f * g) : (a : M) → M) (⇑(g * f) : (a : M) → M)
hgf : IsAdjointPair B B (⇑(g * f) : (a : M) → M) (⇑(f * g) : (a : M) → M)
rw : IsAdjointPair B B (⇑(f * g - g * f) : (a : M) → M) (⇑(g * f - f * g) : (a : M) → M)
⊢ IsAdjointPair B B (⇑(f * g - g * f) : (a : M) → M) (⇑(-(f * g - g * f)) : (a : M) → M)

Tactic:
rw [neg_sub]

Premises used: neg_sub
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑f : (a : M) → M)
hg : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑g : (a : M) → M)
hfg : IsAdjointPair B B (⇑(f * g) : (a : M) → M) (⇑(g * f) : (a : M) → M)
hgf : IsAdjointPair B B (⇑(g * f) : (a : M) → M) (⇑(f * g) : (a : M) → M)
⊢ IsAdjointPair B B (⇑(f * g - g * f) : (a : M) → M) (⇑(g * f - f * g) : (a : M) → M)

Tactic:
hfg.sub hgf

Premises used: LinearMap.IsAdjointPair.sub
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
f g : Module.End R M
hf : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑f : (a : M) → M)
hg : IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑g : (a : M) → M)
hfg : IsAdjointPair B B (⇑(f * g) : (a : M) → M) (⇑(g * f) : (a : M) → M)
hgf : IsAdjointPair B B (⇑(g * f) : (a : M) → M) (⇑(f * g) : (a : M) → M)
⊢ IsAdjointPair B B (⇑(f * g - g * f) : (a : M) → M) (⇑(g * f - f * g) : (a : M) → M)

Tactic:
exact hfg.sub hgf

Premises used: LinearMap.IsAdjointPair.sub
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
e : N ≃ₗ[R] M
apply :
  LieSubalgebra.map e.lieConj.toLieHom
      (skewAdjointLieSubalgebra (LinearMap.compl₁₂ B (↑e : N →ₗ[R] M) (↑e : N →ₗ[R] M))) =
    skewAdjointLieSubalgebra B
⊢ LieEquiv.{u, w, v} R ↥(skewAdjointLieSubalgebra (LinearMap.compl₁₂ B (↑e : N →ₗ[R] M) (↑e : N →ₗ[R] M)))
    ↥(skewAdjointLieSubalgebra B)

Tactic:
apply LieEquiv.ofSubalgebras _ _ e.lieConj

Premises used: LinearEquiv.lieConj, LieEquiv.ofSubalgebras
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
e : N ≃ₗ[R] M
h :
  ∀ (f : Module.End R M),
    f ∈
        LieSubalgebra.map e.lieConj.toLieHom
          (skewAdjointLieSubalgebra (LinearMap.compl₁₂ B (↑e : N →ₗ[R] M) (↑e : N →ₗ[R] M))) ↔
      f ∈ skewAdjointLieSubalgebra B
⊢ LieSubalgebra.map e.lieConj.toLieHom
      (skewAdjointLieSubalgebra (LinearMap.compl₁₂ B (↑e : N →ₗ[R] M) (↑e : N →ₗ[R] M))) =
    skewAdjointLieSubalgebra B

Tactic:
ext f
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
e : N ≃ₗ[R] M
f : Module.End R M
h :
  Membership.mem (α := Module.End R N)
      (skewAdjointLieSubalgebra (LinearMap.compl₁₂ B (↑e : N →ₗ[R] M) (↑e : N →ₗ[R] M))).toSubmodule
      ((e.lieConj.toLinearEquiv.symm : (a : Module.End R M) → Module.End R N) f : Module.End R N) ↔
    f ∈ skewAdjointLieSubalgebra B
⊢ f ∈
      LieSubalgebra.map e.lieConj.toLieHom
        (skewAdjointLieSubalgebra (LinearMap.compl₁₂ B (↑e : N →ₗ[R] M) (↑e : N →ₗ[R] M))) ↔
    f ∈ skewAdjointLieSubalgebra B

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
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
e : N ≃ₗ[R] M
f : Module.End R M
⊢ Membership.mem (α := Module.End R N)
      (skewAdjointLieSubalgebra (LinearMap.compl₁₂ B (↑e : N →ₗ[R] M) (↑e : N →ₗ[R] M))).toSubmodule
      ((e.lieConj.toLinearEquiv.symm : (a : Module.End R M) → Module.End R N) f : Module.End R N) ↔
    f ∈ skewAdjointLieSubalgebra B

Tactic:
(LinearMap.isPairSelfAdjoint_equiv (B := -B) (F := B) e f).symm

Premises used: LinearMap.IsAdjointPair, Set.Mem, LinearMap.IsPairSelfAdjoint, setOf, LinearMap.isPairSelfAdjoint_equiv, Iff.symm
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
e : N ≃ₗ[R] M
f : Module.End R M
⊢ Membership.mem (α := Module.End R N)
      (skewAdjointLieSubalgebra (LinearMap.compl₁₂ B (↑e : N →ₗ[R] M) (↑e : N →ₗ[R] M))).toSubmodule
      ((e.lieConj.toLinearEquiv.symm : (a : Module.End R M) → Module.End R N) f : Module.End R N) ↔
    f ∈ skewAdjointLieSubalgebra B

Tactic:
exact (LinearMap.isPairSelfAdjoint_equiv (B := -B) (F := B) e f).symm

Premises used: LinearMap.isPairSelfAdjoint_equiv, Iff.symm
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
e : N ≃ₗ[R] M
f : ↥(skewAdjointLieSubalgebra (LinearMap.compl₁₂ B (↑e : N →ₗ[R] M) (↑e : N →ₗ[R] M)))
⊢ Eq.{v + 1} (α := Module.End R M)
    ((↑((skewAdjointLieSubalgebraEquiv B e :
              (a : ↥(skewAdjointLieSubalgebra (LinearMap.compl₁₂ B (↑e : N →ₗ[R] M) (↑e : N →ₗ[R] M)))) →
                ↥(skewAdjointLieSubalgebra B))
            f) :
        Module.End R M) :
      Module.End R M)
    ((e.lieConj : (a : Module.End R N) → Module.End R M) (↑f : Module.End R N) : Module.End R M)

Tactic:
simp [skewAdjointLieSubalgebraEquiv]

Premises used: skewAdjointLieSubalgebraEquiv
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : BilinForm R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
e : N ≃ₗ[R] M
f : ↥(skewAdjointLieSubalgebra B)
⊢ Eq.{w + 1} (α := Module.End R N)
    ((↑(((skewAdjointLieSubalgebraEquiv B e).symm :
              (a : ↥(skewAdjointLieSubalgebra B)) →
                ↥(skewAdjointLieSubalgebra (LinearMap.compl₁₂ B (↑e : N →ₗ[R] M) (↑e : N →ₗ[R] M))))
            f) :
        Module.End R N) :
      Module.End R N)
    ((e.symm.lieConj : (a : Module.End R M) → Module.End R N) (↑f : Module.End R M) : Module.End R N)

Tactic:
simp [skewAdjointLieSubalgebraEquiv]

Premises used: skewAdjointLieSubalgebraEquiv
-- Module: Mathlib.Algebra.Lie.SkewAdjoint
Goal:
R : Type u
n : Type w
inst : CommRing R
inst_1 : DecidableEq n
inst_2 : Fintype n
A B : Matrix n n R
⊢ (A * B - B * A)ᵀ = Bᵀ * Aᵀ - Aᵀ * Bᵀ

Tactic:
simp