awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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 : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x : L
hx : Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x}) x
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) y) :
      R)
    (0 : R)
have mem : ∀ (u : L) (hu : Membership.mem (γ := Set L) {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x} u),
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) u : End R M) y) :
      R)
    (0 : R)
Tactic: induction hx using Submodule.span_induction with
  | mem u hu =>
    obtain ⟨a, b, rfl⟩ := hu
    obtain ⟨c : L, hbc : φ c = ⁅y, φ b⁆⟩ := hy (φ b) (LieHom.mem_range_self φ b)
    replace hbc : ⁅φ b, y⁆ = -φ c := by rw [hbc, Module.End.instLieRingModule_eq, lie_skew]
    rw [LieHom.map_lie, LinearMap.trace_lie_mul_eq, Ring.lie_def,
      ← LieRing.of_associative_ring_bracket, ← Module.End.instLieRingModule_eq, hbc, mul_neg,
      map_neg, neg_eq_zero, Module.End.mul_eq_comp, ← traceForm_apply_apply, h,
      LinearMap.zero_apply, LinearMap.zero_apply]
  | zero => simp
  | add u v _ _ hu hv => simp [add_mul, hu, hv]
  | smul t u _ hu => simp [hu]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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 : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x : L
hx : Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x}) x
mem :
  ∀ (u : L) (hu : Membership.mem (γ := Set L) {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x} u),
    Eq.{u_1 + 1} (α := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) u : End R M) y) :
        R)
      (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) y) :
      R)
    (0 : R)
have zero : Eq.{u_1 + 1} (α := R)
  ((trace R M : (a : M →ₗ[R] M) → R) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) 0 * y) : R)
  (0 : R)
Tactic: induction hx using Submodule.span_induction with
  | mem u hu =>
    obtain ⟨a, b, rfl⟩ := hu
    obtain ⟨c : L, hbc : φ c = ⁅y, φ b⁆⟩ := hy (φ b) (LieHom.mem_range_self φ b)
    replace hbc : ⁅φ b, y⁆ = -φ c := by rw [hbc, Module.End.instLieRingModule_eq, lie_skew]
    rw [LieHom.map_lie, LinearMap.trace_lie_mul_eq, Ring.lie_def,
      ← LieRing.of_associative_ring_bracket, ← Module.End.instLieRingModule_eq, hbc, mul_neg,
      map_neg, neg_eq_zero, Module.End.mul_eq_comp, ← traceForm_apply_apply, h,
      LinearMap.zero_apply, LinearMap.zero_apply]
  | zero => simp
  | add u v _ _ hu hv => simp [add_mul, hu, hv]
  | smul t u _ hu => simp [hu]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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 : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
y : End R M
hy :
  ∀ (z : End R M),
    Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) z →
      Membership.mem (γ := LieSubalgebra R (End R M)) (LieHom.range φ) ⁅y, z⁆
x : L
hx : Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x}) x
mem :
  ∀ (u : L) (hu : Membership.mem (γ := Set L) {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x} u),
    Eq.{u_1 + 1} (α := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) u : End R M) y) :
        R)
      (0 : R)
zero :
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) 0 * y) : R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M) y) :
      R)
    (0 : R)
have add : ∀ (u v : L),
  Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x}) u →
    Membership.mem (γ := Submodule R L) (Submodule.span R {x : L | ∃ (u : L) (v : L), ⁅u, v⁆ = x}) v →
      ∀
        (hu :
          Eq.{u_1 + 1} (α := R)
            ((trace R M : (a : M →ₗ[R] M) → R)
                (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) u : End R M)
                  y) :
              R)
            (0 : R))
        (hv :
          Eq.{u_1 + 1} (α := R)
            ((trace R M : (a : M →ₗ[R] M) → R)
                (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) v : End R M)
                  y) :
              R)
            (0 : R)),
        Eq.{u_1 + 1} (α := R)
          ((trace R M : (a : M →ₗ[R] M) → R)
              (HMul.hMul (α := End R M)
                (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) (u + v) : End R M) y) :
            R)
          (0 : R)
