awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
this : (Preorder.toLE : LE (Submodule R M)).1 T (S ⊔ T)
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
this
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
this : (Preorder.toLE : LE (Submodule R M)).1 T (S ⊔ T)
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
exact this
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
s t : M
hs : s ∈ S
ht : t ∈ T
⊢ s + t ∈ S ⊔ T

Tactic:
add_mem (mem_sup_left hs) (mem_sup_right ht)

Premises used: AddMemClass.add_mem, Submodule.mem_sup_left, Submodule.mem_sup_right
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R' : Type u_4
M' : Type u_5
inst : Ring R'
inst_1 : AddCommGroup M'
inst_2 : Module R' M'
S T : Submodule R' M'
s t : M'
hs : s ∈ S
ht : t ∈ T
rw : s + -t ∈ S ⊔ T
⊢ s - t ∈ S ⊔ T

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R' : Type u_4
M' : Type u_5
inst : Ring R'
inst_1 : AddCommGroup M'
inst_2 : Module R' M'
S T : Submodule R' M'
s t : M'
hs : s ∈ S
ht : t ∈ T
⊢ s + -t ∈ S ⊔ T

Tactic:
add_mem_sup hs (neg_mem ht)

Premises used: Set.Mem, Submodule.add_mem_sup, NegMemClass.neg_mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R' : Type u_4
M' : Type u_5
inst : Ring R'
inst_1 : AddCommGroup M'
inst_2 : Module R' M'
S T : Submodule R' M'
s t : M'
hs : s ∈ S
ht : t ∈ T
⊢ s + -t ∈ S ⊔ T

Tactic:
exact add_mem_sup hs (neg_mem ht)

Premises used: Submodule.add_mem_sup, NegMemClass.neg_mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Sort u_4
b : M
p : ι → Submodule R M
i : ι
h : b ∈ p i
⊢ Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) b

Tactic:
(le_iSup p i) h

Premises used: Set.Mem, setOf, le_iSup
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
inst_3 : Fintype ι
f : ι → M
p : ι → Submodule R M
h : ∀ (i : ι), f i ∈ p i
⊢ Membership.mem (γ := Submodule R M) (⨆ (i : ι), p i) (∑ i : ι, f i)

Tactic:
sum_mem fun i _ ↦ mem_iSup_of_mem i (h i)

Premises used: Submodule.mem_iSup_of_mem, sum_mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_4
s : Finset ι
f : ι → M
p : ι → Submodule R M
h : ∀ i ∈ s, f i ∈ p i
⊢ Membership.mem (γ := Submodule R M) (⨆ i ∈ s, p i) (∑ i ∈ s, f i)

Tactic:
sum_mem fun i hi ↦ mem_iSup_of_mem i <| mem_iSup_of_mem hi (h i hi)

Premises used: Submodule.mem_iSup_of_mem, sum_mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
⊢ s ≤ sSup S

Tactic:
have := le_sSup hs
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
this : s ≤ sSup S
⊢ (Preorder.toLE : LE (Submodule R M)).1 s (sSup S)

Tactic:
rw [LE.le] at this

Premises used: LE.le
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
this : (Preorder.toLE : LE (Submodule R M)).1 s (sSup S)
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
this

Premises used: Set.Mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Set (Submodule R M)
s : Submodule R M
hs : s ∈ S
this : (Preorder.toLE : LE (Submodule R M)).1 s (sSup S)
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
exact this
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ (sSup (toAddSubmonoid '' s)).carrier
simp_rw :
  ∀ (h : Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) m),
    Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • m)
⊢ t • m ∈ (sSup (toAddSubmonoid '' s)).carrier

