awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₂ : LieIdeal R L
simp_rw : Submodule.comap (↑I : Submodule R L).subtype (↑I₂ : Submodule R L) = ⊤ ↔ I ≤ I₂
⊢ Submodule.comap (toLieSubalgebra R L I).subtype (↑I₂ : Submodule R L) = ⊤ ↔ I ≤ I₂

Tactic:
simp_rw [toLieSubalgebra_toSubmodule]

Premises used: LieIdeal.toLieSubalgebra_toSubmodule
-- Module: Mathlib.Algebra.Lie.Ideal
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₂
rw₁ rw₂ : I ≤ I₂ ↔ I ≤ I₂
⊢ Submodule.comap (↑I : Submodule R L).subtype (↑I₂ : Submodule R L) = ⊤ ↔ I ≤ I₂

Tactic:
rw [Submodule.comap_subtype_eq_top, LieSubmodule.toSubmodule_le_toSubmodule]

Premises used: LieSubmodule.toSubmodule_le_toSubmodule, Submodule.comap_subtype_eq_top
-- Module: Mathlib.Algebra.Lie.Ideal
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 :
  Submodule.comap (toLieSubalgebra R L I).subtype (↑I₂ : Submodule R L) = ⊥ ↔
    (↑I : Submodule R L) ⊓ (↑I₂ : Submodule R L) = ⊥
⊢ comap I.incl I₂ = ⊥ ↔ Disjoint I I₂

Tactic:
rw [disjoint_iff, ← LieSubmodule.toSubmodule_inj, LieIdeal.comap_toSubmodule,
    LieSubmodule.bot_toSubmodule, ← LieSubmodule.toSubmodule_inj, LieSubmodule.inf_toSubmodule,
    LieSubmodule.bot_toSubmodule, incl_coe]

Premises used: LieSubmodule.bot_toSubmodule, LieIdeal.incl_coe, disjoint_iff, LieSubmodule.toSubmodule_inj, LieIdeal.comap_toSubmodule, LieSubmodule.inf_toSubmodule
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I I₂ : LieIdeal R L
simp_rw :
  Submodule.comap (↑I : Submodule R L).subtype (↑I₂ : Submodule R L) = ⊥ ↔
    (↑I : Submodule R L) ⊓ (↑I₂ : Submodule R L) = ⊥
⊢ Submodule.comap (toLieSubalgebra R L I).subtype (↑I₂ : Submodule R L) = ⊥ ↔
    (↑I : Submodule R L) ⊓ (↑I₂ : Submodule R L) = ⊥

Tactic:
simp_rw [toLieSubalgebra_toSubmodule]

Premises used: LieIdeal.toLieSubalgebra_toSubmodule
-- Module: Mathlib.Algebra.Lie.Ideal
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) = ⊥
rw₁ rw₂ : (↑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) = ⊥

Tactic:
rw [← Submodule.disjoint_iff_comap_eq_bot, disjoint_iff]

Premises used: disjoint_iff, Submodule.disjoint_iff_comap_eq_bot
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : ↥⊤
⊢ (topEquiv : (a : ↥⊤) → L) x = (↑x : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.IdealOperations
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₂
⊢ map f (comap f N₂) ≤ N₂

Tactic:
(N₂ : Set M₂).image_preimage_subset f

Premises used: Set.Mem, setOf, Set.Subset, SetLike.coe, Set.preimage, Set.image_preimage_subset, Set.image, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
rw : (↑(map f (comap f N₂)) : Set M₂) = (↑N₂ : Set M₂)
⊢ map f (comap f N₂) = N₂

Tactic:
rw [SetLike.ext'_iff]

Premises used: SetLike.ext'_iff
-- Module: Mathlib.Algebra.Lie.IdealOperations
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₂)) : Set M₂) = (↑N₂ : Set M₂)

Tactic:
Set.image_preimage_eq_of_subset hf