Tactic: induction hx using Submodule.span_induction with
  | mem u hu =>
    obtain ⟨a, b, rfl⟩ := hu
    obtain ⟨c : L, hbc : φ c = ⁅y, φ b⁆⟩ := hy (φ b) (LieHom.mem_range_self φ b)
    replace hbc : ⁅φ b, y⁆ = -φ c := by rw [hbc, Module.End.instLieRingModule_eq, lie_skew]
    rw [LieHom.map_lie, LinearMap.trace_lie_mul_eq, Ring.lie_def,
      ← LieRing.of_associative_ring_bracket, ← Module.End.instLieRingModule_eq, hbc, mul_neg,
      map_neg, neg_eq_zero, Module.End.mul_eq_comp, ← traceForm_apply_apply, h,
      LinearMap.zero_apply, LinearMap.zero_apply]
  | zero => simp
  | add u v _ _ hu hv => simp [add_mul, hu, hv]
  | smul t u _ hu => simp [hu]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : Free R M
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : LieRing.IsNilpotent L
inst_11 : IsNoetherian R M
inst_12 : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank.{u_1, u_4} R ↥(genWeightSpace M χ)
⊢ (((traceForm.{u_1, u_3, u_4} R L ↥(genWeightSpace M χ) : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y =
    d • (χ x * χ y)
have h₁ : χ y • d • χ x - χ y • HSMul.hSMul (β := R) (χ x) (↑d : R) = 0
Tactic: have h₁ : χ y • d • χ x - χ y • χ x • (d : R) = 0 := by simp [mul_comm (χ x)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : Free R M
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : LieRing.IsNilpotent L
inst_11 : IsNoetherian R M
inst_12 : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank.{u_1, u_4} R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • HSMul.hSMul (β := R) (χ x) (↑d : R) = 0
⊢ (((traceForm.{u_1, u_3, u_4} R L ↥(genWeightSpace M χ) : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y =
    d • (χ x * χ y)
have h₂ : χ x • d • χ y = d • (χ x * χ y)
Tactic: have h₂ : χ x • d • χ y = d • (χ x * χ y) := by
    simpa [nsmul_eq_mul, smul_eq_mul] using mul_left_comm (χ x) d (χ y)
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : Free R M
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : LieRing.IsNilpotent L
inst_11 : IsNoetherian R M
inst_12 : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank.{u_1, u_4} R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • HSMul.hSMul (β := R) (χ x) (↑d : R) = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
⊢ (((traceForm.{u_1, u_3, u_4} R L ↥(genWeightSpace M χ) : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y =
    d • (χ x * χ y)
have this : Eq (α := LinearMap.BilinForm R L) (traceForm.{u_1, u_3, u_4} R L ↥(shiftedGenWeightSpace R L M χ)) 0
Tactic: have := traceForm_eq_zero_of_isNilpotent R L (shiftedGenWeightSpace R L M χ)
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : Free R M
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : LieRing.IsNilpotent L
inst_11 : IsNoetherian R M
inst_12 : LinearWeights R L M
χ : L → R
x y : L
d : ℕ := finrank.{u_1, u_4} R ↥(genWeightSpace M χ)
h₁ : χ y • d • χ x - χ y • HSMul.hSMul (β := R) (χ x) (↑d : R) = 0
h₂ : χ x • d • χ y = d • (χ x * χ y)
this : Eq (α := LinearMap.BilinForm R L) (traceForm.{u_1, u_3, u_4} R L ↥(shiftedGenWeightSpace R L M χ)) 0
⊢ (((traceForm.{u_1, u_3, u_4} R L ↥(genWeightSpace M χ) : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y =
    d • (χ x * χ y)
have this₁ : Eq.{u_1 + 1} (α := R)
  ((((traceForm.{u_1, u_3, u_4} R L ↥(shiftedGenWeightSpace R L M χ) : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) :
        (a : L) → R)
      y :
    R)
  ((((0 : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R)
Tactic: replace this := LinearMap.congr_fun (LinearMap.congr_fun this x) y
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
x y : L
hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L 0) x
hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs 0 ⊥) y
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
have hy₁ : y = 0
Tactic: replace hy : y = 0 := by simpa using hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L (k + 1)) x
hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs (k + 1) ⊥) y
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
have hy₁ : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆
Tactic: rw [LieSubmodule.ucs_succ, LieSubmodule.mem_normalizer] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L (k + 1)) x
hy : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
have hx₁ : Membership.mem (γ := Submodule R L)
  (Submodule.span R
    {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
  x
Tactic: simp_rw [LieIdeal.lcs_succ, ← LieSubmodule.mem_toSubmodule,
      LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_top, true_and] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hy : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆
hx :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    x
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
have succ : ∀ (x : L)
  (h :
    Membership.mem (γ := Set L)
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x} x),
  Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
Tactic: refine Submodule.span_induction ?_ ?_ (fun z w _ _ hz hw ↦ ?_) (fun t z _ hz ↦ ?_) hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hy : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆
hx :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    x
succ :
  ∀ (x : L)
    (h :
      Membership.mem (γ := Set L)
        {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x}
        x),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
have succ₁ : Eq.{u_1 + 1} (α := R) (((traceForm R L M : (a : L) → L →ₗ[R] R) 0 : (a : L) → R) y : R) (0 : R)
Tactic: refine Submodule.span_induction ?_ ?_ (fun z w _ _ hz hw ↦ ?_) (fun t z _ hz ↦ ?_) hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hy : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆
hx :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    x
succ :
  ∀ (x : L)
    (h :
      Membership.mem (γ := Set L)
        {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x}
        x),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
succ₁ : Eq.{u_1 + 1} (α := R) (((traceForm R L M : (a : L) → L →ₗ[R] R) 0 : (a : L) → R) y : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
have succ₂ : ∀ (z w : L),
  Membership.mem (γ := Submodule R L)
      (Submodule.span R
        {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
      z →
    Membership.mem (γ := Submodule R L)
        (Submodule.span R
          {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
        w →
      ∀
        (hz :
          Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R))
        (hw :
          Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) w : L →ₗ[R] R) : (a : L) → R) y : R)
            (0 : R)),
        Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) (z + w) : L →ₗ[R] R) : (a : L) → R) y : R)
          (0 : R)
Tactic: refine Submodule.span_induction ?_ ?_ (fun z w _ _ hz hw ↦ ?_) (fun t z _ hz ↦ ?_) hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hy : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆
hx :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    x
succ :
  ∀ (x : L)
    (h :
      Membership.mem (γ := Set L)
        {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x}
        x),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
succ₁ : Eq.{u_1 + 1} (α := R) (((traceForm R L M : (a : L) → L →ₗ[R] R) 0 : (a : L) → R) y : R) (0 : R)
succ₂ :
  ∀ (z w : L),
    Membership.mem (γ := Submodule R L)
        (Submodule.span R
          {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
        z →
      Membership.mem (γ := Submodule R L)
          (Submodule.span R
            {x : L |
              ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
          w →
        ∀
          (hz :
            Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) y : R)
              (0 : R))
          (hw :
            Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) w : L →ₗ[R] R) : (a : L) → R) y : R)
              (0 : R)),
          Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) (z + w) : L →ₗ[R] R) : (a : L) → R) y : R)
            (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
have succ₃ : ∀ (t : R) (z : L),
  Membership.mem (γ := Submodule R L)
      (Submodule.span R
        {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
      z →
    ∀
      (hz :
        Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)),
      Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) (t • z) : L →ₗ[R] R) : (a : L) → R) y : R)
        (0 : R)
Tactic: refine Submodule.span_induction ?_ ?_ (fun z w _ _ hz hw ↦ ?_) (fun t z _ hz ↦ ?_) hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
k : ℕ
ih :
  ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x)
    (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
x y : L
hy : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) ⁅x, y⁆
hx :
  Membership.mem (γ := Submodule R L)
    (Submodule.span R
      {x : L | ∃ (x_1 : L) (n : L), Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) n ∧ ⁅x_1, n⁆ = x})
    x
