awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
false :
  (∃ (a : α),
      Membership.mem (γ := Option (α ⊕ β))
          (match (motive := Bool → ℕ → Option (α ⊕ β)) Bool.false, n.div2 with
            | Bool.false, m => some (Sum.inl (ofNat α m))
            | x, m => some (Sum.inr (ofNat β m)) :
            Option (α ⊕ β))
          (Sum.inl a) ∧
        encodeSum.{u_1, u_2} (β := β) (Sum.inl a) = bit Bool.false n.div2) ∨
    ∃ (b : β),
      Membership.mem (γ := Option (α ⊕ β))
          (match (motive := Bool → ℕ → Option (α ⊕ β)) Bool.false, n.div2 with
            | Bool.false, m => some (Sum.inl (ofNat α m))
            | x, m => some (Sum.inr (ofNat β m)) :
            Option (α ⊕ β))
          (Sum.inr b) ∧
        encodeSum.{u_1, u_2} (α := α) (Sum.inr b) = bit Bool.false n.div2
true :
  (∃ (a : α),
      Membership.mem (γ := Option (α ⊕ β))
          (match (motive := Bool → ℕ → Option (α ⊕ β)) Bool.true, n.div2 with
            | Bool.false, m => some (Sum.inl (ofNat α m))
            | x, m => some (Sum.inr (ofNat β m)) :
            Option (α ⊕ β))
          (Sum.inl a) ∧
        encodeSum.{u_1, u_2} (β := β) (Sum.inl a) = bit Bool.true n.div2) ∨
    ∃ (b : β),
      Membership.mem (γ := Option (α ⊕ β))
          (match (motive := Bool → ℕ → Option (α ⊕ β)) Bool.true, n.div2 with
            | Bool.false, m => some (Sum.inl (ofNat α m))
            | x, m => some (Sum.inr (ofNat β m)) :
            Option (α ⊕ β))
          (Sum.inr b) ∧
        encodeSum.{u_1, u_2} (α := α) (Sum.inr b) = bit Bool.true n.div2
⊢ (∃ (a : α),
      Membership.mem (γ := Option (α ⊕ β))
          (match (motive := Bool → ℕ → Option (α ⊕ β)) n.bodd, n.div2 with
            | Bool.false, m => some (Sum.inl (ofNat α m))
            | x, m => some (Sum.inr (ofNat β m)) :
            Option (α ⊕ β))
          (Sum.inl a) ∧
        encodeSum.{u_1, u_2} (β := β) (Sum.inl a) = bit n.bodd n.div2) ∨
    ∃ (b : β),
      Membership.mem (γ := Option (α ⊕ β))
          (match (motive := Bool → ℕ → Option (α ⊕ β)) n.bodd, n.div2 with
            | Bool.false, m => some (Sum.inl (ofNat α m))
            | x, m => some (Sum.inr (ofNat β m)) :
            Option (α ⊕ β))
          (Sum.inr b) ∧
        encodeSum.{u_1, u_2} (α := α) (Sum.inr b) = bit n.bodd n.div2

Tactic:
cases bodd n

Premises used: Nat.bodd
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
⊢ (∃ (a : α),
      Membership.mem (γ := Option (α ⊕ β))
          (match (motive := Bool → ℕ → Option (α ⊕ β)) false, n.div2 with
            | false, m => some (Sum.inl (ofNat α m))
            | x, m => some (Sum.inr (ofNat β m)) :
            Option (α ⊕ β))
          (Sum.inl a) ∧
        encodeSum.{u_1, u_2} (β := β) (Sum.inl a) = bit false n.div2) ∨
    ∃ (b : β),
      Membership.mem (γ := Option (α ⊕ β))
          (match (motive := Bool → ℕ → Option (α ⊕ β)) false, n.div2 with
            | false, m => some (Sum.inl (ofNat α m))
            | x, m => some (Sum.inr (ofNat β m)) :
            Option (α ⊕ β))
          (Sum.inr b) ∧
        encodeSum.{u_1, u_2} (α := α) (Sum.inr b) = bit false n.div2

Tactic:
simp [bit_val, encodeSum]

