awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ IsLieAbelian.{v}
    ↥(match (motive := ℕ → LieIdeal R L) derivedLengthOfIdeal R L I with
        | 0 => ⊥
        | k.succ => derivedSeriesOfIdeal R L k I :
        LieIdeal R L)
have zero : ∀ (h : derivedLengthOfIdeal R L I = 0),
  IsLieAbelian.{v}
    ↥(match (motive := ℕ → LieIdeal R L) 0 with
        | 0 => ⊥
        | k.succ => derivedSeriesOfIdeal R L k I :
        LieIdeal R L)
Tactic: rcases h : derivedLengthOfIdeal R L I with - | k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
zero :
  ∀ (h : derivedLengthOfIdeal R L I = 0),
    IsLieAbelian.{v}
      ↥(match (motive := ℕ → LieIdeal R L) 0 with
          | 0 => ⊥
          | k.succ => derivedSeriesOfIdeal R L k I :
          LieIdeal R L)
⊢ IsLieAbelian.{v}
    ↥(match (motive := ℕ → LieIdeal R L) derivedLengthOfIdeal R L I with
        | 0 => ⊥
        | k.succ => derivedSeriesOfIdeal R L k I :
        LieIdeal R L)
have succ : ∀ (k : ℕ) (h : derivedLengthOfIdeal R L I = k + 1),
  IsLieAbelian.{v}
    ↥(match (motive := ℕ → LieIdeal R L) k + 1 with
        | 0 => ⊥
        | k.succ => derivedSeriesOfIdeal R L k I :
        LieIdeal R L)
Tactic: rcases h : derivedLengthOfIdeal R L I with - | k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
k : ℕ
h : derivedLengthOfIdeal R L I = k + 1
⊢ IsLieAbelian.{v}
    ↥(match (motive := ℕ → LieIdeal R L) k + 1 with
        | 0 => ⊥
        | k.succ => derivedSeriesOfIdeal R L k I :
        LieIdeal R L)
