internlm/Lean-Github huggingface dataset:
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
⊢ decodeSubtype (repr s) k = ⟨j, ⋯⟩
Tactic:
have hij := of_decide_eq_true (Fin.find?_some j hj)
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
hij : Setoid.r i j
⊢ decodeSubtype (repr s) k = ⟨j, ⋯⟩
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
hij : Setoid.r i j
⊢ decodeSubtype (repr s) k = ⟨j, ⋯⟩
Tactic:
apply subtype_eq_of_val_equiv_val
Proof 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
Theorem: Fin.specQuotient
Proof 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
Proof 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
Theorem: Fin.specQuotient
Proof 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
Proof state after:
no goals
Theorem: Fin.specQuotient
Proof 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
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
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ absurd ⋯ ⋯ = k
Tactic:
absurd (Fin.find?_none i hnone)
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
hnone : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ ¬decide (Setoid.r i i) = false
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
hnone : (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
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
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
hnone : (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
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
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
hnone : (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
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
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
hnone : (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.specQuotient
Proof 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
Proof 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
Theorem: Fin.specQuotient
Proof 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
Proof 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
Theorem: Fin.specQuotient
Proof 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
Proof 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
Theorem: Fin.specQuotient
Proof 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
Proof 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
Theorem: Fin.specQuotient
Proof 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
Proof 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
Theorem: Fin.specQuotient
Proof 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
Proof 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
Theorem: Fin.specQuotient
Proof 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 ..
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 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
Proof 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
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 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]
Proof 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
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 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
Proof 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
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 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
Proof 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
Theorem: Fin.specQuotient
Proof 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
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 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)
Proof 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
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 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]
Proof 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
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 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
Proof 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
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 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
Proof 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
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 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 ..
Proof state after:
no goals
Theorem: Set.subset_refl
Proof state before:
α : Sort u_1
s✝ t u s : Set α
⊢ s.Subset s
Tactic:
intro x hs
Proof state after:
α : Sort u_1
s✝ t u s : Set α
x : α
hs : x ∈ s
⊢ x ∈ s
Theorem: Set.subset_refl
Proof state before:
α : Sort u_1
s✝ t u s : Set α
x : α
hs : x ∈ s
⊢ x ∈ s
Tactic:
exact hs
Proof state after:
no goals
Theorem: Set.subset_trans
Proof state before:
α : Sort u_1
s t u : Set α
⊢ s.Subset t → t.Subset u → s.Subset u
Tactic:
intro hst htu x hs
Proof state after:
α : Sort u_1
s t u : Set α
hst : s.Subset t
htu : t.Subset u
x : α
hs : x ∈ s
⊢ x ∈ u
Theorem: Set.subset_trans
Proof state before:
α : Sort u_1
s t u : Set α
hst : s.Subset t
htu : t.Subset u
x : α
hs : x ∈ s
⊢ x ∈ u
Tactic:
apply htu
Proof state after:
case a
α : Sort u_1
s t u : Set α
hst : s.Subset t
htu : t.Subset u
x : α
hs : x ∈ s
⊢ x ∈ t
Theorem: Set.subset_trans
Proof state before:
case a
α : Sort u_1
s t u : Set α
hst : s.Subset t
htu : t.Subset u
x : α
hs : x ∈ s
⊢ x ∈ t
Tactic:
apply hst
Proof state after:
case a.a
α : Sort u_1
s t u : Set α
hst : s.Subset t
htu : t.Subset u
x : α
hs : x ∈ s
⊢ x ∈ s
Theorem: Set.subset_trans
Proof state before:
case a.a
α : Sort u_1
s t u : Set α
hst : s.Subset t
htu : t.Subset u
x : α
hs : x ∈ s
⊢ x ∈ s
Tactic:
exact hs
Proof state after:
no goals
Theorem: Set.subset_antisymm
Proof state before:
α : Sort u_1
s t u : Set α
⊢ s.Subset t → t.Subset s → s = t
Tactic:
intro hst hts
Proof state after:
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
⊢ s = t
Theorem: Set.subset_antisymm
Proof state before:
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
⊢ s = t
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
⊢ ∀ (x : α), x ∈ s ↔ x ∈ t
Theorem: Set.subset_antisymm
Proof state before:
case a
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
⊢ ∀ (x : α), x ∈ s ↔ x ∈ t
Tactic:
intro x
Proof state after:
case a
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
x : α
⊢ x ∈ s ↔ x ∈ t
Theorem: Set.subset_antisymm
Proof state before:
case a
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
x : α
⊢ x ∈ s ↔ x ∈ t
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
x : α
⊢ x ∈ s → x ∈ t

case a.mpr
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
x : α
⊢ x ∈ t → x ∈ s
Theorem: Set.subset_antisymm
Proof state before:
case a.mp
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
x : α
⊢ x ∈ s → x ∈ t
Tactic:
exact hst x
Proof state after:
no goals
Theorem: Set.subset_antisymm
Proof state before:
case a.mpr
α : Sort u_1
s t u : Set α
hst : s.Subset t
hts : t.Subset s
x : α
⊢ x ∈ t → x ∈ s
Tactic:
exact hts x
Proof state after:
no goals
Theorem: Set.empty_subset
Proof state before:
α : Sort u_1
s✝ t u s : Set α
⊢ Set.empty.Subset s
Tactic:
intro x h
Proof state after:
α : Sort u_1
s✝ t u s : Set α
x : α
h : x ∈ Set.empty
⊢ x ∈ s
Theorem: Set.empty_subset
Proof state before:
α : Sort u_1
s✝ t u s : Set α
x : α
h : x ∈ Set.empty
⊢ x ∈ s
Tactic:
contradiction
Proof state after:
no goals
Theorem: Set.eq_empty_of_subset_empty
Proof state before:
α : Sort u_1
s t u : Set α
⊢ s.Subset Set.empty → s = Set.empty
Tactic:
intro hs
Proof state after:
α : Sort u_1
s t u : Set α
hs : s.Subset Set.empty
⊢ s = Set.empty
Theorem: Set.eq_empty_of_subset_empty
Proof state before:
α : Sort u_1
s t u : Set α
hs : s.Subset Set.empty
⊢ s = Set.empty
Tactic:
antisymmetry using (.⊆.)
Proof state after:
case a
α : Sort u_1
s t u : Set α
hs : s.Subset Set.empty
⊢ s.Subset Set.empty

case a
α : Sort u_1
s t u : Set α
hs : s.Subset Set.empty
⊢ Set.empty.Subset s
Theorem: Set.eq_empty_of_subset_empty
Proof state before:
case a
α : Sort u_1
s t u : Set α
hs : s.Subset Set.empty
⊢ s.Subset Set.empty
Tactic:
exact hs
Proof state after:
no goals
Theorem: Set.eq_empty_of_subset_empty
Proof state before:
case a
α : Sort u_1
s t u : Set α
hs : s.Subset Set.empty
⊢ Set.empty.Subset s
Tactic:
exact empty_subset s
Proof state after:
no goals
Theorem: Set.subset_univ
Proof state before:
α : Sort u_1
s✝ t u s : Set α
⊢ s.Subset Set.univ
Tactic:
intro _ _
Proof state after:
α : Sort u_1
s✝ t u s : Set α
x✝ : α
a✝ : x✝ ∈ s
⊢ x✝ ∈ Set.univ
Theorem: Set.subset_univ
Proof state before:
α : Sort u_1
s✝ t u s : Set α
x✝ : α
a✝ : x✝ ∈ s
⊢ x✝ ∈ Set.univ
Tactic:
trivial
Proof state after:
no goals
Theorem: Set.eq_univ_of_univ_subset
Proof state before:
α : Sort u_1
s t u : Set α
⊢ Set.univ.Subset s → s = Set.univ
Tactic:
intro hs
Proof state after:
α : Sort u_1
s t u : Set α
hs : Set.univ.Subset s
⊢ s = Set.univ
Theorem: Set.eq_univ_of_univ_subset
Proof state before:
α : Sort u_1
s t u : Set α
hs : Set.univ.Subset s
⊢ s = Set.univ
Tactic:
antisymmetry using (.⊆.)
Proof state after:
case a
α : Sort u_1
s t u : Set α
hs : Set.univ.Subset s
⊢ s.Subset Set.univ

case a
α : Sort u_1
s t u : Set α
hs : Set.univ.Subset s
⊢ Set.univ.Subset s
Theorem: Set.eq_univ_of_univ_subset
Proof state before:
case a
α : Sort u_1
s t u : Set α
hs : Set.univ.Subset s
⊢ s.Subset Set.univ
Tactic:
exact subset_univ s
Proof state after:
no goals
Theorem: Set.eq_univ_of_univ_subset
Proof state before:
case a
α : Sort u_1
s t u : Set α
hs : Set.univ.Subset s
⊢ Set.univ.Subset s
Tactic:
exact hs
Proof state after:
no goals
Theorem: Set.pure_subset_of_mem
Proof state before:
α : Type u_1
s t u : Set α
x : α
⊢ x ∈ s → (pure x).Subset s
Tactic:
intro | hs, _, rfl => exact hs
Proof state after:
no goals
Theorem: Set.pure_subset_of_mem
Proof state before:
α : Type u_1
s t u : Set α
x : α
x✝² : x ∈ s
x✝¹ : α
x✝ : x✝¹ ∈ pure x
hs : x ∈ s
⊢ x ∈ s
Tactic:
exact hs
Proof state after:
no goals
Theorem: Set.subset_union_left
Proof state before:
α : Sort u_1
s✝ t✝ u s t : Set α
⊢ s.Subset (s.union t)
Tactic:
intro x hs
Proof state after:
α : Sort u_1
s✝ t✝ u s t : Set α
x : α
hs : x ∈ s
⊢ x ∈ s.union t
Theorem: Set.subset_union_left
Proof state before:
α : Sort u_1
s✝ t✝ u s t : Set α
x : α
hs : x ∈ s
⊢ x ∈ s.union t
Tactic:
left
Proof state after:
case h
α : Sort u_1
s✝ t✝ u s t : Set α
x : α
hs : x ∈ s
⊢ x ∈ s
Theorem: Set.subset_union_left
Proof state before:
case h
α : Sort u_1
s✝ t✝ u s t : Set α
x : α
hs : x ∈ s
⊢ x ∈ s
Tactic:
exact hs
Proof state after:
no goals
Theorem: Set.subset_union_right
Proof state before:
α : Sort u_1
s✝ t✝ u s t : Set α
⊢ t.Subset (s.union t)
Tactic:
intro x ht
Proof state after:
α : Sort u_1
s✝ t✝ u s t : Set α
x : α
ht : x ∈ t
⊢ x ∈ s.union t
Theorem: Set.subset_union_right
Proof state before:
α : Sort u_1
s✝ t✝ u s t : Set α
x : α
ht : x ∈ t
⊢ x ∈ s.union t
Tactic:
right
Proof state after:
case h
α : Sort u_1
s✝ t✝ u s t : Set α
x : α
ht : x ∈ t
⊢ x ∈ t
Theorem: Set.subset_union_right
Proof state before:
case h
α : Sort u_1
s✝ t✝ u s t : Set α
x : α
ht : x ∈ t
⊢ x ∈ t
Tactic:
exact ht
Proof state after:
no goals
Theorem: Set.union_subset_of_subset_of_subset
Proof state before:
α : Sort u_1
s t u : Set α
⊢ s.Subset u → t.Subset u → (s.union t).Subset u
Tactic:
intro hsu htu x
Proof state after:
α : Sort u_1
s t u : Set α
hsu : s.Subset u
htu : t.Subset u
x : α
⊢ x ∈ s.union t → x ∈ u
Theorem: Set.union_subset_of_subset_of_subset
Proof state before:
α : Sort u_1
s t u : Set α
hsu : s.Subset u
htu : t.Subset u
x : α
⊢ x ∈ s.union t → x ∈ u
Tactic:
intro
| Or.inl hxs =>
  exact hsu x hxs
| Or.inr hxt =>
  exact htu x hxt
Proof state after:
no goals
Theorem: Set.union_subset_of_subset_of_subset
Proof state before:
α : Sort u_1
s t u : Set α
hsu : s.Subset u
htu : t.Subset u
x : α
x✝ : x ∈ s.union t
hxs : x ∈ s
⊢ x ∈ u
Tactic:
exact hsu x hxs
Proof state after:
no goals