Premises used: Nat.bit_val, Encodable.encodeSum
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
⊢ (∃ (a : α),
      Membership.mem (γ := Option (α ⊕ β))
          (match (motive := Bool → ℕ → Option (α ⊕ β)) true, n.div2 with
            | false, m => some (Sum.inl (ofNat α m))
            | x, m => some (Sum.inr (ofNat β m)) :
            Option (α ⊕ β))
          (Sum.inl a) ∧
        encodeSum.{u_1, u_2} (β := β) (Sum.inl a) = bit true n.div2) ∨
    ∃ (b : β),
      Membership.mem (γ := Option (α ⊕ β))
          (match (motive := Bool → ℕ → Option (α ⊕ β)) true, n.div2 with
            | false, m => some (Sum.inl (ofNat α m))
            | x, m => some (Sum.inr (ofNat β m)) :
            Option (α ⊕ β))
          (Sum.inr b) ∧
        encodeSum.{u_1, u_2} (α := α) (Sum.inr b) = bit true n.div2

Tactic:
simp [bit_val, encodeSum]

Premises used: Nat.bit_val, Encodable.encodeSum
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
γ : α → Type u_3
inst_2 : (a : α) → Denumerable (γ a)
n : ℕ
⊢ ∃ (a : Sigma γ), Membership.mem (γ := Option (Sigma γ)) (decode n) a ∧ encode a = n

Tactic:
simp
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
inst : Denumerable α
γ : α → Type u_3
inst_1 : (a : α) → Denumerable (γ a)
n : ℕ
rw :
  Eq (α := Option (Sigma γ))
    (Option.bind (decode (unpair n).1) fun (a : α) ↦ Option.map (Sigma.mk (β := γ) a) (decode (unpair n).2))
    (some (Sigma.mk (β := γ) (ofNat α (unpair n).1) (ofNat (γ (ofNat α (unpair n).1)) (unpair n).2)))
⊢ Eq (α := Option (Sigma γ)) (some (ofNat (Sigma γ) n))
    (some (Sigma.mk (β := γ) (ofNat α (unpair n).1) (ofNat (γ (ofNat α (unpair n).1)) (unpair n).2)))

Tactic:
rw [← decode_eq_ofNat, decode_sigma_val]

Premises used: Encodable.decode_sigma_val, Denumerable.decode_eq_ofNat
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
inst : Denumerable α
γ : α → Type u_3
inst_1 : (a : α) → Denumerable (γ a)
n : ℕ
⊢ Eq (α := Option (Sigma γ))
    (Option.bind (decode (unpair n).1) fun (a : α) ↦ Option.map (Sigma.mk (β := γ) a) (decode (unpair n).2))
    (some (Sigma.mk (β := γ) (ofNat α (unpair n).1) (ofNat (γ (ofNat α (unpair n).1)) (unpair n).2)))

Tactic:
simp
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
⊢ ofNat (α × β) n = (ofNat α (unpair n).1, ofNat β (unpair n).2)

Tactic:
simp
-- Module: Mathlib.Logic.Denumerable
Goal:
h : ∀ (x : ℕ), ofNat (ℕ × ℕ) x = unpair x
⊢ ofNat (ℕ × ℕ) = unpair

Tactic:
funext
-- Module: Mathlib.Logic.Denumerable
Goal:
x : ℕ
⊢ ofNat (ℕ × ℕ) x = unpair x

Tactic:
simp
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
x : (↑s : Type)
by_contra : ∀ (h : ¬∃ (n : ℕ), (↑x : ℕ) + n + 1 ∈ s), False
⊢ ∃ (n : ℕ), (↑x : ℕ) + n + 1 ∈ s

Tactic:
by_contra h
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
x : (↑s : Type)
h : ¬∃ (n : ℕ), (↑x : ℕ) + n + 1 ∈ s
a : ℕ
ha : a ∈ s
hax : (↑x : ℕ) + 1 ≤ a
rwa : (↑x : ℕ) + 1 + (a - ((↑x : ℕ) + 1)) ∈ s
rwa₁ rwa₂ rwa₃ rwa₄ : a ∈ s
⊢ (↑x : ℕ) + (a - ((↑x : ℕ) + 1)) + 1 ∈ s

