Theorem: Nat.pair_le_pair_of_le (Logic/Vorspiel/Vorspiel.lean)

State before:
n a₁ a₂ b₁ b₂ : ℕ
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₁.pair b₁ ≤ a₂.pair b₂
Tactic:
rcases lt_or_eq_of_le ha with (ha | rfl) <;> rcases lt_or_eq_of_le hb with (hb | rfl)
State after:
case inl.inl
n a₁ a₂ b₁ b₂ : ℕ
ha✝ : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₂.pair b₂

case inl.inr
n a₁ a₂ b₁ : ℕ
ha✝ : a₁ ≤ a₂
ha : a₁ < a₂
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₂.pair b₁

case inr.inl
n a₁ b₁ b₂ : ℕ
hb✝ : b₁ ≤ b₂
ha : a₁ ≤ a₁
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₁.pair b₂

case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁

State before:
case inl.inl
n a₁ a₂ b₁ b₂ : ℕ
ha✝ : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₂.pair b₂

case inl.inr
n a₁ a₂ b₁ : ℕ
ha✝ : a₁ ≤ a₂
ha : a₁ < a₂
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₂.pair b₁

case inr.inl
n a₁ b₁ b₂ : ℕ
hb✝ : b₁ ≤ b₂
ha : a₁ ≤ a₁
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₁.pair b₂

case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁
Tactic:
{ exact le_of_lt (lt_trans (Nat.pair_lt_pair_left b₁ ha) (Nat.pair_lt_pair_right a₂ hb)) }
State after:
case inl.inr
n a₁ a₂ b₁ : ℕ
ha✝ : a₁ ≤ a₂
ha : a₁ < a₂
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₂.pair b₁

case inr.inl
n a₁ b₁ b₂ : ℕ
hb✝ : b₁ ≤ b₂
ha : a₁ ≤ a₁
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₁.pair b₂

case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁

State before:
case inl.inr
n a₁ a₂ b₁ : ℕ
ha✝ : a₁ ≤ a₂
ha : a₁ < a₂
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₂.pair b₁

case inr.inl
n a₁ b₁ b₂ : ℕ
hb✝ : b₁ ≤ b₂
ha : a₁ ≤ a₁
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₁.pair b₂

case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁
Tactic:
{ exact le_of_lt (Nat.pair_lt_pair_left b₁ ha) }
State after:
case inr.inl
n a₁ b₁ b₂ : ℕ
hb✝ : b₁ ≤ b₂
ha : a₁ ≤ a₁
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₁.pair b₂

case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁

State before:
case inr.inl
n a₁ b₁ b₂ : ℕ
hb✝ : b₁ ≤ b₂
ha : a₁ ≤ a₁
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₁.pair b₂

case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁
Tactic:
{ exact le_of_lt (Nat.pair_lt_pair_right a₁ hb) }
State after:
case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁

State before:
case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁
Tactic:
{ rfl }
State after:
no goals

State before:
case inl.inl
n a₁ a₂ b₁ b₂ : ℕ
ha✝ : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₂.pair b₂
Tactic:
exact le_of_lt (lt_trans (Nat.pair_lt_pair_left b₁ ha) (Nat.pair_lt_pair_right a₂ hb))
State after:
no goals

State before:
case inl.inr
n a₁ a₂ b₁ : ℕ
ha✝ : a₁ ≤ a₂
ha : a₁ < a₂
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₂.pair b₁
Tactic:
exact le_of_lt (Nat.pair_lt_pair_left b₁ ha)
State after:
no goals

State before:
case inr.inl
n a₁ b₁ b₂ : ℕ
hb✝ : b₁ ≤ b₂
ha : a₁ ≤ a₁
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₁.pair b₂
Tactic:
exact le_of_lt (Nat.pair_lt_pair_right a₁ hb)
State after:
no goals

State before:
case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁
Tactic:
rfl
State after:
no goals