Tactic:
simp_rw [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, sSup_eq_iSup'] at h ⊢

Premises used: AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, sSup_eq_iSup'
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m : M
p : (↑(toAddSubmonoid '' s) : Type u_3)
x : M
hx : x ∈ (↑p : AddSubmonoid M)
mem :
  ∀ (p : Submodule R M) (hp : p ∈ s)
    (hx :
      x ∈
        (↑(Subtype.mk (p := fun (x : AddSubmonoid M) ↦ x ∈ toAddSubmonoid '' s) p.toAddSubmonoid ⋯) : AddSubmonoid M)),
    Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x)
⊢ Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x)

Tactic:
obtain ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ := p

Premises used: Submodule, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ (↑(Subtype.mk (p := fun (x : AddSubmonoid M) ↦ x ∈ toAddSubmonoid '' s) p.toAddSubmonoid ⋯) : AddSubmonoid M)
this : p.toAddSubmonoid ≤ ⨆ (q : (↑(toAddSubmonoid '' s) : Type u_3)), (↑q : AddSubmonoid M)
⊢ Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x)

Tactic:
this (smul_mem p t hx)

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ (↑(Subtype.mk (p := fun (x : AddSubmonoid M) ↦ x ∈ toAddSubmonoid '' s) p.toAddSubmonoid ⋯) : AddSubmonoid M)
this : p.toAddSubmonoid ≤ ⨆ (q : (↑(toAddSubmonoid '' s) : Type u_3)), (↑q : AddSubmonoid M)
⊢ Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x)

Tactic:
exact this (smul_mem p t hx)

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ (↑(Subtype.mk (p := fun (x : AddSubmonoid M) ↦ x ∈ toAddSubmonoid '' s) p.toAddSubmonoid ⋯) : AddSubmonoid M)
mem : p.toAddSubmonoid ≤ ⨆ (q : (↑(toAddSubmonoid '' s) : Type u_3)), (↑q : AddSubmonoid M)
⊢ Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x)

Tactic:
suffices p.toAddSubmonoid ≤ ⨆ q : toAddSubmonoid '' s, (q : AddSubmonoid M) by
            exact this (smul_mem p t hx)
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ (↑(Subtype.mk (p := fun (x : AddSubmonoid M) ↦ x ∈ toAddSubmonoid '' s) p.toAddSubmonoid ⋯) : AddSubmonoid M)
mem :
  Membership.mem (γ := Set (AddSubmonoid M))
    (Set.range fun (q : (↑(toAddSubmonoid '' s) : Type u_3)) ↦ (↑q : AddSubmonoid M)) p.toAddSubmonoid
⊢ p.toAddSubmonoid ≤ ⨆ (q : (↑(toAddSubmonoid '' s) : Type u_3)), (↑q : AddSubmonoid M)

Tactic:
apply le_sSup

Premises used: le_sSup
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ (↑(Subtype.mk (p := fun (x : AddSubmonoid M) ↦ x ∈ toAddSubmonoid '' s) p.toAddSubmonoid ⋯) : AddSubmonoid M)
mem : Membership.mem (γ := Set (AddSubmonoid M)) {x : AddSubmonoid M | x ∈ toAddSubmonoid '' s} p.toAddSubmonoid
⊢ Membership.mem (γ := Set (AddSubmonoid M))
    (Set.range fun (q : (↑(toAddSubmonoid '' s) : Type u_3)) ↦ (↑q : AddSubmonoid M)) p.toAddSubmonoid

Tactic:
rw [Subtype.range_coe_subtype]

Premises used: Subtype.range_coe_subtype
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ (↑(Subtype.mk (p := fun (x : AddSubmonoid M) ↦ x ∈ toAddSubmonoid '' s) p.toAddSubmonoid ⋯) : AddSubmonoid M)
⊢ Membership.mem (γ := Set (AddSubmonoid M)) {x : AddSubmonoid M | x ∈ toAddSubmonoid '' s} p.toAddSubmonoid