Tactic:
rwa [Nat.add_right_comm, Nat.add_sub_cancel' hax]

Premises used: Nat.add_sub_cancel', Nat.add_right_comm
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
x : (↑s : Type)
h : ¬∃ (n : ℕ), (↑x : ℕ) + n + 1 ∈ s
⊢ ∀ (a : ℕ) (ha : a ∈ s), a < (↑x : ℕ) + 1

Tactic:
have (a : ℕ) (ha : a ∈ s) : a < x + 1 :=
    lt_of_not_ge fun hax => h ⟨a - (x + 1), by rwa [Nat.add_right_comm, Nat.add_sub_cancel' hax]⟩
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
x : (↑s : Type)
h : ¬∃ (n : ℕ), (↑x : ℕ) + n + 1 ∈ s
this : ∀ (a : ℕ) (ha : a ∈ s), a < (↑x : ℕ) + 1
⊢ ∀ a ∈ Multiset.filter (fun (x : ℕ) ↦ x ∈ s) (Multiset.range (↑x : ℕ).succ), a ∈ s

Tactic:
simp [-Multiset.range_succ]

Premises used: Multiset.range_succ
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
x : (↑s : Type)
h : ¬∃ (n : ℕ), (↑x : ℕ) + n + 1 ∈ s
this : ∀ (a : ℕ) (ha : a ∈ s), a < (↑x : ℕ) + 1
⊢ ∀ (x_1 : Subtype (Membership.mem s)),
    Membership.mem (γ := Finset (Subtype (Membership.mem s)))
      (Multiset.toFinset
        (Multiset.pmap (p := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := Membership.mem s) y hy)
          (Multiset.filter (fun (x : ℕ) ↦ x ∈ s) (Multiset.range (↑x : ℕ).succ)) ⋯))
      x_1

Tactic:
simpa [Subtype.ext_iff, Multiset.mem_filter, -Multiset.range_succ]

Premises used: Subtype.ext_iff, Multiset.mem_filter, Multiset.range_succ
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
x : (↑s : Type)
h : ¬∃ (n : ℕ), (↑x : ℕ) + n + 1 ∈ s
this : ∀ (a : ℕ) (ha : a ∈ s), a < (↑x : ℕ) + 1
⊢ False

Tactic:
exact Fintype.false
    ⟨(((Multiset.range (succ x)).filter (· ∈ s)).pmap
      (fun (y : ℕ) (hy : y ∈ s) => Subtype.mk y hy) (by simp [-Multiset.range_succ])).toFinset,
      by simpa [Subtype.ext_iff, Multiset.mem_filter, -Multiset.range_succ] ⟩

Premises used: Multiset.toFinset, Membership.mem, Fintype.false, Subtype.mk, Multiset.pmap, Fintype.mk, Multiset.range, Subtype.val, Nat.succ, Multiset.filter
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
x : (↑s : Type)
h : ¬∃ (n : ℕ), (↑x : ℕ) + n + 1 ∈ s
this : ∀ (a : ℕ) (ha : a ∈ s), a < (↑x : ℕ) + 1
⊢ False

Tactic:
classical
  exact Fintype.false
    ⟨(((Multiset.range (succ x)).filter (· ∈ s)).pmap
      (fun (y : ℕ) (hy : y ∈ s) => Subtype.mk y hy) (by simp [-Multiset.range_succ])).toFinset,
      by simpa [Subtype.ext_iff, Multiset.mem_filter, -Multiset.range_succ] ⟩
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x y : (↑s : Type)
h : y < x
hx : ∃ (m : ℕ), (↑y : ℕ) + m + 1 ∈ s
k : ℕ
hk : (↑x : ℕ) = (↑y : ℕ) + k + 1
this : Nat.find (p := fun (n : ℕ) ↦ (↑y : ℕ) + n + 1 ∈ s) hx ≤ k
⊢ (↑y : ℕ) + Nat.find (p := fun (n : ℕ) ↦ (↑y : ℕ) + n + 1 ∈ s) hx + 1 ≤ (↑x : ℕ)

Tactic:
lia
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x y : (↑s : Type)
h : ∀ z < x, z ≤ y
hx : ∃ (m : ℕ), (↑y : ℕ) + m + 1 ∈ s
hxy : (↑y : ℕ) + Nat.find (p := fun (n : ℕ) ↦ (↑y : ℕ) + n + 1 ∈ s) hx + 1 < (↑x : ℕ)
⊢ (↑y : ℕ) < (↑y : ℕ) + Nat.find (p := fun (n : ℕ) ↦ (↑y : ℕ) + n + 1 ∈ s) hx + 1

Tactic:
lia
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : (↑s : Type)
⊢ x < succ (s := s) x

Tactic:
calc
    (x : ℕ) ≤ (x + _) := le_add_right ..
    _ < (succ x) := Nat.lt_succ_self (x + _)

Premises used: Trans.trans, Nat.le_add_right, Nat.lt_succ_self, HAdd.hAdd, Subtype.val
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x y : (↑s : Type)
⊢ x < succ (s := s) y ↔ x ≤ y

Tactic:
⟨fun h => le_of_not_gt fun h' => not_le_of_gt h (succ_le_of_lt h'), fun h =>
    lt_of_le_of_lt h (lt_succ_self _)⟩

