awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
K : LieSubalgebra R L
⊢ K.incl.range = K
have rw : K.incl.range.toSubmodule = K.toSubmodule
Tactic: rw [← toSubmodule_inj]
-- 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₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x y : L₂
hx : x ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
hy : y ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
⊢ ⁅x, y⁆ ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
have hx₁ : x ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).toAddSubsemigroup
Tactic: simp only [AddSubsemigroup.mem_carrier] at hx hy
Cleared hypotheses: hx, hy
-- 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₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x y : L₂
hx : x ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
hy : y ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
hx₁ : x ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).toAddSubsemigroup
⊢ ⁅x, y⁆ ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
have hy₁ : y ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).toAddSubsemigroup
Tactic: simp only [AddSubsemigroup.mem_carrier] at hx hy
Cleared hypotheses: hx, 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₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x y : L₂
hx : x ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).toAddSubsemigroup
hy : y ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).toAddSubsemigroup
⊢ ⁅x, y⁆ ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
have rcases : ∀ (x' : L) (hx' : x' ∈ (↑K.toSubmodule : Set L)),
  Bracket.bracket (L := L₂) (((↑f : L →ₗ[R] L₂) : (a : L) → L₂) x' : L₂) y ∈
    (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
Tactic: rcases hx with ⟨x', hx', rfl⟩
Cleared hypotheses: x, hx
-- 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₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
y : L₂
hy : y ∈ (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).toAddSubsemigroup
x' : L
hx' : x' ∈ (↑K.toSubmodule : Set L)
⊢ Bracket.bracket (L := L₂) (((↑f : L →ₗ[R] L₂) : (a : L) → L₂) x' : L₂) y ∈
    (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
have rcases : ∀ (y' : L) (hy' : y' ∈ (↑K.toSubmodule : Set L)),
  Membership.mem (α := L₂) (Submodule.map (↑f : L →ₗ[R] L₂) K.toSubmodule).carrier
    (Bracket.bracket (L := L₂) (((↑f : L →ₗ[R] L₂) : (a : L) → L₂) x' : L₂) (((↑f : L →ₗ[R] L₂) : (a : L) → L₂) y') :
      L₂)
Tactic: rcases hy with ⟨y', hy', rfl⟩
Cleared hypotheses: y, 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₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x y : L
hx : x ∈ (Submodule.comap (↑f : L →ₗ[R] L₂) K₂.toSubmodule).carrier
hy : y ∈ (Submodule.comap (↑f : L →ₗ[R] L₂) K₂.toSubmodule).carrier
⊢ ⁅x, y⁆ ∈ (Submodule.comap (↑f : L →ₗ[R] L₂) K₂.toSubmodule).carrier
have suffices : Membership.mem (α := L₂) K₂ (Bracket.bracket (L := L₂) ((f : (a : L) → L₂) x : L₂) ((f : (a : L) → L₂) y) : L₂)
Tactic: suffices ⁅f x, f y⁆ ∈ K₂ by simp [this]
-- 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₂
⊢ f.range = map f ⊤
have h : ∀ (x : L₂), x ∈ f.range ↔ x ∈ map f ⊤
Tactic: 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₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
x y : L
hx :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u, v} (R := R) (sInf {x : Submodule R L | ∃ s ∈ S, s.toSubmodule = x}))))
    x
hy :
  Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u, v} (R := R) (sInf {x : Submodule R L | ∃ s ∈ S, s.toSubmodule = x}))))
    y
⊢ Membership.mem (γ := Set L)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u, v} (R := R) (sInf {x : Submodule R L | ∃ s ∈ S, s.toSubmodule = x}))))
    ⁅x, y⁆
have simp : ∀ (hx : ∀ a ∈ S, x ∈ (↑a.toSubmodule : Set L)) (hy : ∀ a ∈ S, y ∈ (↑a.toSubmodule : Set L)),
  ∀ a ∈ S, ⁅x, y⁆ ∈ (↑a.toSubmodule : Set L)
Tactic: simp only [Submodule.mem_carrier, mem_iInter, Submodule.coe_sInf, mem_setOf_eq,
          forall_apply_eq_imp_iff₂, exists_imp, and_imp] at hx hy ⊢