Tactic:
⟨p, hp, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m x : M
p : Submodule R M
hp : p ∈ s
hx : x ∈ (↑(Subtype.mk (p := fun (x : AddSubmonoid M) ↦ x ∈ toAddSubmonoid '' s) p.toAddSubmonoid ⋯) : AddSubmonoid M)
⊢ Membership.mem (γ := Set (AddSubmonoid M)) {x : AddSubmonoid M | x ∈ toAddSubmonoid '' s} p.toAddSubmonoid

Tactic:
exact ⟨p, hp, rfl⟩
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m : M
⊢ Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
    (HSMul.hSMul (β := M) t 0)

Tactic:
simpa only [smul_zero] using zero_mem _

Premises used: smul_zero, ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m x y : M
hx : Membership.mem (γ := AddSubmonoid M) (⨆ (i : (↑(toAddSubmonoid '' s) : Type u_3)), (↑i : AddSubmonoid M)) x
hy : Membership.mem (γ := AddSubmonoid M) (⨆ (i : (↑(toAddSubmonoid '' s) : Type u_3)), (↑i : AddSubmonoid M)) y
mx : Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x)
my : Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • y)
add :
  ∀
    (mx :
      Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x))
    (my :
      Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
        (t • y)),
    Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
      (t • (x + y))
⊢ Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
    (t • (x + y))

Tactic:
revert mx my
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m x y : M
hx : Membership.mem (γ := AddSubmonoid M) (⨆ (i : (↑(toAddSubmonoid '' s) : Type u_3)), (↑i : AddSubmonoid M)) x
hy : Membership.mem (γ := AddSubmonoid M) (⨆ (i : (↑(toAddSubmonoid '' s) : Type u_3)), (↑i : AddSubmonoid M)) y
add :
  ∀
    (mx :
      Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x))
    (my :
      Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
        (t • y)),
    Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
      (t • x + t • y)
⊢ ∀
    (mx :
      Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x))
    (my :
      Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
        (t • y)),
    Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
      (t • (x + y))

Tactic:
simp_rw [smul_add]

Premises used: smul_add
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m x y : M
hx : Membership.mem (γ := AddSubmonoid M) (⨆ (i : (↑(toAddSubmonoid '' s) : Type u_3)), (↑i : AddSubmonoid M)) x
hy : Membership.mem (γ := AddSubmonoid M) (⨆ (i : (↑(toAddSubmonoid '' s) : Type u_3)), (↑i : AddSubmonoid M)) y
⊢ ∀
    (mx :
      Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x))
    (my :
      Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
        (t • y)),
    Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
      (t • x + t • y)

Tactic:
add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m x y : M
hx : Membership.mem (γ := AddSubmonoid M) (⨆ (i : (↑(toAddSubmonoid '' s) : Type u_3)), (↑i : AddSubmonoid M)) x
hy : Membership.mem (γ := AddSubmonoid M) (⨆ (i : (↑(toAddSubmonoid '' s) : Type u_3)), (↑i : AddSubmonoid M)) y
⊢ ∀
    (mx :
      Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x))
    (my :
      Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
        (t • y)),
    Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
      (t • x + t • y)

Tactic:
exact add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
t : R
m : M
h : Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) m
mem :
  ∀ (p : (↑(toAddSubmonoid '' s) : Type u_3)) (x : M) (hx : x ∈ (↑p : AddSubmonoid M)),
    Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • x)
zero :
  Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
    (HSMul.hSMul (β := M) t 0)
add :
  ∀ (x y : M),
    Membership.mem (γ := AddSubmonoid M) (⨆ (i : (↑(toAddSubmonoid '' s) : Type u_3)), (↑i : AddSubmonoid M)) x →
      Membership.mem (γ := AddSubmonoid M) (⨆ (i : (↑(toAddSubmonoid '' s) : Type u_3)), (↑i : AddSubmonoid M)) y →
        ∀
          (mx :
            Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
              (t • x))
          (my :
            Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
              (t • y)),
          Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M))
            (t • (x + y))
⊢ Membership.mem (γ := AddSubmonoid M) (⨆ (a : (↑(toAddSubmonoid '' s) : Type u_3)), (↑a : AddSubmonoid M)) (t • m)

