M : Type u_1
N : Type ?u.30817
P : Type ?u.30820
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
⊢ (conGen fun x y => ∃ c, c ∈ S ∧ ↑c x y) = conGen (⨆ (a : Con M) (_ : a ∈ S), ↑a)
M : Type u_1
N : Type ?u.30817
P : Type ?u.30820
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
⊢ sSup S = conGen (sSup (FunLike.coe '' S))
rw [sSup_eq_conGen, sSup_image]
case e_r.h.h.a
M : Type u_1
N : Type ?u.30817
P : Type ?u.30820
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
x y : M
⊢ (∃ c, c ∈ S ∧ ↑c x y) ↔ iSup (fun a => ⨆ (_ : a ∈ S), ↑a) x y
M : Type u_1
N : Type ?u.30817
P : Type ?u.30820
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
⊢ (conGen fun x y => ∃ c, c ∈ S ∧ ↑c x y) = conGen (⨆ (a : Con M) (_ : a ∈ S), ↑a)
congr with (x y)
no goals
case e_r.h.h.a
M : Type u_1
N : Type ?u.30817
P : Type ?u.30820
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c : Con M
S : Set (Con M)
x y : M
⊢ (∃ c, c ∈ S ∧ ↑c x y) ↔ iSup (fun a => ⨆ (_ : a ∈ S), ↑a) x y
simp only [sSup_image, iSup_apply, iSup_Prop_eq, exists_prop, rel_eq_coe]