Cleared hypotheses: hx, 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
S : Set (LieSubalgebra R L)
⊢ Eq.{v + 1} (α := Set L)
    (⋂ (p : Submodule R L),
      ⋂ (_ : Membership.mem (γ := Set (Submodule R L)) {x : Submodule R L | ∃ s ∈ S, s.toSubmodule = x} p),
        (↑p : Set L))
    (⋂ s ∈ S, (↑s : Set L))
have h : ∀ (x : L),
  Membership.mem (γ := Set L)
      (⋂ (p : Submodule R L),
        ⋂ (_ : Membership.mem (γ := Set (Submodule R L)) {x : Submodule R L | ∃ s ∈ S, s.toSubmodule = x} p),
          (↑p : Set L))
      x ↔
    Membership.mem (γ := Set L) (⋂ s ∈ S, (↑s : Set L)) x
Tactic: ext 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
S : Set (LieSubalgebra R L)
⊢ IsGLB S (sInf S)
have h : ∀ (K K' : LieSubalgebra R L), (↑K : Set L) ≤ (↑K' : Set L) ↔ K ≤ K'
Tactic: have h : ∀ K K' : LieSubalgebra R L, (K : Set L) ≤ K' ↔ K ≤ K' := by
    intros
    exact Iff.rfl
-- 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
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), (↑K : Set L) ≤ (↑K' : Set L) ↔ K ≤ K'
⊢ IsGLB S (sInf S)
have apply : IsGLB (SetLike.coe '' S) (↑(sInf S) : Set L)
Tactic: apply IsGLB.of_image @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
S : Set (LieSubalgebra R L)
h : ∀ (K K' : LieSubalgebra R L), (↑K : Set L) ≤ (↑K' : Set L) ↔ K ≤ K'
⊢ IsGLB (SetLike.coe '' S) (↑(sInf S) : Set L)
have simp : IsGLB (SetLike.coe '' S) (⋂ s ∈ S, (↑s : Set L))
Tactic: simp only [coe_sInf]
-- 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₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
N : LieSubalgebra R L
x : L
h : Membership.mem (γ := LieSubalgebra R L) ⊥ x
⊢ x ∈ N
have h₁ : x = 0
Tactic: rw [mem_bot] 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₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
N : LieSubalgebra R L
x : L
h : x = 0
⊢ x ∈ N
have rw : 0 ∈ N
Tactic: rw [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
K K' : LieSubalgebra R L
x : L
⊢ x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K'
have rw : x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K ∧ x ∈ K'
Tactic: rw [← mem_toSubmodule, ← mem_toSubmodule, ← mem_toSubmodule, inf_toSubmodule,
    Submodule.mem_inf]
-- 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
K K' : LieSubalgebra R L
x : L
rw : x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K ∧ x ∈ K'
⊢ x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K'
have rw₁ : x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ K'
Tactic: rw [← mem_toSubmodule, ← mem_toSubmodule, ← mem_toSubmodule, inf_toSubmodule,
    Submodule.mem_inf]
-- 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
K K' : LieSubalgebra R L
x : L
rw : x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K ∧ x ∈ K'
rw₁ : x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ K'
⊢ x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K'
have rw₂ : x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ K'.toSubmodule
Tactic: rw [← mem_toSubmodule, ← mem_toSubmodule, ← mem_toSubmodule, inf_toSubmodule,
    Submodule.mem_inf]
-- 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
K K' : LieSubalgebra R L
x : L
rw : x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K ∧ x ∈ K'
rw₁ : x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ K'
rw₂ : x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ K'.toSubmodule
⊢ x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K'
have rw₃ : x ∈ K.toSubmodule ⊓ K'.toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ K'.toSubmodule
Tactic: rw [← mem_toSubmodule, ← mem_toSubmodule, ← mem_toSubmodule, inf_toSubmodule,
    Submodule.mem_inf]
-- 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
K K' : LieSubalgebra R L
x : L
rw : x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K ∧ x ∈ K'
rw₁ : x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ K'
rw₂ : x ∈ (K ⊓ K').toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ K'.toSubmodule
rw₃ : x ∈ K.toSubmodule ⊓ K'.toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ K'.toSubmodule
⊢ x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K'
have rw₄ : x ∈ K.toSubmodule ∧ x ∈ K'.toSubmodule ↔ x ∈ K.toSubmodule ∧ x ∈ K'.toSubmodule
Tactic: rw [← mem_toSubmodule, ← mem_toSubmodule, ← mem_toSubmodule, inf_toSubmodule,
    Submodule.mem_inf]
-- 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
K : LieSubalgebra R L
⊢ K = ⊥ ↔ ∀ x ∈ K, x = 0
have rw : K ≤ ⊥ ↔ ∀ x ∈ K, x = 0
Tactic: rw [_root_.eq_bot_iff]
-- 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₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ Subsingleton.{v + 1} (LieSubalgebra R ↥⊥)
have hα : Eq.{v + 1} (α := LieSubalgebra R ↥⊥) ⊥ ⊤
Tactic: apply subsingleton_of_bot_eq_top
-- 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₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
⊢ Eq.{v + 1} (α := LieSubalgebra R ↥⊥) ⊥ ⊤
have hα : ∀ (x : L) (hx : Membership.mem (γ := LieSubalgebra R L) ⊥ x),
  Membership.mem (γ := LieSubalgebra R ↥⊥) ⊥
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) x hx) ↔
    Membership.mem (γ := LieSubalgebra R ↥⊥) ⊤
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) x hx)
Tactic: ext ⟨x, hx⟩
-- 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₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
hx : Membership.mem (γ := LieSubalgebra R L) ⊥ x
⊢ Membership.mem (γ := LieSubalgebra R ↥⊥) ⊥
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) x hx) ↔
    Membership.mem (γ := LieSubalgebra R ↥⊥) ⊤
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) x hx)
have hx₁ : x = 0
Tactic: rw [LieSubalgebra.mem_bot] at hx
-- 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₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
x : L
hx_1 : Membership.mem (γ := LieSubalgebra R L) ⊥ x
hx : x = 0
⊢ Membership.mem (γ := LieSubalgebra R ↥⊥) ⊥
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) x hx_1) ↔
    Membership.mem (γ := LieSubalgebra R ↥⊥) ⊤
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) x hx_1)
have hα : ∀ (hx : Membership.mem (γ := LieSubalgebra R L) ⊥ 0),
  Membership.mem (γ := LieSubalgebra R ↥⊥) ⊥
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) 0 hx) ↔
    Membership.mem (γ := LieSubalgebra R ↥⊥) ⊤
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) 0 hx)
Tactic: subst hx
Cleared hypotheses: x, hx_1, hx
-- 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₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
hx : Membership.mem (γ := LieSubalgebra R L) ⊥ 0
⊢ Membership.mem (γ := LieSubalgebra R ↥⊥) ⊥
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) 0 hx) ↔
    Membership.mem (γ := LieSubalgebra R ↥⊥) ⊤
      (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) 0 hx)