Tactic:
induction h using AddSubmonoid.iSup_induction' with
        | mem p x hx =>
          obtain ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ := p
          suffices p.toAddSubmonoid ≤ ⨆ q : toAddSubmonoid '' s, (q : AddSubmonoid M) by
            exact this (smul_mem p t hx)
          apply le_sSup
          rw [Subtype.range_coe_subtype]
          exact ⟨p, hp, rfl⟩
        | zero => simpa only [smul_zero] using zero_mem _
        | add _ _ _ _ mx my => revert mx my; simp_rw [smul_add]; exact add_mem

Premises used: Submodule, smul_zero, Subtype.range_coe_subtype, AddMemClass.add_mem, Submodule.zero, ZeroMemClass.zero_mem, le_sSup, Submodule.add, smul_add, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
p : Submodule R M :=
  let __AddSubmonoid := sSup (toAddSubmonoid '' s);
  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
⊢ (sSup s).toAddSubmonoid = sSup (toAddSubmonoid '' s)

Tactic:
le_antisymm (?_ : sSup s ≤ p) ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
p : Submodule R M :=
  let __AddSubmonoid := sSup (toAddSubmonoid '' s);
  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
refine_1 : sSup s ≤ p
refine_2 : sSup (toAddSubmonoid '' s) ≤ (sSup s).toAddSubmonoid
⊢ (sSup s).toAddSubmonoid = sSup (toAddSubmonoid '' s)

Tactic:
refine le_antisymm (?_ : sSup s ≤ p) ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
p : Submodule R M :=
  let __AddSubmonoid := sSup (toAddSubmonoid '' s);
  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
⊢ sSup s ≤ p

Tactic:
sSup_le fun q hq ↦ le_sSup <| Set.mem_image_of_mem toAddSubmonoid hq

Premises used: Submodule.toAddSubmonoid, Set.Mem, Set.mem_image_of_mem, le_sSup, sSup_le
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
p : Submodule R M :=
  let __AddSubmonoid := sSup (toAddSubmonoid '' s);
  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
⊢ sSup s ≤ p

Tactic:
exact sSup_le fun q hq ↦ le_sSup <| Set.mem_image_of_mem toAddSubmonoid hq

Premises used: Submodule.toAddSubmonoid, Set.mem_image_of_mem, le_sSup, sSup_le
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
p : Submodule R M :=
  let __AddSubmonoid := sSup (toAddSubmonoid '' s);
  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
⊢ sSup (toAddSubmonoid '' s) ≤ (sSup s).toAddSubmonoid

Tactic:
sSup_le fun _ ⟨q, hq, hq'⟩ ↦ hq'.symm ▸ le_sSup hq

Premises used: Submodule.toAddSubmonoid, Set.Mem, Eq.rec, LE.le, _private.0.Submodule.toAddSubmonoid_sSup.match_2, le_sSup, sSup_le, Eq.symm, SupSet.sSup
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set (Submodule R M)
p : Submodule R M :=
  let __AddSubmonoid := sSup (toAddSubmonoid '' s);
  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
⊢ sSup (toAddSubmonoid '' s) ≤ (sSup s).toAddSubmonoid

Tactic:
exact sSup_le fun _ ⟨q, hq, hq'⟩ ↦ hq'.symm ▸ le_sSup hq
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw : Eq.{u_3 + 1} (α := Submodule R M) ⊥ ⊤ ↔ Subsingleton.{u_3 + 1} (AddSubmonoid M)
rw₁ : Eq.{u_3 + 1} (α := Submodule R M) ⊥ ⊤ ↔ Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ ⊤
rw₂ :
  Eq.{u_3 + 1} (α := AddSubmonoid M) (toAddSubmonoid.{u_1, u_3} (R := R) ⊥) (toAddSubmonoid.{u_1, u_3} (R := R) ⊤) ↔
    Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ ⊤
