awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Submodule
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
m m' : ↥N
⊢ (↑(m + m') : M) = (↑m : M) + (↑m' : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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
m : ↥N
⊢ (↑(-m) : M) = -(↑m : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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
m m' : ↥N
⊢ (↑(m - m') : M) = (↑m : M) - (↑m' : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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
t : R
m : ↥N
⊢ (↑(t • m) : M) = t • (↑m : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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
x : L
m : ↥N
⊢ (↑⁅x, m⁆ : M) = ⁅x, (↑m : M)⁆

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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_1 N' : LieSubmodule R L M
inst_5 : IsNoetherian R M
N : LieSubmodule R L M
⊢ IsNoetherian.{u, w} R ↥N

Tactic:
inferInstanceAs <| IsNoetherian R N.toSubmodule

Premises used: _private.0.LieSubmodule.instIsNoetherianSubtypeMem._proof_1
-- Module: Mathlib.Algebra.Lie.Submodule
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_1 N' : LieSubmodule R L M
inst_5 : IsArtinian R M
N : LieSubmodule R L M
⊢ IsArtinian.{u, w} R ↥N

Tactic:
inferInstanceAs <| IsArtinian R N.toSubmodule

Premises used: _private.0.LieSubmodule.instIsArtinianSubtypeMem._proof_1
-- Module: Mathlib.Algebra.Lie.Submodule
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
inst_5 : Module.IsTorsionFree R M
⊢ Module.IsTorsionFree.{u, w} R ↥N

Tactic:
inferInstanceAs <| Module.IsTorsionFree R N.toSubmodule

Premises used: _private.0.LieSubmodule.instIsTorsionFreeSubtypeMem._proof_1
-- Module: Mathlib.Algebra.Lie.Submodule
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
inst_5 : LieAlgebra R L
N : LieSubmodule R L M
H : LieSubalgebra R L
m : M
⊢ m ∈ N.restr H ↔ m ∈ N

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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
inst_5 : LieAlgebra R L
N : LieSubmodule R L M
H : LieSubalgebra R L
⊢ (↑(N.restr H) : Submodule R M) = (↑N : Submodule R M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
t : R
x : L
y : ↥N
a : (↑⁅t • x, y⁆ : M) = (↑(t • ⁅x, y⁆) : M)
⊢ ⁅t • x, y⁆ = t • ⁅x, y⁆

Tactic:
apply SetCoe.ext

Premises used: SetCoe.ext
-- Module: Mathlib.Algebra.Lie.Submodule
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
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
t : R
x : L
y : ↥N
⊢ (↑⁅t • x, y⁆ : M) = (↑(t • ⁅x, y⁆) : M)

Tactic:
apply smul_lie

Premises used: smul_lie
-- Module: Mathlib.Algebra.Lie.Submodule
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
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
t : R
x : L
y : ↥N
a : (↑⁅x, t • y⁆ : M) = (↑(t • ⁅x, y⁆) : M)
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
apply SetCoe.ext

Premises used: SetCoe.ext
-- Module: Mathlib.Algebra.Lie.Submodule
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
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
t : R
x : L
y : ↥N
⊢ (↑⁅x, t • y⁆ : M) = (↑(t • ⁅x, y⁆) : M)

Tactic:
apply lie_smul

Premises used: lie_smul
-- Module: Mathlib.Algebra.Lie.Submodule
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
p : Submodule R M
mp : (∃ (N : LieSubmodule R L M), (↑N : Submodule R M) = p) → ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
mpr : (∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p) → ∃ (N : LieSubmodule R L M), (↑N : Submodule R M) = p
⊢ (∃ (N : LieSubmodule R L M), (↑N : Submodule R M) = p) ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Submodule
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
x : L
m : M
⊢ m ∈ (↑N : Submodule R M) → ⁅x, m⁆ ∈ (↑N : Submodule R M)

Tactic:
N.lie_mem

Premises used: Set.Mem, LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.Submodule
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
x : L
m : M
⊢ m ∈ (↑N : Submodule R M) → ⁅x, m⁆ ∈ (↑N : Submodule R M)

Tactic:
exact N.lie_mem

Premises used: LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.Submodule
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
p : Submodule R M
h : ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p
w : LieSubmodule R L M
h₁ : (↑{ toSubmodule := p, lie_mem := h : LieSubmodule R L M } : Submodule R M) = p
⊢ ∃ (N : LieSubmodule R L M), (↑N : Submodule R M) = p

Tactic:
use { p with lie_mem := @h }
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
⊢ (↑K.toLieSubmodule : Submodule R L) = K.toSubmodule

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
x : L
⊢ x ∈ K.toLieSubmodule ↔ x ∈ K

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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
⊢ Function.Injective (α := LieSubmodule R L M) SetLike.coe

Tactic:
SetLike.coe_injective

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Lie.Submodule
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
⊢ (↑N : Submodule R M) ≤ (↑N' : Submodule R M) ↔ N ≤ N'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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
⊢ (↑⊥ : Set M) = {0}

Tactic:
rfl

Premises used: setOf, Set.singleton, rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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
⊢ Eq.{w + 1} (α := Submodule R M) (↑⊥ : Submodule R M) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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
rw : (↑N : Submodule R M) = ⊥ ↔ (↑N : Submodule R M) = (↑⊥ : Submodule R M)
rw₁ rw₂ : (↑N : Submodule R M) = ⊥ ↔ (↑N : Submodule R M) = ⊥
⊢ (↑N : Submodule R M) = ⊥ ↔ N = ⊥

Tactic:
rw [← toSubmodule_inj, bot_toSubmodule]

Premises used: LieSubmodule.bot_toSubmodule, LieSubmodule.toSubmodule_inj
-- Module: Mathlib.Algebra.Lie.Submodule
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 : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier
rw : (↑{ toSubmodule := N, lie_mem := @h : LieSubmodule R L M } : Submodule R M) = (↑⊥ : Submodule R M) ↔ N = ⊥
rw₁ rw₂ : (↑{ toSubmodule := N, lie_mem := @h : LieSubmodule R L M } : Submodule R M) = ⊥ ↔ N = ⊥
⊢ { toSubmodule := N, lie_mem := @h : LieSubmodule R L M } = ⊥ ↔ N = ⊥

Tactic:
rw [← toSubmodule_inj, bot_toSubmodule]

Premises used: LieSubmodule.bot_toSubmodule, LieSubmodule.toSubmodule_inj
-- Module: Mathlib.Algebra.Lie.Submodule
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
x : M
⊢ Membership.mem (γ := LieSubmodule R L M) ⊥ x ↔ x = 0

Tactic:
mem_singleton_iff

Premises used: Set.Mem, setOf, Set.mem_singleton_iff, Set.singleton
-- Module: Mathlib.Algebra.Lie.Submodule
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
⊢ (↑⊤ : Set M) = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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
⊢ Eq.{w + 1} (α := Submodule R M) (↑⊤ : Submodule R M) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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
rw : (↑N : Submodule R M) = ⊤ ↔ (↑N : Submodule R M) = (↑⊤ : Submodule R M)
rw₁ rw₂ : (↑N : Submodule R M) = ⊤ ↔ (↑N : Submodule R M) = ⊤
⊢ (↑N : Submodule R M) = ⊤ ↔ N = ⊤

Tactic:
rw [← toSubmodule_inj, top_toSubmodule]

Premises used: LieSubmodule.top_toSubmodule, LieSubmodule.toSubmodule_inj
-- Module: Mathlib.Algebra.Lie.Submodule
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 : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier
rw : (↑{ toSubmodule := N, lie_mem := @h : LieSubmodule R L M } : Submodule R M) = (↑⊤ : Submodule R M) ↔ N = ⊤
rw₁ rw₂ : (↑{ toSubmodule := N, lie_mem := @h : LieSubmodule R L M } : Submodule R M) = ⊤ ↔ N = ⊤
⊢ { toSubmodule := N, lie_mem := @h : LieSubmodule R L M } = ⊤ ↔ N = ⊤

Tactic:
rw [← toSubmodule_inj, top_toSubmodule]

Premises used: LieSubmodule.top_toSubmodule, LieSubmodule.toSubmodule_inj
-- Module: Mathlib.Algebra.Lie.Submodule
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
x : M
⊢ Membership.mem (γ := LieSubmodule R L M) ⊤ x

Tactic:
mem_univ x

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.Algebra.Lie.Submodule
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
S : Set (LieSubmodule R L M)
x : L
m : M
h :
  Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u, w} (R := R) (sInf {x : Submodule R M | ∃ s ∈ S, (↑s : Submodule R M) = x}))))
    m
simp : ∀ (h : ∀ a ∈ S, m ∈ (↑(↑a : Submodule R M) : Set M)), ∀ a ∈ S, ⁅x, m⁆ ∈ (↑(↑a : Submodule R M) : Set M)
⊢ Membership.mem (γ := Set M)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u, w} (R := R) (sInf {x : Submodule R M | ∃ s ∈ S, (↑s : Submodule R M) = x}))))
    ⁅x, m⁆

