M : Type u_1
N : Type ?u.28395
P : Type ?u.28398
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
⊢ c ⊔ d = sInf {s | ∀ (x y : M), ↑c x y ∨ ↑d x y → ↑s x y}
M : Type u_1
N : Type ?u.28395
P : Type ?u.28398
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
⊢ c ⊔ d = conGen fun x y => ↑c x y ∨ ↑d x y
rw [conGen_eq]
M : Type u_1
N : Type ?u.28395
P : Type ?u.28398
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
⊢ {x | c ≤ x ∧ d ≤ x} = {s | ∀ (x y : M), ↑c x y ∨ ↑d x y → ↑s x y}
M : Type u_1
N : Type ?u.28395
P : Type ?u.28398
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
⊢ c ⊔ d = sInf {s | ∀ (x y : M), ↑c x y ∨ ↑d x y → ↑s x y}
apply congr_arg sInf
no goals
M : Type u_1
N : Type ?u.28395
P : Type ?u.28398
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
⊢ {x | c ≤ x ∧ d ≤ x} = {s | ∀ (x y : M), ↑c x y ∨ ↑d x y → ↑s x y}
simp only [le_def, or_imp, ← forall_and]