awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
y : L
m : M
hm :
  ∀ (k : ℕ),
    ∃ (n : M),
      (HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y :
                Module.End R M)
              k :
            (a : M) → M)
          n =
        m
⊢ m ∈ LieSubmodule.comap f (posFittingCompOf R M₂ y)
have simp : ∀ (k : ℕ),
  ∃ (n : M₂),
    Eq (α := M₂)
      ((HPow.hPow (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) y :
                Module.End R M₂)
              k :
            (a : M₂) → M₂)
          n :
        M₂)
      ((f : (a : M) → M₂) m : M₂)
Tactic: simp only [LieSubmodule.mem_comap, mem_posFittingCompOf]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
y : L
m : M
hm :
  ∀ (k : ℕ),
    ∃ (n : M),
      (HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y :
                Module.End R M)
              k :
            (a : M) → M)
          n =
        m
k : ℕ
⊢ ∃ (n : M₂),
    Eq (α := M₂)
      ((HPow.hPow (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) y :
                Module.End R M₂)
              k :
            (a : M₂) → M₂)
          n :
        M₂)
      ((f : (a : M) → M₂) m : M₂)
have obtain : ∀ (n : M)
  (hn :
    (HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y :
              Module.End R M)
            k :
          (a : M) → M)
        n =
      m),
  ∃ (n : M₂),
    Eq (α := M₂)
      ((HPow.hPow (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) y :
                Module.End R M₂)
              k :
            (a : M₂) → M₂)
          n :
        M₂)
      ((f : (a : M) → M₂) m : M₂)
Tactic: obtain ⟨n, hn⟩ := hm k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
y : L
m : M
hm :
  ∀ (k : ℕ),
    ∃ (n : M),
      (HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y :
                Module.End R M)
              k :
            (a : M) → M)
          n =
        m
k : ℕ
n : M
hn :
  (HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
          k :
        (a : M) → M)
      n =
    m
⊢ ∃ (n : M₂),
    Eq (α := M₂)
      ((HPow.hPow (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) y :
                Module.End R M₂)
              k :
            (a : M₂) → M₂)
          n :
        M₂)
      ((f : (a : M) → M₂) m : M₂)
have h : Eq (α := M₂)
  ((HPow.hPow (α := Module.End R M₂)
          (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) y :
            Module.End R M₂)
          k :
        (a : M₂) → M₂)
      ((f : (a : M) → M₂) n : M₂) :
    M₂)
  ((f : (a : M) → M₂) m : M₂)
Tactic: use f n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
y : L
m : M
hm :
  ∀ (k : ℕ),
    ∃ (n : M),
      (HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y :
                Module.End R M)
              k :
            (a : M) → M)
          n =
        m
k : ℕ
n : M
hn :
  (HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
          k :
        (a : M) → M)
      n =
    m
⊢ Eq (α := M₂)
    ((HPow.hPow (α := Module.End R M₂)
            (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) y :
              Module.End R M₂)
            k :
          (a : M₂) → M₂)
        ((f : (a : M) → M₂) n : M₂) :
      M₂)
    ((f : (a : M) → M₂) m : M₂)
have h : Eq.{u_5 + 1} (α := M₂)
  ((f : (a : M) → M₂)
      ((HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y :
                Module.End R M)
              k :
            (a : M) → M)
          n :
        M) :
    M₂)
  ((f : (a : M) → M₂) m : M₂)
Tactic: rw [LieModule.toEnd_pow_apply_map, hn]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
y : L
m : M
hm :
  ∀ (k : ℕ),
    ∃ (n : M),
      (HPow.hPow (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y :
                Module.End R M)
              k :
            (a : M) → M)
          n =
        m
k : ℕ
n : M
hn :
  (HPow.hPow (α := Module.End R M)
          (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
          k :
        (a : M) → M)
      n =
    m
h :
  Eq.{u_5 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        ((HPow.hPow (α := Module.End R M)
                (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y :
                  Module.End R M)
                k :
              (a : M) → M)
            n :
          M) :
      M₂)
    ((f : (a : M) → M₂) m : M₂)
⊢ Eq (α := M₂)
    ((HPow.hPow (α := Module.End R M₂)
            (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) y :
              Module.End R M₂)
            k :
          (a : M₂) → M₂)
        ((f : (a : M) → M₂) n : M₂) :
      M₂)
    ((f : (a : M) → M₂) m : M₂)
