case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ insert b t ↔ (x, y) ∈ (fun a => (a, b)) '' s ∪ s ×ˢ t
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s ×ˢ insert b t = (fun a => (a, b)) '' s ∪ s ×ˢ t
ext ⟨x, y⟩
case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
⊢ x ∈ s ∧ (y = b ∨ y ∈ t) ↔ (∃ a, a ∈ s ∧ a = x ∧ b = y) ∨ x ∈ s ∧ y ∈ t
case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ insert b t ↔ (x, y) ∈ (fun a => (a, b)) '' s ∪ s ×ˢ t
simp [image, or_imp]
case h.mk.refine_1
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
h : x ∈ s ∧ (y = b ∨ y ∈ t)
⊢ (∃ a, a ∈ s ∧ a = x ∧ b = y) ∨ x ∈ s ∧ y ∈ t

case h.mk.refine_2
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
h : (∃ a, a ∈ s ∧ a = x ∧ b = y) ∨ x ∈ s ∧ y ∈ t
⊢ x ∈ s ∧ (y = b ∨ y ∈ t)
case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
⊢ x ∈ s ∧ (y = b ∨ y ∈ t) ↔ (∃ a, a ∈ s ∧ a = x ∧ b = y) ∨ x ∈ s ∧ y ∈ t
refine ⟨fun h => ?_, fun h => ?_⟩
case h.mk.refine_1.intro.inl
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a x : α
y : β
hx : x ∈ s
⊢ (∃ a, a ∈ s ∧ a = x ∧ y = y) ∨ x ∈ s ∧ y ∈ t

case h.mk.refine_1.intro.inr
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
hx : x ∈ s
hy : y ∈ t
⊢ (∃ a, a ∈ s ∧ a = x ∧ b = y) ∨ x ∈ s ∧ y ∈ t
case h.mk.refine_1
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
h : x ∈ s ∧ (y = b ∨ y ∈ t)
⊢ (∃ a, a ∈ s ∧ a = x ∧ b = y) ∨ x ∈ s ∧ y ∈ t
obtain ⟨hx, rfl|hy⟩ := h
no goals
case h.mk.refine_1.intro.inl
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a x : α
y : β
hx : x ∈ s
⊢ (∃ a, a ∈ s ∧ a = x ∧ y = y) ∨ x ∈ s ∧ y ∈ t
exact Or.inl ⟨x, hx, rfl, rfl⟩
no goals
case h.mk.refine_1.intro.inr
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
hx : x ∈ s
hy : y ∈ t
⊢ (∃ a, a ∈ s ∧ a = x ∧ b = y) ∨ x ∈ s ∧ y ∈ t
exact Or.inr ⟨hx, hy⟩
case h.mk.refine_2.inl.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
hx : x ∈ s
⊢ x ∈ s ∧ (b = b ∨ b ∈ t)

case h.mk.refine_2.inr.intro
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
hx : x ∈ s
hy : y ∈ t
⊢ x ∈ s ∧ (y = b ∨ y ∈ t)
case h.mk.refine_2
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
h : (∃ a, a ∈ s ∧ a = x ∧ b = y) ∨ x ∈ s ∧ y ∈ t
⊢ x ∈ s ∧ (y = b ∨ y ∈ t)
obtain ⟨x, hx, rfl, rfl⟩|⟨hx, hy⟩ := h
no goals
case h.mk.refine_2.inl.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
hx : x ∈ s
⊢ x ∈ s ∧ (b = b ∨ b ∈ t)
exact ⟨hx, Or.inl rfl⟩
no goals
case h.mk.refine_2.inr.intro
α : Type u_1
β : Type u_2
γ : Type ?u.20280
δ : Type ?u.20283
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
hx : x ∈ s
hy : y ∈ t
⊢ x ∈ s ∧ (y = b ∨ y ∈ t)
exact ⟨hx, Or.inr hy⟩