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 γ₂
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₂
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₂
⊢ 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 b | b := 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 : β₁ ⊕ β₂
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₂
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₂
⊢ 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 b | b := 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 γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₁
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₂
⊢ 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:
rw [sumLexLift, mem_map]

Premises used: Finset.mem_map, Finset.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 : γ₁
hc : c ∈ f₁ a b
⊢ (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
      Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧
        Eq (α := β₁ ⊕ β₂) (inl b) (inl b₁) ∧
          Eq (α := γ₁ ⊕ γ₂) ((Embedding.inl : (a : γ₁) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inl c₁ : γ₁ ⊕ γ₂) ∧ c₁ ∈ f₁ a₁ b₁) ∨
    (∃ (a₁ : α₁) (b₂ : β₂) (c₁ : γ₁),
        Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧
          inl b = inr b₂ ∧
            Eq (α := γ₁ ⊕ γ₂) ((Embedding.inl : (a : γ₁) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inl c₁ : γ₁ ⊕ γ₂) ∧ c₁ ∈ g₁ a₁ b₂) ∨
      (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂),
          Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧
            inl b = inr b₂ ∧
              Eq (α := γ₁ ⊕ γ₂) ((Embedding.inl : (a : γ₁) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inr c₂ : γ₁ ⊕ γ₂) ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
          inl a = inr a₂ ∧
            inl b = inr b₂ ∧
              Eq (α := γ₁ ⊕ γ₂) ((Embedding.inl : (a : γ₁) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inr c₂ : γ₁ ⊕ γ₂) ∧ c₂ ∈ f₂ a₂ b₂

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

Premises used: And.intro, Exists.intro, Or.inl, 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 : γ₁
hc : c ∈ f₁ a b
⊢ (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
      Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧
        Eq (α := β₁ ⊕ β₂) (inl b) (inl b₁) ∧
          Eq (α := γ₁ ⊕ γ₂) ((Embedding.inl : (a : γ₁) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inl c₁ : γ₁ ⊕ γ₂) ∧ c₁ ∈ f₁ a₁ b₁) ∨
    (∃ (a₁ : α₁) (b₂ : β₂) (c₁ : γ₁),
        Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧
          inl b = inr b₂ ∧
            Eq (α := γ₁ ⊕ γ₂) ((Embedding.inl : (a : γ₁) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inl c₁ : γ₁ ⊕ γ₂) ∧ c₁ ∈ g₁ a₁ b₂) ∨
      (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂),
          Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧
            inl b = inr b₂ ∧
              Eq (α := γ₁ ⊕ γ₂) ((Embedding.inl : (a : γ₁) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inr c₂ : γ₁ ⊕ γ₂) ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
          inl a = inr a₂ ∧
            inl b = inr b₂ ∧
              Eq (α := γ₁ ⊕ γ₂) ((Embedding.inl : (a : γ₁) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inr c₂ : γ₁ ⊕ γ₂) ∧ c₂ ∈ f₂ a₂ b₂

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

Premises used: Or.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 γ₁
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₂

Tactic:
fun h ↦ (mem_disjSum.1 h).elim ?_ ?_

Premises used: Finset.mem_disjSum, Iff.mp, Or.elim
-- 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 γ₂
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₂
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₂
⊢ 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:
refine fun h ↦ (mem_disjSum.1 h).elim ?_ ?_

Premises used: Finset.mem_disjSum, Iff.mp, Or.elim
-- 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 ∈ g₁ a b
h : inl c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)
⊢ (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
      Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ inr b = inl b₁ ∧ Eq (α := γ₁ ⊕ γ₂) (inl c) (inl c₁) ∧ c₁ ∈ f₁ a₁ b₁) ∨
    (∃ (a₁ : α₁) (b₂ : β₂) (c₁ : γ₁),
        Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧
          Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ Eq (α := γ₁ ⊕ γ₂) (inl c) (inl c₁) ∧ c₁ ∈ g₁ a₁ b₂) ∨
      (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂),
          Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ inl c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
          inl a = inr a₂ ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ inl c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

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

Premises used: And.intro, Exists.intro, Or.inl, 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₂
c : γ₁
hc : c ∈ g₁ a b
h : inl c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)
⊢ (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
      Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ inr b = inl b₁ ∧ Eq (α := γ₁ ⊕ γ₂) (inl c) (inl c₁) ∧ c₁ ∈ f₁ a₁ b₁) ∨
    (∃ (a₁ : α₁) (b₂ : β₂) (c₁ : γ₁),
        Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧
          Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ Eq (α := γ₁ ⊕ γ₂) (inl c) (inl c₁) ∧ c₁ ∈ g₁ a₁ b₂) ∨
      (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂),
          Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ inl c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
          inl a = inr a₂ ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ inl c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

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

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

Tactic:
Or.inr (Or.inr <| Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩)

Premises used: And.intro, Exists.intro, Or.inl, 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₂
c : γ₂
hc : c ∈ g₂ a b
h : inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)
⊢ (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
      Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ inr b = inl b₁ ∧ inr c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
    (∃ (a₁ : α₁) (b₂ : β₂) (c₁ : γ₁),
        Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ inr c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
      (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂),
          Eq (α := α₁ ⊕ α₂) (inl a) (inl a₁) ∧
            Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ Eq (α := γ₁ ⊕ γ₂) (inr c) (inr c₂) ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
          inl a = inr a₂ ∧ Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧ Eq (α := γ₁ ⊕ γ₂) (inr c) (inr c₂) ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
exact Or.inr (Or.inr <| Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩)

Premises used: Or.inl, 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
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:
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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
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:
exact 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₂
b : β₂
mp :
  (∃ a_1 ∈ f₂ a b, ({ toFun := inr, inj' := ⋯ } : (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₂
⊢ 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:
rw [sumLexLift, mem_map]

Premises used: Finset.mem_map, Finset.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 : γ₂
hc : c ∈ f₂ a b
⊢ (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
      inr a = inl a₁ ∧
        inr b = inl b₁ ∧
          Eq (α := γ₁ ⊕ γ₂) (({ toFun := inr, inj' := ⋯ } : (a : γ₂) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inl c₁ : γ₁ ⊕ γ₂) ∧
            c₁ ∈ f₁ a₁ b₁) ∨
    (∃ (a₁ : α₁) (b₂ : β₂) (c₁ : γ₁),
        inr a = inl a₁ ∧
          Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧
            Eq (α := γ₁ ⊕ γ₂) (({ toFun := inr, inj' := ⋯ } : (a : γ₂) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inl c₁ : γ₁ ⊕ γ₂) ∧
              c₁ ∈ g₁ a₁ b₂) ∨
      (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂),
          inr a = inl a₁ ∧
            Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧
              Eq (α := γ₁ ⊕ γ₂) (({ toFun := inr, inj' := ⋯ } : (a : γ₂) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inr c₂ : γ₁ ⊕ γ₂) ∧
                c₂ ∈ g₂ a₁ b₂) ∨
        ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
          Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧
            Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧
              Eq (α := γ₁ ⊕ γ₂) (({ toFun := inr, inj' := ⋯ } : (a : γ₂) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inr c₂ : γ₁ ⊕ γ₂) ∧
                c₂ ∈ f₂ a₂ b₂

Tactic:
Or.inr (Or.inr <| 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 γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₂
b : β₂
c : γ₂
hc : c ∈ f₂ a b
⊢ (∃ (a₁ : α₁) (b₁ : β₁) (c₁ : γ₁),
      inr a = inl a₁ ∧
        inr b = inl b₁ ∧
          Eq (α := γ₁ ⊕ γ₂) (({ toFun := inr, inj' := ⋯ } : (a : γ₂) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inl c₁ : γ₁ ⊕ γ₂) ∧
            c₁ ∈ f₁ a₁ b₁) ∨
    (∃ (a₁ : α₁) (b₂ : β₂) (c₁ : γ₁),
        inr a = inl a₁ ∧
          Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧
            Eq (α := γ₁ ⊕ γ₂) (({ toFun := inr, inj' := ⋯ } : (a : γ₂) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inl c₁ : γ₁ ⊕ γ₂) ∧
              c₁ ∈ g₁ a₁ b₂) ∨
      (∃ (a₁ : α₁) (b₂ : β₂) (c₂ : γ₂),
          inr a = inl a₁ ∧
            Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧
              Eq (α := γ₁ ⊕ γ₂) (({ toFun := inr, inj' := ⋯ } : (a : γ₂) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inr c₂ : γ₁ ⊕ γ₂) ∧
                c₂ ∈ g₂ a₁ b₂) ∨
        ∃ (a₂ : α₂) (b₂ : β₂) (c₂ : γ₂),
          Eq (α := α₁ ⊕ α₂) (inr a) (inr a₂) ∧
            Eq (α := β₁ ⊕ β₂) (inr b) (inr b₂) ∧
              Eq (α := γ₁ ⊕ γ₂) (({ toFun := inr, inj' := ⋯ } : (a : γ₂) → γ₁ ⊕ γ₂) c : γ₁ ⊕ γ₂) (inr c₂ : γ₁ ⊕ γ₂) ∧
                c₂ ∈ f₂ a₂ b₂

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

Tactic:
mem_map_of_mem _ hc

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

Tactic:
inl_mem_disjSum.2 hc

Premises used: Iff.mpr, Set.Mem, setOf, Finset.inl_mem_disjSum
-- 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 ∈ g₁ a b
⊢ inl c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)

Tactic:
exact inl_mem_disjSum.2 hc

Premises used: Iff.mpr, Finset.inl_mem_disjSum
-- 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 ∈ g₂ a b
⊢ inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)

Tactic:
inr_mem_disjSum.2 hc

Premises used: Iff.mpr, Set.Mem, Finset.inr_mem_disjSum, 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₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁
b : β₂
c : γ₂
hc : c ∈ g₂ a b
⊢ inr c ∈ sumLexLift f₁ f₂ g₁ g₂ (inl a) (inr b)

Tactic:
exact inr_mem_disjSum.2 hc

Premises used: Iff.mpr, Finset.inr_mem_disjSum
-- 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:
mem_map_of_mem _ hc

Premises used: Set.Mem, setOf, Finset.mem_map_of_mem