M : Type u_1
N : Type ?u.26925
P : Type ?u.26928
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ : Con M
r : M → M → Prop
c : Con M
h : ∀ (x y : M), r x y → Setoid.r x y
⊢ sInf {s | ∀ (x y : M), r x y → ↑s x y} ≤ c
M : Type u_1
N : Type ?u.26925
P : Type ?u.26928
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ : Con M
r : M → M → Prop
c : Con M
h : ∀ (x y : M), r x y → Setoid.r x y
⊢ conGen r ≤ c
rw [conGen_eq]
no goals
M : Type u_1
N : Type ?u.26925
P : Type ?u.26928
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ : Con M
r : M → M → Prop
c : Con M
h : ∀ (x y : M), r x y → Setoid.r x y
⊢ sInf {s | ∀ (x y : M), r x y → ↑s x y} ≤ c
exact sInf_le h