z w : L
hw : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) w
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅z, w⁆ : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
have succ : Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) w : L →ₗ[R] R) : (a : L) → R) ⁅z, y⁆ : R) (0 : R)
Tactic: rw [← lie_skew, map_neg, LinearMap.neg_apply, neg_eq_zero, traceForm_apply_lie_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
x y : L
k : ℕ
hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L k) x
hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs k ⊥) y
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
have zero : ∀ {x y : L} (hx : Membership.mem (γ := LieSubmodule R L L) (LieIdeal.lcs ⊤ L 0) x)
  (hy : Membership.mem (γ := LieSubmodule R L L) (LieSubmodule.ucs 0 ⊥) y),
  Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
Tactic: induction k generalizing x y with
  | zero =>
    replace hy : y = 0 := by simpa using hy
    simp [hy]
  | succ k ih =>
    rw [LieSubmodule.ucs_succ, LieSubmodule.mem_normalizer] at hy
    simp_rw [LieIdeal.lcs_succ, ← LieSubmodule.mem_toSubmodule,
      LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.mem_top, true_and] at hx
    refine Submodule.span_induction ?_ ?_ (fun z w _ _ hz hw ↦ ?_) (fun t z _ hz ↦ ?_) hx
    · rintro - ⟨z, w, hw, rfl⟩
      rw [← lie_skew, map_neg, LinearMap.neg_apply, neg_eq_zero, traceForm_apply_lie_apply]
      exact ih hw (hy _)
    · simp
    · simp [hz, hw]
    · simp [hz]
Cleared hypotheses: x, y, k, hx, hy