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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₂
b : β₂
c : γ₂
hc : c ∈ f₂ a b
⊢ inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr b)

Tactic:
exact mem_map_of_mem _ hc

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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ inl c₁ ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
    (∃ (a₁ : α₁) (b₁ : β₁), a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      ∃ (a₁ : α₁) (b₂ : β₂), a = inl a₁ ∧ b = inr b₂ ∧ c₁ ∈ g₁ a₁ b₂

Tactic:
simp [mem_sumLexLift]

Premises used: Finset.mem_sumLexLift
-- 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₂ : γ₂
⊢ inr c₂ ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
    (∃ (a₁ : α₁) (b₂ : β₂), a = inl a₁ ∧ b = inr b₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
      ∃ (a₂ : α₂) (b₂ : β₂), a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
simp [mem_sumLexLift]

Premises used: Finset.mem_sumLexLift
-- 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₁ f₁' : α₁ → β₁ → Finset γ₁
f₂ f₂' : α₂ → β₂ → Finset γ₂
g₁ g₁' : α₁ → β₂ → Finset γ₁
g₂ g₂' : α₁ → β₂ → Finset γ₂
hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b
hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b
hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b
hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
inl : ∀ (val : α₁), sumLexLift f₁ f₂ g₁ g₂ (Sum.inl val) b ⊆ sumLexLift f₁' f₂' g₁' g₂' (Sum.inl val) b
inr : ∀ (val : α₂), sumLexLift f₁ f₂ g₁ g₂ (Sum.inr val) b ⊆ sumLexLift f₁' f₂' g₁' g₂' (Sum.inr val) b
⊢ sumLexLift f₁ f₂ g₁ g₂ a b ⊆ sumLexLift f₁' f₂' g₁' 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₁ f₁' : α₁ → β₁ → Finset γ₁
f₂ f₂' : α₂ → β₂ → Finset γ₂
g₁ g₁' : α₁ → β₂ → Finset γ₁
g₂ g₂' : α₁ → β₂ → Finset γ₂
hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b
hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b
hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b
hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b
b : β₁ ⊕ β₂
val : α₁
inl :
  ∀ (val_1 : β₁),
    sumLexLift f₁ f₂ g₁ g₂ (Sum.inl val) (Sum.inl val_1) ⊆ sumLexLift f₁' f₂' g₁' g₂' (Sum.inl val) (Sum.inl val_1)
inl₁ :
  ∀ (val_1 : β₂),
    sumLexLift f₁ f₂ g₁ g₂ (Sum.inl val) (inr val_1) ⊆ sumLexLift f₁' f₂' g₁' g₂' (Sum.inl val) (inr val_1)
⊢ sumLexLift f₁ f₂ g₁ g₂ (Sum.inl val) b ⊆ sumLexLift f₁' f₂' g₁' g₂' (Sum.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₁ f₁' : α₁ → β₁ → Finset γ₁
f₂ f₂' : α₂ → β₂ → Finset γ₂
g₁ g₁' : α₁ → β₂ → Finset γ₁
g₂ g₂' : α₁ → β₂ → Finset γ₂
hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b
hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b
hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b
hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b
b : β₁ ⊕ β₂
val : α₂
inr :
  ∀ (val_1 : β₁),
    sumLexLift f₁ f₂ g₁ g₂ (Sum.inr val) (inl val_1) ⊆ sumLexLift f₁' f₂' g₁' g₂' (Sum.inr val) (inl val_1)
inr₁ :
  ∀ (val_1 : β₂),
    sumLexLift f₁ f₂ g₁ g₂ (Sum.inr val) (Sum.inr val_1) ⊆ sumLexLift f₁' f₂' g₁' g₂' (Sum.inr val) (Sum.inr val_1)
⊢ sumLexLift f₁ f₂ g₁ g₂ (Sum.inr val) b ⊆ sumLexLift f₁' f₂' g₁' g₂' (Sum.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₁ f₁' : α₁ → β₁ → Finset γ₁
f₂ f₂' : α₂ → β₂ → Finset γ₂
g₁ g₁' : α₁ → β₂ → Finset γ₁
g₂ g₂' : α₁ → β₂ → Finset γ₂
hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b
hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b
hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b
hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b
val : α₁
val_1 : β₁
⊢ sumLexLift f₁ f₂ g₁ g₂ (inl val) (inl val_1) ⊆ sumLexLift f₁' f₂' g₁' g₂' (inl val) (inl val_1)

Tactic:
map_subset_map.2 (hf₁ _ _)

Premises used: Iff.mpr, Set.Mem, setOf, Finset.map_subset_map
-- 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₁ f₁' : α₁ → β₁ → Finset γ₁
f₂ f₂' : α₂ → β₂ → Finset γ₂
g₁ g₁' : α₁ → β₂ → Finset γ₁
g₂ g₂' : α₁ → β₂ → Finset γ₂
hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b
hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b
hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b
hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b
val : α₁
val_1 : β₂
⊢ sumLexLift f₁ f₂ g₁ g₂ (inl val) (inr val_1) ⊆ sumLexLift f₁' f₂' g₁' g₂' (inl val) (inr val_1)

Tactic:
disjSum_mono (hg₁ _ _) (hg₂ _ _)

Premises used: Set.Mem, setOf, Finset.disjSum_mono
-- 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₁ f₁' : α₁ → β₁ → Finset γ₁
f₂ f₂' : α₂ → β₂ → Finset γ₂
g₁ g₁' : α₁ → β₂ → Finset γ₁
g₂ g₂' : α₁ → β₂ → Finset γ₂
hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b
hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b
hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b
hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b
val : α₂
val_1 : β₁
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr val) (inl val_1) ⊆ sumLexLift f₁' f₂' g₁' g₂' (inr val) (inl val_1)

Tactic:
Subset.rfl

Premises used: Finset.Subset.rfl, Set.Mem, setOf
-- 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₁ f₁' : α₁ → β₁ → Finset γ₁
f₂ f₂' : α₂ → β₂ → Finset γ₂
g₁ g₁' : α₁ → β₂ → Finset γ₁
g₂ g₂' : α₁ → β₂ → Finset γ₂
hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b
hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b
hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b
hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b
val : α₂
val_1 : β₂
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr val) (inr val_1) ⊆ sumLexLift f₁' f₂' g₁' g₂' (inr val) (inr val_1)

Tactic:
map_subset_map.2 (hf₂ _ _)

Premises used: Iff.mpr, Set.Mem, setOf, Finset.map_subset_map
-- 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₁ f₁' : α₁ → β₁ → Finset γ₁
f₂ f₂' : α₂ → β₂ → Finset γ₂
g₁ g₁' : α₁ → β₂ → Finset γ₁
g₂ g₂' : α₁ → β₂ → Finset γ₂
hf₁ : ∀ (a : α₁) (b : β₁), f₁ a b ⊆ f₁' a b
hf₂ : ∀ (a : α₂) (b : β₂), f₂ a b ⊆ f₂' a b
hg₁ : ∀ (a : α₁) (b : β₂), g₁ a b ⊆ g₁' a b
hg₂ : ∀ (a : α₁) (b : β₂), g₂ a b ⊆ g₂' a b
val : α₁
val_1 : β₁
⊢ sumLexLift f₁ f₂ g₁ g₂ (inl val) (inl val_1) ⊆ sumLexLift f₁' f₂' g₁' g₂' (inl val) (inl val_1)

Tactic:
exacts [map_subset_map.2 (hf₁ _ _), disjSum_mono (hg₁ _ _) (hg₂ _ _), Subset.rfl,
    map_subset_map.2 (hf₂ _ _)]

Premises used: Iff.mpr, Finset.Subset.rfl, Finset.disjSum_mono, Finset.map_subset_map
-- 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₂ a b = ∅ ↔
    (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
      (∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
        ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅

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

Premises used: And.intro, 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
refine_1 : ∀ (h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅) (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅
refine_2 :
  ∀ (h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅) (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅
refine_3 : ∀ (h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅) (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅
refine_4 :
  ∀
    (h :
      (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
        (∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
          ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅),
    sumLexLift f₁ f₂ g₁ g₂ a b = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ a b = ∅ ↔
    (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
      (∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
        ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₁
h : sumLexLift f₁ f₂ g₁ 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₁
h : sumLexLift f₁ f₂ g₁ 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₂
h : sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b) = ∅
⊢ g₁ a b = ∅ ∧ g₂ a b = ∅

Tactic:
map_eq_empty.1 h

Premises used: Unit.unit, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Iff.mp, Function.const, Lean.Name, Finset.map_eq_empty, OfNat.ofNat
-- 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 : β₂
h : sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₂
b : β₂
h : sumLexLift f₁ f₂ g₁ g₂ (inr a) (inr 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₂
h : sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b) = ∅
⊢ g₁ a b = ∅ ∧ g₂ a b = ∅

Tactic:
disjSum_eq_empty.1 h

Premises used: Finset.disjSum_eq_empty, Iff.mp
-- 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 : β₂
h : sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b) = ∅
⊢ g₁ a b = ∅ ∧ g₂ a b = ∅

Tactic:
exact disjSum_eq_empty.1 h

Premises used: Finset.disjSum_eq_empty, Iff.mp
-- 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 : β₁ ⊕ β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅
refine_4 :
  ∀ (val : α₁)
    (h :
      (∀ (a₁ : α₁) (b₁ : β₁), Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
        (∀ (a₁ : α₁) (b₂ : β₂), Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
          ∀ (a₂ : α₂) (b₂ : β₂), inl val = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅),
    sumLexLift f₁ f₂ g₁ g₂ (inl val) b = ∅
refine_4₁ :
  ∀ (val : α₂)
    (h :
      (∀ (a₁ : α₁) (b₁ : β₁), inr val = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
        (∀ (a₁ : α₁) (b₂ : β₂), inr val = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
          ∀ (a₂ : α₂) (b₂ : β₂), Eq (α := α₁ ⊕ α₂) (inr val) (inr a₂) → b = inr b₂ → f₂ a₂ b₂ = ∅),
    sumLexLift f₁ f₂ g₁ g₂ (inr val) b = ∅
⊢ sumLexLift f₁ f₂ g₁ 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
val : α₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), inl val = inr a₂ → b = inr b₂ → f₂ a₂ b₂ = ∅
refine_4 :
  ∀ (val_1 : β₁)
    (h :
      (∀ (a₁ : α₁) (b₁ : β₁),
          Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → Eq (α := β₁ ⊕ β₂) (inl val_1) (inl b₁) → f₁ a₁ b₁ = ∅) ∧
        (∀ (a₁ : α₁) (b₂ : β₂),
            Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → inl val_1 = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
          ∀ (a₂ : α₂) (b₂ : β₂), inl val = inr a₂ → inl val_1 = inr b₂ → f₂ a₂ b₂ = ∅),
    sumLexLift f₁ f₂ g₁ g₂ (inl val) (inl val_1) = ∅
refine_4₁ :
  ∀ (val_1 : β₂)
    (h :
      (∀ (a₁ : α₁) (b₁ : β₁), Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → inr val_1 = inl b₁ → f₁ a₁ b₁ = ∅) ∧
        (∀ (a₁ : α₁) (b₂ : β₂),
            Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) →
              Eq (α := β₁ ⊕ β₂) (inr val_1) (inr b₂) → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
          ∀ (a₂ : α₂) (b₂ : β₂), inl val = inr a₂ → Eq (α := β₁ ⊕ β₂) (inr val_1) (inr b₂) → f₂ a₂ b₂ = ∅),
    sumLexLift f₁ f₂ g₁ g₂ (inl val) (inr val_1) = ∅
⊢ sumLexLift f₁ f₂ g₁ 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
val : α₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val = inl a₁ → b = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), inr val = inl a₁ → b = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), Eq (α := α₁ ⊕ α₂) (inr val) (inr a₂) → b = inr b₂ → f₂ a₂ b₂ = ∅
refine_4 :
  ∀ (val_1 : β₁)
    (h :
      (∀ (a₁ : α₁) (b₁ : β₁), inr val = inl a₁ → Eq (α := β₁ ⊕ β₂) (inl val_1) (inl b₁) → f₁ a₁ b₁ = ∅) ∧
        (∀ (a₁ : α₁) (b₂ : β₂), inr val = inl a₁ → inl val_1 = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
          ∀ (a₂ : α₂) (b₂ : β₂), Eq (α := α₁ ⊕ α₂) (inr val) (inr a₂) → inl val_1 = inr b₂ → f₂ a₂ b₂ = ∅),
    sumLexLift f₁ f₂ g₁ g₂ (inr val) (inl val_1) = ∅
refine_4₁ :
  ∀ (val_1 : β₂)
    (h :
      (∀ (a₁ : α₁) (b₁ : β₁), inr val = inl a₁ → inr val_1 = inl b₁ → f₁ a₁ b₁ = ∅) ∧
        (∀ (a₁ : α₁) (b₂ : β₂),
            inr val = inl a₁ → Eq (α := β₁ ⊕ β₂) (inr val_1) (inr b₂) → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
          ∀ (a₂ : α₂) (b₂ : β₂),
            Eq (α := α₁ ⊕ α₂) (inr val) (inr a₂) → Eq (α := β₁ ⊕ β₂) (inr val_1) (inr b₂) → f₂ a₂ b₂ = ∅),
    sumLexLift f₁ f₂ g₁ g₂ (inr val) (inr val_1) = ∅
⊢ sumLexLift f₁ f₂ g₁ 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → 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₂ : β₂), Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → inl val_1 = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), inl val = inr a₂ → inl val_1 = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ 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.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 γ₂
val : α₁
val_1 : β₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁),
      Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → Eq (α := β₁ ⊕ β₂) (inl val_1) (inl b₁) → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → inl val_1 = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), inl val = inr a₂ → inl val_1 = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
val : α₁
val_1 : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → inr val_1 = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂),
        Eq (α := α₁ ⊕ α₂) (inl val) (inl a₁) → Eq (α := β₁ ⊕ β₂) (inr val_1) (inr b₂) → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), inl val = inr a₂ → Eq (α := β₁ ⊕ β₂) (inr val_1) (inr b₂) → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inl val) (inr val_1) = ∅

Tactic:
simp [h.2.1 _ _ rfl rfl]

Premises used: And.right, And.left, 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 γ₂
val : α₂
val_1 : β₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val = inl a₁ → Eq (α := β₁ ⊕ β₂) (inl val_1) (inl b₁) → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), inr val = inl a₁ → inl val_1 = inr b₂ → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂), Eq (α := α₁ ⊕ α₂) (inr val) (inr a₂) → inl val_1 = inr b₂ → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
val : α₂
val_1 : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val = inl a₁ → inr val_1 = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), inr val = inl a₁ → Eq (α := β₁ ⊕ β₂) (inr val_1) (inr b₂) → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂),
        Eq (α := α₁ ⊕ α₂) (inr val) (inr a₂) → Eq (α := β₁ ⊕ β₂) (inr val_1) (inr b₂) → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr val) (inr val_1) = ∅

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

Premises used: Iff.mpr, And.right, Finset.map_eq_empty, 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 γ₂
val : α₂
val_1 : β₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val = inl a₁ → inr val_1 = inl b₁ → f₁ a₁ b₁ = ∅) ∧
    (∀ (a₁ : α₁) (b₂ : β₂), inr val = inl a₁ → Eq (α := β₁ ⊕ β₂) (inr val_1) (inr b₂) → g₁ a₁ b₂ = ∅ ∧ g₂ a₁ b₂ = ∅) ∧
      ∀ (a₂ : α₂) (b₂ : β₂),
        Eq (α := α₁ ⊕ α₂) (inr val) (inr a₂) → Eq (α := β₁ ⊕ β₂) (inr val_1) (inr b₂) → f₂ a₂ b₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr val) (inr val_1) = ∅

