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

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

State before:
case mk
m n : ℕ
y : Fin n
x : ℕ
hx : x < m
⊢ (⟨x, hx⟩.pair y).pair_right = y
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_right = ⟨y, hy⟩

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

State before:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
⊢ (x * n + y) % n = y
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 = y

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

State before:
case mk.mk
m n x : ℕ
hx : x < m
y : ℕ
hy : y < n
this : n > 0
⊢ y % n = y
Tactic:
apply Nat.mod_eq_of_lt hy
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