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

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
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

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
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

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
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

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
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

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)
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

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
State after:
no goals

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
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

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
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

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 ..
State after:
no goals

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]
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, ⋯⟩

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
⊢ decodeSubtype (repr s) k = ⟨j, ⋯⟩
Tactic:
have hij := of_decide_eq_true (Fin.find?_some j hj)
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
hij : Setoid.r i j
⊢ decodeSubtype (repr s) k = ⟨j, ⋯⟩

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
hij : Setoid.r i j
⊢ decodeSubtype (repr s) k = ⟨j, ⋯⟩
Tactic:
apply subtype_eq_of_val_equiv_val
State after:
case a
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
hij : Setoid.r i j
⊢ Setoid.r (decodeSubtype (repr s) k).val ⟨j, ⋯⟩.val

State before:
case a
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
hij : Setoid.r i j
⊢ Setoid.r (decodeSubtype (repr s) k).val ⟨j, ⋯⟩.val
Tactic:
transitivity i
State after:
case a.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
j : Fin n
hj : (Fin.find? fun b => decide (Setoid.r i b)) = some j
hij : Setoid.r i j
⊢ Setoid.r (decodeSubtype (repr s) k).val i

case a.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
j : Fin n
hj : (Fin.find? fun b => decide (Setoid.r i b)) = some j
hij : Setoid.r i j
⊢ Setoid.r i ⟨j, ⋯⟩.val

State before:
case a.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
j : Fin n
hj : (Fin.find? fun b => decide (Setoid.r i b)) = some j
hij : Setoid.r i j
⊢ Setoid.r (decodeSubtype (repr s) k).val i
Tactic:
exact h
State after:
no goals

State before:
case a.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
j : Fin n
hj : (Fin.find? fun b => decide (Setoid.r i b)) = some j
hij : Setoid.r i j
⊢ Setoid.r i ⟨j, ⋯⟩.val
Tactic:
exact hij
State after:
no goals

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
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ absurd ⋯ ⋯ = k
Tactic:
absurd (Fin.find?_none i hnone)
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
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ ¬decide (Setoid.r i i) = false

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
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ ¬decide (Setoid.r i i) = false
Tactic:
rw [decide_eq_false_iff_not]
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
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ ¬¬Setoid.r i i

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
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ ¬¬Setoid.r i i
Tactic:
intro h
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
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : ¬Setoid.r i i
⊢ False

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
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : ¬Setoid.r i i
⊢ False
Tactic:
apply h
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
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : ¬Setoid.r i i
⊢ Setoid.r i i

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
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : ¬Setoid.r i i
⊢ Setoid.r i i
Tactic:
exact Setoid.refl ..
State after:
no goals

State before:
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
Tactic:
intro h
State after:
case h.mpr
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
⊢ Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i

State before:
case h.mpr
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
⊢ Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
Tactic:
have h : getRepr s i = k := h
State after:
case h.mpr
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
h : Fin.getRepr s i = k
⊢ Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i

State before:
case h.mpr
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
h : Fin.getRepr s i = k
⊢ Quotient.mk s (decodeSubtype (repr s) k).val = Quotient.mk s i
Tactic:
apply Quotient.sound
State after:
case h.mpr.a
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
h : Fin.getRepr s i = k
⊢ (decodeSubtype (repr s) k).val ≈ i

