Theorem: Fin.toIndView_eq_iff_toFin_eq (GMLInit/Data/Fin/Basic.lean)

State before:
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
⊢ ⟨0, isLt✝⟩.toIndView = IndView.zero ↔ IndView.zero.toFin = ⟨0, isLt✝⟩
Tactic:
constructor
State after:
case mp
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
⊢ ⟨0, isLt✝⟩.toIndView = IndView.zero → IndView.zero.toFin = ⟨0, isLt✝⟩

case mpr
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
⊢ IndView.zero.toFin = ⟨0, isLt✝⟩ → ⟨0, isLt✝⟩.toIndView = IndView.zero

State before:
case mp
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
⊢ ⟨0, isLt✝⟩.toIndView = IndView.zero → IndView.zero.toFin = ⟨0, isLt✝⟩
Tactic:
intro
State after:
case mp
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
a✝ : ⟨0, isLt✝⟩.toIndView = IndView.zero
⊢ IndView.zero.toFin = ⟨0, isLt✝⟩

State before:
case mp
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
a✝ : ⟨0, isLt✝⟩.toIndView = IndView.zero
⊢ IndView.zero.toFin = ⟨0, isLt✝⟩
Tactic:
reflexivity
State after:
no goals

State before:
case mpr
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
⊢ IndView.zero.toFin = ⟨0, isLt✝⟩ → ⟨0, isLt✝⟩.toIndView = IndView.zero
Tactic:
intro
State after:
case mpr
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
a✝ : IndView.zero.toFin = ⟨0, isLt✝⟩
⊢ ⟨0, isLt✝⟩.toIndView = IndView.zero

State before:
case mpr
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
a✝ : IndView.zero.toFin = ⟨0, isLt✝⟩
⊢ ⟨0, isLt✝⟩.toIndView = IndView.zero
Tactic:
reflexivity
State after:
no goals

State before:
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
⊢ ⟨0, isLt✝⟩.toIndView = j.succ ↔ j.succ.toFin = ⟨0, isLt✝⟩
Tactic:
constructor
State after:
case mp
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
⊢ ⟨0, isLt✝⟩.toIndView = j.succ → j.succ.toFin = ⟨0, isLt✝⟩

case mpr
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
⊢ j.succ.toFin = ⟨0, isLt✝⟩ → ⟨0, isLt✝⟩.toIndView = j.succ

State before:
case mp
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
⊢ ⟨0, isLt✝⟩.toIndView = j.succ → j.succ.toFin = ⟨0, isLt✝⟩
Tactic:
intro
State after:
case mp
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
a✝ : ⟨0, isLt✝⟩.toIndView = j.succ
⊢ j.succ.toFin = ⟨0, isLt✝⟩

State before:
case mp
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
a✝ : ⟨0, isLt✝⟩.toIndView = j.succ
⊢ j.succ.toFin = ⟨0, isLt✝⟩
Tactic:
contradiction
State after:
no goals

State before:
case mpr
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
⊢ j.succ.toFin = ⟨0, isLt✝⟩ → ⟨0, isLt✝⟩.toIndView = j.succ
Tactic:
intro h
State after:
case mpr
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
h : j.succ.toFin = ⟨0, isLt✝⟩
⊢ ⟨0, isLt✝⟩.toIndView = j.succ

State before:
case mpr
n✝¹ n✝ : Nat
i : Fin n✝
j✝ : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
j : Fin.IndView n
h : j.succ.toFin = ⟨0, isLt✝⟩
⊢ ⟨0, isLt✝⟩.toIndView = j.succ
Tactic:
cases h
State after:
no goals

State before:
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
⊢ ⟨i + 1, hi⟩.toIndView = IndView.zero ↔ IndView.zero.toFin = ⟨i + 1, hi⟩
Tactic:
constructor
State after:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
⊢ ⟨i + 1, hi⟩.toIndView = IndView.zero → IndView.zero.toFin = ⟨i + 1, hi⟩

case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
⊢ IndView.zero.toFin = ⟨i + 1, hi⟩ → ⟨i + 1, hi⟩.toIndView = IndView.zero

State before:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
⊢ ⟨i + 1, hi⟩.toIndView = IndView.zero → IndView.zero.toFin = ⟨i + 1, hi⟩
Tactic:
intro
State after:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
a✝ : ⟨i + 1, hi⟩.toIndView = IndView.zero
⊢ IndView.zero.toFin = ⟨i + 1, hi⟩

State before:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
a✝ : ⟨i + 1, hi⟩.toIndView = IndView.zero
⊢ IndView.zero.toFin = ⟨i + 1, hi⟩
Tactic:
contradiction
State after:
no goals

State before:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
⊢ IndView.zero.toFin = ⟨i + 1, hi⟩ → ⟨i + 1, hi⟩.toIndView = IndView.zero
Tactic:
intro h
State after:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
h : IndView.zero.toFin = ⟨i + 1, hi⟩
⊢ ⟨i + 1, hi⟩.toIndView = IndView.zero

