Theorem: Fin.subtype_eq_of_val_equiv_val (GMLInit/Data/Fin/Coding.lean)

State before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Subtype (repr s)
⊢ Setoid.r i.val j.val → i = j
Tactic:
intro hij
State after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Subtype (repr s)
hij : Setoid.r i.val j.val
⊢ i = j

State before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : repr s i
j : Fin n
hrj : repr s j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
⊢ ⟨i, hri⟩ = ⟨j, hrj⟩
Tactic:
unfold repr at hri hrj
State after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
⊢ ⟨i, hri⟩ = ⟨j, hrj⟩

State before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
⊢ ⟨i, hri⟩ = ⟨j, hrj⟩
Tactic:
apply Subtype.eq
State after:
case a
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
⊢ ⟨i, hri⟩.val = ⟨j, hrj⟩.val

State before:
case a
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
⊢ ⟨i, hri⟩.val = ⟨j, hrj⟩.val
Tactic:
apply Option.some.inj
State after:
case a.x
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
⊢ some ⟨i, hri⟩.val = some ⟨j, hrj⟩.val

State before:
case a.x
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
⊢ some ⟨i, hri⟩.val = some ⟨j, hrj⟩.val
Tactic:
rw [←hri, ←hrj]
State after:
case a.x
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
⊢ (Fin.find? fun b => decide (Setoid.r i b)) = Fin.find? fun b => decide (Setoid.r j b)

State before:
case a.x
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
⊢ (Fin.find? fun b => decide (Setoid.r i b)) = Fin.find? fun b => decide (Setoid.r j b)
Tactic:
congr
State after:
case a.x.e_p
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
⊢ (fun b => decide (Setoid.r i b)) = fun b => decide (Setoid.r j b)

State before:
case a.x.e_p
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
⊢ (fun b => decide (Setoid.r i b)) = fun b => decide (Setoid.r j b)
Tactic:
funext k
State after:
case a.x.e_p.h
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
⊢ decide (Setoid.r i k) = decide (Setoid.r j k)

State before:
case a.x.e_p.h
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
⊢ decide (Setoid.r i k) = decide (Setoid.r j k)
Tactic:
rw [decide_eq_decide]
State after:
case a.x.e_p.h
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
⊢ Setoid.r i k ↔ Setoid.r j k

State before:
case a.x.e_p.h
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
⊢ Setoid.r i k ↔ Setoid.r j k
Tactic:
constructor
State after:
case a.x.e_p.h.mp
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
⊢ Setoid.r i k → Setoid.r j k

case a.x.e_p.h.mpr
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
⊢ Setoid.r j k → Setoid.r i k

State before:
case a.x.e_p.h.mp
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
⊢ Setoid.r i k → Setoid.r j k
Tactic:
intro hik
State after:
case a.x.e_p.h.mp
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
hik : Setoid.r i k
⊢ Setoid.r j k

State before:
case a.x.e_p.h.mp
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
hik : Setoid.r i k
⊢ Setoid.r j k
Tactic:
transitivity i
State after:
case a.x.e_p.h.mp.left
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
hik : Setoid.r i k
⊢ Setoid.r j i

case a.x.e_p.h.mp.right
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
hik : Setoid.r i k
⊢ Setoid.r i k

State before:
case a.x.e_p.h.mp.left
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
hik : Setoid.r i k
⊢ Setoid.r j i
Tactic:
symmetry
State after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
hik : Setoid.r i k
⊢ Setoid.r i j

State before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
hik : Setoid.r i k
⊢ Setoid.r i j
Tactic:
exact hij
State after:
no goals

State before:
case a.x.e_p.h.mp.right
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
hik : Setoid.r i k
⊢ Setoid.r i k
Tactic:
exact hik
State after:
no goals

State before:
case a.x.e_p.h.mpr
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
⊢ Setoid.r j k → Setoid.r i k
Tactic:
intro hjk
State after:
case a.x.e_p.h.mpr
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
hjk : Setoid.r j k
⊢ Setoid.r i k

State before:
case a.x.e_p.h.mpr
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
hjk : Setoid.r j k
⊢ Setoid.r i k
Tactic:
transitivity j
State after:
case a.x.e_p.h.mpr.left
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
hjk : Setoid.r j k
⊢ Setoid.r i j

case a.x.e_p.h.mpr.right
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
hjk : Setoid.r j k
⊢ Setoid.r j k

State before:
case a.x.e_p.h.mpr.left
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
hjk : Setoid.r j k
⊢ Setoid.r i j
Tactic:
exact hij
State after:
no goals

State before:
case a.x.e_p.h.mpr.right
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i✝ j✝ : Subtype (repr s)
i : Fin n
hri : (Fin.find? fun b => decide (Setoid.r i b)) = some i
j : Fin n
hrj : (Fin.find? fun b => decide (Setoid.r j b)) = some j
hij : Setoid.r ⟨i, hri⟩.val ⟨j, hrj⟩.val
k : Fin n
hjk : Setoid.r j k
⊢ Setoid.r j k
Tactic:
exact hjk
State after:
no goals