Theorem: Fin.lexfold_inj (Algdata/Data/Fin/Basic.lean)

State before:
m n : Nat
x₁ x₂ : Fin m
y₁ y₂ : Fin n
h : ↑x₁ * n + ↑y₁ = ↑x₂ * n + ↑y₂
this : y₁ = y₂
⊢ x₁ = x₂ ∧ y₁ = y₂
Tactic:
cases this
State after:
case refl
m n : Nat
x₁ x₂ : Fin m
y₁ : Fin n
h : ↑x₁ * n + ↑y₁ = ↑x₂ * n + ↑y₁
⊢ x₁ = x₂ ∧ y₁ = y₁

State before:
case refl
m n : Nat
x₁ x₂ : Fin m
y₁ : Fin n
h : ↑x₁ * n + ↑y₁ = ↑x₂ * n + ↑y₁
⊢ x₁ = x₂ ∧ y₁ = y₁
Tactic:
have : 0 < n := trans y₁.val.zero_le y₁.isLt
State after:
case refl
m n : Nat
x₁ x₂ : Fin m
y₁ : Fin n
h : ↑x₁ * n + ↑y₁ = ↑x₂ * n + ↑y₁
this : 0 < n
⊢ x₁ = x₂ ∧ y₁ = y₁

State before:
case refl
m n : Nat
x₁ x₂ : Fin m
y₁ : Fin n
h : ↑x₁ * n + ↑y₁ = ↑x₂ * n + ↑y₁
this✝ : 0 < n
this : x₁ = x₂
⊢ x₁ = x₂ ∧ y₁ = y₁
Tactic:
exact ⟨this, rfl⟩
State after:
no goals