Premises used: lt_of_le_of_lt, le_of_not_gt, Nat.Subtype.lt_succ_self, Iff.intro, not_le_of_gt, Nat.Subtype.succ_le_of_lt
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
a : ℕ
ha : a ∈ List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)
⊢ a ∈ s

Tactic:
simpa using (List.mem_filter.mp ha).2

Premises used: And.right, List.mem_filter, Iff.mp
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
⊢ let t : List (↑s : Type) :=
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯;
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯

Tactic:
set t : List s :=
      ((List.range x).filter fun y => y ∈ s).pmap
        (fun (y : ℕ) (hy : y ∈ s) => ⟨y, hy⟩)
        (by intro a ha; simpa using (List.mem_filter.mp ha).2) with ht

Premises used: Membership.mem, Set.Elem, List.range, List.pmap, List, List.filter, Decidable.decide
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
⊢ ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx

Tactic:
simp [List.mem_filter, Subtype.ext_iff, ht]

Premises used: Subtype.ext_iff, List.mem_filter
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
⊢ ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx

Tactic:
have hmt : ∀ {y : s}, y ∈ t ↔ y < ⟨x, hx⟩ := by
      simp [List.mem_filter, Subtype.ext_iff, ht]
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
hmax : t.maximum = ⊥
⊢ ∃ (a : ℕ), ofNat s a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx

Tactic:
⟨0, le_antisymm bot_le (le_of_not_gt fun h => List.not_mem_nil (a := (⊥ : s)) ?_)⟩

Premises used: le_of_not_gt, le_antisymm, Exists.intro, OfNat.ofNat, bot_le, List.not_mem_nil
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
hmax : t.maximum = ⊥
bot : ∀ (h : ofNat s 0 < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx), Membership.mem (γ := List (↑s : Type)) [] ⊥
⊢ ∃ (a : ℕ), ofNat s a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx

Tactic:
refine ⟨0, le_antisymm bot_le (le_of_not_gt fun h => List.not_mem_nil (a := (⊥ : s)) ?_)⟩
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
hmax : t.maximum = ⊥
h : ofNat s 0 < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
bot : ⊥ ∈ t
bot₁ bot₂ bot₃ bot₄ : ⊥ < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
⊢ Membership.mem (γ := List (↑s : Type)) [] ⊥

Tactic:
rwa [← List.maximum_eq_bot.1 hmax, hmt]

Premises used: List.maximum_eq_bot, Iff.mp
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
m : (↑s : Type)
hmax : t.maximum = (↑m : WithBot (↑s : Type))
⊢ (↑m : ℕ) < x

Tactic:
simpa using hmt.mp (List.maximum_mem hmax)

Premises used: Iff.mp, List.maximum_mem
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
m : (↑s : Type)
hmax : t.maximum = (↑m : WithBot (↑s : Type))
⊢ (↑m : ℕ) < x

Tactic:
have wf : ↑m < x := by simpa using hmt.mp (List.maximum_mem hmax)
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
m : (↑s : Type)
hmax : t.maximum = (↑m : WithBot (↑s : Type))
wf : (↑m : ℕ) < x
coe :
  ∀ (a : ℕ) (hmax : t.maximum = (↑(ofNat s a) : WithBot (↑s : Type))) (wf : (↑(ofNat s a) : ℕ) < x),
    ∃ (a : ℕ), ofNat s a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
⊢ ∃ (a : ℕ), ofNat s a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx

Tactic:
rcases ofNat_surjective m with ⟨a, rfl⟩

