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

State before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ i₁ = i₂ ∧ j₁ = j₂
Tactic:
constructor <;> ext
State after:
case left.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ ↑i₁ = ↑i₂

case right.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ ↑j₁ = ↑j₂

State before:
case left.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ ↑i₁ = ↑i₂

case right.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ ↑j₁ = ↑j₂
Tactic:
. rw [← rlexProd_val_mod (i:=i₁) (j:=j₁), ← rlexProd_val_mod (i:=i₂) (j:= j₂), h]
State after:
case right.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ ↑j₁ = ↑j₂

State before:
case right.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ ↑j₁ = ↑j₂
Tactic:
. rw [← rlexProd_val_div (i:=i₁) (j:=j₁), ← rlexProd_val_div (i:=i₂) (j:= j₂), h]
State after:
no goals

State before:
case left.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ ↑i₁ = ↑i₂
Tactic:
rw [← rlexProd_val_mod (i:=i₁) (j:=j₁), ← rlexProd_val_mod (i:=i₂) (j:= j₂), h]
State after:
no goals

State before:
case right.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ ↑j₁ = ↑j₂
Tactic:
rw [← rlexProd_val_div (i:=i₁) (j:=j₁), ← rlexProd_val_div (i:=i₂) (j:= j₂), h]
State after:
no goals