Theorem: Fin.rlexProd_lt_of_snd (Fifteen/Data/Fin/Basic.lean)

State before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : j₁ < j₂
⊢ rlexProd i₁ j₁ < rlexProd i₂ j₂
Tactic:
calc i₁.1 + m * j₁.1
  _ < m + m * j₁.1 := Nat.add_lt_add_right i₁.2 _
  _ = m * (j₁.1 + 1) := by rewrite [Nat.add_comm m]; rfl
  _ ≤ m * j₂.1 := Nat.mul_le_mul_left m h
  _ ≤ i₂.1 + m * j₂.1 := Nat.le_add_left ..
State after:
no goals

State before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : j₁ < j₂
⊢ m + m * ↑j₁ = m * (↑j₁ + 1)
Tactic:
rewrite [Nat.add_comm m]
State after:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : j₁ < j₂
⊢ m * ↑j₁ + m = m * (↑j₁ + 1)

State before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : j₁ < j₂
⊢ m * ↑j₁ + m = m * (↑j₁ + 1)
Tactic:
rfl
State after:
no goals