have h₁ : IsLieAbelian.{v} ↥(derivedSeriesOfIdeal R L k I) ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
Tactic: rw [derivedSeries_of_derivedLength_succ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
inst_3 : IsSolvable.{v} ↥I
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
⊢ derivedLengthOfIdeal R L I = 0 ↔ I = ⊥
have change : sInf s = 0 ↔ I = ⊥
Tactic: change sInf s = 0 ↔ _
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
inst_3 : IsSolvable.{v} ↥I
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
hk : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥
⊢ k ∈ s
have rwa : ∀ (hk : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeriesOfIdeal R (↥I) k ⊤) ⊥), k ∈ s
Tactic: rwa [derivedSeries_def, LieIdeal.derivedSeries_eq_bot_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
inst_3 : IsSolvable.{v} ↥I
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
hk : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeries R (↥I) k) ⊥
rwa : ∀ (hk : Eq.{v + 1} (α := LieIdeal R ↥I) (derivedSeriesOfIdeal R (↥I) k ⊤) ⊥), k ∈ s
⊢ k ∈ s
have rwa₁ : ∀ (hk : derivedSeriesOfIdeal R L k I = ⊥), k ∈ s
Tactic: rwa [derivedSeries_def, LieIdeal.derivedSeries_eq_bot_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
inst_3 : IsSolvable.{v} ↥I
s : Set ℕ := {k : ℕ | derivedSeriesOfIdeal R L k I = ⊥}
⊢ sInf s = 0 ↔ I = ⊥
have hne : s.Nonempty
Tactic: have hne : s.Nonempty :=
    have ⟨k, hk⟩ := IsSolvable.solvable R I
    ⟨k, by rwa [derivedSeries_def, LieIdeal.derivedSeries_eq_bot_iff] at hk⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h : IsSolvable.{v} ↥I
⊢ Eq.{v + 1} (α := LieIdeal R L)
      (match (motive := ℕ → LieIdeal R L) derivedLengthOfIdeal R L I with
        | 0 => ⊥
        | k.succ => derivedSeriesOfIdeal R L k I :
        LieIdeal R L)
      (⊥ : LieIdeal R L) ↔
    I = ⊥
have h_1 : ∀ (x : ℕ), derivedLengthOfIdeal R L I = 0 → (Eq.{v + 1} (α := LieIdeal R L) ⊥ ⊥ ↔ I = ⊥)
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h : IsSolvable.{v} ↥I
h_1 : ∀ (x : ℕ), derivedLengthOfIdeal R L I = 0 → (Eq.{v + 1} (α := LieIdeal R L) ⊥ ⊥ ↔ I = ⊥)
⊢ Eq.{v + 1} (α := LieIdeal R L)
      (match (motive := ℕ → LieIdeal R L) derivedLengthOfIdeal R L I with
        | 0 => ⊥
        | k.succ => derivedSeriesOfIdeal R L k I :
        LieIdeal R L)
      (⊥ : LieIdeal R L) ↔
    I = ⊥
have h_2 : ∀ (x k : ℕ), derivedLengthOfIdeal R L I = k.succ → (derivedSeriesOfIdeal R L k I = ⊥ ↔ I = ⊥)
Tactic: split
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h_1 : IsSolvable.{v} ↥I
x k : ℕ
h : derivedLengthOfIdeal R L I = k.succ
⊢ derivedSeriesOfIdeal R L k I = ⊥ ↔ I = ⊥
have left : IsLieAbelian.{v} ↥(derivedSeriesOfIdeal R L k I)
Tactic: obtain ⟨_, h₂⟩ := (derivedSeries_of_derivedLength_succ R L I k).mp h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h_1 : IsSolvable.{v} ↥I
x k : ℕ
h : derivedLengthOfIdeal R L I = k.succ
left : IsLieAbelian.{v} ↥(derivedSeriesOfIdeal R L k I)
⊢ derivedSeriesOfIdeal R L k I = ⊥ ↔ I = ⊥
have h₂ : derivedSeriesOfIdeal R L k I ≠ ⊥
Tactic: obtain ⟨_, h₂⟩ := (derivedSeries_of_derivedLength_succ R L I k).mp h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x k : ℕ
h_1 : IsSolvable.{v} ↥⊥
h : derivedLengthOfIdeal R L ⊥ = k.succ
left : IsLieAbelian.{v} ↥(derivedSeriesOfIdeal R L k ⊥)
h₂ : Ne (α := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊥) ⊥
⊢ False
have apply : Eq (α := LieIdeal R L) (derivedSeriesOfIdeal R L k ⊥) ⊥
Tactic: apply h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Solvable (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h_1 : IsSolvable.{v} ↥I
x k : ℕ
h : derivedLengthOfIdeal R L I = k.succ
left : IsLieAbelian.{v} ↥(derivedSeriesOfIdeal R L k I)
h₂ : derivedSeriesOfIdeal R L k I ≠ ⊥
⊢ derivedSeriesOfIdeal R L k I = ⊥ ↔ I = ⊥
have h₃ : I ≠ ⊥
Tactic: have h₃ : I ≠ ⊥ := by rintro rfl; apply h₂; apply derivedSeries_of_bot_eq_bot
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y : L
hx :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, v} (R := R) 0))) x
_hy :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, v} (R := R) 0))) y
⊢ Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, v} (R := R) 0))) ⁅x, y⁆
have rw : Membership.mem (γ := Set L)
  (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid.{u, v} (R := R) 0))) 0
