awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
S : Set (LieSubmodule R L M)
x : L
m : 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⁆
have 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⁆
Tactic: (hm : m ∈ sSup {(p : Submodule R M) | p ∈ S})
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
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
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
have 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⁆
Tactic: obtain ⟨s, hs, hsm⟩ := Submodule.mem_sSup_iff_exists_finset.mp hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (hypothesis)
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
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
have hsm₁ : m = 0
Tactic: replace hsm : m = 0 := by simpa using hsm
Cleared hypotheses: hsm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (hypothesis)
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
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
have hsm₁ : m ∈ q ⊔ ⨆ x ∈ t, x
Tactic: rw [Finset.iSup_insert] at hsm
Cleared hypotheses: hsm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
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 : m ∈ q ⊔ ⨆ x ∈ t, x
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
have 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⁆
Tactic: obtain ⟨m', hm', u, hu, rfl⟩ := Submodule.mem_sup.mp hsm
Cleared hypotheses: m, hsm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
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
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m' + u⁆
have insert : Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) (⁅x, m'⁆ + ⁅x, u⁆)
Tactic: rw [lie_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
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
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) (⁅x, m'⁆ + ⁅x, u⁆)
have insert : Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m'⁆
Tactic: refine add_mem ?_ (ih (Subset.trans (by simp) hs) hu)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
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
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m'⁆
have insert : ∀ (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),
  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)
Cleared hypotheses: q, hqt, hs, hm', hsm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
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
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m'⁆
have insert : (↑p : Submodule R M) ≤ sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}
Tactic: suffices p ≤ sSup {(p : Submodule R M) | p ∈ S} by exact this (p.lie_mem hm')
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
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
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
have 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⁆
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⟩
Cleared hypotheses: m, s, hs, hsm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
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⁆
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
have 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 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),
  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⟩
Cleared hypotheses: m, s, hs, hsm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
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
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
have 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⁆
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⟩
Cleared hypotheses: m, s, hs, hsm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
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⁆
⊢ Membership.mem (γ := Submodule R M) (sSup {x : Submodule R M | ∃ p ∈ S, (↑p : Submodule R M) = x}) ⁅x, m⁆
have 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 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),
  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⟩
Cleared hypotheses: m, s, hs, hsm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
S : Set (LieSubmodule R L M)
⊢ (↑(sSup S) : Submodule R M) = ⨆ N ∈ S, (↑N : Submodule R M)
have 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))
Tactic: rw [sSup_toSubmodule, ← Set.image, sSup_image]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
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))
⊢ (↑(sSup S) : Submodule R M) = ⨆ N ∈ S, (↑N : Submodule R M)
have rw₁ : sSup (toSubmodule '' S) = ⨆ N ∈ S, (↑N : Submodule R M)
Tactic: rw [sSup_toSubmodule, ← Set.image, sSup_image]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
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)
⊢ (↑(sSup S) : Submodule R M) = ⨆ N ∈ S, (↑N : Submodule R M)
have rw₂ : Eq.{w + 1} (α := Submodule R M) (⨆ a ∈ S, (↑a : Submodule R M)) (⨆ N ∈ S, (↑N : Submodule R M))
Tactic: rw [sSup_toSubmodule, ← Set.image, sSup_image]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ 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))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (hypothesis)
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)
⊢ motive x
have hx₁ : Membership.mem (γ := Submodule R M) (⨆ (i : ι), (↑(N i) : Submodule R M)) x
Tactic: rw [← LieSubmodule.mem_toSubmodule, LieSubmodule.iSup_toSubmodule] at hx
Cleared hypotheses: hx, mem, zero, add
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
ι : Sort u_1
N : ι → LieSubmodule R L M
motive : (x : M) → Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x)
    (hy : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x
⊢ motive x hx
have refine : ∃ (x_1 : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x x_1
Tactic: refine Exists.elim ?_ fun (hx : x ∈ ⨆ i, N i) (hc : motive x hx) => hc
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
ι : Sort u_1
N : ι → LieSubmodule R L M
motive : (x : M) → Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x)
    (hy : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x
⊢ ∃ (x_1 : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x x_1
have refine_1 : ∀ (i : ι) (x : M) (hx : x ∈ N i),
  (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x hx) x
Tactic: refine iSup_induction N (motive := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, N i), motive x hx) hx
    (fun i x hx => ?_) ?_ fun x y => ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (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
ι : Sort u_1
N : ι → LieSubmodule R L M
motive : (x : M) → Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ N i), motive x ⋯
zero : motive 0 ⋯
add :
  ∀ (x y : M) (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x)
    (hy : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) y), motive x hx → motive y hy → motive (x + y) ⋯
x : M
hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x
refine_1 :
  ∀ (i : ι) (x : M) (hx : x ∈ N i),
    (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x hx) x
⊢ ∃ (x_1 : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x x_1
have refine_2 : (fun (x : M) ↦ ∃ (hx : Membership.mem (γ := LieSubmodule R L M) (⨆ (i : ι), N i) x), motive x hx) 0
Tactic: refine iSup_induction N (motive := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, N i), motive x hx) hx
    (fun i x hx => ?_) ?_ fun x y => ?_