internlm/Lean-Github huggingface dataset:
Theorem: Fin.specSubtype
Proof state before:
case e_val.e_val.e_a.left
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k✝ : Fin (count p)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ ↑(decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩).1 = ↑⟨⟨i, ⋯⟩, hp⟩.val
Tactic:
apply congrArg Fin.val
Proof state after:
case e_val.e_val.e_a.left
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k✝ : Fin (count p)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ (decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩).1 = ⟨⟨i, ⋯⟩, hp⟩.val
Theorem: Fin.specSubtype
Proof state before:
case e_val.e_val.e_a.left
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k✝ : Fin (count p)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ (decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩).1 = ⟨⟨i, ⋯⟩, hp⟩.val
Tactic:
apply congrArg Subtype.val
Proof state after:
case e_val.e_val.e_a.left
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k✝ : Fin (count p)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
Theorem: Fin.specSubtype
Proof state before:
case e_val.e_val.e_a.left
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k✝ : Fin (count p)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ decodeSubtype (fun i => p i.succ) ⟨↑⟨k, hk⟩, ⋯⟩ = ⟨⟨i, ⋯⟩, hp⟩
Tactic:
simp only [Nat.add_eq, Nat.add_zero, ih]
Proof state after:
case e_val.e_val.e_a.left
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k✝ : Fin (count p)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨k, ⋯⟩
Theorem: Fin.specSubtype
Proof state before:
case e_val.e_val.e_a.left
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k✝ : Fin (count p)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩ = ⟨k, ⋯⟩
Tactic:
apply Fin.eq
Proof state after:
case e_val.e_val.e_a.left.a
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k✝ : Fin (count p)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨k, ⋯⟩
Theorem: Fin.specSubtype
Proof state before:
case e_val.e_val.e_a.left.a
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k✝ : Fin (count p)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨k, ⋯⟩
Tactic:
have h := Fin.val_eq_of_eq h
Proof state after:
case e_val.e_val.e_a.left.a
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k✝ : Fin (count p)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h✝ : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
h : ↑(encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩) = ↑⟨k, hk⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨k, ⋯⟩
Theorem: Fin.specSubtype
Proof state before:
case e_val.e_val.e_a.left.a
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k✝ : Fin (count p)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h✝ : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
h : ↑(encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩) = ↑⟨k, hk⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨k, ⋯⟩
Tactic:
simp only [encodeSubtype, dif_neg h0, val_ndrec] at h
Proof state after:
case e_val.e_val.e_a.left.a
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k✝ : Fin (count p)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h✝ : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
h : ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = k
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨k, ⋯⟩
Theorem: Fin.specSubtype
Proof state before:
case e_val.e_val.e_a.left.a
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k✝ : Fin (count p)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h✝ : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
h : ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = k
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨k, ⋯⟩
Tactic:
cases h
Proof state after:
case e_val.e_val.e_a.left.a.refl
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i✝ : { i // p i }
h0 : ¬p 0
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩), hk⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩), ⋯⟩
Theorem: Fin.specSubtype
Proof state before:
case e_val.e_val.e_a.left.a.refl
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k : Fin (count p)
i✝ : { i // p i }
h0 : ¬p 0
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
hk : ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) < count p
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩), hk⟩
⊢ ↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩) = ↑⟨↑(encodeSubtype (fun i => p i.succ) ⟨⟨i, ⋯⟩, hp⟩), ⋯⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.specSubtype
Proof state before:
case e_val.e_val.e_a.right
n : Nat
ih :
  ∀ (p : Fin n → Prop) [inst : DecidablePred p] (k : Fin (count p)) (i : { i // p i }),
    decodeSubtype p k = i ↔ encodeSubtype p i = k
p : Fin (n + 1) → Prop
inst : DecidablePred p
k✝ : Fin (count p)
i✝ : { i // p i }
h0 : ¬p 0
k : Nat
hk : k < count p
i : Nat
hi : i + 1 < n + 1
hp : p ⟨i + 1, hi⟩
h : encodeSubtype p ⟨⟨i + 1, hi⟩, hp⟩ = ⟨k, hk⟩
⊢ ↑⟨⟨i, ⋯⟩, hp⟩.val = i
Tactic:
rfl
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
⊢ Setoid.r i j → Fin.getRepr s i = Fin.getRepr s j
Tactic:
intro hij
Proof 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
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
⊢ Fin.getRepr s i = Fin.getRepr s j
Tactic:
unfold getRepr
Proof 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 ⋯ ⋯
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
⊢ (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
Proof 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 ⋯ ⋯
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof 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 ..
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'
⊢ (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
Proof 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 ⋯ ⋯
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof 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 ..
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'
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
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'
j' : Fin n
hj' : (Fin.find? fun b => decide (Setoid.r j b)) = some j'
⊢ encodeSubtype (repr s) ⟨i', ⋯⟩ = encodeSubtype (repr s) ⟨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'
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
Proof 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'
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof 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
Proof 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'
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof 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']
Proof 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)
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof 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
Proof 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)
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof 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
Proof 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)
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof 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]
Proof 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
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof 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
Proof 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
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof 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
Proof 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
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof 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
Proof 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
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof 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
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'
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
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'
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
Proof state after:
no goals
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof 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
Proof state after:
no goals
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof 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
Proof 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
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof 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
Proof 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
Theorem: Fin.getRepr_eq_getRepr_of_equiv
Proof 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
Proof state after:
no goals