Tactic:
exact map_eq_empty.2 (h.2.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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
⊢ (sumLexLift f₁ f₂ g₁ g₂ a b).Nonempty ↔
    (∃ (a₁ : α₁) (b₁ : β₁), a = inl a₁ ∧ b = inl b₁ ∧ (f₁ a₁ b₁).Nonempty) ∨
      (∃ (a₁ : α₁) (b₂ : β₂), a = inl a₁ ∧ b = inr b₂ ∧ ((g₁ a₁ b₂).Nonempty ∨ (g₂ a₁ b₂).Nonempty)) ∨
        ∃ (a₂ : α₂) (b₂ : β₂), a = inr a₂ ∧ b = inr b₂ ∧ (f₂ a₂ b₂).Nonempty

Tactic:
simp only [nonempty_iff_ne_empty, Ne, sumLexLift_eq_empty, not_and_or, exists_prop, not_forall]

Premises used: Finset.sumLexLift_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
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Icc Icc a b ↔ a ≤ x ∧ x ≤ b

Tactic:
simp
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Ico Ico a b ↔ a ≤ x ∧ x < b

Tactic:
simp
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Ioc Ioc a b ↔ a < x ∧ x ≤ b

Tactic:
simp
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
⊢ ∀ (a b x : α ⊕ β), x ∈ sumLift₂ Ioo Ioo a b ↔ a < x ∧ x < b

Tactic:
simp
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
a₁ a₂ : α
⊢ Eq (α := Finset (α ⊕ β)) (Icc (inl a₁) (inl a₂)) (map Embedding.inl (Icc a₁ a₂))

Tactic:
rfl

Premises used: Finset.map, Finset.Icc, Finset.sumLift₂, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
a₁ a₂ : α
⊢ Eq (α := Finset (α ⊕ β)) (Ico (inl a₁) (inl a₂)) (map Embedding.inl (Ico a₁ a₂))

Tactic:
rfl

Premises used: Finset.map, Finset.Ico, Finset.sumLift₂, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
a₁ a₂ : α
⊢ Eq (α := Finset (α ⊕ β)) (Ioc (inl a₁) (inl a₂)) (map Embedding.inl (Ioc a₁ a₂))

Tactic:
rfl

Premises used: Finset.map, Finset.sumLift₂, rfl, Finset.Ioc
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
a₁ a₂ : α
⊢ Eq (α := Finset (α ⊕ β)) (Ioo (inl a₁) (inl a₂)) (map Embedding.inl (Ioo a₁ a₂))

Tactic:
rfl

Premises used: Finset.map, Finset.Ioo, Finset.sumLift₂, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
a₁ : α
b₂ : β
⊢ Icc (inl a₁) (inr b₂) = ∅

Tactic:
rfl

Premises used: Finset.Icc, Finset.sumLift₂, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
a₁ : α
b₂ : β
⊢ Ico (inl a₁) (inr b₂) = ∅

Tactic:
rfl

Premises used: Finset.Ico, Finset.sumLift₂, rfl
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
a₁ : α
b₂ : β
⊢ Ioc (inl a₁) (inr b₂) = ∅

Tactic:
rfl

Premises used: Finset.sumLift₂, rfl, Finset.Ioc
-- Module: Mathlib.Data.Sum.Interval
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : LocallyFiniteOrder α
inst_3 : LocallyFiniteOrder β
a₁ : α
b₂ : β
⊢ Ioo (inl a₁) (inr b₂) = ∅

Tactic:
rfl

Premises used: Finset.Ioo, Finset.sumLift₂, rfl