Tactic: rw [(Submodule.mem_bot R).1 hx, zero_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' L'' : LieSubalgebra R L
h :
  Eq.{v + 1} (α := Set L) ((fun (L' : LieSubalgebra R L) ↦ L'.carrier) L')
    ((fun (L' : LieSubalgebra R L) ↦ L'.carrier) L'')
⊢ L' = L''
have rcases : ∀ (toAddSubmonoid : AddSubmonoid L)
  (smul_mem' : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier)
  (lie_mem' :
    ∀ {x y : L},
      x ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier →
        y ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier →
          ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier)
  (h :
    Eq.{v + 1} (α := Set L)
      ((fun (L' : LieSubalgebra R L) ↦ L'.carrier)
        { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' })
      ((fun (L' : LieSubalgebra R L) ↦ L'.carrier) L'')),
  { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' : LieSubalgebra R L } = L''
Tactic: rcases L' with ⟨⟨⟩⟩
Cleared hypotheses: L', h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L'' : LieSubalgebra R L
toAddSubmonoid : AddSubmonoid L
smul_mem' : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier
lie_mem' :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier
h :
  Eq.{v + 1} (α := Set L)
    ((fun (L' : LieSubalgebra R L) ↦ L'.carrier)
      { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' })
    ((fun (L' : LieSubalgebra R L) ↦ L'.carrier) L'')
⊢ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' : LieSubalgebra R L } = L''
have rcases : ∀ (toAddSubmonoid_1 : AddSubmonoid L)
  (smul_mem'_1 : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid_1.carrier → c • x ∈ toAddSubmonoid_1.carrier)
  (lie_mem'_1 :
    ∀ {x y : L},
      x ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier →
        y ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier →
          ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier)
  (h :
    Eq.{v + 1} (α := Set L)
      ((fun (L' : LieSubalgebra R L) ↦ L'.carrier)
        { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' })
      ((fun (L' : LieSubalgebra R L) ↦ L'.carrier)
        { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1, lie_mem' := @lie_mem'_1 })),
  { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' : LieSubalgebra R L } =
    { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1, lie_mem' := @lie_mem'_1 }
Tactic: rcases L'' with ⟨⟨⟩⟩
Cleared hypotheses: L'', h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
toAddSubmonoid : AddSubmonoid L
smul_mem' : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier
lie_mem' :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R L }.carrier
toAddSubmonoid_1 : AddSubmonoid L
smul_mem'_1 : ∀ (c : R) {x : L}, x ∈ toAddSubmonoid_1.carrier → c • x ∈ toAddSubmonoid_1.carrier
lie_mem'_1 :
  ∀ {x y : L},
    x ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier →
      y ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier →
        ⁅x, y⁆ ∈ { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 : Submodule R L }.carrier
h :
  Eq.{v + 1} (α := Set L)
    ((fun (L' : LieSubalgebra R L) ↦ L'.carrier)
      { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' })
    ((fun (L' : LieSubalgebra R L) ↦ L'.carrier)
      { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1, lie_mem' := @lie_mem'_1 })
⊢ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem', lie_mem' := @lie_mem' : LieSubalgebra R L } =
    { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1, lie_mem' := @lie_mem'_1 }
have e_toSubmodule : toAddSubmonoid = toAddSubmonoid_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
x y z : ↥L'
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑(x + y) : L), (↑z : L)⁆ ⋯ =
    Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑z : L)⁆ ⋯ +
      Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑y : L), (↑z : L)⁆ ⋯
have a : (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑(x + y) : L), (↑z : L)⁆ sorry) : L) =
  (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑z : L)⁆ sorry +
        Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑y : L), (↑z : L)⁆ sorry) :
    L)
Tactic: apply SetCoe.ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
x y z : ↥L'
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑(y + z) : L)⁆ ⋯ =
    Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑y : L)⁆ ⋯ +
      Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑z : L)⁆ ⋯
have a : (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑(y + z) : L)⁆ sorry) : L) =
  (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑y : L)⁆ sorry +
        Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑z : L)⁆ sorry) :
    L)
Tactic: apply SetCoe.ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
x : ↥L'
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑x : L)⁆ ⋯ = 0
have a : (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑x : L)⁆ sorry) : L) = (↑0 : L)
Tactic: apply SetCoe.ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
x y z : ↥L'
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ L')
      ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑y : L), (↑z : L)⁆ ⋯) : L)⁆ ⋯ =
    Subtype.mk (p := fun (x : L) ↦ x ∈ L')
        ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑y : L)⁆ ⋯) : L), (↑z : L)⁆ ⋯ +
      Subtype.mk (p := fun (x : L) ↦ x ∈ L')
        ⁅(↑y : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑z : L)⁆ ⋯) : L)⁆ ⋯