Premises used: Set.Mem, setOf, Set.preimage, Set.image_preimage_eq_of_subset, Set.image
-- Module: Mathlib.Algebra.Lie.IdealOperations
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₂)) : Set M₂) = (↑N₂ : Set M₂)

Tactic:
exact Set.image_preimage_eq_of_subset hf

Premises used: Set.image_preimage_eq_of_subset
-- Module: Mathlib.Algebra.Lie.IdealOperations
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₂
⊢ N ≤ comap f (map f N)

Tactic:
(N : Set M).subset_preimage_image f

Premises used: Set.Mem, setOf, Set.Subset, SetLike.coe, Set.preimage, Set.image, DFunLike.coe, Set.subset_preimage_image
-- Module: Mathlib.Algebra.Lie.IdealOperations
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 = ⊥
rw : (↑(comap f (map f N)) : Set M) = (↑N : Set M)
⊢ comap f (map f N) = N

Tactic:
rw [SetLike.ext'_iff]

Premises used: SetLike.ext'_iff
-- Module: Mathlib.Algebra.Lie.IdealOperations
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)) : Set M) = (↑N : Set M)

Tactic:
(N : Set M).preimage_image_eq (f.ker_eq_bot.mp hf)

Premises used: LieModuleHom.ker_eq_bot, Set.Mem, setOf, SetLike.coe, Set.preimage, Iff.mp, Set.preimage_image_eq, Set.image
-- Module: Mathlib.Algebra.Lie.IdealOperations
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)) : Set M) = (↑N : Set M)

Tactic:
exact (N : Set M).preimage_image_eq (f.ker_eq_bot.mp hf)

Premises used: LieModuleHom.ker_eq_bot, SetLike.coe, Iff.mp, Set.preimage_image_eq
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
rw : (↑(map N.incl (comap N.incl N')) : Submodule R M) = (↑(N ⊓ N') : Submodule R M)
⊢ map N.incl (comap N.incl N') = N ⊓ N'

Tactic:
rw [← toSubmodule_inj]

Premises used: LieSubmodule.toSubmodule_inj
-- Module: Mathlib.Algebra.Lie.IdealOperations
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')) : Submodule R M) = (↑(N ⊓ N') : Submodule R M)

Tactic:
(N : Submodule R M).map_comap_subtype N'

Premises used: Set.Mem, LieSubmodule.toSubmodule, Submodule.map_comap_subtype, Submodule.map
-- Module: Mathlib.Algebra.Lie.IdealOperations
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')) : Submodule R M) = (↑(N ⊓ N') : Submodule R M)

Tactic:
exact (N : Submodule R M).map_comap_subtype N'

Premises used: LieSubmodule.toSubmodule, Submodule.map_comap_subtype
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
⊢ ⁅I, N⁆ = lieSpan R L {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.IdealOperations
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}
a₁ : Submodule.span R {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ≤ (↑⁅I, N⁆ : Submodule R M)
⊢ (↑⁅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

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Lie.IdealOperations
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'⁆

Tactic:
Submodule.span_induction (R := R) (M := M) (s := s)
        (p := fun m' _ ↦ ⁅y, m'⁆ ∈ Submodule.span R s) ?_ ?_ ?_ ?_ hm'

Premises used: Submodule.span_induction
-- Module: Mathlib.Algebra.Lie.IdealOperations
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) ⋯
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) ⋯
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆

Tactic:
refine Submodule.span_induction (R := R) (M := M) (s := s)
        (p := fun m' _ ↦ ⁅y, m'⁆ ∈ Submodule.span R s) ?_ ?_ ?_ ?_ hm'

Premises used: Submodule.span_induction
-- Module: Mathlib.Algebra.Lie.IdealOperations
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)⁆ + ⁅(↑x : L), ⁅y, (↑n : M)⁆⁆)
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m''⁆

Tactic:
rw [← hm'', leibniz_lie]

Premises used: leibniz_lie
-- Module: Mathlib.Algebra.Lie.IdealOperations
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)⁆⁆)

Tactic:
Submodule.add_mem _ ?_ ?_

