case refine'_1
α₁ : Type u_3
α₂ : Type u_4
β₁ : Type u_5
β₂ : Type u_6
γ₁ : Type u_1
γ₂ : Type u_2
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₂ = ∅

case refine'_2
α₁ : Type u_3
α₂ : Type u_4
β₁ : Type u_5
β₂ : Type u_6
γ₁ : Type u_1
γ₂ : Type u_2
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 = ∅
α₁ : Type u_3
α₂ : Type u_4
β₁ : Type u_5
β₂ : Type u_6
γ₁ : Type u_1
γ₂ : Type u_2
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₂ = ∅
refine' ⟨fun h ↦ _, fun h ↦ _⟩
case refine'_2.inl.inl
α₁ : Type u_3
α₂ : Type u_4
β₁ : Type u_5
β₂ : Type u_6
γ₁ : Type u_1
γ₂ : Type u_2
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✝) = ∅

case refine'_2.inl.inr
α₁ : Type u_3
α₂ : Type u_4
β₁ : Type u_5
β₂ : Type u_6
γ₁ : Type u_1
γ₂ : Type u_2
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✝) = ∅

case refine'_2.inr.inl
α₁ : Type u_3
α₂ : Type u_4
β₁ : Type u_5
β₂ : Type u_6
γ₁ : Type u_1
γ₂ : Type u_2
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✝) = ∅

case refine'_2.inr.inr
α₁ : Type u_3
α₂ : Type u_4
β₁ : Type u_5
β₂ : Type u_6
γ₁ : Type u_1
γ₂ : Type u_2
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✝) = ∅
case refine'_2
α₁ : Type u_3
α₂ : Type u_4
β₁ : Type u_5
β₂ : Type u_6
γ₁ : Type u_1
γ₂ : Type u_2
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 = ∅
cases a <;> cases b
case refine'_1.right
α₁ : Type u_3
α₂ : Type u_4
β₁ : Type u_5
β₂ : Type u_6
γ₁ : Type u_1
γ₂ : Type u_2
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₂
h : sumLift₂ f g (inr a) (inr b) = ∅
⊢ g a b = ∅
case refine'_1.right
α₁ : Type u_3
α₂ : Type u_4
β₁ : Type u_5
β₂ : Type u_6
γ₁ : Type u_1
γ₂ : Type u_2
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₂ = ∅
rintro a b rfl rfl
no goals
case refine'_1.right
α₁ : Type u_3
α₂ : Type u_4
β₁ : Type u_5
β₂ : Type u_6
γ₁ : Type u_1
γ₂ : Type u_2
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₂
h : sumLift₂ f g (inr a) (inr b) = ∅
⊢ g a b = ∅
exact map_eq_empty.1 h
no goals
case refine'_2.inl.inl
α₁ : Type u_3
α₂ : Type u_4
β₁ : Type u_5
β₂ : Type u_6
γ₁ : Type u_1
γ₂ : Type u_2
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✝) = ∅
exact map_eq_empty.2 (h.1 _ _ rfl rfl)
no goals
case refine'_2.inl.inr
α₁ : Type u_3
α₂ : Type u_4
β₁ : Type u_5
β₂ : Type u_6
γ₁ : Type u_1
γ₂ : Type u_2
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✝) = ∅
rfl
no goals
case refine'_2.inr.inl
α₁ : Type u_3
α₂ : Type u_4
β₁ : Type u_5
β₂ : Type u_6
γ₁ : Type u_1
γ₂ : Type u_2
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✝) = ∅
rfl
no goals
case refine'_2.inr.inr
α₁ : Type u_3
α₂ : Type u_4
β₁ : Type u_5
β₂ : Type u_6
γ₁ : Type u_1
γ₂ : Type u_2
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✝) = ∅
exact map_eq_empty.2 (h.2 _ _ rfl rfl)