awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₂
⊢ c ∈ sumLift₂ f g (inl a) (inr b) →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
refine fun h ↦ (notMem_empty _ h).elim

Premises used: False.elim, Finset.notMem_empty
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₁
⊢ c ∈ sumLift₂ f g (inr a) (inl b) →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), inr a = inl a₁ ∧ Eq (α := β₁ ⊕ β₂) (inl b) (inl b₁) ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
fun h ↦ (notMem_empty _ h).elim

Premises used: False.elim, Finset.notMem_empty
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₁
⊢ c ∈ sumLift₂ f g (inr a) (inl b) →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), inr a = inl a₁ ∧ Eq (α := β₁ ⊕ β₂) (inl b) (inl b₁) ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
refine fun h ↦ (notMem_empty _ h).elim

Premises used: False.elim, Finset.notMem_empty
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₂
mp :
  (∃ a_1 ∈ g a b, (Embedding.inr : (a : γ₂) → γ₁ ⊕ γ₂) a_1 = c) →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), inr a = inl a₁ ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
        Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inr c₂ ∧ c₂ ∈ g 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₂ : γ₂),
        Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
rw [sumLift₂, mem_map]

Premises used: Finset.mem_map, Finset.sumLift₂
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₂
b : β₂
c : γ₂
hc : c ∈ g a b
⊢ (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
      inr a = inl a₁ ∧
        inr b = inl b₁ ∧
          Eq (α := γ₁ ⊕ γ₂) ((Embedding.inr : (a : γ₂) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inl c₁ : γ₁ ⊕ γ₂) ∧ c₁ ∈ f a₁ b₁) ∨
    ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
      Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧
        Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧
          Eq (α := γ₁ ⊕ γ₂) ((Embedding.inr : (a : γ₂) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inr c₂ : γ₁ ⊕ γ₂) ∧ c₂ ∈ g a₂ b₂

Tactic:
Or.inr ⟨a, b, c, rfl, rfl, rfl, hc⟩

Premises used: And.intro, Exists.intro, Or.inr, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₂
b : β₂
c : γ₂
hc : c ∈ g a b
⊢ (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
      inr a = inl a₁ ∧
        inr b = inl b₁ ∧
          Eq (α := γ₁ ⊕ γ₂) ((Embedding.inr : (a : γ₂) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inl c₁ : γ₁ ⊕ γ₂) ∧ c₁ ∈ f a₁ b₁) ∨
    ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
      Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧
        Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧
          Eq (α := γ₁ ⊕ γ₂) ((Embedding.inr : (a : γ₂) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inr c₂ : γ₁ ⊕ γ₂) ∧ c₂ ∈ g a₂ b₂

Tactic:
exact Or.inr ⟨a, b, c, rfl, rfl, rfl, hc⟩

Premises used: Or.inr
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁
b : β₁
c : γ₁
h : c ∈ f a b
⊢ inl c ∈ sumLift₂ f g (inl a) (inl b)

Tactic:
mem_map_of_mem _ h

Premises used: Set.Mem, setOf, Finset.mem_map_of_mem
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁
b : β₁
c : γ₁
h : c ∈ f a b
⊢ inl c ∈ sumLift₂ f g (inl a) (inl b)

Tactic:
exact mem_map_of_mem _ h

Premises used: Finset.mem_map_of_mem
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₂
b : β₂
c : γ₂
h : c ∈ g a b
⊢ inr c ∈ sumLift₂ f g (inr a) (inr b)

Tactic:
mem_map_of_mem _ h

Premises used: Set.Mem, setOf, Finset.mem_map_of_mem
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₂
b : β₂
c : γ₂
h : c ∈ g a b
⊢ inr c ∈ sumLift₂ f g (inr a) (inr b)

Tactic:
exact mem_map_of_mem _ h

Premises used: Finset.mem_map_of_mem
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
rw :
  (∃ (a₁ : α₁) (b₁ : β₁) (c₁_1 : γ₁),
      a = inl a₁ ∧ b = inl b₁ ∧ Eq (α := γ₁ ⊕ γ₂) (inl c₁) (inl c₁_1) ∧ c₁_1 ∈ f a₁ b₁) ↔
    ∃ (a₁ : α₁) (b₁ : β₁), a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁
rw₁ : ¬∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ inl c₁ = inr c₂ ∧ c₂ ∈ g a₂ b₂
⊢ inl c₁ ∈ sumLift₂ f g a b ↔ ∃ (a₁ : α₁) (b₁ : β₁), a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁

Tactic:
rw [mem_sumLift₂, or_iff_left]

Premises used: Finset.mem_sumLift₂, or_iff_left
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ (∃ (a₁ : α₁) (b₁ : β₁) (c₁_1 : γ₁),
      a = inl a₁ ∧ b = inl b₁ ∧ Eq (α := γ₁ ⊕ γ₂) (inl c₁) (inl c₁_1) ∧ c₁_1 ∈ f a₁ b₁) ↔
    ∃ (a₁ : α₁) (b₁ : β₁), a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁

Tactic:
simp only [inl.injEq, exists_and_left, exists_eq_left']

Premises used: exists_and_left, exists_eq_left', Sum.inl.injEq
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
w : α₂
w_1 : β₂
c₂ : γ₂
left : a = inr w
left_1 : b = inr w_1
h : inl c₁ = inr c₂
right : c₂ ∈ g w w_1
⊢ False

Tactic:
inl_ne_inr h

Premises used: Sum.inl_ne_inr
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
w : α₂
w_1 : β₂
c₂ : γ₂
left : a = inr w
left_1 : b = inr w_1
h : inl c₁ = inr c₂
right : c₂ ∈ g w w_1
⊢ False

Tactic:
exact inl_ne_inr h

Premises used: Sum.inl_ne_inr
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂ : γ₂
rw :
  (∃ (a₂ : α₂) (b₂ : β₂) (c₂_1 : γ₂),
      a = inr a₂ ∧ b = inr b₂ ∧ Eq (α := γ₁ ⊕ γ₂) (inr c₂) (inr c₂_1) ∧ c₂_1 ∈ g a₂ b₂) ↔
    ∃ (a₂ : α₂) (b₂ : β₂), a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂
rw₁ : ¬∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ inr c₂ = inl c₁ ∧ c₁ ∈ f a₁ b₁
⊢ inr c₂ ∈ sumLift₂ f g a b ↔ ∃ (a₂ : α₂) (b₂ : β₂), a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
rw [mem_sumLift₂, or_iff_right]

Premises used: Finset.mem_sumLift₂, or_iff_right
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂ : γ₂
⊢ (∃ (a₂ : α₂) (b₂ : β₂) (c₂_1 : γ₂),
      a = inr a₂ ∧ b = inr b₂ ∧ Eq (α := γ₁ ⊕ γ₂) (inr c₂) (inr c₂_1) ∧ c₂_1 ∈ g a₂ b₂) ↔
    ∃ (a₂ : α₂) (b₂ : β₂), a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
simp only [inr.injEq, exists_and_left, exists_eq_left']

Premises used: Sum.inr.injEq, exists_and_left, exists_eq_left'
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂_1 : γ₂
w : α₁
w_1 : β₁
c₂ : γ₁
left : a = inl w
left_1 : b = inl w_1
h : inr c₂_1 = inl c₂
right : c₂ ∈ f w w_1
⊢ False

Tactic:
inr_ne_inl h

Premises used: Sum.inr_ne_inl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₂_1 : γ₂
w : α₁
w_1 : β₁
c₂ : γ₁
left : a = inl w
left_1 : b = inl w_1
h : inr c₂_1 = inl c₂
right : c₂ ∈ f w w_1
⊢ False

Tactic:
exact inr_ne_inl h

Premises used: Sum.inr_ne_inl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
⊢ 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₂ = ∅

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
refine_1 :
  ∀ (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₂ = ∅
refine_2 :
  ∀
    (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 = ∅
⊢ 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₂ = ∅

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLift₂ f g a b = ∅
refine_1 : ∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅
refine_1₁ : ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → 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₂ = ∅

Tactic:
constructor
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁
b : β₁
h : sumLift₂ f g (inl a) (inl b) = ∅
⊢ f a b = ∅

Tactic:
map_eq_empty.1 h

Premises used: Iff.mp, Finset.map_eq_empty
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁
b : β₁
h : sumLift₂ f g (inl a) (inl b) = ∅
⊢ f a b = ∅

Tactic:
exact map_eq_empty.1 h

Premises used: Iff.mp, Finset.map_eq_empty
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₂
b : β₂
h : sumLift₂ f g (inr a) (inr b) = ∅
⊢ g a b = ∅

Tactic:
map_eq_empty.1 h

Premises used: Iff.mp, Finset.map_eq_empty
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₂
b : β₂
h : sumLift₂ f g (inr a) (inr b) = ∅
⊢ g a b = ∅

Tactic:
exact map_eq_empty.1 h

Premises used: Iff.mp, Finset.map_eq_empty
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
refine_2 :
  ∀ (val : α₁)
    (h :
      (∀ (a₁ : α₁) (b₁ : β₁), Eq (α := α₁ ⊕ α₂) (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 = ∅
refine_2₁ :
  ∀ (val : α₂)
    (h :
      (∀ (a₁ : α₁) (b₁ : β₁), inr val = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
        ∀ (a₂ : α₂) (b₂ : β₂), Eq (α := α₁ ⊕ α₂) (inr val) (inr a₂) → b = inr b₂ → g a₂ b₂ = ∅),
    sumLift₂ f g (inr val) b = ∅
⊢ sumLift₂ f g a b = ∅

Tactic:
cases a
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
val : α₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inl val = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
refine_2 :
  ∀ (val_1 : β₁)
    (h :
      (∀ (a₁ : α₁) (b₁ : β₁),
          Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → Eq (α := β₁ ⊕ β₂) (inl val_1) (inl b₁) → f a₁ b₁ = ∅) ∧
        ∀ (a₂ : α₂) (b₂ : β₂), inl val = inr a₂ → inl val_1 = inr b₂ → g a₂ b₂ = ∅),
    sumLift₂ f g (inl val) (inl val_1) = ∅
refine_2₁ :
  ∀ (val_1 : β₂)
    (h :
      (∀ (a₁ : α₁) (b₁ : β₁), Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → inr val_1 = inl b₁ → f a₁ b₁ = ∅) ∧
        ∀ (a₂ : α₂) (b₂ : β₂), inl val = inr a₂ → Eq (α := β₁ ⊕ β₂) (inr val_1) (inr b₂) → g a₂ b₂ = ∅),
    sumLift₂ f g (inl val) (inr val_1) = ∅
⊢ sumLift₂ f g (inl val) b = ∅

Tactic:
cases b
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
val : α₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), Eq (α := α₁ ⊕ α₂) (inr val) (inr a₂) → b = inr b₂ → g a₂ b₂ = ∅
refine_2 :
  ∀ (val_1 : β₁)
    (h :
      (∀ (a₁ : α₁) (b₁ : β₁), inr val = inl a₁ → Eq (α := β₁ ⊕ β₂) (inl val_1) (inl b₁) → f a₁ b₁ = ∅) ∧
        ∀ (a₂ : α₂) (b₂ : β₂), Eq (α := α₁ ⊕ α₂) (inr val) (inr a₂) → inl val_1 = inr b₂ → g a₂ b₂ = ∅),
    sumLift₂ f g (inr val) (inl val_1) = ∅
refine_2₁ :
  ∀ (val_1 : β₂)
    (h :
      (∀ (a₁ : α₁) (b₁ : β₁), inr val = inl a₁ → inr val_1 = inl b₁ → f a₁ b₁ = ∅) ∧
        ∀ (a₂ : α₂) (b₂ : β₂),
          Eq (α := α₁ ⊕ α₂) (inr val) (inr a₂) → Eq (α := β₁ ⊕ β₂) (inr val_1) (inr b₂) → g a₂ b₂ = ∅),
    sumLift₂ f g (inr val) (inr val_1) = ∅
⊢ sumLift₂ f g (inr val) b = ∅

Tactic:
cases b
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val : α₁
val_1 : β₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → Eq (α := β₁ ⊕ β₂) (inl val_1) (inl b₁) → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inl val = inr a₂ → inl val_1 = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inl val) (inl val_1) = ∅

Tactic:
map_eq_empty.2 (h.1 _ _ rfl rfl)

Premises used: Iff.mpr, And.left, Finset.map_eq_empty, Finset.sumLift₂, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val : α₁
val_1 : β₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → Eq (α := β₁ ⊕ β₂) (inl val_1) (inl b₁) → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inl val = inr a₂ → inl val_1 = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inl val) (inl val_1) = ∅

Tactic:
exact map_eq_empty.2 (h.1 _ _ rfl rfl)

Premises used: Iff.mpr, And.left, Finset.map_eq_empty, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val : α₁
val_1 : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → inr val_1 = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inl val = inr a₂ → Eq (α := β₁ ⊕ β₂) (inr val_1) (inr b₂) → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inl val) (inr val_1) = ∅

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val : α₂
val_1 : β₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val = inl a₁ → Eq (α := β₁ ⊕ β₂) (inl val_1) (inl b₁) → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), Eq (α := α₁ ⊕ α₂) (inr val) (inr a₂) → inl val_1 = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val) (inl val_1) = ∅

Tactic:
rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val : α₂
val_1 : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val = inl a₁ → inr val_1 = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), Eq (α := α₁ ⊕ α₂) (inr val) (inr a₂) → Eq (α := β₁ ⊕ β₂) (inr val_1) (inr b₂) → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val) (inr val_1) = ∅

Tactic:
map_eq_empty.2 (h.2 _ _ rfl rfl)

Premises used: Iff.mpr, And.right, Finset.map_eq_empty, Finset.sumLift₂, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
val : α₂
val_1 : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val = inl a₁ → inr val_1 = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), Eq (α := α₁ ⊕ α₂) (inr val) (inr a₂) → Eq (α := β₁ ⊕ β₂) (inr val_1) (inr b₂) → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val) (inr val_1) = ∅

Tactic:
exact map_eq_empty.2 (h.2 _ _ rfl rfl)

Premises used: Iff.mpr, And.right, Finset.map_eq_empty, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
⊢ (sumLift₂ f g a b).Nonempty ↔
    (∃ (a₁ : α₁) (b₁ : β₁), a = inl a₁ ∧ b = inl b₁ ∧ (f a₁ b₁).Nonempty) ∨
      ∃ (a₂ : α₂) (b₂ : β₂), a = inr a₂ ∧ b = inr b₂ ∧ (g a₂ b₂).Nonempty

Tactic:
simp only [nonempty_iff_ne_empty, Ne, sumLift₂_eq_empty, not_and_or, not_forall, exists_prop]

Premises used: Finset.sumLift₂_eq_empty, Ne, Finset.nonempty_iff_ne_empty, exists_prop, not_and_or, Classical.not_forall
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₁
⊢ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inl b) = map Embedding.inl (f₁ a b)

Tactic:
rfl

Premises used: Finset.sumLexLift, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₂
⊢ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b) = (g₁ a b).disjSum (g₂ a b)

