M : Type u_1
N : Type ?u.30054
P : Type ?u.30057
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
⊢ sSup S = sInf {s | ∀ (x y : M), (∃ c, c ∈ S ∧ ↑c x y) → ↑s x y}
M : Type u_1
N : Type ?u.30054
P : Type ?u.30057
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
⊢ sSup S = conGen fun x y => ∃ c, c ∈ S ∧ ↑c x y
rw [conGen_eq]
M : Type u_1
N : Type ?u.30054
P : Type ?u.30057
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
⊢ upperBounds S = {s | ∀ (x y : M), (∃ c, c ∈ S ∧ ↑c x y) → ↑s x y}
M : Type u_1
N : Type ?u.30054
P : Type ?u.30057
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
⊢ sSup S = sInf {s | ∀ (x y : M), (∃ c, c ∈ S ∧ ↑c x y) → ↑s x y}
apply congr_arg sInf
case h
M : Type u_1
N : Type ?u.30054
P : Type ?u.30057
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
x✝ : Con M
⊢ x✝ ∈ upperBounds S ↔ x✝ ∈ {s | ∀ (x y : M), (∃ c, c ∈ S ∧ ↑c x y) → ↑s x y}
M : Type u_1
N : Type ?u.30054
P : Type ?u.30057
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
⊢ upperBounds S = {s | ∀ (x y : M), (∃ c, c ∈ S ∧ ↑c x y) → ↑s x y}
ext
no goals
case h
M : Type u_1
N : Type ?u.30054
P : Type ?u.30057
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
x✝ : Con M
⊢ x✝ ∈ upperBounds S ↔ x✝ ∈ {s | ∀ (x y : M), (∃ c, c ∈ S ∧ ↑c x y) → ↑s x y}
exact ⟨fun h _ _ ⟨r, hr⟩ => h hr.1 hr.2, fun h r hS _ _ hr => h _ _ ⟨r, hS, hr⟩⟩