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 N' : LieSubmodule R L M
S : Set (LieSubmodule R L M)
x : L
m : M
hs : (↑∅ : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
hsm :
  Membership.mem (γ := Submodule R M)
    (⨆ (i : Submodule R M), ⨆ (_ : Membership.mem (γ := Finset (Submodule R M)) ∅ i), i) m
⊢ m = 0

Tactic:
simpa using hsm
-- 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
hs : (↑∅ : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
hsm :
  Membership.mem (γ := Submodule R M)
    (⨆ (i : Submodule R M), ⨆ (_ : Membership.mem (γ := Finset (Submodule R M)) ∅ i), i) m
⊢ m = 0

Tactic:
replace hsm : m = 0 := by simpa using hsm
-- 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
hs : (↑∅ : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
hsm : m = 0
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆

Tactic:
simp [hsm]
-- 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
q : Submodule R M
t : Finset (Submodule R M)
hqt : q ∉ t
ih :
  ∀ {m : M} (hs : (↑t : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ t, i) m),
    Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
m : M
hs : (↑(insert q t) : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ insert q t, i) m
⊢ m ∈ q ⊔ ⨆ x ∈ t, x

Tactic:
rw [Finset.iSup_insert] at hsm

Premises used: Finset.iSup_insert
-- 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
q : Submodule R M
t : Finset (Submodule R M)
hqt : q ∉ t
ih :
  ∀ {m : M} (hs : (↑t : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ t, i) m),
    Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
m : M
hs : (↑(Insert.insert q t) : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
hsm : m ∈ q ⊔ ⨆ x ∈ t, x
insert :
  ∀ (m' : M) (hm' : m' ∈ q) (u : M) (hu : Membership.mem (γ := Submodule R M) (⨆ x ∈ t, x) u)
    (hsm : m' + u ∈ q ⊔ ⨆ x ∈ t, x),
    Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m' + u⁆
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆

Tactic:
obtain ⟨m', hm', u, hu, rfl⟩ := Submodule.mem_sup.mp hsm

Premises used: Iff.mp, Submodule.mem_sup, 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
S : Set (LieSubmodule R L M)
x : L
q : Submodule R M
t : Finset (Submodule R M)
hqt : q ∉ t
ih :
  ∀ {m : M} (hs : (↑t : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ t, i) m),
    Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
hs : (↑(Insert.insert q t) : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
m' : M
hm' : m' ∈ q
u : M
hu : Membership.mem (γ := Submodule R M) (⨆ x ∈ t, x) u
hsm : m' + u ∈ q ⊔ ⨆ x ∈ t, x
insert :
  Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) (⁅x, m'⁆ + ⁅x, u⁆)
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m' + u⁆

Tactic:
rw [lie_add]

Premises used: 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 N' : LieSubmodule R L M
S : Set (LieSubmodule R L M)
x : L
q : Submodule R M
t : Finset (Submodule R M)
hqt : q ∉ t
ih :
  ∀ {m : M} (hs : (↑t : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ t, i) m),
    Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
hs : (↑(insert q t) : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
m' : M
hm' : m' ∈ q
u : M
hu : Membership.mem (γ := Submodule R M) (⨆ x ∈ t, x) u
hsm : m' + u ∈ q ⊔ ⨆ x ∈ t, x
⊢ (↑t : Set (Submodule R M)) ⊆ (↑(insert q t) : Set (Submodule R M))

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
N N' : LieSubmodule R L M
S : Set (LieSubmodule R L M)
x : L
q : Submodule R M
t : Finset (Submodule R M)
hqt : q ∉ t
ih :
  ∀ {m : M} (hs : (↑t : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ t, i) m),
    Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
hs : (↑(Insert.insert q t) : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
m' : M
hm' : m' ∈ q
u : M
hu : Membership.mem (γ := Submodule R M) (⨆ x ∈ t, x) u
hsm : m' + u ∈ q ⊔ ⨆ x ∈ t, x
insert : 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'⁆ + ⁅x, u⁆)

Tactic:
refine add_mem ?_ (ih (Subset.trans (by simp) hs) hu)

Premises used: Set.Subset.trans, AddMemClass.add_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
S : Set (LieSubmodule R L M)
x : L
q : Submodule R M
t : Finset (Submodule R M)
hqt : q ∉ t
ih :
  ∀ {m : M} (hs : (↑t : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ t, i) m),
    Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
hs : (↑(insert q t) : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
m' : M
hm' : m' ∈ q
u : M
hu : Membership.mem (γ := Submodule R M) (⨆ x ∈ t, x) u
hsm : m' + u ∈ q ⊔ ⨆ x ∈ t, x
⊢ ∃ p ∈ S, (↑p : Submodule R M) = q

Tactic:
hs (Finset.mem_insert_self q t)

Premises used: Finset.mem_insert_self, Set.Mem, setOf
-- 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
q : Submodule R M
t : Finset (Submodule R M)
hqt : q ∉ t
ih :
  ∀ {m : M} (hs : (↑t : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ t, i) m),
    Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
hs : (↑(Insert.insert q t) : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
m' : M
hm' : m' ∈ q
u : M
hu : Membership.mem (γ := Submodule R M) (⨆ x ∈ t, x) u
hsm : m' + u ∈ q ⊔ ⨆ x ∈ t, x
insert :
  ∀ (p : LieSubmodule R L M) (hp : p ∈ S) (hqt : (↑p : Submodule R M) ∉ t)
    (hs :
      (↑(Insert.insert (↑p : Submodule R M) t) : Set (Submodule R M)) ⊆
        {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hm' : m' ∈ (↑p : Submodule R M)) (hsm : m' + u ∈ (↑p : Submodule R M) ⊔ ⨆ x ∈ t, x),
    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 ⟨p, hp, rfl⟩ : ∃ p ∈ S, ↑p = q := hs (Finset.mem_insert_self q t)

Premises used: Finset.mem_insert_self, 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
S : Set (LieSubmodule R L M)
x : L
t : Finset (Submodule R M)
ih :
  ∀ {m : M} (hs : (↑t : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ t, i) m),
    Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
m' u : M
hu : Membership.mem (γ := Submodule R M) (⨆ x ∈ t, x) u
p : LieSubmodule R L M
hp : p ∈ S
hqt : (↑p : Submodule R M) ∉ t
hs : (↑(insert (↑p : Submodule R M) t) : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
hm' : m' ∈ (↑p : Submodule R M)
hsm : m' + u ∈ (↑p : Submodule R M) ⊔ ⨆ x ∈ t, x
this : (↑p : Submodule R M) ≤ sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m'⁆

Tactic:
this (p.lie_mem hm')

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
S : Set (LieSubmodule R L M)
x : L
t : Finset (Submodule R M)
ih :
  ∀ {m : M} (hs : (↑t : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ t, i) m),
    Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
m' u : M
hu : Membership.mem (γ := Submodule R M) (⨆ x ∈ t, x) u
p : LieSubmodule R L M
hp : p ∈ S
hqt : (↑p : Submodule R M) ∉ t
hs : (↑(insert (↑p : Submodule R M) t) : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
hm' : m' ∈ (↑p : Submodule R M)
hsm : m' + u ∈ (↑p : Submodule R M) ⊔ ⨆ x ∈ t, x
this : (↑p : Submodule R M) ≤ sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m'⁆

Tactic:
exact this (p.lie_mem hm')

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
S : Set (LieSubmodule R L M)
x : L
t : Finset (Submodule R M)
ih :
  ∀ {m : M} (hs : (↑t : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ t, i) m),
    Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
m' u : M
hu : Membership.mem (γ := Submodule R M) (⨆ x ∈ t, x) u
p : LieSubmodule R L M
hp : p ∈ S
hqt : (↑p : Submodule R M) ∉ t
hs :
  (↑(Insert.insert (↑p : Submodule R M) t) : Set (Submodule R M)) ⊆
    {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
hm' : m' ∈ (↑p : Submodule R M)
hsm : m' + u ∈ (↑p : Submodule R M) ⊔ ⨆ x ∈ t, x
insert : (↑p : Submodule R M) ≤ sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m'⁆

Tactic:
suffices p ≤ sSup {(p : Submodule R M) | p ∈ S} by exact this (p.lie_mem hm')
-- 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
t : Finset (Submodule R M)
ih :
  ∀ {m : M} (hs : (↑t : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ t, i) m),
    Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
m' u : M
hu : Membership.mem (γ := Submodule R M) (⨆ x ∈ t, x) u
p : LieSubmodule R L M
hp : p ∈ S
hqt : (↑p : Submodule R M) ∉ t
hs : (↑(insert (↑p : Submodule R M) t) : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
hm' : m' ∈ (↑p : Submodule R M)
hsm : m' + u ∈ (↑p : Submodule R M) ⊔ ⨆ x ∈ t, x
⊢ (↑p : Submodule R M) ≤ sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}

Tactic:
le_sSup ⟨p, hp, rfl⟩

Premises used: Set.Mem, And.intro, Exists.intro, le_sSup, 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
S : Set (LieSubmodule R L M)
x : L
t : Finset (Submodule R M)
ih :
  ∀ {m : M} (hs : (↑t : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ t, i) m),
    Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
m' u : M
hu : Membership.mem (γ := Submodule R M) (⨆ x ∈ t, x) u
p : LieSubmodule R L M
hp : p ∈ S
hqt : (↑p : Submodule R M) ∉ t
hs : (↑(insert (↑p : Submodule R M) t) : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
hm' : m' ∈ (↑p : Submodule R M)
hsm : m' + u ∈ (↑p : Submodule R M) ⊔ ⨆ x ∈ t, x
⊢ (↑p : Submodule R M) ≤ sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}

Tactic:
exact le_sSup ⟨p, hp, 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
S : Set (LieSubmodule R L M)
x : L
m : M
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
empty :
  ∀ {m : M} (hs : (↑∅ : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm :
      Membership.mem (γ := Submodule R M)
        (⨆ (i : Submodule R M), ⨆ (_ : Membership.mem (γ := Finset (Submodule R M)) ∅ i), i) m),
    Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
insert :
  ∀ (q : Submodule R M) (t : Finset (Submodule R M)) (hqt : q ∉ t)
    (ih :
      ∀ {m : M} (hs : (↑t : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
        (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ t, i) m),
        Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆)
    {m : M}
    (hs : (↑(Insert.insert q t) : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ Insert.insert q t, 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:
induction s using Finset.induction_on generalizing m with
        | empty =>
          replace hsm : m = 0 := by simpa using hsm
          simp [hsm]
        | insert q t hqt ih =>
          rw [Finset.iSup_insert] at hsm
          obtain ⟨m', hm', u, hu, rfl⟩ := Submodule.mem_sup.mp hsm
          rw [lie_add]
          refine add_mem ?_ (ih (Subset.trans (by simp) hs) hu)
          obtain ⟨p, hp, rfl⟩ : ∃ p ∈ S, ↑p = q := hs (Finset.mem_insert_self q t)
          suffices p ≤ sSup {(p : Submodule R M) | p ∈ S} by exact this (p.lie_mem hm')
          exact le_sSup ⟨p, hp, rfl⟩

Premises used: Insert.insert, Finset.iSup_insert, Iff.mp, Submodule.mem_sup, rfl, 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 N' : LieSubmodule R L M
S : Set (LieSubmodule R L M)
x : L
m : M
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
empty :
  ∀ {m : M} (hs : (↑∅ : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm :
      Membership.mem (γ := Submodule R M)
        (⨆ (i : Submodule R M), ⨆ (_ : Membership.mem (γ := Finset (Submodule R M)) ∅ i), i) m),
    Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
insert :
  ∀ (q : Submodule R M) (t : Finset (Submodule R M)) (hqt : q ∉ t)
    (ih :
      ∀ {m : M} (hs : (↑t : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
        (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ t, i) m),
        Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆)
    {m : M}
    (hs : (↑(Insert.insert q t) : Set (Submodule R M)) ⊆ {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x})
    (hsm : Membership.mem (γ := Submodule R M) (⨆ i ∈ Insert.insert q t, 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:
classical
        induction s using Finset.induction_on generalizing m with
        | empty =>
          replace hsm : m = 0 := by simpa using hsm
          simp [hsm]
        | insert q t hqt ih =>
          rw [Finset.iSup_insert] at hsm
          obtain ⟨m', hm', u, hu, rfl⟩ := Submodule.mem_sup.mp hsm
          rw [lie_add]
          refine add_mem ?_ (ih (Subset.trans (by simp) hs) hu)
          obtain ⟨p, hp, rfl⟩ : ∃ p ∈ S, ↑p = q := hs (Finset.mem_insert_self q t)
          suffices p ≤ sSup {(p : Submodule R M) | p ∈ S} by exact this (p.lie_mem hm')
          exact le_sSup ⟨p, hp, rfl⟩

Premises used: Insert.insert, Finset.iSup_insert, Iff.mp, Submodule.mem_sup, rfl, 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 N' : LieSubmodule R L M
⊢ (↑(N ⊔ N') : Submodule R M) = (↑N : Submodule R M) ⊔ (↑N' : Submodule R M)

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
S : Set (LieSubmodule R L M)
⊢ (↑(sSup S) : Submodule R M) = sSup {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) (sSup {x : Submodule R M | ∃ s ∈ S, (↑s : Submodule R M) = x})
    (⨆ N ∈ S, (↑N : Submodule R M))
rw₁ : sSup (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))
⊢ (↑(sSup S) : Submodule R M) = ⨆ N ∈ S, (↑N : Submodule R M)

Tactic:
rw [sSup_toSubmodule, ← Set.image, sSup_image]

Premises used: LieSubmodule.sSup_toSubmodule, sSup_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)
        (sSup
          {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)
    (sSup
      {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)
      (sSup
        {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 [Submodule.mem_sSup, Submodule.mem_iSup]

Premises used: Submodule.mem_sSup, Submodule.mem_iSup
-- 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
b : M
N : ι → LieSubmodule R L M
i : ι
h : b ∈ N i
⊢ Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) b

Tactic:
(le_iSup N i) h

Premises used: Set.Mem, setOf, le_iSup
-- 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
N : ι → LieSubmodule R L M
motive : M → Prop
x : M
hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x
mem : ∀ (i : ι), ∀ y ∈ N i, motive y
zero : motive 0
add : ∀ (y z : M), motive y → motive z → motive (y + z)
⊢ Membership.mem (γ := Submodule R M) (⨆ (i : ι), (↑(N i) : Submodule R M)) x

Tactic:
rw [← LieSubmodule.mem_toSubmodule, LieSubmodule.iSup_toSubmodule] at hx

Premises used: LieSubmodule.iSup_toSubmodule, LieSubmodule.mem_toSubmodule
-- 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
N : ι → LieSubmodule R L M
motive : M → Prop
x : M
hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x
mem : ∀ (i : ι), ∀ y ∈ N i, motive y
zero : motive 0
add : ∀ (y z : M), motive y → motive z → motive (y + z)
hx₁ : Membership.mem (γ := Submodule R M) (⨆ (i : ι), (↑(N i) : Submodule R M)) x
⊢ ∀ (i : ι), ∀ y ∈ N i, motive y

Tactic:
rw [← LieSubmodule.mem_toSubmodule, LieSubmodule.iSup_toSubmodule] at hx

Premises used: LieSubmodule.iSup_toSubmodule, LieSubmodule.mem_toSubmodule