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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₂
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₂
⊢ 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) (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 = inl a₁ ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂),
            inr a = inl a₁ ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
            Eq (α := α₁ ⊕ α₂) (inr 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 γ₂
c : γ₁ ⊕ γ₂
a : α₁
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₂
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₁ : γ₁),
        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: rw [sumLexLift, 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₁
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₂
have mp : ∀ (h : c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)),
  (∃ a_1 ∈ g₁ a b, inl a_1 = c) →
    (∃ (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: refine fun h ↦ (mem_disjSum.1 h).elim ?_ ?_
-- 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 γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₂
mp :
  ∀ (h : c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)),
    (∃ a_1 ∈ g₁ a b, inl a_1 = c) →
      (∃ (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₂
⊢ 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₂
have mp₁ : ∀ (h : c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)),
  (∃ b_1 ∈ g₂ a b, inr b_1 = c) →
    (∃ (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: refine fun h ↦ (mem_disjSum.1 h).elim ?_ ?_
-- 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 γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₂
⊢ c ∈ sumLexLift f₁ f₂ g₁ 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 = inl a₁ ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂),
            inr a = inl a₁ ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
            Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
have mp : (∃ a_1 ∈ f₂ a b, ({ toFun := inr, inj' := sorry } : (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₁ : γ₁),
        inr a = inl a₁ ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
      (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂),
          inr a = inl a₁ ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
          Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂
Tactic: rw [sumLexLift, 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₁ 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 : β₁ ⊕ β₂
⊢ sumLexLift f₁ f₂ g₁ g₂ a b ⊆ sumLexLift f₁' f₂' g₁' g₂' a b
have inl : ∀ (val : α₁), sumLexLift f₁ f₂ g₁ g₂ (inl val) b ⊆ sumLexLift f₁' f₂' g₁' g₂' (inl val) b
Tactic: cases 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₁ 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
⊢ sumLexLift f₁ f₂ g₁ g₂ a b ⊆ sumLexLift f₁' f₂' g₁' g₂' a b
have inr : ∀ (val : α₂), sumLexLift f₁ f₂ g₁ g₂ (inr val) b ⊆ sumLexLift f₁' f₂' g₁' g₂' (inr val) b
Tactic: cases 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₁ 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 : α₁
⊢ sumLexLift f₁ f₂ g₁ g₂ (inl val) b ⊆ sumLexLift f₁' f₂' g₁' g₂' (inl val) b
have inl : ∀ (val_1 : β₁), sumLexLift f₁ f₂ g₁ g₂ (inl val) (inl val_1) ⊆ sumLexLift f₁' f₂' g₁' g₂' (inl val) (inl val_1)
Tactic: cases 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₁ 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)
⊢ sumLexLift f₁ f₂ g₁ g₂ (Sum.inl val) b ⊆ sumLexLift f₁' f₂' g₁' g₂' (Sum.inl val) b
have 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)
Tactic: cases 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₁ 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 : α₂
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr val) b ⊆ sumLexLift f₁' f₂' g₁' g₂' (inr val) b
have inr : ∀ (val_1 : β₁), sumLexLift f₁ f₂ g₁ g₂ (inr val) (inl val_1) ⊆ sumLexLift f₁' f₂' g₁' g₂' (inr val) (inl val_1)
Tactic: cases 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₁ 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)
⊢ sumLexLift f₁ f₂ g₁ g₂ (Sum.inr val) b ⊆ sumLexLift f₁' f₂' g₁' g₂' (Sum.inr val) b
have 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)
Tactic: cases 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 γ₂
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₂ = ∅
have refine_1 : ∀ (h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅) (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f₁ 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 γ₁
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₁ = ∅
⊢ 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₂ = ∅
have refine_2 : ∀ (h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅) (a₁ : α₁) (b₂ : β₂), a = inl a₁ → b = inr b₂ → g₁ a₁ 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 γ₁
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₂ = ∅
⊢ 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₂ = ∅
have refine_3 : ∀ (h : sumLexLift f₁ f₂ g₁ g₂ a b = ∅) (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → f₂ 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 γ₁
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₂ = ∅
⊢ 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₂ = ∅
have 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 = ∅
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 γ₁
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₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ a b = ∅
have 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 = ∅
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 γ₁
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 = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ a b = ∅
have 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 = ∅
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 γ₁
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₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inl val) b = ∅
have 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) = ∅
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 γ₂
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) = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inl val) b = ∅
have 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) = ∅
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 γ₂
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₂ = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr val) b = ∅
have 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) = ∅
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 γ₂
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) = ∅
⊢ sumLexLift f₁ f₂ g₁ g₂ (inr val) b = ∅
have 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) = ∅
Tactic: cases b
Cleared hypotheses: b, h