awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (goal)
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)
⊢ x = 0
have 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
Tactic: obtain ⟨t, ht⟩ := Submodule.mem_span_singleton.mp hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (goal)
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
⊢ x = 0
have suffices : t = 0
Tactic: suffices t = 0 by simp [← toEnd_eq_zero_iff (R := k) (L := L) (M := M), ← ht, this]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (goal)
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
hx : Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) x
mem :
  ∀ (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)
⊢ 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)
have zero : 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: induction hx using LieSubalgebra.lieSpan_induction with
  | mem u hu => simpa using hs u hu
  | zero => simp
  | add u v _ _ hu hv => simp [hu, hv]
  | smul t u _ hu => simp [hu]
  | lie u v _ _ _ _ => simp
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (goal)
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
hx : Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) x
mem :
  ∀ (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)
zero :
  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)
⊢ 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)
have add : ∀ (u v : L),
  Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) u →
    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: induction hx using LieSubalgebra.lieSpan_induction with
  | mem u hu => simpa using hs u hu
  | zero => simp
  | add u v _ _ hu hv => simp [hu, hv]
  | smul t u _ hu => simp [hu]
  | lie u v _ _ _ _ => simp
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (goal)
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
hx : Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) x
mem :
  ∀ (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)
zero :
  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)
add :
  ∀ (u v : L),
    Membership.mem (γ := LieSubalgebra R L) (LieSubalgebra.lieSpan R L s) u →
      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)
