α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
p : α → Prop
⊢ (∀ (c : α), (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = c) → p c) ↔
    ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → Disjoint a b → p (a ⊔ b)
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
p : α → Prop
⊢ (∀ (c : α), c ∈ s ○ t → p c) ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → Disjoint a b → p (a ⊔ b)
simp_rw [mem_disjSups]
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
p : α → Prop
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → Disjoint a b → p (a ⊔ b)) →
    ∀ (c : α), (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = c) → p c
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
p : α → Prop
⊢ (∀ (c : α), (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = c) → p c) ↔
    ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → Disjoint a b → p (a ⊔ b)
refine' ⟨fun h a ha b hb hab => h _ ⟨_, ha, _, hb, hab, rfl⟩, _⟩
case intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a✝ b✝ c : α
p : α → Prop
h : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → Disjoint a b → p (a ⊔ b)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
⊢ p (a ⊔ b)
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a b c : α
p : α → Prop
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → Disjoint a b → p (a ⊔ b)) →
    ∀ (c : α), (∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ Disjoint a b ∧ a ⊔ b = c) → p c
rintro h _ ⟨a, ha, b, hb, hab, rfl⟩
no goals
case intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s s₁ s₂ t t₁ t₂ u : Finset α
a✝ b✝ c : α
p : α → Prop
h : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → Disjoint a b → p (a ⊔ b)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
⊢ p (a ⊔ b)
exact h _ ha _ hb hab