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

State before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
⊢ rlexProd i₁ j₁ < rlexProd i₂ j₂ ↔ j₁ < j₂ ∨ j₁ = j₂ ∧ i₁ < i₂
Tactic:
dsimp [rlexProd]
State after:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
⊢ { val := ↑i₁ + m * ↑j₁, isLt := (_ : ↑i₁ + m * ↑j₁ < m * n) } <
      { val := ↑i₂ + m * ↑j₂, isLt := (_ : ↑i₂ + m * ↑j₂ < m * n) } ↔
    j₁ < j₂ ∨ j₁ = j₂ ∧ i₁ < i₂

State before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
⊢ { val := ↑i₁ + m * ↑j₁, isLt := (_ : ↑i₁ + m * ↑j₁ < m * n) } <
      { val := ↑i₂ + m * ↑j₂, isLt := (_ : ↑i₂ + m * ↑j₂ < m * n) } ↔
    j₁ < j₂ ∨ j₁ = j₂ ∧ i₁ < i₂
Tactic:
simp only [Fin.lt_def]
State after:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ ↑j₁ < ↑j₂ ∨ j₁ = j₂ ∧ ↑i₁ < ↑i₂

State before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ ↑j₁ < ↑j₂ ∨ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Tactic:
if hj : j₁.1 < j₂.1 then
  simp only [hj, true_or, iff_true]
  exact rlexProd_lt_of_snd i₁ i₂ hj
else
  simp only [hj, false_or]
  rewrite [Nat.not_lt] at hj
  cases Nat.eq_or_lt_of_le hj with
  | inl heq =>
    cases Fin.eq_of_val_eq heq
    simp only [true_and]
    exact Nat.add_lt_add_iff_right _ i₁.1 i₂.1
  | inr hlt =>
    have : j₁ ≠ j₂ := fun h =>
      Nat.lt_irrefl _ (h ▸ hlt)
    simp only [this, false_and, iff_false, Nat.not_lt]
    apply Nat.le_of_lt
    exact rlexProd_lt_of_snd i₂ i₁ hlt
State after:
no goals

State before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₁ < ↑j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ ↑j₁ < ↑j₂ ∨ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Tactic:
simp only [hj, true_or, iff_true]
State after:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₁ < ↑j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂

State before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₁ < ↑j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂
Tactic:
exact rlexProd_lt_of_snd i₁ i₂ hj
State after:
no goals

State before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ¬↑j₁ < ↑j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ ↑j₁ < ↑j₂ ∨ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Tactic:
simp only [hj, false_or]
State after:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ¬↑j₁ < ↑j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂

State before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ¬↑j₁ < ↑j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Tactic:
rewrite [Nat.not_lt] at hj
State after:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂

State before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Tactic:
cases Nat.eq_or_lt_of_le hj with
| inl heq =>
  cases Fin.eq_of_val_eq heq
  simp only [true_and]
  exact Nat.add_lt_add_iff_right _ i₁.1 i₂.1
| inr hlt =>
  have : j₁ ≠ j₂ := fun h =>
    Nat.lt_irrefl _ (h ▸ hlt)
  simp only [this, false_and, iff_false, Nat.not_lt]
  apply Nat.le_of_lt
  exact rlexProd_lt_of_snd i₂ i₁ hlt
State after:
no goals

State before:
case inl
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
heq : ↑j₂ = ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Tactic:
cases Fin.eq_of_val_eq heq
State after:
case inl.refl
m n : Nat
i₁ i₂ : Fin m
j₁ : Fin n
hj : ↑j₁ ≤ ↑j₁
heq : ↑j₁ = ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₁ ↔ j₁ = j₁ ∧ ↑i₁ < ↑i₂

State before:
case inl.refl
m n : Nat
i₁ i₂ : Fin m
j₁ : Fin n
hj : ↑j₁ ≤ ↑j₁
heq : ↑j₁ = ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₁ ↔ j₁ = j₁ ∧ ↑i₁ < ↑i₂
Tactic:
simp only [true_and]
State after:
case inl.refl
m n : Nat
i₁ i₂ : Fin m
j₁ : Fin n
hj : ↑j₁ ≤ ↑j₁
heq : ↑j₁ = ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₁ ↔ ↑i₁ < ↑i₂

State before:
case inl.refl
m n : Nat
i₁ i₂ : Fin m
j₁ : Fin n
hj : ↑j₁ ≤ ↑j₁
heq : ↑j₁ = ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₁ ↔ ↑i₁ < ↑i₂
Tactic:
exact Nat.add_lt_add_iff_right _ i₁.1 i₂.1
State after:
no goals

State before:
case inr
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
hlt : ↑j₂ < ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Tactic:
have : j₁ ≠ j₂ := fun h =>
  Nat.lt_irrefl _ (h ▸ hlt)
State after:
case inr
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
hlt : ↑j₂ < ↑j₁
this : j₁ ≠ j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂

State before:
case inr
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
hlt : ↑j₂ < ↑j₁
this : j₁ ≠ j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Tactic:
simp only [this, false_and, iff_false, Nat.not_lt]
State after:
case inr
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
hlt : ↑j₂ < ↑j₁
this : j₁ ≠ j₂
⊢ ↑i₂ + m * ↑j₂ ≤ ↑i₁ + m * ↑j₁

State before:
case inr
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
hlt : ↑j₂ < ↑j₁
this : j₁ ≠ j₂
⊢ ↑i₂ + m * ↑j₂ ≤ ↑i₁ + m * ↑j₁
Tactic:
apply Nat.le_of_lt
State after:
case inr.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
hlt : ↑j₂ < ↑j₁
this : j₁ ≠ j₂
⊢ ↑i₂ + m * ↑j₂ < ↑i₁ + m * ↑j₁

State before:
case inr.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
hlt : ↑j₂ < ↑j₁
this : j₁ ≠ j₂
⊢ ↑i₂ + m * ↑j₂ < ↑i₁ + m * ↑j₁
Tactic:
exact rlexProd_lt_of_snd i₂ i₁ hlt
State after:
no goals