Premises used: Submodule.add_mem
-- Module: Mathlib.Algebra.Lie.IdealOperations
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)⁆
refine_1₁ : Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅(↑x : L), ⁅y, (↑n : M)⁆⁆
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) (⁅⁅y, (↑x : L)⁆, (↑n : M)⁆ + ⁅(↑x : L), ⁅y, (↑n : M)⁆⁆)

Tactic:
refine Submodule.add_mem _ ?_ ?_

Premises used: Submodule.add_mem
-- Module: Mathlib.Algebra.Lie.IdealOperations
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 : ⁅⁅y, (↑x : L)⁆, (↑n : M)⁆ ∈ s
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅⁅y, (↑x : L)⁆, (↑n : M)⁆

Tactic:
apply Submodule.subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.Algebra.Lie.IdealOperations
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 : ⁅(↑x : L), ⁅y, (↑n : M)⁆⁆ ∈ s
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅(↑x : L), ⁅y, (↑n : M)⁆⁆

Tactic:
apply Submodule.subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
h : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) ⁅y, (↑x : L)⁆ ⋯) : L), (↑n : M)⁆ = ⁅⁅y, (↑x : L)⁆, (↑n : M)⁆
⊢ ⁅⁅y, (↑x : L)⁆, (↑n : M)⁆ ∈ s

Tactic:
use ⟨⁅y, ↑x⁆, I.lie_mem x.property⟩, n
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
h : ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) ⁅y, (↑n : M)⁆ ⋯) : M)⁆ = ⁅(↑x : L), ⁅y, (↑n : M)⁆⁆
⊢ ⁅(↑x : L), ⁅y, (↑n : M)⁆⁆ ∈ s

Tactic:
use x, ⟨⁅y, ↑n⁆, N.lie_mem n.property⟩
-- Module: Mathlib.Algebra.Lie.IdealOperations
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'
⊢ (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 ⋯

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
refine_3 :
  ∀ (hx : Membership.mem (γ := Submodule R M) (Submodule.span R s) m₁)
    (hy : Membership.mem (γ := Submodule R M) (Submodule.span R s) m₂),
    (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'⁆)
        m₁ 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'⁆)
          m₂ 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'⁆)
          (m₁ + m₂) ⋯
⊢ ∀ (hx : Membership.mem (γ := Submodule R M) (Submodule.span R s) m₁)
    (hy : Membership.mem (γ := Submodule R M) (Submodule.span R s) m₂),
    (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'⁆)
        m₁ 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'⁆)
          m₂ 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'⁆)
          (m₁ + m₂) ⋯

Tactic:
_
-- Module: Mathlib.Algebra.Lie.IdealOperations
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₁
refine_3 :
  ∀ (hy : Membership.mem (γ := Submodule R M) (Submodule.span R s) m₂),
    (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'⁆)
        m₁ 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'⁆)
          m₂ 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'⁆)
          (m₁ + m₂) ⋯
⊢ ∀ (hy : Membership.mem (γ := Submodule R M) (Submodule.span R s) m₂),
    (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'⁆)
        m₁ 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'⁆)
          m₂ 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'⁆)
          (m₁ + m₂) ⋯

Tactic:
_
-- Module: Mathlib.Algebra.Lie.IdealOperations
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₂⁆
refine_3 : Membership.mem (γ := Submodule R M) (Submodule.span R s) (⁅y, m₁⁆ + ⁅y, m₂⁆)
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m₁ + m₂⁆

Tactic:
rw [lie_add]

Premises used: lie_add
-- Module: Mathlib.Algebra.Lie.IdealOperations
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₁⁆ + ⁅y, m₂⁆)

Tactic:
Submodule.add_mem _ hm₁ hm₂

Premises used: Submodule.add_mem
-- Module: Mathlib.Algebra.Lie.IdealOperations
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₁⁆ + ⁅y, m₂⁆)

Tactic:
exact Submodule.add_mem _ hm₁ hm₂

Premises used: Submodule.add_mem