have hα : Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieSubalgebra R L) ⊥ x) 0 hx = 0
Tactic: simp only [mem_bot, mem_top, iff_true]
-- 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
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
⊢ x ∈ ofLe h ↔ (↑x : L) ∈ K
have simp : (∃ (y : ↥K), Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑y : L) sorry = x) ↔ (↑x : L) ∈ K
Tactic: simp only [ofLe, inclusion_apply, LieHom.mem_range]
-- 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
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
⊢ (∃ (y : ↥K), Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑y : L) ⋯ = x) ↔ (↑x : L) ∈ K
have mp : (∃ (y : ↥K), Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑y : L) sorry = x) → (↑x : L) ∈ K
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
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
mp : (∃ (y : ↥K), Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑y : L) ⋯ = x) → (↑x : L) ∈ K
⊢ (∃ (y : ↥K), Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑y : L) ⋯ = x) ↔ (↑x : L) ∈ K
have mpr : (↑x : L) ∈ K → ∃ (y : ↥K), Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑y : L) sorry = x
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
K K' : LieSubalgebra R L
h_1 : K ≤ K'
x : ↥K'
h : (↑x : L) ∈ K
⊢ ∃ (y : ↥K), Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑y : L) ⋯ = x
have w : ↥K
Tactic: use ⟨(x : 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
K K' : LieSubalgebra R L
h_1 : K ≤ K'
x : ↥K'
h : (↑x : L) ∈ K
w : ↥K
⊢ ∃ (y : ↥K), Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑y : L) ⋯ = x
have h₁ : Subtype.mk (p := fun (x : L) ↦ x ∈ K') (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ K) (↑x : L) h) : L) sorry = x
Tactic: use ⟨(x : 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
K K' : LieSubalgebra R L
h : K ≤ K'
⊢ ofLe h = comap K'.incl K
have h₁ : ∀ (x : ↥K'), x ∈ ofLe h ↔ x ∈ comap K'.incl K
Tactic: 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
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
⊢ x ∈ ofLe h ↔ x ∈ comap K'.incl K
have h₁ : (↑x : L) ∈ K ↔ x ∈ comap K'.incl K
Tactic: rw [mem_ofLe]
-- 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
s : Set L
x : L
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) x ↔ ∀ (K : LieSubalgebra R L), s ⊆ (↑K : Set L) → x ∈ K
have rw : Membership.mem (γ := Set L)
    (⋂ (s_1 : LieSubalgebra R L),
      ⋂ (_ : Membership.mem (γ := Set (LieSubalgebra R L)) {N : LieSubalgebra R L | s ⊆ (↑N : Set L)} s_1),
        (↑s_1 : Set L))
    x ↔
  ∀ (K : LieSubalgebra R L), s ⊆ (↑K : Set L) → x ∈ K
Tactic: rw [← SetLike.mem_coe, lieSpan, coe_sInf]
-- 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
s : Set L
m : L
hm : m ∈ s
⊢ m ∈ (↑(lieSpan R L s) : Set L)
have rw : ∀ (K : LieSubalgebra R L), s ⊆ (↑K : Set L) → m ∈ K
Tactic: rw [SetLike.mem_coe, mem_lieSpan]
-- 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
s : Set L
⊢ LE.le (α := Submodule R L) (Submodule.span R s) (toSubmodule (lieSpan R L s))
have rw : s ⊆ (↑(lieSpan R L s) : Set L)
Tactic: rw [Submodule.span_le, coe_toSubmodule]
-- 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
s : Set L
K : LieSubalgebra R L
⊢ lieSpan R L s ≤ K ↔ s ⊆ (↑K : Set L)
have mp : lieSpan R L s ≤ K → s ⊆ (↑K : Set L)
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
s : Set L
K : LieSubalgebra R L
mp : lieSpan R L s ≤ K → s ⊆ (↑K : Set L)
⊢ lieSpan R L s ≤ K ↔ s ⊆ (↑K : Set L)
have mpr : s ⊆ (↑K : Set L) → lieSpan R L s ≤ K
Tactic: constructor
-- 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
s : Set L
K : LieSubalgebra R L
hs : s ⊆ (↑K : Set L)
m : L
hm : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L s) m
⊢ m ∈ K
have hm₁ : ∀ (K : LieSubalgebra R L), s ⊆ (↑K : Set L) → m ∈ K
Tactic: rw [mem_lieSpan] at hm
Cleared hypotheses: hm
-- 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
s t : Set L
h : s ⊆ t
⊢ LE.le (α := LieSubalgebra R L) (lieSpan R L s) (lieSpan R L t)
have rw : s ⊆ (↑(lieSpan R L t) : Set L)
Tactic: rw [lieSpan_le]
-- 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
⊢ toSubmodule (lieSpan R L (↑p : Set L)) = p ↔ ∃ (K : LieSubalgebra R L), K.toSubmodule = p
have rw : toSubmodule (lieSpan R L (↑p : Set L)) = p ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
Tactic: rw [p.exists_lieSubalgebra_coe_eq_iff]
-- 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
⊢ toSubmodule (lieSpan R L (↑p : Set L)) = p ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
have mp : toSubmodule (lieSpan R L (↑p : Set L)) = 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 : toSubmodule (lieSpan R L (↑p : Set L)) = p → ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ toSubmodule (lieSpan R L (↑p : Set L)) = p ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
have mpr : (∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p) → toSubmodule (lieSpan R L (↑p : Set L)) = 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 : toSubmodule (lieSpan R L (↑p : Set L)) = p
x m : L
hm : x ∈ p
⊢ m ∈ p → ⁅x, m⁆ ∈ p
have mp : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (↑p : Set L)) m →
  Membership.mem (γ := Submodule R L) (toSubmodule (lieSpan R L (↑p : Set L))) ⁅x, m⁆