State before:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
h : IndView.zero.toFin = ⟨i + 1, hi⟩
⊢ ⟨i + 1, hi⟩.toIndView = IndView.zero
Tactic:
cases h
State after:
no goals

State before:
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
⊢ ⟨i + 1, hi⟩.toIndView = j.succ ↔ j.succ.toFin = ⟨i + 1, hi⟩
Tactic:
have hsucc : ⟨i+1, hi⟩ = Fin.succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ := rfl
State after:
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
⊢ ⟨i + 1, hi⟩.toIndView = j.succ ↔ j.succ.toFin = ⟨i + 1, hi⟩

State before:
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
⊢ ⟨i + 1, hi⟩.toIndView = j.succ ↔ j.succ.toFin = ⟨i + 1, hi⟩
Tactic:
constructor
State after:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
⊢ ⟨i + 1, hi⟩.toIndView = j.succ → j.succ.toFin = ⟨i + 1, hi⟩

case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
⊢ j.succ.toFin = ⟨i + 1, hi⟩ → ⟨i + 1, hi⟩.toIndView = j.succ

State before:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
⊢ ⟨i + 1, hi⟩.toIndView = j.succ → j.succ.toFin = ⟨i + 1, hi⟩
Tactic:
intro h
State after:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : ⟨i + 1, hi⟩.toIndView = j.succ
⊢ j.succ.toFin = ⟨i + 1, hi⟩

State before:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : ⟨i + 1, hi⟩.toIndView = j.succ
⊢ j.succ.toFin = ⟨i + 1, hi⟩
Tactic:
rw [IndView.toFin, hsucc]
State after:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : ⟨i + 1, hi⟩.toIndView = j.succ
⊢ j.toFin.succ = ⟨i, ⋯⟩.succ

State before:
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : ⟨i + 1, hi⟩.toIndView = j.succ
⊢ j.toFin.succ = ⟨i, ⋯⟩.succ
Tactic:
congr
State after:
case mp.e_a
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : ⟨i + 1, hi⟩.toIndView = j.succ
⊢ j.toFin = ⟨i, ⋯⟩

State before:
case mp.e_a
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : ⟨i + 1, hi⟩.toIndView = j.succ
⊢ j.toFin = ⟨i, ⋯⟩
Tactic:
rw [←toIndView_eq_iff_toFin_eq]
State after:
case mp.e_a
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : ⟨i + 1, hi⟩.toIndView = j.succ
⊢ ⟨i, ⋯⟩.toIndView = j

State before:
case mp.e_a
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : ⟨i + 1, hi⟩.toIndView = j.succ
⊢ ⟨i, ⋯⟩.toIndView = j
Tactic:
exact IndView.succ.inj h
State after:
no goals

State before:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
⊢ j.succ.toFin = ⟨i + 1, hi⟩ → ⟨i + 1, hi⟩.toIndView = j.succ
Tactic:
intro h
State after:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.succ.toFin = ⟨i + 1, hi⟩
⊢ ⟨i + 1, hi⟩.toIndView = j.succ

State before:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.succ.toFin = ⟨i + 1, hi⟩
⊢ ⟨i + 1, hi⟩.toIndView = j.succ
Tactic:
rw [IndView.toFin, hsucc] at h
State after:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.toFin.succ = ⟨i, ⋯⟩.succ
⊢ ⟨i + 1, hi⟩.toIndView = j.succ

State before:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.toFin.succ = ⟨i, ⋯⟩.succ
⊢ ⟨i + 1, hi⟩.toIndView = j.succ
Tactic:
rw [Fin.toIndView]
State after:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.toFin.succ = ⟨i, ⋯⟩.succ
⊢ ⟨i, ⋯⟩.toIndView.succ = j.succ

State before:
case mpr
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.toFin.succ = ⟨i, ⋯⟩.succ
⊢ ⟨i, ⋯⟩.toIndView.succ = j.succ
Tactic:
congr
State after:
case mpr.e_a
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.toFin.succ = ⟨i, ⋯⟩.succ
⊢ ⟨i, ⋯⟩.toIndView = j

State before:
case mpr.e_a
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.toFin.succ = ⟨i, ⋯⟩.succ
⊢ ⟨i, ⋯⟩.toIndView = j
Tactic:
rw [toIndView_eq_iff_toFin_eq]
State after:
case mpr.e_a
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.toFin.succ = ⟨i, ⋯⟩.succ
⊢ j.toFin = ⟨i, ⋯⟩

State before:
case mpr.e_a
n✝¹ n✝ : Nat
i✝ : Fin n✝
j✝ : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
j : Fin.IndView n
hsucc : ⟨i + 1, hi⟩ = ⟨i, ⋯⟩.succ
h : j.toFin.succ = ⟨i, ⋯⟩.succ
⊢ j.toFin = ⟨i, ⋯⟩
Tactic:
exact succ_inj.mp h
State after:
no goals