have h₁ : Eq.{u_5 + 1} (α := M₂) ((f : (a : M) → M₂) m : M₂) ((f : (a : M) → M₂) m : M₂)
Tactic: rw [LieModule.toEnd_pow_apply_map, hn]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
⊢ LieSubmodule.map f (genWeightSpace M χ) ≤ genWeightSpace M₂ χ
have rw : genWeightSpace M χ ≤ LieSubmodule.comap f (genWeightSpace M₂ χ)
Tactic: rw [LieSubmodule.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
⊢ m ∈ LieSubmodule.comap f (genWeightSpace M₂ χ)
have simp : ∀ (x : L),
  ∃ (k : ℕ),
    Eq (α := M₂)
      ((HSub.hSub (α := Module.End R M₂)
                (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                  Module.End R M₂)
                (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
              k :
            (a : M₂) → M₂)
          ((f : (a : M) → M₂) m : M₂) :
        M₂)
      (0 : M₂)
Tactic: simp only [LieSubmodule.mem_comap, mem_genWeightSpace]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
x : L
⊢ HSub.hSub (α := Module.End R M₂)
        (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
          Module.End R M₂)
        (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ∘ₗ
      (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ
      HSub.hSub (α := Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        (HSMul.hSMul (β := Module.End R M) (χ x) 1)
have h : ∀ (x_1 : M),
  Eq.{u_5 + 1} (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ∘ₗ
            (↑f : M →ₗ[R] M₂) :
          (a : M) → M₂)
        x_1 :
      M₂)
    (((↑f : M →ₗ[R] M₂) ∘ₗ
            HSub.hSub (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                Module.End R M)
              (HSMul.hSMul (β := Module.End R M) (χ x) 1) :
          (a : M) → M₂)
        x_1 :
      M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
x : L
⊢ ∃ (k : ℕ),
    Eq (α := M₂)
      ((HSub.hSub (α := Module.End R M₂)
                (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                  Module.End R M₂)
                (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
              k :
            (a : M₂) → M₂)
          ((f : (a : M) → M₂) m : M₂) :
        M₂)
      (0 : M₂)
have this : HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ∘ₗ
    (↑f : M →ₗ[R] M₂) =
  (↑f : M →ₗ[R] M₂) ∘ₗ
    HSub.hSub (α := Module.End R M)
      (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
      (HSMul.hSMul (β := Module.End R M) (χ x) 1)
Tactic: have : (toEnd R L M₂ x - χ x • ↑1) ∘ₗ f = f ∘ₗ (toEnd R L M x - χ x • ↑1) := by
    ext; simp
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
x : L
this :
  HSub.hSub (α := Module.End R M₂)
        (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
          Module.End R M₂)
        (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ∘ₗ
      (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ
      HSub.hSub (α := Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        (HSMul.hSMul (β := Module.End R M) (χ x) 1)
⊢ ∃ (k : ℕ),
    Eq (α := M₂)
      ((HSub.hSub (α := Module.End R M₂)
                (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                  Module.End R M₂)
                (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
              k :
            (a : M₂) → M₂)
          ((f : (a : M) → M₂) m : M₂) :
        M₂)
      (0 : M₂)
have obtain : ∀ (k : ℕ)
  (h :
    Eq (α := M)
      ((HSub.hSub (α := Module.End R M)
                (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                  Module.End R M)
                (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
              k :
            (a : M) → M)
          m :
        M)
      (0 : M)),
  ∃ (k : ℕ),
    Eq (α := M₂)
      ((HSub.hSub (α := Module.End R M₂)
                (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                  Module.End R M₂)
                (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
              k :
            (a : M₂) → M₂)
          ((f : (a : M) → M₂) m : M₂) :
        M₂)
      (0 : M₂)
Tactic: obtain ⟨k, h⟩ := (mem_genWeightSpace _ _ _).mp hm x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
m : M
hm : Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
x : L
this :
  HSub.hSub (α := Module.End R M₂)
        (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
          Module.End R M₂)
        (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ∘ₗ
      (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ
      HSub.hSub (α := Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        (HSMul.hSMul (β := Module.End R M) (χ x) 1)
k : ℕ
h :
  Eq (α := M)
    ((HSub.hSub (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                Module.End R M)
              (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
            k :
          (a : M) → M)
        m :
      M)
    (0 : M)
⊢ ∃ (k : ℕ),
    Eq (α := M₂)
      ((HSub.hSub (α := Module.End R M₂)
                (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                  Module.End R M₂)
                (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
              k :
            (a : M₂) → M₂)
          ((f : (a : M) → M₂) m : M₂) :
        M₂)
      (0 : M₂)
have refine : Eq (α := M₂)
  ((HSub.hSub (α := Module.End R M₂)
            (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
              Module.End R M₂)
            (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
          k :
        (a : M₂) → M₂)
      ((f : (a : M) → M₂) m : M₂) :
    M₂)
  (0 : M₂)
Tactic: refine ⟨k, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ LieSubmodule.comap f (genWeightSpace M₂ χ) = genWeightSpace M χ
have refine_1 : ∀ (m : M) (hm : m ∈ LieSubmodule.comap f (genWeightSpace M₂ χ)),
  Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
Tactic: refine le_antisymm (fun m hm ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
refine_1 :
  ∀ (m : M) (hm : m ∈ LieSubmodule.comap f (genWeightSpace M₂ χ)),
    Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
⊢ LieSubmodule.comap f (genWeightSpace M₂ χ) = genWeightSpace M χ
have refine_2 : genWeightSpace M χ ≤ LieSubmodule.comap f (genWeightSpace M₂ χ)
Tactic: refine le_antisymm (fun m hm ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (hypothesis)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
m : M
hm : m ∈ LieSubmodule.comap f (genWeightSpace M₂ χ)
⊢ Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
have hm₁ : ∀ (x : L),
  ∃ (k : ℕ),
    Eq (α := M₂)
      ((HSub.hSub (α := Module.End R M₂)
                (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                  Module.End R M₂)
                (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
              k :
            (a : M₂) → M₂)
          ((f : (a : M) → M₂) m : M₂) :
        M₂)
      (0 : M₂)
Tactic: simp only [LieSubmodule.mem_comap, mem_genWeightSpace] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
m : M
hm :
  ∀ (x : L),
    ∃ (k : ℕ),
      Eq (α := M₂)
        ((HSub.hSub (α := Module.End R M₂)
                  (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                    Module.End R M₂)
                  (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
                k :
              (a : M₂) → M₂)
            ((f : (a : M) → M₂) m : M₂) :
          M₂)
        (0 : M₂)
⊢ Membership.mem (γ := LieSubmodule R L M) (genWeightSpace M χ) m
have refine_1 : ∀ (x : L),
  ∃ (k : ℕ),
    Eq (α := M)
      ((HSub.hSub (α := Module.End R M)
                (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                  Module.End R M)
                (HSMul.hSMul (β := Module.End R M) (χ x) 1) ^
              k :
            (a : M) → M)
          m :
        M)
      (0 : M)
Tactic: simp only [mem_genWeightSpace]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Basic (goal)
Goal:
R : Type u_2
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 : LieRing.IsNilpotent L
M₂ : Type u_5
inst_8 : AddCommGroup M₂
inst_9 : Module R M₂
inst_10 : LieRingModule L M₂
inst_11 : LieModule R L M₂
χ : L → R
f : M →ₗ⁅R,L⁆ M₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
m : M
hm :
  ∀ (x : L),
    ∃ (k : ℕ),
      Eq (α := M₂)
        ((HSub.hSub (α := Module.End R M₂)
                  (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                    Module.End R M₂)
                  (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ^
                k :
              (a : M₂) → M₂)
            ((f : (a : M) → M₂) m : M₂) :
          M₂)
        (0 : M₂)
x : L
⊢ HSub.hSub (α := Module.End R M₂)
        (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
          Module.End R M₂)
        (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ∘ₗ
      (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ
      HSub.hSub (α := Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        (HSMul.hSMul (β := Module.End R M) (χ x) 1)
have h : ∀ (x_1 : M),
  Eq.{u_5 + 1} (α := M₂)
    ((HSub.hSub (α := Module.End R M₂)
              (((toEnd R L M₂ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x :
                Module.End R M₂)
              (HSMul.hSMul (β := Module.End R M₂) (χ x) 1) ∘ₗ
            (↑f : M →ₗ[R] M₂) :
          (a : M) → M₂)
        x_1 :
      M₂)
    (((↑f : M →ₗ[R] M₂) ∘ₗ
            HSub.hSub (α := Module.End R M)
              (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x :
                Module.End R M)
              (HSMul.hSMul (β := Module.End R M) (χ x) 1) :
          (a : M) → M₂)
        x_1 :
      M₂)
Tactic: ext