M : Type u_1
N : Type ?u.29654
P : Type ?u.29657
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
⊢ (conGen fun x y => ↑c x y ∨ ↑d x y) = conGen (r ⊔ r)
M : Type u_1
N : Type ?u.29654
P : Type ?u.29657
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
⊢ c ⊔ d = conGen (r ⊔ r)
rw [sup_eq_conGen]
no goals
M : Type u_1
N : Type ?u.29654
P : Type ?u.29657
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c d : Con M
⊢ (conGen fun x y => ↑c x y ∨ ↑d x y) = conGen (r ⊔ r)
rfl