-- Mathlib/Data/Sum/Interval.lean
lemma mem_sumLexLift :
    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₂

Proof state:
case mp.inr.inr.intro.intro
α₁ : 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₁ ∧ { toFun := inr, inj' := ⋯ } c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
    (∃ a₁ b₂ c₁, inr a = inl a₁ ∧ inr b = inr b₂ ∧ { toFun := inr, inj' := ⋯ } c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
      (∃ a₁ b₂ c₂, inr a = inl a₁ ∧ inr b = inr b₂ ∧ { toFun := inr, inj' := ⋯ } c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inr b = inr b₂ ∧ { toFun := inr, inj' := ⋯ } c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

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

Result:
no goals

Proof state:
case mpr.inr.inr.inl.intro.intro.intro.intro.intro.intro
α₁ : 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

Result:
no goals

Proof state:
case mp.inl.inr.refine_1.intro.intro
α₁ : 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₁, inl a = inl a₁ ∧ inr b = inl b₁ ∧ inl c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
    (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ inr b = inr b₂ ∧ inl c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
      (∃ a₁ b₂ c₂, inl a = inl a₁ ∧ inr b = inr b₂ ∧ inl c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ 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⟩)

Result:
no goals

Proof state:
case mpr.inr.inr.inr.intro.intro.intro.intro.intro.intro
α₁ : 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

Result:
no goals

Proof state:
case mp.inr.inl
α₁ : 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₁ ∧ 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₂, inr a = inr a₂ ∧ inl b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
exact fun h ↦ (not_mem_empty _ h).elim

Result:
no goals

Proof state:
case mp.inl.inl.intro.intro
α₁ : 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₁, inl a = inl a₁ ∧ inl b = inl b₁ ∧ Embedding.inl c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
    (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ inl b = inr b₂ ∧ Embedding.inl c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
      (∃ a₁ b₂ c₂, inl a = inl a₁ ∧ inl b = inr b₂ ∧ Embedding.inl c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inl b = inr b₂ ∧ Embedding.inl c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

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

Result:
no goals

Proof state:
case mp.inl.inl
α₁ : 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₁, inl a = inl a₁ ∧ inl b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ inl b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, 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]

Result:
case mp.inl.inl
α₁ : 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 : β₁
⊢ (∃ a_1 ∈ f₁ a b, Embedding.inl a_1 = c) →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inl b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
      (∃ a₁ b₂ c₁, inl a = inl a₁ ∧ inl b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, 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₂

Proof state:
case mp.inr.inr
α₁ : 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 : β₂
⊢ (∃ a_1 ∈ f₂ a b, { toFun := inr, inj' := ⋯ } 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₁ ∧ inr b = inr b₂ ∧ c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
        (∃ a₁ b₂ c₂, inr a = inl a₁ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
          ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂

Tactic:
rintro ⟨c, hc, rfl⟩

Result:
case mp.inr.inr.intro.intro
α₁ : 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₁ ∧ { toFun := inr, inj' := ⋯ } c = inl c₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
    (∃ a₁ b₂ c₁, inr a = inl a₁ ∧ inr b = inr b₂ ∧ { toFun := inr, inj' := ⋯ } c = inl c₁ ∧ c₁ ∈ g₁ a₁ b₂) ∨
      (∃ a₁ b₂ c₂, inr a = inl a₁ ∧ inr b = inr b₂ ∧ { toFun := inr, inj' := ⋯ } c = inr c₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
        ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ inr b = inr b₂ ∧ { toFun := inr, inj' := ⋯ } c = inr c₂ ∧ c₂ ∈ f₂ a₂ b₂