case mp
α₁ : 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 : γ₁ ⊕ γ₂
⊢ 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₂

case mpr
α₁ : 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 : γ₁ ⊕ γ₂
⊢ ((∃ 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
α₁ : 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 : γ₁ ⊕ γ₂
⊢ 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₂
constructor
case mp.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 : γ₁ ⊕ γ₂
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₂

case mp.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 : γ₁ ⊕ γ₂
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₂

case mp.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 : γ₁ ⊕ γ₂
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₂

case mp.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 : γ₁ ⊕ γ₂
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₂
case mp
α₁ : 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 : γ₁ ⊕ γ₂
⊢ 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₂
cases' a with a a <;> cases' b with b b
case mp.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 : γ₁ ⊕ γ₂
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₂
case mp.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 : γ₁ ⊕ γ₂
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₂
rw [sumLift₂, mem_map]
case mp.inl.inl.intro.intro
α₁ : 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 : γ₁
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₂
case mp.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 : γ₁ ⊕ γ₂
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₂
rintro ⟨c, hc, rfl⟩
no goals
case mp.inl.inl.intro.intro
α₁ : 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 : γ₁
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₂
exact Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩
no goals
case mp.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 : γ₁ ⊕ γ₂
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₂
refine' fun h ↦ (not_mem_empty _ h).elim
no goals
case mp.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 : γ₁ ⊕ γ₂
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₂
refine' fun h ↦ (not_mem_empty _ h).elim
case mp.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 : γ₁ ⊕ γ₂
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₂
case mp.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 : γ₁ ⊕ γ₂
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₂
rw [sumLift₂, mem_map]
case mp.inr.inr.intro.intro
α₁ : 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 : γ₂
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₂
case mp.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 : γ₁ ⊕ γ₂
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₂
rintro ⟨c, hc, rfl⟩
no goals
case mp.inr.inr.intro.intro
α₁ : 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 : γ₂
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₂
exact Or.inr ⟨a, b, c, rfl, rfl, rfl, hc⟩
no goals
case mpr
α₁ : 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 : γ₁ ⊕ γ₂
⊢ ((∃ 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
rintro (⟨a, b, c, rfl, rfl, rfl, h⟩ | ⟨a, b, c, rfl, rfl, rfl, h⟩) <;> exact mem_map_of_mem _ h