awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : (↑(map f I) : Set L') = (⇑f : (a : L) → L') '' (↑I : Set L)
rw : (↑(comap f (map f I)) : Submodule R L) = (↑(I ⊔ f.ker) : Submodule R L)
rw₁ : Submodule.comap (↑f : L →ₗ[R] L') (↑(map f I) : Submodule R L') = (↑(I ⊔ f.ker) : Submodule R L)
rw₂ :
  Submodule.comap (↑f : L →ₗ[R] L') (Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)) =
    (↑(I ⊔ f.ker) : Submodule R L)
⊢ comap f (map f I) = I ⊔ f.ker
have rw₃ : Submodule.comap (↑f : L →ₗ[R] L') (Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)) =
  (↑I : Submodule R L) ⊔ (↑f.ker : Submodule R L)
Tactic: rw [← LieSubmodule.toSubmodule_inj, comap_toSubmodule, I.map_toSubmodule f h,
    LieSubmodule.sup_toSubmodule, f.ker_toSubmodule, Submodule.comap_map_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : (↑(map f I) : Set L') = (⇑f : (a : L) → L') '' (↑I : Set L)
rw : (↑(comap f (map f I)) : Submodule R L) = (↑(I ⊔ f.ker) : Submodule R L)
rw₁ : Submodule.comap (↑f : L →ₗ[R] L') (↑(map f I) : Submodule R L') = (↑(I ⊔ f.ker) : Submodule R L)
rw₂ :
  Submodule.comap (↑f : L →ₗ[R] L') (Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)) =
    (↑(I ⊔ f.ker) : Submodule R L)
rw₃ :
  Submodule.comap (↑f : L →ₗ[R] L') (Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)) =
    (↑I : Submodule R L) ⊔ (↑f.ker : Submodule R L)
⊢ comap f (map f I) = I ⊔ f.ker
have rw₄ : Submodule.comap (↑f : L →ₗ[R] L') (Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)) =
  (↑I : Submodule R L) ⊔ (↑f : L →ₗ[R] L').ker
Tactic: rw [← LieSubmodule.toSubmodule_inj, comap_toSubmodule, I.map_toSubmodule f h,
    LieSubmodule.sup_toSubmodule, f.ker_toSubmodule, Submodule.comap_map_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : (↑(map f I) : Set L') = (⇑f : (a : L) → L') '' (↑I : Set L)
rw : (↑(comap f (map f I)) : Submodule R L) = (↑(I ⊔ f.ker) : Submodule R L)
rw₁ : Submodule.comap (↑f : L →ₗ[R] L') (↑(map f I) : Submodule R L') = (↑(I ⊔ f.ker) : Submodule R L)
rw₂ :
  Submodule.comap (↑f : L →ₗ[R] L') (Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)) =
    (↑(I ⊔ f.ker) : Submodule R L)
rw₃ :
  Submodule.comap (↑f : L →ₗ[R] L') (Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)) =
    (↑I : Submodule R L) ⊔ (↑f.ker : Submodule R L)
rw₄ :
  Submodule.comap (↑f : L →ₗ[R] L') (Submodule.map (↑f : L →ₗ[R] L') (↑I : Submodule R L)) =
    (↑I : Submodule R L) ⊔ (↑f : L →ₗ[R] L').ker
⊢ comap f (map f I) = I ⊔ f.ker
have rw₅ : (↑I : Submodule R L) ⊔ (↑f : L →ₗ[R] L').ker = (↑I : Submodule R L) ⊔ (↑f : L →ₗ[R] L').ker
Tactic: rw [← LieSubmodule.toSubmodule_inj, comap_toSubmodule, I.map_toSubmodule f h,
    LieSubmodule.sup_toSubmodule, f.ker_toSubmodule, Submodule.comap_map_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ comap I.incl I = ⊤
have h : ∀ (m : ↥I), m ∈ comap I.incl I ↔ Membership.mem (γ := LieSubmodule R ↥I ↥I) ⊤ m
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ I.incl.ker = ⊥
have h : ∀ (m : ↥I), m ∈ I.incl.ker ↔ Membership.mem (γ := LieSubmodule R ↥I ↥I) ⊥ m
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ I.incl.idealRange = I
have rw : ∃ (N : LieSubmodule R L L), (↑N : Submodule R L) = (↑I : Submodule R L)
Tactic: rw [LieHom.idealRange_eq_lieSpan_range, ← LieSubalgebra.coe_toSubmodule, ←
    LieSubmodule.toSubmodule_inj, incl_range, toLieSubalgebra_toSubmodule,
    LieSubmodule.coe_lieSpan_submodule_eq_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ ∃ (N : LieSubmodule R L L), (↑N : Submodule R L) = (↑I : Submodule R L)
have w : LieSubmodule R L L
Tactic: use I
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
w : LieSubmodule R L L
⊢ ∃ (N : LieSubmodule R L L), (↑N : Submodule R L) = (↑I : Submodule R L)
have h : (↑I : Submodule R L) = (↑I : Submodule R L)
Tactic: use I
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ I.incl.IsIdealMorphism
have rw : toLieSubalgebra R L I = I.incl.range
Tactic: rw [I.incl.isIdealMorphism_def, incl_idealRange]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₂ : LieIdeal R L
⊢ comap I.incl I₂ = ⊤ ↔ I ≤ I₂
have rw : Submodule.comap (toLieSubalgebra R L I).subtype (↑I₂ : Submodule R L) = ⊤ ↔ I ≤ I₂
Tactic: rw [← LieSubmodule.toSubmodule_inj, LieIdeal.comap_toSubmodule, LieSubmodule.top_toSubmodule,
    incl_coe]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₂ : LieIdeal R L
⊢ Submodule.comap (toLieSubalgebra R L I).subtype (↑I₂ : Submodule R L) = ⊤ ↔ I ≤ I₂
have simp_rw : Submodule.comap (↑I : Submodule R L).subtype (↑I₂ : Submodule R L) = ⊤ ↔ I ≤ I₂
Tactic: simp_rw [toLieSubalgebra_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₂ : LieIdeal R L
⊢ Submodule.comap (↑I : Submodule R L).subtype (↑I₂ : Submodule R L) = ⊤ ↔ I ≤ I₂
have rw : (↑I : Submodule R L) ≤ (↑I₂ : Submodule R L) ↔ I ≤ I₂
Tactic: rw [Submodule.comap_subtype_eq_top, LieSubmodule.toSubmodule_le_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₂ : LieIdeal R L
rw : (↑I : Submodule R L) ≤ (↑I₂ : Submodule R L) ↔ I ≤ I₂
⊢ Submodule.comap (↑I : Submodule R L).subtype (↑I₂ : Submodule R L) = ⊤ ↔ I ≤ I₂
have rw₁ : I ≤ I₂ ↔ I ≤ I₂
Tactic: rw [Submodule.comap_subtype_eq_top, LieSubmodule.toSubmodule_le_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₂ : LieIdeal R L
⊢ comap I.incl I₂ = ⊥ ↔ Disjoint I I₂
have rw : Submodule.comap (toLieSubalgebra R L I).subtype (↑I₂ : Submodule R L) = ⊥ ↔
  (↑I : Submodule R L) ⊓ (↑I₂ : Submodule R L) = ⊥
Tactic: rw [disjoint_iff, ← LieSubmodule.toSubmodule_inj, LieIdeal.comap_toSubmodule,
    LieSubmodule.bot_toSubmodule, ← LieSubmodule.toSubmodule_inj, LieSubmodule.inf_toSubmodule,
    LieSubmodule.bot_toSubmodule, incl_coe]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₂ : LieIdeal R L
⊢ Submodule.comap (toLieSubalgebra R L I).subtype (↑I₂ : Submodule R L) = ⊥ ↔
    (↑I : Submodule R L) ⊓ (↑I₂ : Submodule R L) = ⊥
have simp_rw : Submodule.comap (↑I : Submodule R L).subtype (↑I₂ : Submodule R L) = ⊥ ↔
  (↑I : Submodule R L) ⊓ (↑I₂ : Submodule R L) = ⊥
Tactic: simp_rw [toLieSubalgebra_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₂ : LieIdeal R L
⊢ Submodule.comap (↑I : Submodule R L).subtype (↑I₂ : Submodule R L) = ⊥ ↔
    (↑I : Submodule R L) ⊓ (↑I₂ : Submodule R L) = ⊥
have rw : Disjoint (↑I : Submodule R L) (↑I₂ : Submodule R L) ↔ (↑I : Submodule R L) ⊓ (↑I₂ : Submodule R L) = ⊥
Tactic: rw [← Submodule.disjoint_iff_comap_eq_bot, disjoint_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Ideal (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₂ : LieIdeal R L
rw : Disjoint (↑I : Submodule R L) (↑I₂ : Submodule R L) ↔ (↑I : Submodule R L) ⊓ (↑I₂ : Submodule R L) = ⊥
⊢ Submodule.comap (↑I : Submodule R L).subtype (↑I₂ : Submodule R L) = ⊥ ↔
    (↑I : Submodule R L) ⊓ (↑I₂ : Submodule R L) = ⊥
have rw₁ : (↑I : Submodule R L) ⊓ (↑I₂ : Submodule R L) = ⊥ ↔ (↑I : Submodule R L) ⊓ (↑I₂ : Submodule R L) = ⊥
Tactic: rw [← Submodule.disjoint_iff_comap_eq_bot, disjoint_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : LieRingModule L M₂
N₂ : LieSubmodule R L M₂
f : M →ₗ⁅R,L⁆ M₂
hf : N₂ ≤ f.range
⊢ map f (comap f N₂) = N₂
have rw : (↑(map f (comap f N₂)) : Set M₂) = (↑N₂ : Set M₂)
Tactic: rw [SetLike.ext'_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : f.ker = ⊥
⊢ comap f (map f N) = N
have rw : (↑(comap f (map f N)) : Set M) = (↑N : Set M)
Tactic: rw [SetLike.ext'_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
⊢ map N.incl (comap N.incl N') = N ⊓ N'
have rw : (↑(map N.incl (comap N.incl N')) : Submodule R M) = (↑(N ⊓ N') : Submodule R M)
Tactic: rw [← toSubmodule_inj]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
⊢ (↑⁅I, N⁆ : Submodule R M) = Submodule.span R {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
have a : (↑⁅I, N⁆ : Submodule R M) ≤ Submodule.span R {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
a : (↑⁅I, N⁆ : Submodule R M) ≤ Submodule.span R {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
⊢ (↑⁅I, N⁆ : Submodule R M) = Submodule.span R {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
have a₁ : Submodule.span R {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ≤ (↑⁅I, N⁆ : Submodule R M)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
s : Set M := {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆
have refine_1 : ∀ (x : M) (h : x ∈ s),
  (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
      Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
    x sorry
Tactic: refine Submodule.span_induction (R := R) (M := M) (s := s)
        (p := fun m' _ ↦ ⁅y, m'⁆ ∈ Submodule.span R s) ?_ ?_ ?_ ?_ hm'
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
s : Set M := {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
refine_1 :
  ∀ (x : M) (h : x ∈ s),
    (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
        Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
      x ⋯
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆
have refine_2 : (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
    Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
  0 sorry
Tactic: refine Submodule.span_induction (R := R) (M := M) (s := s)
        (p := fun m' _ ↦ ⁅y, m'⁆ ∈ Submodule.span R s) ?_ ?_ ?_ ?_ hm'
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
s : Set M := {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
refine_1 :
  ∀ (x : M) (h : x ∈ s),
    (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
        Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
      x ⋯
refine_2 : Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, 0⁆
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆
have refine_3 : ∀ (x y_1 : M) (hx : Membership.mem (γ := Submodule R M) (Submodule.span R s) x)
  (hy : Membership.mem (γ := Submodule R M) (Submodule.span R s) y_1),
  (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
        Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
      x hx →
    (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
          Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
        y_1 hy →
      (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
          Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
        (x + y_1) sorry
Tactic: refine Submodule.span_induction (R := R) (M := M) (s := s)
        (p := fun m' _ ↦ ⁅y, m'⁆ ∈ Submodule.span R s) ?_ ?_ ?_ ?_ hm'
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
s : Set M := {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
refine_1 :
  ∀ (x : M) (h : x ∈ s),
    (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
        Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
      x ⋯
refine_2 : Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, 0⁆
refine_3 :
  ∀ (x y_1 : M) (hx : Membership.mem (γ := Submodule R M) (Submodule.span R s) x)
    (hy : Membership.mem (γ := Submodule R M) (Submodule.span R s) y_1),
    (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
          Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
        x hx →
      (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
            Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
          y_1 hy →
        (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
            Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
          (x + y_1) ⋯
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆
have refine_4 : ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (Submodule.span R s) x),
  (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
        Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
      x hx →
    (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
        Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
      (a • x) sorry
Tactic: refine Submodule.span_induction (R := R) (M := M) (s := s)
        (p := fun m' _ ↦ ⁅y, m'⁆ ∈ Submodule.span R s) ?_ ?_ ?_ ?_ hm'
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
s : Set M := {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
m'' : M
x : ↥I
n : ↥N
hm'' : ⁅(↑x : L), (↑n : M)⁆ = m''
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m''⁆
have refine_1 : Membership.mem (γ := Submodule R M) (Submodule.span R s) (⁅⁅y, (↑x : L)⁆, (↑n : M)⁆ + ⁅(↑x : L), ⁅y, (↑n : M)⁆⁆)
Tactic: rw [← hm'', leibniz_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
s : Set M := {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
m'' : M
x : ↥I
n : ↥N
hm'' : ⁅(↑x : L), (↑n : M)⁆ = m''
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) (⁅⁅y, (↑x : L)⁆, (↑n : M)⁆ + ⁅(↑x : L), ⁅y, (↑n : M)⁆⁆)
have refine_1 : Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅⁅y, (↑x : L)⁆, (↑n : M)⁆
Tactic: refine Submodule.add_mem _ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
s : Set M := {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
m'' : M
x : ↥I
n : ↥N
hm'' : ⁅(↑x : L), (↑n : M)⁆ = m''
refine_1 : Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅⁅y, (↑x : L)⁆, (↑n : M)⁆
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) (⁅⁅y, (↑x : L)⁆, (↑n : M)⁆ + ⁅(↑x : L), ⁅y, (↑n : M)⁆⁆)
have refine_1₁ : Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅(↑x : L), ⁅y, (↑n : M)⁆⁆
Tactic: refine Submodule.add_mem _ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
s : Set M := {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
m'' : M
x : ↥I
n : ↥N
hm'' : ⁅(↑x : L), (↑n : M)⁆ = m''
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅⁅y, (↑x : L)⁆, (↑n : M)⁆
have refine_1 : ⁅⁅y, (↑x : L)⁆, (↑n : M)⁆ ∈ s
Tactic: apply Submodule.subset_span
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
s : Set M := {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
m'' : M
x : ↥I
n : ↥N
hm'' : ⁅(↑x : L), (↑n : M)⁆ = m''
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅(↑x : L), ⁅y, (↑n : M)⁆⁆
have refine_1 : ⁅(↑x : L), ⁅y, (↑n : M)⁆⁆ ∈ s
Tactic: apply Submodule.subset_span
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
s : Set M := {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
m'' : M
x : ↥I
n : ↥N
hm'' : ⁅(↑x : L), (↑n : M)⁆ = m''
w : ↥I
w₁ : ↥N
⊢ ⁅⁅y, (↑x : L)⁆, (↑n : M)⁆ ∈ s
have h : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) ⁅y, (↑x : L)⁆ sorry) : L), (↑n : M)⁆ = ⁅⁅y, (↑x : L)⁆, (↑n : M)⁆
Tactic: use ⟨⁅y, ↑x⁆, I.lie_mem x.property⟩, n
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
s : Set M := {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
m'' : M
x : ↥I
n : ↥N
hm'' : ⁅(↑x : L), (↑n : M)⁆ = m''
w : ↥I
w₁ : ↥N
⊢ ⁅(↑x : L), ⁅y, (↑n : M)⁆⁆ ∈ s
have h : ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑n : M)⁆ sorry) : M)⁆ = ⁅(↑x : L), ⁅y, (↑n : M)⁆⁆
Tactic: use x, ⟨⁅y, ↑n⁆, N.lie_mem n.property⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
s : Set M := {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
m₁ m₂ : M
hx : Membership.mem (γ := Submodule R M) (Submodule.span R s) m₁
hy : Membership.mem (γ := Submodule R M) (Submodule.span R s) m₂
hm₁ : Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m₁⁆
hm₂ : Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m₂⁆
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m₁ + m₂⁆
have refine_3 : Membership.mem (γ := Submodule R M) (Submodule.span R s) (⁅y, m₁⁆ + ⁅y, m₂⁆)
Tactic: rw [lie_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
s : Set M := {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
t : R
m'' : M
hx : Membership.mem (γ := Submodule R M) (Submodule.span R s) m''
hm'' : Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m''⁆
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, t • m''⁆
have refine_4 : Membership.mem (γ := Submodule R M) (Submodule.span R s) (t • ⁅y, m''⁆)
Tactic: rw [lie_smul]