awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
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₂ : γ₂), Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
have mp : ∀ (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: rcases b with b | b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
Goal:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₂
mp :
  ∀ (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₂
⊢ 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₂ : γ₂), Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
have mp₁ : ∀ (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: rcases b with b | b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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) (inl b) →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
        Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ Eq (α := β₁ ⊕ β₂) (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₂
have mp : (∃ a_1 ∈ f a b, (Embedding.inl : (a : γ₁) → γ₁ ⊕ γ₂) a_1 = c) →
  (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
      Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ Eq (α := β₁ ⊕ β₂) (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₂
Tactic: rw [sumLift₂, mem_map]
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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) (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₂
have 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₂
Tactic: rw [sumLift₂, mem_map]
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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₁ : γ₁
⊢ inl c₁ ∈ sumLift₂ f g a b ↔ ∃ (a₁ : α₁) (b₁ : β₁), a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁
have 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₁
Tactic: rw [mem_sumLift₂, or_iff_left]
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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₁
⊢ inl c₁ ∈ sumLift₂ f g a b ↔ ∃ (a₁ : α₁) (b₁ : β₁), a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁
have rw₁ : ¬∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), a = inr a₂ ∧ b = inr b₂ ∧ inl c₁ = inr c₂ ∧ c₂ ∈ g a₂ b₂
Tactic: rw [mem_sumLift₂, or_iff_left]
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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₂ : γ₂
⊢ inr c₂ ∈ sumLift₂ f g a b ↔ ∃ (a₂ : α₂) (b₂ : β₂), a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂
have 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₂
Tactic: rw [mem_sumLift₂, or_iff_right]
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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₂
⊢ inr c₂ ∈ sumLift₂ f g a b ↔ ∃ (a₂ : α₂) (b₂ : β₂), a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ g a₂ b₂
have rw₁ : ¬∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁), a = inl a₁ ∧ b = inl b₁ ∧ inr c₂ = inl c₁ ∧ c₁ ∈ f a₁ b₁
Tactic: rw [mem_sumLift₂, or_iff_right]
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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₂ = ∅
have 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₂ = ∅
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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₂ = ∅
⊢ 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₂ = ∅
have 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 = ∅
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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 = ∅
⊢ (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
have refine_1 : ∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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₁ = ∅
⊢ (∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
have refine_1₁ : ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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₂ = ∅
⊢ sumLift₂ f g a b = ∅
have 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 = ∅
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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 = ∅
⊢ sumLift₂ f g a b = ∅
have 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 = ∅
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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₂ = ∅
⊢ sumLift₂ f g (inl val) b = ∅
have 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) = ∅
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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) = ∅
⊢ sumLift₂ f g (inl val) b = ∅
have 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) = ∅
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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₂ = ∅
⊢ sumLift₂ f g (inr val) b = ∅
have 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) = ∅
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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) = ∅
⊢ sumLift₂ f g (inr val) b = ∅
have 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) = ∅
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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 : γ₁ ⊕ γ₂
⊢ 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₂
have 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₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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₂
⊢ 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₂
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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 : γ₁ ⊕ γ₂
⊢ 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₂
have 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₂
Tactic: obtain a | a := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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₂
⊢ 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₂
have 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₂
Tactic: obtain a | a := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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 : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
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₂
have mp : ∀ (b : β₁),
  c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inl b) →
    (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
        Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ Eq (α := β₁ ⊕ β₂) (inl b) (inl b₁) ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ (a₁ : α₁) (b₂ : β₂) (c₁ : γ₁),
          Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ inl b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂),
            Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
Tactic: obtain b | b := b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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 : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₁
mp :
  ∀ (b : β₁),
    c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inl b) →
      (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
          Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ Eq (α := β₁ ⊕ β₂) (inl b) (inl b₁) ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
        (∃ (a₁ : α₁) (b₂ : β₂) (c₁ : γ₁),
            Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ inl b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
          (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂),
              Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
            ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂), inl a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
⊢ 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₂
have mp₁ : ∀ (b : β₂),
  c ∈ sumLexLift f₁ f₂ g₁ 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₁ : γ₁),
          Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂),
            Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
            inl a = inr a₂ ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
Tactic: obtain b | b := b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Interval (goal)
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 : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
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₂
have mp : ∀ (b : β₁),
  c ∈ sumLexLift f₁ f₂ g₁ 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₁ : γ₁), inr a = inl a₁ ∧ inl b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂), inr a = inl a₁ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
            Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
Tactic: obtain b | b := b
Cleared hypotheses: b