Tactic:
rfl

Premises used: Finset.sumLexLift, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₂
b : β₁
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr a) (inl b) = ∅

Tactic:
rfl

Premises used: Finset.sumLexLift, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₂
b : β₂
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr b) = map { toFun := inr, inj' := ⋯ } (f₂ a b)

Tactic:
rfl

Premises used: Finset.sumLexLift, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
mp :
  c ∈ sumLexLift f₁ f₂ g₁ g₂ a b →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ (a₁ : α₁) (b₂ : β₂) (c₁ : γ₁), a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂), a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
mpr :
  ((∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ (a₁ : α₁) (b₂ : β₂) (c₁ : γ₁), a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂), a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂) →
    c ∈ sumLexLift f₁ f₂ g₁ g₂ a b
⊢ c ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ (a₁ : α₁) (b₂ : β₂) (c₁ : γ₁), a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂), a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
constructor
-- Module: Mathlib.Data.Sum.Interval
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
mp :
  ∀ (a : α₁),
    c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) b →
      (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
        (∃ (a₁ : α₁) (b₂ : β₂) (c₁ : γ₁),
            Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
          (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂),
              Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
            ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
mp₁ :
  ∀ (a : α₂),
    c ∈ sumLexLift f₁ f₂ g₁ 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 = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
          (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂), inr a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
            ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
              Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
⊢ c ∈ sumLexLift f₁ f₂ g₁ g₂ a b →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ (a₁ : α₁) (b₂ : β₂) (c₁ : γ₁), a = inl a₁ ∧ b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂), a = inl a₁ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
obtain a | a := a