State before:
case h.mpr.a
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
h : Fin.getRepr s i = k
⊢ (decodeSubtype (repr s) k).val ≈ i
Tactic:
unfold getRepr at h
State after:
case h.mpr.a
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
h :
  (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
⊢ (decodeSubtype (repr s) k).val ≈ i

State before:
case h.mpr.a
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
h :
  (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
⊢ (decodeSubtype (repr s) k).val ≈ i
Tactic:
split at h
State after:
case h.mpr.a.h_1
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
j✝ : Fin n
heq✝ : (Fin.find? fun b => decide (Setoid.r i b)) = some j✝
h :
  (let_fun this := ⋯;
    encodeSubtype (repr s) ⟨j✝, this⟩) =
    k
⊢ (decodeSubtype (repr s) k).val ≈ i

case h.mpr.a.h_2
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
heq✝ : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : absurd ⋯ ⋯ = k
⊢ (decodeSubtype (repr s) k).val ≈ i

State before:
case h.mpr.a.h_1
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
j✝ : Fin n
heq✝ : (Fin.find? fun b => decide (Setoid.r i b)) = some j✝
h :
  (let_fun this := ⋯;
    encodeSubtype (repr s) ⟨j✝, this⟩) =
    k
⊢ (decodeSubtype (repr s) k).val ≈ i

case h.mpr.a.h_2
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
heq✝ : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : absurd ⋯ ⋯ = k
⊢ (decodeSubtype (repr s) k).val ≈ i
Tactic:
next j hj =>
  rw [←specSubtype] at h
  rw [h]
  symmetry
  apply of_decide_eq_true
  exact Fin.find?_some j hj
State after:
case h.mpr.a.h_2
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
heq✝ : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : absurd ⋯ ⋯ = k
⊢ (decodeSubtype (repr s) k).val ≈ i

State before:
case h.mpr.a.h_2
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
heq✝ : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : absurd ⋯ ⋯ = k
⊢ (decodeSubtype (repr s) k).val ≈ i
Tactic:
next hnone =>
  absurd (Fin.find?_none i hnone)
  rw [decide_eq_false_iff_not]
  intro h
  apply h
  exact Setoid.refl ..
State after:
no goals

State before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
j : Fin n
hj : (Fin.find? fun b => decide (Setoid.r i b)) = some j
h :
  (let_fun this := ⋯;
    encodeSubtype (repr s) ⟨j, this⟩) =
    k
⊢ (decodeSubtype (repr s) k).val ≈ i
Tactic:
rw [←specSubtype] at h
State after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
j : Fin n
hj : (Fin.find? fun b => decide (Setoid.r i b)) = some j
h : decodeSubtype (repr s) k = ⟨j, ⋯⟩
⊢ (decodeSubtype (repr s) k).val ≈ i

State before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
j : Fin n
hj : (Fin.find? fun b => decide (Setoid.r i b)) = some j
h : decodeSubtype (repr s) k = ⟨j, ⋯⟩
⊢ (decodeSubtype (repr s) k).val ≈ i
Tactic:
rw [h]
State after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
j : Fin n
hj : (Fin.find? fun b => decide (Setoid.r i b)) = some j
h : decodeSubtype (repr s) k = ⟨j, ⋯⟩
⊢ ⟨j, ⋯⟩.val ≈ i

State before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
j : Fin n
hj : (Fin.find? fun b => decide (Setoid.r i b)) = some j
h : decodeSubtype (repr s) k = ⟨j, ⋯⟩
⊢ ⟨j, ⋯⟩.val ≈ i
Tactic:
symmetry
State after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
j : Fin n
hj : (Fin.find? fun b => decide (Setoid.r i b)) = some j
h : decodeSubtype (repr s) k = ⟨j, ⋯⟩
⊢ i ≈ ⟨j, ⋯⟩.val

State before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
j : Fin n
hj : (Fin.find? fun b => decide (Setoid.r i b)) = some j
h : decodeSubtype (repr s) k = ⟨j, ⋯⟩
⊢ i ≈ ⟨j, ⋯⟩.val
Tactic:
apply of_decide_eq_true
State after:
case a
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
j : Fin n
hj : (Fin.find? fun b => decide (Setoid.r i b)) = some j
h : decodeSubtype (repr s) k = ⟨j, ⋯⟩
⊢ decide (i ≈ ⟨j, ⋯⟩.val) = true

State before:
case a
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
j : Fin n
hj : (Fin.find? fun b => decide (Setoid.r i b)) = some j
h : decodeSubtype (repr s) k = ⟨j, ⋯⟩
⊢ decide (i ≈ ⟨j, ⋯⟩.val) = true
Tactic:
exact Fin.find?_some j hj
State after:
no goals

State before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : absurd ⋯ ⋯ = k
⊢ (decodeSubtype (repr s) k).val ≈ i
Tactic:
absurd (Fin.find?_none i hnone)
State after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : absurd ⋯ ⋯ = k
⊢ ¬decide (Setoid.r i i) = false

State before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : absurd ⋯ ⋯ = k
⊢ ¬decide (Setoid.r i i) = false
Tactic:
rw [decide_eq_false_iff_not]
State after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : absurd ⋯ ⋯ = k
⊢ ¬¬Setoid.r i i

State before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
h : absurd ⋯ ⋯ = k
⊢ ¬¬Setoid.r i i
Tactic:
intro h
State after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝¹ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
h✝ : absurd ⋯ ⋯ = k
h : ¬Setoid.r i i
⊢ False

State before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝¹ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
h✝ : absurd ⋯ ⋯ = k
h : ¬Setoid.r i i
⊢ False
Tactic:
apply h
State after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝¹ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
h✝ : absurd ⋯ ⋯ = k
h : ¬Setoid.r i i
⊢ Setoid.r i i

State before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
k : Fin (quot s)
i : Fin n
h✝¹ : (Quotient.mk s i).liftOn (Fin.getRepr s) ⋯ = k
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
h✝ : absurd ⋯ ⋯ = k
h : ¬Setoid.r i i
⊢ Setoid.r i i
Tactic:
exact Setoid.refl ..
State after:
no goals