[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ c ∈ sumLift₂ f g a b ↔
    (∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
constructor
[GOAL]
case mp
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ c ∈ sumLift₂ f g a b →
    (∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
cases' a with a a
[GOAL]
case mp.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₁
⊢ c ∈ sumLift₂ f g (inl a) b →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
cases' b with b b
[GOAL]
case mp.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₂
⊢ c ∈ sumLift₂ f g (inr a) b →
    (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
cases' b with b b
[GOAL]
case mp.inl.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₁
⊢ c ∈ sumLift₂ f g (inl a) (inl b) →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inl b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
rw [sumLift₂, mem_map]
[GOAL]
case mp.inl.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₁
⊢ (∃ a_1, a_1 ∈ f a b ∧ ↑Embedding.inl a_1 = c) →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inl b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
rintro ⟨c, hc, rfl⟩
[GOAL]
case mp.inl.inl.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁
b : β₁
c : γ₁
hc : c ∈ f a b
⊢ (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inl b = inl b₁ ∧ ↑Embedding.inl c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
    ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inl b = inr b₂ ∧ ↑Embedding.inl c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
exact Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩
[GOAL]
case mp.inl.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₂
⊢ c ∈ sumLift₂ f g (inl a) (inr b) →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
refine' fun h ↦ (not_mem_empty _ h).elim
[GOAL]
case mp.inr.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₁
⊢ c ∈ sumLift₂ f g (inr a) (inl b) →
    (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ inl b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
refine' fun h ↦ (not_mem_empty _ h).elim
[GOAL]
case mp.inr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₂
⊢ c ∈ sumLift₂ f g (inr a) (inr b) →
    (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
rw [sumLift₂, mem_map]
[GOAL]
case mp.inr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₂
⊢ (∃ a_1, a_1 ∈ g a b ∧ ↑Embedding.inr a_1 = c) →
    (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
rintro ⟨c, hc, rfl⟩
[GOAL]
case mp.inr.inr.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₂
b : β₂
c : γ₂
hc : c ∈ g a b
⊢ (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ inr b = inl b₁ ∧ ↑Embedding.inr c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
    ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inr b = inr b₂ ∧ ↑Embedding.inr c = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
exact Or.inr ⟨a, b, c, rfl, rfl, rfl, hc⟩
[GOAL]
case mpr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ ((∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂) →
    c ∈ sumLift₂ f g a b
[PROOFSTEP]
rintro (⟨a, b, c, rfl, rfl, rfl, h⟩ | ⟨a, b, c, rfl, rfl, rfl, h⟩)
[GOAL]
case mpr.inl.intro.intro.intro.intro.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁
b : β₁
c : γ₁
h : c ∈ f a b
⊢ inl c ∈ sumLift₂ f g (inl a) (inl b)
[PROOFSTEP]
exact mem_map_of_mem _ h
[GOAL]
case mpr.inr.intro.intro.intro.intro.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₂
b : β₂
c : γ₂
h : c ∈ g a b
⊢ inr c ∈ sumLift₂ f g (inr a) (inr b)
[PROOFSTEP]
exact mem_map_of_mem _ h
[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₁ : γ₁
⊢ inl c₁ ∈ sumLift₂ f g a b ↔ ∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁
[PROOFSTEP]
rw [mem_sumLift₂, or_iff_left]
[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₁ : γ₁
⊢ (∃ a₁ b₁ c₁_1, a = inl a₁ ∧ b = inl b₁ ∧ inl c₁ = inl c₁_1 ∧ c₁_1 ∈ f a₁ b₁) ↔
    ∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₁ : γ₁
⊢ ¬∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ inl c₁ = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
simp only [inl.injEq, exists_and_left, exists_eq_left']
[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₁ : γ₁
⊢ ¬∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ inl c₁ = inr c₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
rintro ⟨_, _, c₂, _, _, h, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₁ : γ₁
w✝¹ : α₂
w✝ : β₂
c₂ : γ₂
left✝¹ : a = inr w✝¹
left✝ : b = inr w✝
h : inl c₁ = inr c₂
right✝ : c₂ ∈ g w✝¹ w✝
⊢ False
[PROOFSTEP]
exact inl_ne_inr h
[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₂ : γ₂
⊢ inr c₂ ∈ sumLift₂ f g a b ↔ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂
[PROOFSTEP]
rw [mem_sumLift₂, or_iff_right]
[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₂ : γ₂
⊢ (∃ a₂ b₂ c₂_1, a = inr a₂ ∧ b = inr b₂ ∧ inr c₂ = inr c₂_1 ∧ c₂_1 ∈ g a₂ b₂) ↔
    ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₂ : γ₂
⊢ ¬∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ inr c₂ = inl c₁ ∧ c₁ ∈ f a₁ b₁
[PROOFSTEP]
simp only [inr.injEq, exists_and_left, exists_eq_left']
[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₂ : γ₂
⊢ ¬∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ inr c₂ = inl c₁ ∧ c₁ ∈ f a₁ b₁
[PROOFSTEP]
rintro ⟨_, _, c₂, _, _, h, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
c₂✝ : γ₂
w✝¹ : α₁
w✝ : β₁
c₂ : γ₁
left✝¹ : a = inl w✝¹
left✝ : b = inl w✝
h : inr c₂✝ = inl c₂
right✝ : c₂ ∈ f w✝¹ w✝
⊢ False
[PROOFSTEP]
exact inr_ne_inl h
[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ sumLift₂ f g a b = ∅ ↔
    (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun h ↦ _⟩
[GOAL]
case refine'_1
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
h : sumLift₂ f g a b = ∅
⊢ (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
[PROOFSTEP]
constructor
[GOAL]
case refine'_1.left
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
h : sumLift₂ f g a b = ∅
⊢ ∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅
[PROOFSTEP]
rintro a b rfl rfl
[GOAL]
case refine'_1.left
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₁
h : sumLift₂ f g (inl a) (inl b) = ∅
⊢ f a b = ∅
[PROOFSTEP]
exact map_eq_empty.1 h
[GOAL]
case refine'_1.right
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
h : sumLift₂ f g a b = ∅
⊢ ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
[PROOFSTEP]
rintro a b rfl rfl
[GOAL]
case refine'_1.right
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₂
h : sumLift₂ f g (inr a) (inr b) = ∅
⊢ g a b = ∅
[PROOFSTEP]
exact map_eq_empty.1 h
[GOAL]
case refine'_2
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g a b = ∅
[PROOFSTEP]
cases a
[GOAL]
case refine'_2.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
val✝ : α₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inl val✝ = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inl val✝ = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inl val✝) b = ∅
[PROOFSTEP]
cases b
[GOAL]
case refine'_2.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
val✝ : α₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝ = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inr val✝ = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val✝) b = ∅
[PROOFSTEP]
cases b
[GOAL]
case refine'_2.inl.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
val✝¹ : α₁
val✝ : β₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inl val✝¹ = inl a₁ → inl val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inl val✝¹ = inr a₂ → inl val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inl val✝¹) (inl val✝) = ∅
[PROOFSTEP]
exact map_eq_empty.2 (h.1 _ _ rfl rfl)
[GOAL]
case refine'_2.inl.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
val✝¹ : α₁
val✝ : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inl val✝¹ = inl a₁ → inr val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inl val✝¹ = inr a₂ → inr val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inl val✝¹) (inr val✝) = ∅
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.inr.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
val✝¹ : α₂
val✝ : β₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝¹ = inl a₁ → inl val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inr val✝¹ = inr a₂ → inl val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val✝¹) (inl val✝) = ∅
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.inr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
val✝¹ : α₂
val✝ : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝¹ = inl a₁ → inr val✝ = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inr val✝¹ = inr a₂ → inr val✝ = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val✝¹) (inr val✝) = ∅
[PROOFSTEP]
exact map_eq_empty.2 (h.2 _ _ rfl rfl)
[GOAL]
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ Finset.Nonempty (sumLift₂ f g a b) ↔
    (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ Finset.Nonempty (f a₁ b₁)) ∨
      ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ Finset.Nonempty (g a₂ b₂)
[PROOFSTEP]
simp only [nonempty_iff_ne_empty, Ne, sumLift₂_eq_empty, not_and_or, not_forall, not_imp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Icc Icc a b ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
rintro (a | a) (b | b) (x | x)
[GOAL]
case inl.inl.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b x : α
⊢ inl x ∈ sumLift₂ Icc Icc (inl a) (inl b) ↔ inl a ≤ inl x ∧ inl x ≤ inl b
[PROOFSTEP]
simp
[GOAL]
case inl.inl.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b : α
x : β
⊢ inr x ∈ sumLift₂ Icc Icc (inl a) (inl b) ↔ inl a ≤ inr x ∧ inr x ≤ inl b
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : α
b : β
x : α
⊢ inl x ∈ sumLift₂ Icc Icc (inl a) (inr b) ↔ inl a ≤ inl x ∧ inl x ≤ inr b
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : α
b x : β
⊢ inr x ∈ sumLift₂ Icc Icc (inl a) (inr b) ↔ inl a ≤ inr x ∧ inr x ≤ inr b
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : β
b x : α
⊢ inl x ∈ sumLift₂ Icc Icc (inr a) (inl b) ↔ inr a ≤ inl x ∧ inl x ≤ inl b
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : β
b : α
x : β
⊢ inr x ∈ sumLift₂ Icc Icc (inr a) (inl b) ↔ inr a ≤ inr x ∧ inr x ≤ inl b
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b : β
x : α
⊢ inl x ∈ sumLift₂ Icc Icc (inr a) (inr b) ↔ inr a ≤ inl x ∧ inl x ≤ inr b
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b x : β
⊢ inr x ∈ sumLift₂ Icc Icc (inr a) (inr b) ↔ inr a ≤ inr x ∧ inr x ≤ inr b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Ico Ico a b ↔ a ≤ x ∧ x < b
[PROOFSTEP]
rintro (a | a) (b | b) (x | x)
[GOAL]
case inl.inl.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b x : α
⊢ inl x ∈ sumLift₂ Ico Ico (inl a) (inl b) ↔ inl a ≤ inl x ∧ inl x < inl b
[PROOFSTEP]
simp
[GOAL]
case inl.inl.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b : α
x : β
⊢ inr x ∈ sumLift₂ Ico Ico (inl a) (inl b) ↔ inl a ≤ inr x ∧ inr x < inl b
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : α
b : β
x : α
⊢ inl x ∈ sumLift₂ Ico Ico (inl a) (inr b) ↔ inl a ≤ inl x ∧ inl x < inr b
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : α
b x : β
⊢ inr x ∈ sumLift₂ Ico Ico (inl a) (inr b) ↔ inl a ≤ inr x ∧ inr x < inr b
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : β
b x : α
⊢ inl x ∈ sumLift₂ Ico Ico (inr a) (inl b) ↔ inr a ≤ inl x ∧ inl x < inl b
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : β
b : α
x : β
⊢ inr x ∈ sumLift₂ Ico Ico (inr a) (inl b) ↔ inr a ≤ inr x ∧ inr x < inl b
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b : β
x : α
⊢ inl x ∈ sumLift₂ Ico Ico (inr a) (inr b) ↔ inr a ≤ inl x ∧ inl x < inr b
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b x : β
⊢ inr x ∈ sumLift₂ Ico Ico (inr a) (inr b) ↔ inr a ≤ inr x ∧ inr x < inr b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Ioc Ioc a b ↔ a < x ∧ x ≤ b
[PROOFSTEP]
rintro (a | a) (b | b) (x | x)
[GOAL]
case inl.inl.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b x : α
⊢ inl x ∈ sumLift₂ Ioc Ioc (inl a) (inl b) ↔ inl a < inl x ∧ inl x ≤ inl b
[PROOFSTEP]
simp
[GOAL]
case inl.inl.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b : α
x : β
⊢ inr x ∈ sumLift₂ Ioc Ioc (inl a) (inl b) ↔ inl a < inr x ∧ inr x ≤ inl b
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : α
b : β
x : α
⊢ inl x ∈ sumLift₂ Ioc Ioc (inl a) (inr b) ↔ inl a < inl x ∧ inl x ≤ inr b
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : α
b x : β
⊢ inr x ∈ sumLift₂ Ioc Ioc (inl a) (inr b) ↔ inl a < inr x ∧ inr x ≤ inr b
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : β
b x : α
⊢ inl x ∈ sumLift₂ Ioc Ioc (inr a) (inl b) ↔ inr a < inl x ∧ inl x ≤ inl b
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : β
b : α
x : β
⊢ inr x ∈ sumLift₂ Ioc Ioc (inr a) (inl b) ↔ inr a < inr x ∧ inr x ≤ inl b
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b : β
x : α
⊢ inl x ∈ sumLift₂ Ioc Ioc (inr a) (inr b) ↔ inr a < inl x ∧ inl x ≤ inr b
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b x : β
⊢ inr x ∈ sumLift₂ Ioc Ioc (inr a) (inr b) ↔ inr a < inr x ∧ inr x ≤ inr b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Ioo Ioo a b ↔ a < x ∧ x < b
[PROOFSTEP]
rintro (a | a) (b | b) (x | x)
[GOAL]
case inl.inl.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b x : α
⊢ inl x ∈ sumLift₂ Ioo Ioo (inl a) (inl b) ↔ inl a < inl x ∧ inl x < inl b
[PROOFSTEP]
simp
[GOAL]
case inl.inl.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b : α
x : β
⊢ inr x ∈ sumLift₂ Ioo Ioo (inl a) (inl b) ↔ inl a < inr x ∧ inr x < inl b
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : α
b : β
x : α
⊢ inl x ∈ sumLift₂ Ioo Ioo (inl a) (inr b) ↔ inl a < inl x ∧ inl x < inr b
[PROOFSTEP]
simp
[GOAL]
case inl.inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : α
b x : β
⊢ inr x ∈ sumLift₂ Ioo Ioo (inl a) (inr b) ↔ inl a < inr x ∧ inr x < inr b
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : β
b x : α
⊢ inl x ∈ sumLift₂ Ioo Ioo (inr a) (inl b) ↔ inr a < inl x ∧ inl x < inl b
[PROOFSTEP]
simp
[GOAL]
case inr.inl.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a : β
b : α
x : β
⊢ inr x ∈ sumLift₂ Ioo Ioo (inr a) (inl b) ↔ inr a < inr x ∧ inr x < inl b
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b : β
x : α
⊢ inl x ∈ sumLift₂ Ioo Ioo (inr a) (inr b) ↔ inr a < inl x ∧ inl x < inr b
[PROOFSTEP]
simp
[GOAL]
case inr.inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a b x : β
⊢ inr x ∈ sumLift₂ Ioo Ioo (inr a) (inr b) ↔ inr a < inr x ∧ inr x < inr b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ a₂ : α
b₁ b₂ : β
a b : α ⊕ β
⊢ Ioo (inl a₁) (inr b₂) = ∅
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ a₂ : α
b₁ b₂ : β
a b : α ⊕ β
⊢ Ioo (inr b₁) (inl a₂) = ∅
[PROOFSTEP]
rfl