Tactic:
simp only [Submodule.mem_carrier, mem_iInter, Submodule.coe_sInf, mem_setOf_eq,
          forall_apply_eq_imp_iff₂, forall_exists_index, and_imp] at h ⊢

Premises used: and_imp, forall_exists_index, Set.mem_setOf_eq, Set.mem_iInter, Submodule.mem_carrier, forall_apply_eq_imp_iff₂, Submodule.coe_sInf
-- Module: Mathlib.Algebra.Lie.Submodule
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_1 N' : LieSubmodule R L M
S : Set (LieSubmodule R L M)
x : L
m : M
h : ∀ a ∈ S, m ∈ (↑(↑a : Submodule R M) : Set M)
N : LieSubmodule R L M
hN : N ∈ S
⊢ ⁅x, m⁆ ∈ (↑(↑N : Submodule R M) : Set M)

Tactic:
apply N.lie_mem (h N hN)

Premises used: LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.Submodule
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
⊢ (↑(N ⊓ N') : Set M) = (↑N : Set M) ∩ (↑N' : Set M)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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
⊢ (↑(N ⊓ N') : Submodule R M) = (↑N : Submodule R M) ⊓ (↑N' : Submodule R M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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
S : Set (LieSubmodule R L M)
⊢ (↑(sInf S) : Submodule R M) = sInf {x : Submodule R M | ∃ s ∈ S, (↑s : Submodule R M) = x}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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
S : Set (LieSubmodule R L M)
rw :
  Eq.{w + 1} (α := Submodule R M) (sInf {x : Submodule R M | ∃ s ∈ S, (↑s : Submodule R M) = x})
    (⨅ N ∈ S, (↑N : Submodule R M))
rw₁ : sInf (toSubmodule '' S) = ⨅ N ∈ S, (↑N : Submodule R M)
rw₂ rw₃ : Eq.{w + 1} (α := Submodule R M) (⨅ a ∈ S, (↑a : Submodule R M)) (⨅ N ∈ S, (↑N : Submodule R M))
⊢ (↑(sInf S) : Submodule R M) = ⨅ N ∈ S, (↑N : Submodule R M)

Tactic:
rw [sInf_toSubmodule, ← Set.image, sInf_image]

Premises used: LieSubmodule.sInf_toSubmodule, sInf_image, Set.image
-- Module: Mathlib.Algebra.Lie.Submodule
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
ι : Sort u_1
p : ι → LieSubmodule R L M
h :
  ∀ (x : M),
    Membership.mem (γ := Submodule R M)
        (sInf
          {x : Submodule R M |
            ∃ (s : LieSubmodule R L M),
              Membership.mem (γ := Set (LieSubmodule R L M)) (range fun (i : ι) ↦ p i) s ∧ (↑s : Submodule R M) = x})
        x ↔
      Membership.mem (γ := Submodule R M) (⨅ (i : ι), (↑(p i) : Submodule R M)) x
⊢ Eq.{w + 1} (α := Submodule R M)
    (sInf
      {x : Submodule R M |
        ∃ (s : LieSubmodule R L M),
          Membership.mem (γ := Set (LieSubmodule R L M)) (range fun (i : ι) ↦ p i) s ∧ (↑s : Submodule R M) = x})
    (⨅ (i : ι), (↑(p i) : Submodule R M))

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Submodule
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
ι : Sort u_1
p : ι → LieSubmodule R L M
x : M
⊢ Membership.mem (γ := Submodule R M)
      (sInf
        {x : Submodule R M |
          ∃ (s : LieSubmodule R L M),
            Membership.mem (γ := Set (LieSubmodule R L M)) (range fun (i : ι) ↦ p i) s ∧ (↑s : Submodule R M) = x})
      x ↔
    Membership.mem (γ := Submodule R M) (⨅ (i : ι), (↑(p i) : Submodule R M)) x

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Submodule
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
S : Set (LieSubmodule R L M)
h :
  ∀ (m : M),
    Membership.mem (γ := Set M)
        (⋂ (p : Submodule R M),
          ⋂ (_ : Membership.mem (γ := Set (Submodule R M)) {x : Submodule R M | ∃ s ∈ S, (↑s : Submodule R M) = x} p),
            (↑p : Set M))
        m ↔
      Membership.mem (γ := Set M) (⋂ s ∈ S, (↑s : Set M)) m
⊢ Eq.{w + 1} (α := Set M)
    (⋂ (p : Submodule R M),
      ⋂ (_ : Membership.mem (γ := Set (Submodule R M)) {x : Submodule R M | ∃ s ∈ S, (↑s : Submodule R M) = x} p),
        (↑p : Set M))
    (⋂ s ∈ S, (↑s : Set M))

Tactic:
ext m
-- Module: Mathlib.Algebra.Lie.Submodule
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
S : Set (LieSubmodule R L M)
m : M
⊢ Membership.mem (γ := Set M)
      (⋂ (p : Submodule R M),
        ⋂ (_ : Membership.mem (γ := Set (Submodule R M)) {x : Submodule R M | ∃ s ∈ S, (↑s : Submodule R M) = x} p),
          (↑p : Set M))
      m ↔
    Membership.mem (γ := Set M) (⋂ s ∈ S, (↑s : Set M)) m

Tactic:
simp only [mem_iInter, mem_setOf_eq, forall_apply_eq_imp_iff₂, exists_imp,
    and_imp, SetLike.mem_coe, mem_toSubmodule]

Premises used: LieSubmodule.mem_toSubmodule, and_imp, Set.mem_setOf_eq, Set.mem_iInter, SetLike.mem_coe, exists_imp, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Algebra.Lie.Submodule
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
ι : Sort u_1
p : ι → LieSubmodule R L M
rw :
  Eq.{w + 1} (α := Set M)
    (⋂ (s : LieSubmodule R L M),
      ⋂ (_ : Membership.mem (γ := Set (LieSubmodule R L M)) (range fun (i : ι) ↦ p i) s), (↑s : Set M))
    (⋂ (i : ι), (↑(p i) : Set M))
⊢ (↑(⨅ (i : ι), p i) : Set M) = ⋂ (i : ι), (↑(p i) : Set M)

Tactic:
rw [iInf, coe_sInf]

Premises used: iInf, LieSubmodule.coe_sInf
-- Module: Mathlib.Algebra.Lie.Submodule
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
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ Eq.{w + 1} (α := Set M)
    (⋂ (s : LieSubmodule R L M),
      ⋂ (_ : Membership.mem (γ := Set (LieSubmodule R L M)) (range fun (i : ι) ↦ p i) s), (↑s : Set M))
    (⋂ (i : ι), (↑(p i) : Set M))

Tactic:
simp only [Set.mem_range, Set.iInter_exists, Set.iInter_iInter_eq']

Premises used: Set.mem_range, Set.iInter_exists, Set.iInter_iInter_eq'
-- Module: Mathlib.Algebra.Lie.Submodule
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
ι : Sort u_1
p : ι → LieSubmodule R L M
x : M
rw : (∀ (i : ι), x ∈ (↑(p i) : Set M)) ↔ ∀ (i : ι), x ∈ p i
⊢ Membership.mem (γ := LieSubmodule R L M) (⨅ (i : ι), p i) x ↔ ∀ (i : ι), x ∈ p i

Tactic:
rw [← SetLike.mem_coe, coe_iInf, Set.mem_iInter]

Premises used: Set.mem_iInter, SetLike.mem_coe, LieSubmodule.coe_iInf
-- Module: Mathlib.Algebra.Lie.Submodule
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
ι : Sort u_1
p : ι → LieSubmodule R L M
x : M
⊢ (∀ (i : ι), x ∈ (↑(p i) : Set M)) ↔ ∀ (i : ι), x ∈ p i

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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_1 N'_1 N N' : LieSubmodule R L M
x : L
m : M
hm : m ∈ (↑N : Submodule R M) ⊔ (↑N' : Submodule R M)
rw :
  ∀ (hm : ∃ y ∈ (↑N : Submodule R M), ∃ z ∈ (↑N' : Submodule R M), y + z = m),
    ∃ y ∈ (↑N : Submodule R M), ∃ z ∈ (↑N' : Submodule R M), y + z = ⁅x, m⁆
⊢ ⁅x, m⁆ ∈ (↑N : Submodule R M) ⊔ (↑N' : Submodule R M)

Tactic:
rw [Submodule.mem_sup] at hm ⊢

Premises used: Submodule.mem_sup
-- Module: Mathlib.Algebra.Lie.Submodule
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_1 N'_1 N N' : LieSubmodule R L M
x : L
m : M
hm : ∃ y ∈ (↑N : Submodule R M), ∃ z ∈ (↑N' : Submodule R M), y + z = m
obtain :
  ∀ (y : M) (hy : y ∈ (↑N : Submodule R M)) (z : M) (hz : z ∈ (↑N' : Submodule R M)),
    ∃ y_1 ∈ (↑N : Submodule R M), ∃ z_1 ∈ (↑N' : Submodule R M), y_1 + z_1 = ⁅x, y + z⁆
⊢ ∃ y ∈ (↑N : Submodule R M), ∃ z ∈ (↑N' : Submodule R M), y + z = ⁅x, m⁆

Tactic:
obtain ⟨y, hy, z, hz, rfl⟩ := hm

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Submodule
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_1 N'_1 N N' : LieSubmodule R L M
x : L
y : M
hy : y ∈ (↑N : Submodule R M)
z : M
hz : z ∈ (↑N' : Submodule R M)
⊢ ∃ y_1 ∈ (↑N : Submodule R M), ∃ z_1 ∈ (↑N' : Submodule R M), y_1 + z_1 = ⁅x, y + z⁆

Tactic:
⟨⁅x, y⁆, N.lie_mem hy, ⁅x, z⁆, N'.lie_mem hz, (lie_add _ _ _).symm⟩

Premises used: Bracket.bracket, LieSubmodule.lie_mem, And.intro, Exists.intro, Eq.symm, lie_add
-- Module: Mathlib.Algebra.Lie.Submodule
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_1 N'_1 N N' : LieSubmodule R L M
x : L
y : M
hy : y ∈ (↑N : Submodule R M)
z : M
hz : z ∈ (↑N' : Submodule R M)
⊢ ∃ y_1 ∈ (↑N : Submodule R M), ∃ z_1 ∈ (↑N' : Submodule R M), y_1 + z_1 = ⁅x, y + z⁆

Tactic:
exact ⟨⁅x, y⁆, N.lie_mem hy, ⁅x, z⁆, N'.lie_mem hz, (lie_add _ _ _).symm⟩
-- Module: Mathlib.Algebra.Lie.Submodule
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
S : Set (LieSubmodule R L M)
x : L
m : M
m₁ :
  ∀ (hm : Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) m),
    Membership.mem (γ := Set M)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid.{u, w} (R := R) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}))))
      ⁅x, m⁆
⊢ Membership.mem (γ := Set M)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid.{u, w} (R := R) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}))))
      m →
    Membership.mem (γ := Set M)
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid.{u, w} (R := R) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}))))
      ⁅x, m⁆

Tactic:
(hm : m ∈ sSup {(p : Submodule R M) | p ∈ S})
-- Module: Mathlib.Algebra.Lie.Submodule
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
S : Set (LieSubmodule R L M)
x : L
m : M
hm : Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) m
obtain :
  ∀ (s : Finset (Submodule R M))
    (hs : (↑s : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ s, i) m),
    Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆

Tactic:
obtain ⟨s, hs, hsm⟩ := Submodule.mem_sSup_iff_exists_finset.mp hm

Premises used: Iff.mp, Submodule.mem_sSup_iff_exists_finset