-- Mathlib/Order/Disjoint.lean
theorem disjoint_iff [OrderBot α] [OrderBot β] {x y : α × β} :
    Disjoint x y ↔ Disjoint x.1 y.1 ∧ Disjoint x.2 y.2

Proof state:
case mpr.intro
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
ha : Disjoint x.fst y.fst
hb : Disjoint x.snd y.snd
z : α × β
hza : z ≤ x
hzb : z ≤ y
⊢ z ≤ ⊥

Tactic:
exact ⟨ha hza.1 hzb.1, hb hza.2 hzb.2⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x y → Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd

Tactic:
intro h

Result:
case mp
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd

Tactic:
refine ⟨fun a hx hy ↦ (@h (a, ⊥) ⟨hx, ?_⟩ ⟨hy, ?_⟩).1,
  fun b hx hy ↦ (@h (⊥, b) ⟨?_, hx⟩ ⟨?_, hy⟩).2⟩

Result:
case mp.refine_1
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
a : α
hx : a ≤ x.fst
hy : a ≤ y.fst
⊢ (a, ⊥).snd ≤ x.snd

case mp.refine_2
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
a : α
hx : a ≤ x.fst
hy : a ≤ y.fst
⊢ (a, ⊥).snd ≤ y.snd

case mp.refine_3
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ (⊥, b).fst ≤ x.fst

case mp.refine_4
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ (⊥, b).fst ≤ y.fst

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd → Disjoint x y

Tactic:
rintro ⟨ha, hb⟩ z hza hzb

Result:
case mpr.intro
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
ha : Disjoint x.fst y.fst
hb : Disjoint x.snd y.snd
z : α × β
hza : z ≤ x
hzb : z ≤ y
⊢ z ≤ ⊥

Proof state:
case mp.refine_1
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
a : α
hx : a ≤ x.fst
hy : a ≤ y.fst
⊢ (a, ⊥).snd ≤ x.snd

case mp.refine_2
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
a : α
hx : a ≤ x.fst
hy : a ≤ y.fst
⊢ (a, ⊥).snd ≤ y.snd

case mp.refine_3
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ (⊥, b).fst ≤ x.fst

case mp.refine_4
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ (⊥, b).fst ≤ y.fst

Tactic:
all_goals exact bot_le

Result:
no goals

Proof state:
case mp.refine_4
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ (⊥, b).fst ≤ y.fst

Tactic:
exact bot_le

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x y ↔ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x y → Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd

case mpr
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd → Disjoint x y