rw₃ :
  Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ (toAddSubmonoid.{u_1, u_3} (R := R) ⊤) ↔ Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ ⊤
rw₄ rw₅ : Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ ⊤ ↔ Eq.{u_3 + 1} (α := AddSubmonoid M) ⊥ ⊤
⊢ Subsingleton.{u_3 + 1} (Submodule R M) ↔ Subsingleton.{u_3 + 1} (AddSubmonoid M)

Tactic:
rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toAddSubmonoid_inj,
      bot_toAddSubmonoid, top_toAddSubmonoid]

Premises used: Submodule.top_toAddSubmonoid, Submodule.bot_toAddSubmonoid, Submodule.toAddSubmonoid_inj, subsingleton_iff_bot_eq_top
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Nontrivial.{u_3} (Submodule R M) ↔ Nontrivial M

Tactic:
not_iff_not.mp
    ((not_nontrivial_iff_subsingleton.trans <| subsingleton_iff R).trans
      not_nontrivial_iff_subsingleton.symm)

Premises used: not_iff_not, Submodule.subsingleton_iff, not_nontrivial_iff_subsingleton, Iff.mp, Iff.trans, Iff.symm
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
p q : Submodule R M
inst_7 : Subsingleton R
⊢ Subsingleton M

Tactic:
haveI := Module.subsingleton R M
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
p q : Submodule R M
inst_7 : Subsingleton R
this : Subsingleton M
⊢ Unique (Submodule R M)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
p q : Submodule R M
inst_7 : Nontrivial M
⊢ Nontrivial.{u_3} (Submodule R M)

Tactic:
(nontrivial_iff R).mpr ‹_›

Premises used: Iff.mpr, Submodule.nontrivial_iff
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p p' : Submodule R M
⊢ (∀ (x : M), x ∈ p ∧ x ∈ p' → Membership.mem (γ := Set M) {0} x) ↔ ∀ x ∈ p, x ∈ p' → x = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p p' : Submodule R M
⊢ Disjoint p p' ↔ ∀ x ∈ p, ∀ y ∈ p', x = y → x = 0

Tactic:
disjoint_def.trans
    ⟨fun h x hx _ hy hxy ↦ h x hx <| hxy.symm ▸ hy, fun h x hx hx' ↦ h _ hx x hx' rfl⟩

Premises used: Eq.rec, Iff.intro, Iff.trans, Submodule.disjoint_def, Eq.symm, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
hpq : Disjoint p q
a : ↥p
ha : (↑a : M) ∈ q
⊢ a = 0

Tactic:
mod_cast disjoint_def.mp hpq a (coe_mem a) ha

Premises used: ZeroMemClass.coe_eq_zero._simp_1, cast, Submodule.coe_mem, Iff.mp, Submodule.disjoint_def, Subtype.val
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p p' : Submodule R M
h : Disjoint p p'
x : ↥p
⊢ (↑x : M) ∈ p' ↔ x = 0

Tactic:
⟨fun hx => coe_eq_zero.1 <| disjoint_def.1 h x x.2 hx, fun h => h.symm ▸ p'.zero_mem⟩

Premises used: Eq.rec, Submodule.zero_mem, Iff.intro, Iff.mp, Submodule.coe_eq_zero, Submodule.disjoint_def, Eq.symm, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Module.Submodule.Lattice
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p p' : Submodule R M
h : Disjoint p p'
x : ↥p'
⊢ (↑x : M) ∈ p ↔ x = 0

Tactic:
⟨fun hx => coe_eq_zero.1 <| disjoint_def.1 h x hx x.2, fun h => h.symm ▸ p.zero_mem⟩

Premises used: Eq.rec, Submodule.zero_mem, Iff.intro, Iff.mp, Submodule.coe_eq_zero, Submodule.disjoint_def, Eq.symm, Subtype.val, Subtype.property