internlm/Lean-Github huggingface dataset:
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof state before:
case e_i.e_val.x.e_p.h.mpr.right
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
i' : Fin n
hi' : (Fin.find? fun b => decide (Setoid.r i b)) = some i'
j' : Fin n
hj' : (Fin.find? fun b => decide (Setoid.r j b)) = some j'
k : Fin n
hjk : Setoid.r j k
⊢ Setoid.r j k
Tactic:
exact hjk
Proof state after:
no goals
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof state before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
i' : Fin n
hi' : (Fin.find? fun b => decide (Setoid.r i b)) = some i'
h : (Fin.find? fun b => decide (Setoid.r j b)) = none
⊢ (let_fun this := ⋯;
    encodeSubtype (repr s) ⟨i', this⟩) =
    absurd ⋯ ⋯
Tactic:
absurd (Fin.find?_none j h)
Proof state after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
i' : Fin n
hi' : (Fin.find? fun b => decide (Setoid.r i b)) = some i'
h : (Fin.find? fun b => decide (Setoid.r j b)) = none
⊢ ¬decide (Setoid.r j j) = false
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof state before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
i' : Fin n
hi' : (Fin.find? fun b => decide (Setoid.r i b)) = some i'
h : (Fin.find? fun b => decide (Setoid.r j b)) = none
⊢ ¬decide (Setoid.r j j) = false
Tactic:
rw [decide_eq_false_iff_not]
Proof state after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
i' : Fin n
hi' : (Fin.find? fun b => decide (Setoid.r i b)) = some i'
h : (Fin.find? fun b => decide (Setoid.r j b)) = none
⊢ ¬¬Setoid.r j j
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof state before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
i' : Fin n
hi' : (Fin.find? fun b => decide (Setoid.r i b)) = some i'
h : (Fin.find? fun b => decide (Setoid.r j b)) = none
⊢ ¬¬Setoid.r j j
Tactic:
intro h
Proof state after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
i' : Fin n
hi' : (Fin.find? fun b => decide (Setoid.r i b)) = some i'
h✝ : (Fin.find? fun b => decide (Setoid.r j b)) = none
h : ¬Setoid.r j j
⊢ False
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof state before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
i' : Fin n
hi' : (Fin.find? fun b => decide (Setoid.r i b)) = some i'
h✝ : (Fin.find? fun b => decide (Setoid.r j b)) = none
h : ¬Setoid.r j j
⊢ False
Tactic:
apply h
Proof state after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
i' : Fin n
hi' : (Fin.find? fun b => decide (Setoid.r i b)) = some i'
h✝ : (Fin.find? fun b => decide (Setoid.r j b)) = none
h : ¬Setoid.r j j
⊢ Setoid.r j j
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof state before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
i' : Fin n
hi' : (Fin.find? fun b => decide (Setoid.r i b)) = some i'
h✝ : (Fin.find? fun b => decide (Setoid.r j b)) = none
h : ¬Setoid.r j j
⊢ Setoid.r j j
Tactic:
exact Setoid.refl ..
Proof state after:
no goals
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof state before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
h : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ absurd ⋯ ⋯ =
    match h : Fin.find? fun b => decide (Setoid.r j b) with
    | some j_1 =>
      let_fun this := ⋯;
      encodeSubtype (repr s) ⟨j_1, this⟩
    | none => absurd ⋯ ⋯
Tactic:
absurd (Fin.find?_none i h)
Proof state after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
h : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ ¬decide (Setoid.r i i) = false
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof state before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
h : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ ¬decide (Setoid.r i i) = false
Tactic:
rw [decide_eq_false_iff_not]
Proof state after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
h : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ ¬¬Setoid.r i i
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof state before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
h : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ ¬¬Setoid.r i i
Tactic:
intro h
Proof state after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
h✝ : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : ¬Setoid.r i i
⊢ False
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof state before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
h✝ : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : ¬Setoid.r i i
⊢ False
Tactic:
apply h
Proof state after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
h✝ : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : ¬Setoid.r i i
⊢ Setoid.r i i
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof state before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
h✝ : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : ¬Setoid.r i i
⊢ Setoid.r i i
Tactic:
exact Setoid.refl ..
Proof state after:
no goals
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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
Proof 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
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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
Proof 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⟩
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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
Proof 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
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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
Proof 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
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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]
Proof 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)
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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
Proof 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)
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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
Proof 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)
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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]
Proof 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
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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
Proof 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
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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
Proof 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
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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
Proof 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
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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
Proof 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
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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
Proof state after:
no goals
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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
Proof state after:
no goals
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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
Proof 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
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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
Proof 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
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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
Proof state after:
no goals
Theorem: Fin.subtype_eq_of_val_equiv_val
Proof 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
Proof state after:
no goals
Theorem: Fin.specQuotient
Proof state before:
case h
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
⊢ decodeQuotient s k = Quotient.mk s i ↔ encodeQuotient s (Quotient.mk s i) = k
Tactic:
unfold decodeQuotient encodeQuotient
Proof state after:
case h
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
⊢ Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i ↔ (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
Theorem: Fin.specQuotient
Proof state before:
case h
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
⊢ Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i ↔ (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
Tactic:
constructor
Proof state after:
case h.mp
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
⊢ Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i → (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k

case h.mpr
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
⊢ (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k → Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
Theorem: Fin.specQuotient
Proof state before:
case h.mp
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
⊢ Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i → (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
Tactic:
intro h
Proof state after:
case h.mp
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
⊢ (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
Theorem: Fin.specQuotient
Proof state before:
case h.mp
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
⊢ (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
Tactic:
have h := Quotient.exact h
Proof state after:
case h.mp
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
h : (decodeSubtype (repr s) k).val ≈ i
⊢ (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
Theorem: Fin.specQuotient
Proof state before:
case h.mp
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
h : (decodeSubtype (repr s) k).val ≈ i
⊢ (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
Tactic:
transitivity (getRepr s i)
Proof state after:
case h.mp.left
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
h : (decodeSubtype (repr s) k).val ≈ i
⊢ (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = Fin.getRepr s i

case h.mp.right
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
h : (decodeSubtype (repr s) k).val ≈ i
⊢ Fin.getRepr s i = k
Theorem: Fin.specQuotient
Proof state before:
case h.mp.left
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
h : (decodeSubtype (repr s) k).val ≈ i
⊢ (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = Fin.getRepr s i
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.specQuotient
Proof state before:
case h.mp.right
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
h : (decodeSubtype (repr s) k).val ≈ i
⊢ Fin.getRepr s i = k
Tactic:
unfold getRepr
Proof state after:
case h.mp.right
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
h : (decodeSubtype (repr s) k).val ≈ i
⊢ (match h : Fin.find? fun b => decide (Setoid.r i b) with
    | some j =>
      let_fun this := ⋯;
      encodeSubtype (repr s) ⟨j, this⟩
    | none => absurd ⋯ ⋯) =
    k
Theorem: Fin.specQuotient
Proof state before:
case h.mp.right
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
h : (decodeSubtype (repr s) k).val ≈ i
⊢ (match h : Fin.find? fun b => decide (Setoid.r i b) with
    | some j =>
      let_fun this := ⋯;
      encodeSubtype (repr s) ⟨j, this⟩
    | none => absurd ⋯ ⋯) =
    k
Tactic:
split
Proof state after:
case h.mp.right.h_1
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
h : (decodeSubtype (repr s) k).val ≈ i
j✝ : Fin n
heq✝ : (Fin.find? fun b => decide (Setoid.r i b)) = some j✝
⊢ (let_fun this := ⋯;
    encodeSubtype (repr s) ⟨j✝, this⟩) =
    k

case h.mp.right.h_2
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
h : (decodeSubtype (repr s) k).val ≈ i
heq✝ : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ absurd ⋯ ⋯ = k
Theorem: Fin.specQuotient
Proof state before:
case h.mp.right.h_2
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
h : (decodeSubtype (repr s) k).val ≈ i
heq✝ : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ absurd ⋯ ⋯ = k
Tactic:
next hnone =>
  absurd (Fin.find?_none i hnone)
  rw [decide_eq_false_iff_not]
  intro h
  apply h
  exact Setoid.refl ..
Proof state after:
no goals
Theorem: Fin.specQuotient
Proof state before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
h : (decodeSubtype (repr s) k).val ≈ i
j : Fin n
hj : (Fin.find? fun b => decide (Setoid.r i b)) = some j
⊢ (let_fun this := ⋯;
    encodeSubtype (repr s) ⟨j, this⟩) =
    k
Tactic:
rw [←specSubtype]
Proof state after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
h : (decodeSubtype (repr s) k).val ≈ i
j : Fin n
hj : (Fin.find? fun b => decide (Setoid.r i b)) = some j
⊢ decodeSubtype (repr s) k = ⟨j, ⋯⟩