M : Type u_1
N : Type ?u.27586
P : Type ?u.27589
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c : Con M
⊢ sInf {s | ∀ (x y : M), ↑c x y → ↑s x y} ≤ c
M : Type u_1
N : Type ?u.27586
P : Type ?u.27589
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c : Con M
⊢ conGen ↑c ≤ c
rw [conGen_eq]
no goals
M : Type u_1
N : Type ?u.27586
P : Type ?u.27589
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c : Con M
⊢ sInf {s | ∀ (x y : M), ↑c x y → ↑s x y} ≤ c
exact sInf_le fun _ _ => id