Premises used: rfl
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
a : ℕ
hmax : t.maximum = (↑(ofNat s a) : WithBot (↑s : Type))
wf : (↑(ofNat s a) : ℕ) < x
⊢ ∃ (a : ℕ), ofNat s a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx

Tactic:
⟨a + 1, le_antisymm (succ_le_of_lt wf) ?_⟩

Premises used: le_antisymm, HAdd.hAdd, Exists.intro, Nat.Subtype.succ_le_of_lt, OfNat.ofNat
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
a : ℕ
hmax : t.maximum = (↑(ofNat s a) : WithBot (↑s : Type))
wf : (↑(ofNat s a) : ℕ) < x
coe : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx ≤ ofNat s (a + 1)
⊢ ∃ (a : ℕ), ofNat s a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx

Tactic:
refine ⟨a + 1, le_antisymm (succ_le_of_lt wf) ?_⟩
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
a : ℕ
hmax : t.maximum = (↑(ofNat s a) : WithBot (↑s : Type))
wf : (↑(ofNat s a) : ℕ) < x
⊢ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx ≤ ofNat s (a + 1)

Tactic:
le_succ_of_forall_lt_le fun z hz => List.le_maximum_of_mem (hmt.2 hz) hmax

Premises used: Iff.mpr, List.le_maximum_of_mem, Nat.Subtype.le_succ_of_forall_lt_le
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
a : ℕ
hmax : t.maximum = (↑(ofNat s a) : WithBot (↑s : Type))
wf : (↑(ofNat s a) : ℕ) < x
⊢ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx ≤ ofNat s (a + 1)

Tactic:
exact le_succ_of_forall_lt_le fun z hz => List.le_maximum_of_mem (hmt.2 hz) hmax

Premises used: Iff.mpr, List.le_maximum_of_mem, Nat.Subtype.le_succ_of_forall_lt_le
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List (↑s : Type) :=
  List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
    (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
ht :
  t =
    List.pmap (P := Membership.mem s) (fun (y : ℕ) (hy : y ∈ s) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) y hy)
      (List.filter (fun (y : ℕ) ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : (↑s : Type)}, y ∈ t ↔ y < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
cases :
  ∀ (x_1 : WithBot (↑s : Type)) (hmax : t.maximum = x_1),
    ∃ (a : ℕ), ofNat s a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
⊢ ∃ (a : ℕ), ofNat s a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx

Tactic:
cases hmax : List.maximum t with
    | bot =>
      refine ⟨0, le_antisymm bot_le (le_of_not_gt fun h => List.not_mem_nil (a := (⊥ : s)) ?_)⟩
      rwa [← List.maximum_eq_bot.1 hmax, hmt]
    | coe m =>
      have wf : ↑m < x := by simpa using hmt.mp (List.maximum_mem hmax)
      rcases ofNat_surjective m with ⟨a, rfl⟩
      refine ⟨a + 1, le_antisymm (succ_le_of_lt wf) ?_⟩
      exact le_succ_of_forall_lt_le fun z hz => List.le_maximum_of_mem (hmt.2 hz) hmax

Premises used: List.maximum, rfl
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
⊢ Set.range (ofNat s) = Set.univ

Tactic:
ofNat_surjective.range_eq

Premises used: Function.Surjective.range_eq, Nat.Subtype.ofNat_surjective
-- Module: Mathlib.Logic.Denumerable
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
rw : Subtype.val (p := fun (x : ℕ) ↦ x ∈ s) '' Set.range (ofNat s) = s
rw₁ : Set.image (α := { x : ℕ // x ∈ s }) (Subtype.val (p := fun (x : ℕ) ↦ x ∈ s)) Set.univ = s
rw₂ : Set.range (ι := { x : ℕ // x ∈ s }) (Subtype.val (p := fun (x : ℕ) ↦ x ∈ s)) = s
rw₃ rw₄ : s = s
⊢ Set.range (Subtype.val (p := fun (x : ℕ) ↦ x ∈ s) ∘ ofNat s) = s

Tactic:
rw [Set.range_comp Subtype.val, ofNat_range, Set.image_univ, Subtype.range_coe]

Premises used: Set.range_comp, Set.image_univ, Subtype.range_coe, Nat.Subtype.ofNat_range, Subtype.val