⊢ 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)
have smul : ∀ (t : R) (u : L),
  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: induction hx using LieSubalgebra.lieSpan_induction with
  | mem u hu => simpa using hs u hu
  | zero => simp
  | add u v _ _ hu hv => simp [hu, hv]
  | smul t u _ hu => simp [hu]
  | lie u v _ _ _ _ => simp
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.SerreConstruction (hypothesis)
Goal:
R : Type u
B : Type v
inst : CommRing R
CM : Matrix B B ℤ
i : B
h : CM i i = 2
⊢ Eq (α := FreeLieAlgebra.{u, v} R (Generators B)) (adE R CM (i, i)) 0
have h' : Int.toNat (-2) = 0
Tactic: have h' : (-2 : ℤ).toNat = 0 := rfl
-- Lean 4 proof step from Mathlib.Algebra.Lie.SerreConstruction (hypothesis)
Goal:
R : Type u
B : Type v
inst : CommRing R
CM : Matrix B B ℤ
i : B
h : CM i i = 2
⊢ Eq (α := FreeLieAlgebra.{u, v} R (Generators B)) (adF R CM (i, i)) 0
have h' : Int.toNat (-2) = 0
Tactic: have h' : (-2 : ℤ).toNat = 0 := rfl
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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
⊢ Membership.mem (γ := Submodule R (Module.End R M)) (skewAdjointSubmodule (M₂ := R) B) ⁅f, g⁆
have 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)
Tactic: rw [mem_skewAdjointSubmodule] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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)
have rw : IsAdjointPair B B (⇑(f * g) : (a : M) → M) (⇑(-g * -f) : (a : M) → M)
Tactic: rw [← neg_mul_neg g f]
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (hypothesis)
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)
⊢ IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑⁅f, g⁆ : (a : M) → M)
have hfg : 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
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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)
have rw : IsAdjointPair B B (⇑(g * f) : (a : M) → M) (⇑(-f * -g) : (a : M) → M)
Tactic: rw [← neg_mul_neg f g]
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (hypothesis)
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)
⊢ IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑⁅f, g⁆ : (a : M) → M)
have hgf : 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
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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)
⊢ IsSkewAdjoint.{u, v, u} (R := R) (M := M) (M₂ := R) B (⇑⁅f, g⁆ : (a : M) → M)
have change : IsAdjointPair B B (⇑(f * g - g * f) : (a : M) → M) (⇑(-(f * g - g * f)) : (a : M) → M)
Tactic: change IsAdjointPair B B (f * g - g * f) (-(f * g - g * f))
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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) (⇑(-(f * g - g * f)) : (a : M) → M)
have rw : IsAdjointPair B B (⇑(f * g - g * f) : (a : M) → M) (⇑(g * f - f * g) : (a : M) → M)
Tactic: rw [neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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
⊢ LieEquiv.{u, w, v} R ↥(skewAdjointLieSubalgebra (LinearMap.compl₁₂ B (↑e : N →ₗ[R] M) (↑e : N →ₗ[R] M)))
    ↥(skewAdjointLieSubalgebra B)
have apply : LieSubalgebra.map e.lieConj.toLieHom
    (skewAdjointLieSubalgebra (LinearMap.compl₁₂ B (↑e : N →ₗ[R] M) (↑e : N →ₗ[R] M))) =
  skewAdjointLieSubalgebra B
Tactic: apply LieEquiv.ofSubalgebras _ _ e.lieConj
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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
⊢ LieSubalgebra.map e.lieConj.toLieHom
      (skewAdjointLieSubalgebra (LinearMap.compl₁₂ B (↑e : N →ₗ[R] M) (↑e : N →ₗ[R] M))) =
    skewAdjointLieSubalgebra B
have 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
Tactic: ext f
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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
⊢ f ∈
      LieSubalgebra.map e.lieConj.toLieHom
        (skewAdjointLieSubalgebra (LinearMap.compl₁₂ B (↑e : N →ₗ[R] M) (↑e : N →ₗ[R] M))) ↔
    f ∈ skewAdjointLieSubalgebra B
have 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
Tactic: simp only [Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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
⊢ Membership.mem (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule J) ⁅A, B⁆
have simp : ∀ (hA : J.IsSkewAdjoint A) (hB : J.IsSkewAdjoint B), J.IsSkewAdjoint ⁅A, B⁆
Tactic: simp only [mem_skewAdjointMatricesSubmodule] at *
Cleared hypotheses: hA, hB
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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
⊢ J.IsSkewAdjoint ⁅A, B⁆
have change : ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆
Tactic: change ⁅A, B⁆ᵀ * J = J * (-⁅A, B⁆)
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (hypothesis)
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, B⁆ᵀ * J = J * -⁅A, B⁆
have hA₁ : Aᵀ * J = J * -A
Tactic: change Aᵀ * J = J * (-A) at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (hypothesis)
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
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆
have hB₁ : Bᵀ * J = J * -B
Tactic: change Bᵀ * J = J * (-B) at hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆
have rw : J * -B * -A - J * -A * -B = J * -(A * B - B * A)
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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
⊢ J * -B * -A - J * -A * -B = J * -(A * B - B * A)
have noncomm_ring : - -(J * (B * A)) + - - -(J * (A * B)) = -(J * (A * B) + -(J * (B * A)))
Tactic: noncomm_ring
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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
⊢ LieSubalgebra.map (P.lieConj h).symm.toLieHom (skewAdjointMatricesLieSubalgebra J) =
    skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)
have 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
Tactic: ext A
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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
⊢ A ∈ LieSubalgebra.map (P.lieConj h).symm.toLieHom (skewAdjointMatricesLieSubalgebra J) ↔
    Membership.mem (γ := LieSubalgebra R (Matrix n n R)) (skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)) A
have 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
Tactic: simp only [Submodule.mem_map_equiv, LieSubalgebra.mem_map_submodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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
⊢ A ∈ LieSubalgebra.map (P.lieConj h).symm.toLieHom (skewAdjointMatricesLieSubalgebra J) ↔
    Membership.mem (γ := LieSubalgebra R (Matrix n n R)) (skewAdjointMatricesLieSubalgebra (Pᵀ * J * P)) A
have 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
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
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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ᵀ)
⊢ 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))
have 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
Tactic: ext A
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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
⊢ 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
have 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
Tactic: suffices J.IsSkewAdjoint (e.symm A) ↔ (e J).IsSkewAdjoint A by
      simpa [-LieSubalgebra.mem_map, LieSubalgebra.mem_map_submodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.SkewAdjoint (goal)
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
⊢ Membership.mem (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule (u • J)) A ↔
    Membership.mem (γ := Submodule R (Matrix n n R)) (skewAdjointMatricesSubmodule J) A
have simp : Aᵀ * u • J = u • J * -A ↔ Aᵀ * J = J * -A
Tactic: simp only [mem_skewAdjointMatricesSubmodule, Matrix.IsSkewAdjoint, Matrix.IsAdjointPair]