-- Mathlib/Algebra/Module/Submodule/Lattice.lean
theorem toAddSubmonoid_sSup (s : Set (Submodule R M)) :
    (sSup s).toAddSubmonoid = sSup (toAddSubmonoid '' s)

Proof state:
case refine_1.mk.intro.intro.a
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
p : Submodule R M
hp : p ∈ s
x : M
hx : x ∈ p
⊢ p.toAddSubmonoid ∈ Set.range fun q => ↑q

Tactic:
rw [Subtype.range_coe_subtype]

Result:
case refine_1.mk.intro.intro.a
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
p : Submodule R M
hp : p ∈ s
x : M
hx : x ∈ p
⊢ p.toAddSubmonoid ∈ {x | x ∈ toAddSubmonoid '' s}

Proof state:
case refine_1
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
⊢ ∀ (i : ↑(toAddSubmonoid '' s)) (x : M) (hxS : x ∈ ↑i), (fun x x_1 => t • x ∈ ⨆ p, ↑p) x ⋯

Tactic:
rintro ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ x (hx : x ∈ p)

Result:
case refine_1.mk.intro.intro
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
p : Submodule R M
hp : p ∈ s
x : M
hx : x ∈ p
⊢ t • x ∈ ⨆ p, ↑p

Proof state:
case refine_1.mk.intro.intro
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
p : Submodule R M
hp : p ∈ s
x : M
hx : x ∈ p
⊢ t • x ∈ ⨆ p, ↑p

Tactic:
suffices p.toAddSubmonoid ≤ ⨆ q : toAddSubmonoid '' s, (q : AddSubmonoid M) by
  exact this (smul_mem p t hx)

Result:
case refine_1.mk.intro.intro
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
p : Submodule R M
hp : p ∈ s
x : M
hx : x ∈ p
⊢ p.toAddSubmonoid ≤ ⨆ q, ↑q

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
⊢ t • m ∈ ⨆ a, ↑a

Tactic:
refine AddSubmonoid.iSup_induction' _
  (C := fun x _ ↦ t • x ∈ ⨆ p : toAddSubmonoid '' s, (p : AddSubmonoid M)) ?_ ?_
  (fun x y _ _ ↦ ?_) h

Result:
case refine_1
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
⊢ ∀ (i : ↑(toAddSubmonoid '' s)) (x : M) (hxS : x ∈ ↑i), (fun x x_1 => t • x ∈ ⨆ p, ↑p) x ⋯

case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
⊢ (fun x x_1 => t • x ∈ ⨆ p, ↑p) 0 ⋯

case refine_3
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
x y : M
x✝¹ : x ∈ ⨆ i, ↑i
x✝ : y ∈ ⨆ i, ↑i
⊢ (fun x x_1 => t • x ∈ ⨆ p, ↑p) x x✝¹ → (fun x x_1 => t • x ∈ ⨆ p, ↑p) y x✝ → (fun x x_1 => t • x ∈ ⨆ p, ↑p) (x + y) ⋯

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
p : Submodule R M
hp : p ∈ s
x : M
hx : x ∈ p
this : p.toAddSubmonoid ≤ ⨆ q, ↑q
⊢ t • x ∈ ⨆ p, ↑p

Tactic:
exact this (smul_mem p t hx)

Result:
no goals

Proof state:
case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
⊢ (fun x x_1 => t • x ∈ ⨆ p, ↑p) 0 ⋯

Tactic:
simpa only [smul_zero] using zero_mem _

Result:
no goals

Proof state:
case refine_1.mk.intro.intro.a
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
p : Submodule R M
hp : p ∈ s
x : M
hx : x ∈ p
⊢ p.toAddSubmonoid ∈ {x | x ∈ toAddSubmonoid '' s}

Tactic:
exact ⟨p, hp, rfl⟩

Result:
no goals

Proof state:
case refine_1.mk.intro.intro
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
p : Submodule R M
hp : p ∈ s
x : M
hx : x ∈ p
⊢ p.toAddSubmonoid ≤ ⨆ q, ↑q

Tactic:
apply le_sSup

Result:
case refine_1.mk.intro.intro.a
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
p : Submodule R M
hp : p ∈ s
x : M
hx : x ∈ p
⊢ p.toAddSubmonoid ∈ Set.range fun q => ↑q

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ (sSup (toAddSubmonoid '' s)).carrier
⊢ t • m ∈ (sSup (toAddSubmonoid '' s)).carrier

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

Result:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
⊢ t • m ∈ ⨆ a, ↑a

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
p : Submodule R M := { toAddSubmonoid := sSup (toAddSubmonoid '' s), smul_mem' := ⋯ }
⊢ (sSup s).toAddSubmonoid = sSup (toAddSubmonoid '' s)

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

Result:
case refine_1
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
p : Submodule R M := { toAddSubmonoid := sSup (toAddSubmonoid '' s), smul_mem' := ⋯ }
⊢ sSup s ≤ p

case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
p : Submodule R M := { toAddSubmonoid := sSup (toAddSubmonoid '' s), smul_mem' := ⋯ }
⊢ sSup (toAddSubmonoid '' s) ≤ (sSup s).toAddSubmonoid

Proof state:
case refine_3
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
x y : M
x✝¹ : x ∈ ⨆ i, ↑i
x✝ : y ∈ ⨆ i, ↑i
⊢ (fun x x_1 => t • x ∈ ⨆ p, ↑p) x x✝¹ → (fun x x_1 => t • x ∈ ⨆ p, ↑p) y x✝ → (fun x x_1 => t • x ∈ ⨆ p, ↑p) (x + y) ⋯

Tactic:
simp_rw [smul_add]

Result:
case refine_3
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
x y : M
x✝¹ : x ∈ ⨆ i, ↑i
x✝ : y ∈ ⨆ i, ↑i
⊢ t • x ∈ ⨆ p, ↑p → t • y ∈ ⨆ p, ↑p → t • x + t • y ∈ ⨆ p, ↑p

Proof state:
case refine_1
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
p : Submodule R M := { toAddSubmonoid := sSup (toAddSubmonoid '' s), smul_mem' := ⋯ }
⊢ sSup s ≤ p

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

Result:
no goals

Proof state:
case refine_3
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
h : m ∈ ⨆ a, ↑a
x y : M
x✝¹ : x ∈ ⨆ i, ↑i
x✝ : y ∈ ⨆ i, ↑i
⊢ t • x ∈ ⨆ p, ↑p → t • y ∈ ⨆ p, ↑p → t • x + t • y ∈ ⨆ p, ↑p

Tactic:
exact add_mem

Result:
no goals

Proof state:
case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
p : Submodule R M := { toAddSubmonoid := sSup (toAddSubmonoid '' s), smul_mem' := ⋯ }
⊢ sSup (toAddSubmonoid '' s) ≤ (sSup s).toAddSubmonoid

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

Result:
no goals