Theorem: Fin.pair_left_pair (LeanColls/MathlibUpstream.lean)

State before:
m n : ℕ
x : Fin m
y : Fin n
⊢ (x.pair y).pair_left = x
Tactic:
rcases x with ⟨x,hx⟩
State after:
case mk
m n : ℕ
y : Fin n
x : ℕ
hx : x < m
⊢ (⟨x, hx⟩.pair y).pair_left = ⟨x, hx⟩

State before:
case mk
m n : ℕ
y : Fin n
x : ℕ
hx : x < m
⊢ (⟨x, hx⟩.pair y).pair_left = ⟨x, hx⟩
Tactic:
rcases y with ⟨y,hy⟩
State after:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
⊢ (⟨x, hx⟩.pair ⟨y, hy⟩).pair_left = ⟨x, hx⟩

State before:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
⊢ (⟨x, hx⟩.pair ⟨y, hy⟩).pair_left = ⟨x, hx⟩
Tactic:
simp [pair_left, pair]
State after:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
⊢ (x * n + y) / n = x

State before:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
⊢ (x * n + y) / n = x
Tactic:
have : n > 0 := by by_contra; simp_all
State after:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
this : n > 0
⊢ (x * n + y) / n = x

State before:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
this : n > 0
⊢ (x * n + y) / n = x
Tactic:
rw [Nat.mul_comm, Nat.mul_add_div this, (Nat.div_eq_zero_iff this).mpr hy]
State after:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
this : n > 0
⊢ x + 0 = x

State before:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
this : n > 0
⊢ x + 0 = x
Tactic:
simp
State after:
no goals

State before:
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
⊢ n > 0
Tactic:
by_contra
State after:
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
x✝ : ¬n > 0
⊢ False

State before:
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
x✝ : ¬n > 0
⊢ False
Tactic:
simp_all
State after:
no goals