Tactic: rw [← h, mem_toSubmodule]
-- 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
⊢ toSubmodule (lieSpan R L (↑p : Set L)) = p
have mpr : toSubmodule (lieSpan R L (↑{ toSubmodule := p, lie_mem' := h : LieSubalgebra R L }.toSubmodule : Set L)) =
  { toSubmodule := p, lie_mem' := h : LieSubalgebra R L }.toSubmodule
Tactic: rw [← toSubmodule_mk p @h, coe_toSubmodule, toSubmodule_inj, lieSpan_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
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
mpr :
  toSubmodule (lieSpan R L (↑{ toSubmodule := p, lie_mem' := h : LieSubalgebra R L }.toSubmodule : Set L)) =
    { toSubmodule := p, lie_mem' := h : LieSubalgebra R L }.toSubmodule
⊢ toSubmodule (lieSpan R L (↑p : Set L)) = p
have mpr₁ : toSubmodule (lieSpan R L (↑{ toSubmodule := p, lie_mem' := h : LieSubalgebra R L } : Set L)) =
  { toSubmodule := p, lie_mem' := h : LieSubalgebra R L }.toSubmodule
Tactic: rw [← toSubmodule_mk p @h, coe_toSubmodule, toSubmodule_inj, lieSpan_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
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
mpr :
  toSubmodule (lieSpan R L (↑{ toSubmodule := p, lie_mem' := h : LieSubalgebra R L }.toSubmodule : Set L)) =
    { toSubmodule := p, lie_mem' := h : LieSubalgebra R L }.toSubmodule
mpr₁ :
  toSubmodule (lieSpan R L (↑{ toSubmodule := p, lie_mem' := h : LieSubalgebra R L } : Set L)) =
    { toSubmodule := p, lie_mem' := h : LieSubalgebra R L }.toSubmodule
⊢ toSubmodule (lieSpan R L (↑p : Set L)) = p
have mpr₂ : lieSpan R L (↑{ toSubmodule := p, lie_mem' := h : LieSubalgebra R L } : Set L) =
  { toSubmodule := p, lie_mem' := h : LieSubalgebra R L }
Tactic: rw [← toSubmodule_mk p @h, coe_toSubmodule, toSubmodule_inj, lieSpan_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
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
mpr :
  toSubmodule (lieSpan R L (↑{ toSubmodule := p, lie_mem' := h : LieSubalgebra R L }.toSubmodule : Set L)) =
    { toSubmodule := p, lie_mem' := h : LieSubalgebra R L }.toSubmodule
mpr₁ :
  toSubmodule (lieSpan R L (↑{ toSubmodule := p, lie_mem' := h : LieSubalgebra R L } : Set L)) =
    { toSubmodule := p, lie_mem' := h : LieSubalgebra R L }.toSubmodule
mpr₂ :
  lieSpan R L (↑{ toSubmodule := p, lie_mem' := h : LieSubalgebra R L } : Set L) =
    { toSubmodule := p, lie_mem' := h : LieSubalgebra R L }
⊢ toSubmodule (lieSpan R L (↑p : Set L)) = p
have mpr₃ : { toSubmodule := p, lie_mem' := h : LieSubalgebra R L } = { toSubmodule := p, lie_mem' := h }
Tactic: rw [← toSubmodule_mk p @h, coe_toSubmodule, toSubmodule_inj, lieSpan_eq]