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

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

State before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
⊢ Fin.getRepr s i = Fin.getRepr s j
Tactic:
unfold getRepr
State after:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
⊢ (match h : Fin.find? fun b => decide (Setoid.r i b) with
    | some j =>
      let_fun this := ⋯;
      encodeSubtype (repr s) ⟨j, this⟩
    | 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 ⋯ ⋯

State before:
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
⊢ (match h : Fin.find? fun b => decide (Setoid.r i b) with
    | some j =>
      let_fun this := ⋯;
      encodeSubtype (repr s) ⟨j, this⟩
    | 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:
split
State after:
case h_1
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
j✝ : Fin n
heq✝ : (Fin.find? fun b => decide (Setoid.r i b)) = some j✝
⊢ (let_fun this := ⋯;
    encodeSubtype (repr s) ⟨j✝, this⟩) =
    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 ⋯ ⋯

case h_2
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
heq✝ : (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 ⋯ ⋯

State before:
case h_2
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
heq✝ : (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:
next h =>
  absurd (Fin.find?_none i h)
  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
i j : Fin n
hij : Setoid.r i j
i' : Fin n
hi' : (Fin.find? fun b => decide (Setoid.r i b)) = some i'
⊢ (let_fun this := ⋯;
    encodeSubtype (repr s) ⟨i', this⟩) =
    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:
split
State after:
case h_1
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
heq✝ : (Fin.find? fun b => decide (Setoid.r j b)) = some j✝
⊢ (let_fun this := ⋯;
    encodeSubtype (repr s) ⟨i', this⟩) =
    let_fun this := ⋯;
    encodeSubtype (repr s) ⟨j✝, this⟩

case h_2
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'
heq✝ : (Fin.find? fun b => decide (Setoid.r j b)) = none
⊢ (let_fun this := ⋯;
    encodeSubtype (repr s) ⟨i', this⟩) =
    absurd ⋯ ⋯

State before:
case h_2
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'
heq✝ : (Fin.find? fun b => decide (Setoid.r j b)) = none
⊢ (let_fun this := ⋯;
    encodeSubtype (repr s) ⟨i', this⟩) =
    absurd ⋯ ⋯
Tactic:
next h =>
  absurd (Fin.find?_none j h)
  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
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'
⊢ (let_fun this := ⋯;
    encodeSubtype (repr s) ⟨i', this⟩) =
    let_fun this := ⋯;
    encodeSubtype (repr s) ⟨j', this⟩
Tactic:
clean
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'
j' : Fin n
hj' : (Fin.find? fun b => decide (Setoid.r j b)) = some j'
⊢ encodeSubtype (repr s) ⟨i', ⋯⟩ = encodeSubtype (repr s) ⟨j', ⋯⟩

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'
j' : Fin n
hj' : (Fin.find? fun b => decide (Setoid.r j b)) = some j'
⊢ encodeSubtype (repr s) ⟨i', ⋯⟩ = encodeSubtype (repr s) ⟨j', ⋯⟩
Tactic:
congr
State after:
case e_i.e_val
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'
⊢ i' = j'

State before:
case e_i.e_val
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'
⊢ i' = j'
Tactic:
apply Option.some.inj
State after:
case e_i.e_val.x
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'
⊢ some i' = some j'

State before:
case e_i.e_val.x
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'
⊢ some i' = some j'
Tactic:
rw [←hi', ←hj']
State after:
case e_i.e_val.x
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'
⊢ (Fin.find? fun b => decide (Setoid.r i b)) = Fin.find? fun b => decide (Setoid.r j b)

State before:
case e_i.e_val.x
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'
⊢ (Fin.find? fun b => decide (Setoid.r i b)) = Fin.find? fun b => decide (Setoid.r j b)
Tactic:
congr
State after:
case e_i.e_val.x.e_p
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'
⊢ (fun b => decide (Setoid.r i b)) = fun b => decide (Setoid.r j b)

State before:
case e_i.e_val.x.e_p
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'
⊢ (fun b => decide (Setoid.r i b)) = fun b => decide (Setoid.r j b)
Tactic:
funext k
State after:
case e_i.e_val.x.e_p.h
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
⊢ decide (Setoid.r i k) = decide (Setoid.r j k)

State before:
case e_i.e_val.x.e_p.h
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
⊢ decide (Setoid.r i k) = decide (Setoid.r j k)
Tactic:
rw [decide_eq_decide]
State after:
case e_i.e_val.x.e_p.h
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
⊢ Setoid.r i k ↔ Setoid.r j k

State before:
case e_i.e_val.x.e_p.h
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
⊢ Setoid.r i k ↔ Setoid.r j k
Tactic:
constructor
State after:
case e_i.e_val.x.e_p.h.mp
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
⊢ Setoid.r i k → Setoid.r j k

case e_i.e_val.x.e_p.h.mpr
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
⊢ Setoid.r j k → Setoid.r i k

State before:
case e_i.e_val.x.e_p.h.mp
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
⊢ Setoid.r i k → Setoid.r j k
Tactic:
intro hik
State after:
case e_i.e_val.x.e_p.h.mp
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
hik : Setoid.r i k
⊢ Setoid.r j k

State before:
case e_i.e_val.x.e_p.h.mp
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
hik : Setoid.r i k
⊢ Setoid.r j k
Tactic:
transitivity i
State after:
case e_i.e_val.x.e_p.h.mp.left
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
hik : Setoid.r i k
⊢ Setoid.r j i

case e_i.e_val.x.e_p.h.mp.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
hik : Setoid.r i k
⊢ Setoid.r i k

State before:
case e_i.e_val.x.e_p.h.mp.left
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
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 : 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
hik : Setoid.r i k
⊢ Setoid.r i j

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'
j' : Fin n
hj' : (Fin.find? fun b => decide (Setoid.r j b)) = some j'
k : Fin n
hik : Setoid.r i k
⊢ Setoid.r i j
Tactic:
exact hij
State after:
no goals

State before:
case e_i.e_val.x.e_p.h.mp.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
hik : Setoid.r i k
⊢ Setoid.r i k
Tactic:
exact hik
State after:
no goals

State before:
case e_i.e_val.x.e_p.h.mpr
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
⊢ Setoid.r j k → Setoid.r i k
Tactic:
intro hjk
State after:
case e_i.e_val.x.e_p.h.mpr
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 i k

State before:
case e_i.e_val.x.e_p.h.mpr
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 i k
Tactic:
transitivity j
State after:
case e_i.e_val.x.e_p.h.mpr.left
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 i j

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

State before:
case e_i.e_val.x.e_p.h.mpr.left
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 i j
Tactic:
exact hij
State after:
no goals

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

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

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

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

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

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

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

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

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

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

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