have a : (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L')
        ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑y : L), (↑z : L)⁆ sorry) : L)⁆ sorry) :
    L) =
  (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L')
          ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑y : L)⁆ sorry) : L), (↑z : L)⁆ sorry +
        Subtype.mk (p := fun (x : L) ↦ x ∈ L')
          ⁅(↑y : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ L') ⁅(↑x : L), (↑z : L)⁆ sorry) : L)⁆ sorry) :
    L)
Tactic: apply SetCoe.ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
t : R
x y : ↥L'
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆
have a : (↑⁅x, t • y⁆ : L) = (↑(t • ⁅x, y⁆) : L)
Tactic: apply SetCoe.ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
apply : ∀ (t : R) (x y : ↥L'), ⁅x, t • y⁆ = t • ⁅x, y⁆
⊢ ∀ (t : R) (x y : ↥L'), ⁅x, t • y⁆ = t • ⁅x, y⁆
have a : ∀ (t : R) (x y : ↥L'), (↑⁅x, t • y⁆ : L) = (↑(t • ⁅x, y⁆) : L)
Tactic: { intros
      apply SetCoe.ext
      apply lie_smul }
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L₁' L₂' : LieSubalgebra R L
h : L₁'.toSubmodule = L₂'.toSubmodule
⊢ L₁' = L₂'
have h₁ : (↑L₁'.toSubmodule : Set L) = (↑L₂'.toSubmodule : Set L)
Tactic: rw [SetLike.ext'_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L₁' L₂' : LieSubalgebra R L
h : (↑L₁'.toSubmodule : Set L) = (↑L₂'.toSubmodule : Set L)
⊢ L₁' = L₂'
have rw : (↑L₁' : Set L) = (↑L₂' : Set L)
Tactic: rw [← coe_set_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
M : Type w
inst_3 : AddCommGroup M
inst_4 : LieRingModule L M
N : Type w₁
inst_5 : AddCommGroup N
inst_6 : LieRingModule L N
inst_7 : Module R N
inst_8 : Module R M
inst_9 : LieModule R L M
t : R
x : ↥L'
m : M
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆
have rw : ⁅(↑(t • x) : L), m⁆ = t • ⁅x, m⁆
Tactic: rw [coe_bracket_of_module, Submodule.coe_smul_of_tower, smul_lie, coe_bracket_of_module]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
M : Type w
inst_3 : AddCommGroup M
inst_4 : LieRingModule L M
N : Type w₁
inst_5 : AddCommGroup N
inst_6 : LieRingModule L N
inst_7 : Module R N
inst_8 : Module R M
inst_9 : LieModule R L M
t : R
x : ↥L'
m : M
rw : ⁅(↑(t • x) : L), m⁆ = t • ⁅x, m⁆
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆
have rw₁ : ⁅t • (↑x : L), m⁆ = t • ⁅x, m⁆
Tactic: rw [coe_bracket_of_module, Submodule.coe_smul_of_tower, smul_lie, coe_bracket_of_module]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
M : Type w
inst_3 : AddCommGroup M
inst_4 : LieRingModule L M
N : Type w₁
inst_5 : AddCommGroup N
inst_6 : LieRingModule L N
inst_7 : Module R N
inst_8 : Module R M
inst_9 : LieModule R L M
t : R
x : ↥L'
m : M
rw : ⁅(↑(t • x) : L), m⁆ = t • ⁅x, m⁆
rw₁ : ⁅t • (↑x : L), m⁆ = t • ⁅x, m⁆
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆
have rw₂ : t • ⁅(↑x : L), m⁆ = t • ⁅x, m⁆
Tactic: rw [coe_bracket_of_module, Submodule.coe_smul_of_tower, smul_lie, coe_bracket_of_module]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L' : LieSubalgebra R L
M : Type w
inst_3 : AddCommGroup M
inst_4 : LieRingModule L M
N : Type w₁
inst_5 : AddCommGroup N
inst_6 : LieRingModule L N
inst_7 : Module R N
inst_8 : Module R M
inst_9 : LieModule R L M
t : R
x : ↥L'
m : M
rw : ⁅(↑(t • x) : L), m⁆ = t • ⁅x, m⁆
rw₁ : ⁅t • (↑x : L), m⁆ = t • ⁅x, m⁆
rw₂ : t • ⁅(↑x : L), m⁆ = t • ⁅x, m⁆
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆
have rw₃ : t • ⁅(↑x : L), m⁆ = t • ⁅(↑x : L), m⁆
Tactic: rw [coe_bracket_of_module, Submodule.coe_smul_of_tower, smul_lie, coe_bracket_of_module]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x y : L
⊢ Eq (α := ↥f.range)
    (AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) ⁅x, y⁆ : ↥(↑f : L →ₗ[R] L₂).range)
    (Bracket.bracket (L := ↥f.range)
      (AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) x : ↥(↑f : L →ₗ[R] L₂).range)
      (AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) y))
have a : (↑(AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) ⁅x, y⁆) : L₂) =
  (↑(Bracket.bracket (L := ↥f.range)
        (AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) x : ↥(↑f : L →ₗ[R] L₂).range)
        (AddHom.toFun (LinearMap.toAddHom (↑f : L →ₗ[R] L₂).rangeRestrict) y)) :
    L₂)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy : y ∈ f.range
⊢ ∃ (a : L), (f.rangeRestrict : (a : L) → ↥f.range) a = Subtype.mk (p := fun (x : L₂) ↦ x ∈ f.range) y hy
have hy₁ : ∃ (y_1 : L), (f : (a : L) → L₂) y_1 = y
Tactic: rw [mem_range] at hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
y : L₂
hy_1 : y ∈ f.range
hy : ∃ (y_1 : L), (f : (a : L) → L₂) y_1 = y
⊢ ∃ (a : L), (f.rangeRestrict : (a : L) → ↥f.range) a = Subtype.mk (p := fun (x : L₂) ↦ x ∈ f.range) y hy_1
have obtain : ∀ (x : L) (hy : Membership.mem (α := L₂) f.range ((f : (a : L) → L₂) x : L₂)),
  ∃ (a : L),
    Eq.{w + 1} (α := ↥f.range) ((f.rangeRestrict : (a : L) → ↥f.range) a : ↥f.range)
      (Subtype.mk (p := fun (x : L₂) ↦ x ∈ f.range) ((f : (a : L) → L₂) x) hy : ↥f.range)
Tactic: obtain ⟨x, rfl⟩ := hy
Cleared hypotheses: y, hy_1, hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
x : L
hy : Membership.mem (α := L₂) f.range ((f : (a : L) → L₂) x : L₂)
⊢ ∃ (a : L),
    Eq.{w + 1} (α := ↥f.range) ((f.rangeRestrict : (a : L) → ↥f.range) a : ↥f.range)
      (Subtype.mk (p := fun (x : L₂) ↦ x ∈ f.range) ((f : (a : L) → L₂) x) hy : ↥f.range)
have h : Eq.{w + 1} (α := ↥f.range) ((f.rangeRestrict : (a : L) → ↥f.range) x : ↥f.range)
  (Subtype.mk (p := fun (x : L₂) ↦ x ∈ f.range) ((f : (a : L) → L₂) x) hy : ↥f.range)
Tactic: use x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
h : Function.Injective.{v + 1, w + 1} (α := L) (β := L₂) (⇑f : (a : L) → L₂)
x y : L
hxy :
  Eq.{w + 1} (α := ↥f.range) ((f.rangeRestrict : (a : L) → ↥f.range) x : ↥f.range)
    ((f.rangeRestrict : (a : L) → ↥f.range) y : ↥f.range)
⊢ x = y
have hxy₁ : Eq.{w + 1} (α := L₂) ((f : (a : L) → L₂) x : L₂) ((f : (a : L) → L₂) y : L₂)
Tactic: simp only [Subtype.mk_eq_mk, rangeRestrict_apply] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
p : Submodule R L
⊢ (∃ (K : LieSubalgebra R L), K.toSubmodule = p) ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
have mp : (∃ (K : LieSubalgebra R L), K.toSubmodule = p) → ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
p : Submodule R L
mp : (∃ (K : LieSubalgebra R L), K.toSubmodule = p) → ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ (∃ (K : LieSubalgebra R L), K.toSubmodule = p) ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
have mpr : (∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p) → ∃ (K : LieSubalgebra R L), K.toSubmodule = p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ ∃ (K : LieSubalgebra R L), K.toSubmodule = p
have w : LieSubalgebra R L
Tactic: use { p with lie_mem' := h _ _ }
-- Lean 4 proof step from Mathlib.Algebra.Lie.Subalgebra (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
w : LieSubalgebra R L
⊢ ∃ (K : LieSubalgebra R L), K.toSubmodule = p
have h₁ : { toSubmodule := p, lie_mem' := sorry : LieSubalgebra R L }.toSubmodule = p
Tactic: use { p with lie_mem' := h _ _ }