awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
P : Prop
inst : Decidable P
Q : P → Prop
R : ¬P → Prop
pos : ∀ (h : P), dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h
have neg : ∀ (h : ¬P), dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h
Tactic: by_cases h : P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_3
β : Sort u_4
p : β → Prop
inst : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
h_1 : Eq.{u_3} (α := α) ((fun (x : β) ↦ if p x then g x else f x) x) ((fun (x : β) ↦ if p x then g x else f x) y)
⊢ x = y
have inl : ∀ (hx : p x), x = y
Tactic: rcases em (p x) with (hx | hx)
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_3
β : Sort u_4
p : β → Prop
inst : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
h_1 : Eq.{u_3} (α := α) ((fun (x : β) ↦ if p x then g x else f x) x) ((fun (x : β) ↦ if p x then g x else f x) y)
inl : ∀ (hx : p x), x = y
⊢ x = y
have inr : ∀ (hx : ¬p x), x = y
Tactic: rcases em (p x) with (hx | hx)
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_3
β : Sort u_4
p : β → Prop
inst : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
h_1 : Eq.{u_3} (α := α) ((fun (x : β) ↦ if p x then g x else f x) x) ((fun (x : β) ↦ if p x then g x else f x) y)
hx : p x
⊢ x = y
have inl : ∀ (hy : p y), x = y
Tactic: rcases em (p y) with (hy | hy)
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_3
β : Sort u_4
p : β → Prop
inst : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
h_1 : Eq.{u_3} (α := α) ((fun (x : β) ↦ if p x then g x else f x) x) ((fun (x : β) ↦ if p x then g x else f x) y)
hx : p x
inl : ∀ (hy : p y), x = y
⊢ x = y
have inl₁ : ∀ (hy : ¬p y), x = y
Tactic: rcases em (p y) with (hy | hy)
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_3
β : Sort u_4
p : β → Prop
inst : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
h_1 : Eq.{u_3} (α := α) ((fun (x : β) ↦ if p x then g x else f x) x) ((fun (x : β) ↦ if p x then g x else f x) y)
hx : ¬p x
⊢ x = y
have inr : ∀ (hy : p y), x = y
Tactic: rcases em (p y) with (hy | hy)
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_3
β : Sort u_4
p : β → Prop
inst : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
h_1 : Eq.{u_3} (α := α) ((fun (x : β) ↦ if p x then g x else f x) x) ((fun (x : β) ↦ if p x then g x else f x) y)
hx : ¬p x
inr : ∀ (hy : p y), x = y
⊢ x = y
have inr₁ : ∀ (hy : ¬p y), x = y
Tactic: rcases em (p y) with (hy | hy)
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Membership α β
p : Prop
inst_1 : Decidable p
a : α
s : p → β
t : ¬p → β
⊢ Membership.mem.{u_1, u_2} (γ := β) (if h : p then s h else t h) a ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h
have pos : ∀ (h : p),
  Membership.mem.{u_1, u_2} (γ := β) (if h : p then s h else t h) a ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h
Tactic: by_cases h : p
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Membership α β
p : Prop
inst_1 : Decidable p
a : α
s : p → β
t : ¬p → β
pos :
  ∀ (h : p),
    Membership.mem.{u_1, u_2} (γ := β) (if h : p then s h else t h) a ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h
⊢ Membership.mem.{u_1, u_2} (γ := β) (if h : p then s h else t h) a ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h
have neg : ∀ (h : ¬p),
  Membership.mem.{u_1, u_2} (γ := β) (if h : p then s h else t h) a ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h
Tactic: by_cases h : p
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Membership α β
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
s : β
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s
have pos : ∀ (h : p), (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s
Tactic: by_cases h : p
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Membership α β
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
s : β
pos : ∀ (h : p), (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s
have neg : ∀ (h : ¬p), (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s
Tactic: by_cases h : p
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁ == a₂) = (b₁ == b₂) ↔ (a₁ = a₂ ↔ b₁ = b₂)
have rw : ((a₁ == a₂) = true ↔ (b₁ == b₂) = true) ↔ (a₁ = a₂ ↔ b₁ = b₂)
Tactic: rw [Bool.eq_iff_iff]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Type u_1
inst1 inst2 : BEq α
h : ∀ (x y : α), (x == y) = (x == y)
⊢ inst1 = inst2
have have : ∀ (beq1 : α → α → Bool) (h : ∀ (x y : α), (x == y) = (x == y)), { beq := beq1 : BEq α } = inst2
Tactic: have ⟨beq1⟩ := inst1
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Type u_1
inst1 inst2 : BEq α
beq1 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
⊢ { beq := beq1 : BEq α } = inst2
have e_beq : beq1 = BEq.beq
Tactic: congr
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Type u_1
inst1 inst2 : BEq α
beq1 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
⊢ beq1 = BEq.beq
have e_beq : ∀ (x y : α), beq1 x y = (x == y)
Tactic: funext x y
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Type u_1
inst1 inst2 : BEq α
inst : LawfulBEq α
inst_1 : LawfulBEq α
⊢ inst1 = inst2
have h : ∀ (x y : α), (x == y) = (x == y)
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
inst : Denumerable α
n : ℕ
⊢ encode (ofNat α n) = n
have obtain : ∀ (a : α) (h : Membership.mem (γ := Option α) (decode n) a) (e : encode a = n), encode (ofNat α n) = n
Tactic: obtain ⟨a, h, e⟩ := decode_inv (α := α) n
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ ofNat β n = (e.symm : (a : α) → β) (ofNat α n)
have refine : Eq.{u_4 + 1} (α := Option β) (decode n : Option β) (some ((e.symm : (a : α) → β) (ofNat α n)) : Option β)
Tactic: refine ofNat_of_decode ?_
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ Eq.{u_4 + 1} (α := Option β) (decode n : Option β) (some ((e.symm : (a : α) → β) (ofNat α n)) : Option β)
have rw : Eq.{u_4 + 1} (α := Option β) (Option.map.{u_3, u_4} (α := α) (⇑e.symm : (a : α) → β) (decode n) : Option β)
  (some ((e.symm : (a : α) → β) (ofNat α n)) : Option β)
Tactic: rw [decode_ofEquiv e]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
⊢ ∃ (a : Option α), Membership.mem (γ := Option (Option α)) (decode 0) a ∧ encode a = 0
have zero : Membership.mem (γ := Option (Option α)) (decode 0) none
Tactic: refine ⟨none, ?_, encode_none⟩
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
⊢ Membership.mem (γ := Option (Option α)) (decode 0) none
have zero : Membership.mem (γ := Option (Option α)) (some none) none
Tactic: rw [decode_option_zero, Option.mem_def]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
zero : Membership.mem (γ := Option (Option α)) (some none) none
⊢ Membership.mem (γ := Option (Option α)) (decode 0) none
have zero₁ : Eq.{u_1 + 1} (α := Option (Option α)) (some none) (some none)
Tactic: rw [decode_option_zero, Option.mem_def]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
⊢ ∃ (a : Option α), Membership.mem (γ := Option (Option α)) (decode (n + 1)) a ∧ encode a = n + 1
have succ : Membership.mem (γ := Option (Option α)) (decode (n + 1)) (some (ofNat α n))
Tactic: refine ⟨some (ofNat α n), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
succ : Membership.mem (γ := Option (Option α)) (decode (n + 1)) (some (ofNat α n))
⊢ ∃ (a : Option α), Membership.mem (γ := Option (Option α)) (decode (n + 1)) a ∧ encode a = n + 1
have succ₁ : encode (some (ofNat α n)) = n + 1
Tactic: refine ⟨some (ofNat α n), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
⊢ Membership.mem (γ := Option (Option α)) (decode (n + 1)) (some (ofNat α n))
have succ : Membership.mem (γ := Option (Option α)) (Option.map some (decode n)) (some (ofNat α n))
Tactic: rw [decode_option_succ, decode_eq_ofNat, Option.map_some, Option.mem_def]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
succ : Membership.mem (γ := Option (Option α)) (Option.map some (decode n)) (some (ofNat α n))
⊢ Membership.mem (γ := Option (Option α)) (decode (n + 1)) (some (ofNat α n))
have succ₁ : some (ofNat α n) ∈ Option.map some (some (ofNat α n))
Tactic: rw [decode_option_succ, decode_eq_ofNat, Option.map_some, Option.mem_def]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
succ : Membership.mem (γ := Option (Option α)) (Option.map some (decode n)) (some (ofNat α n))
succ₁ : some (ofNat α n) ∈ Option.map some (some (ofNat α n))
⊢ Membership.mem (γ := Option (Option α)) (decode (n + 1)) (some (ofNat α n))
have succ₂ : some (ofNat α n) ∈ some (some (ofNat α n))
Tactic: rw [decode_option_succ, decode_eq_ofNat, Option.map_some, Option.mem_def]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
succ : Membership.mem (γ := Option (Option α)) (Option.map some (decode n)) (some (ofNat α n))
succ₁ : some (ofNat α n) ∈ Option.map some (some (ofNat α n))
succ₂ : some (ofNat α n) ∈ some (some (ofNat α n))
⊢ Membership.mem (γ := Option (Option α)) (decode (n + 1)) (some (ofNat α n))
have succ₃ : some (some (ofNat α n)) = some (some (ofNat α n))
Tactic: rw [decode_option_succ, decode_eq_ofNat, Option.map_some, Option.mem_def]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
⊢ encode (some (ofNat α n)) = n + 1
have succ : (encode (ofNat α n)).succ = n + 1
Tactic: rw [encode_some, encode_ofNat]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
succ : (encode (ofNat α n)).succ = n + 1
⊢ encode (some (ofNat α n)) = n + 1
have succ₁ : n.succ = n + 1
Tactic: rw [encode_some, encode_ofNat]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
⊢ ∃ (a : Option α), Membership.mem (γ := Option (Option α)) (decode n) a ∧ encode a = n
have zero : ∃ (a : Option α), Membership.mem (γ := Option (Option α)) (decode 0) a ∧ encode a = 0
Tactic: cases n with
    | zero =>
      refine ⟨none, ?_, encode_none⟩
      rw [decode_option_zero, Option.mem_def]
    | succ n =>
      refine ⟨some (ofNat α n), ?_, ?_⟩
      · rw [decode_option_succ, decode_eq_ofNat, Option.map_some, Option.mem_def]
      rw [encode_some, encode_ofNat]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
zero : ∃ (a : Option α), Membership.mem (γ := Option (Option α)) (decode 0) a ∧ encode a = 0
⊢ ∃ (a : Option α), Membership.mem (γ := Option (Option α)) (decode n) a ∧ encode a = n
have succ : ∀ (n : ℕ), ∃ (a : Option α), Membership.mem (γ := Option (Option α)) (decode (n + 1)) a ∧ encode a = n + 1
Tactic: cases n with
    | zero =>
      refine ⟨none, ?_, encode_none⟩
      rw [decode_option_zero, Option.mem_def]
    | succ n =>
      refine ⟨some (ofNat α n), ?_, ?_⟩
      · rw [decode_option_succ, decode_eq_ofNat, Option.map_some, Option.mem_def]
      rw [encode_some, encode_ofNat]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
⊢ ∃ (a : α ⊕ β), Membership.mem (γ := Option (α ⊕ β)) (decode n) a ∧ encode a = n
have suffices : ∃ (a : α ⊕ β), Membership.mem (γ := Option (α ⊕ β)) (decodeSum n) a ∧ encodeSum a = bit n.bodd n.div2
Tactic: suffices ∃ a ∈ @decodeSum α β _ _ n, encodeSum a = bit (bodd n) (div2 n) by
      simpa [bit_bodd_div2]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
⊢ ∃ (a : α ⊕ β), Membership.mem (γ := Option (α ⊕ β)) (decodeSum n) a ∧ encodeSum a = bit n.bodd n.div2
have simp : (∃ (a : α),
    Membership.mem (γ := Option (α ⊕ β))
        (match (motive := Bool → ℕ → Option (α ⊕ β)) n.bodd, 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 n.bodd n.div2) ∨
  ∃ (b : β),
    Membership.mem (γ := Option (α ⊕ β))
        (match (motive := Bool → ℕ → Option (α ⊕ β)) n.bodd, 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 n.bodd n.div2
Tactic: simp only [decodeSum, decode_eq_ofNat, Option.map_some, Sum.exists]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
⊢ (∃ (a : α),
      Membership.mem (γ := Option (α ⊕ β))
          (match (motive := Bool → ℕ → Option (α ⊕ β)) n.bodd, 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 n.bodd n.div2) ∨
    ∃ (b : β),
      Membership.mem (γ := Option (α ⊕ β))
          (match (motive := Bool → ℕ → Option (α ⊕ β)) n.bodd, 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 n.bodd n.div2
have false : (∃ (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: cases bodd n
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
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
⊢ (∃ (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
have true : (∃ (a : α),
    Membership.mem (γ := Option (α ⊕ β))
        (match (motive := Bool → ℕ → Option (α ⊕ β)) 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 true n.div2) ∨
  ∃ (b : β),
    Membership.mem (γ := Option (α ⊕ β))
        (match (motive := Bool → ℕ → Option (α ⊕ β)) 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 true n.div2
Tactic: cases bodd n
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
α : Type u_1
inst : Denumerable α
γ : α → Type u_3
inst_1 : (a : α) → Denumerable (γ a)
n : ℕ
⊢ Eq (α := Option (Sigma γ)) (some (ofNat (Sigma γ) n))
    (some (Sigma.mk (β := γ) (ofNat α (unpair n).1) (ofNat (γ (ofNat α (unpair n).1)) (unpair n).2)))
have 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)))
Tactic: rw [← decode_eq_ofNat, decode_sigma_val]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
⊢ ofNat (ℕ × ℕ) = unpair
have h : ∀ (x : ℕ), ofNat (ℕ × ℕ) x = unpair x
Tactic: funext
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
x : (↑s : Type)
⊢ ∃ (n : ℕ), (↑x : ℕ) + n + 1 ∈ s
have by_contra : ∀ (h : ¬∃ (n : ℕ), (↑x : ℕ) + n + 1 ∈ s), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
x : (↑s : Type)
h : ¬∃ (n : ℕ), (↑x : ℕ) + n + 1 ∈ s
a : ℕ
ha : a ∈ s
hax : (↑x : ℕ) + 1 ≤ a
⊢ (↑x : ℕ) + (a - ((↑x : ℕ) + 1)) + 1 ∈ s
have rwa : (↑x : ℕ) + 1 + (a - ((↑x : ℕ) + 1)) ∈ s
Tactic: rwa [Nat.add_right_comm, Nat.add_sub_cancel' hax]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (hypothesis)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
x : (↑s : Type)
h : ¬∃ (n : ℕ), (↑x : ℕ) + n + 1 ∈ s
⊢ False
have this : ∀ (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]⟩
-- Lean 4 proof step from Mathlib.Logic.Denumerable (hypothesis)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
x : ℕ
hx : x ∈ s
⊢ ∃ (a : ℕ), ofNat s a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
have ht : 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)) sorry;
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)) sorry
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
-- Lean 4 proof step from Mathlib.Logic.Denumerable (hypothesis)
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)) ⋯
⊢ ∃ (a : ℕ), ofNat s a = Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
have hmt : ∀ {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]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
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
have bot : ∀ (h : ofNat s 0 < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx), Membership.mem (γ := List (↑s : Type)) [] ⊥
Tactic: refine ⟨0, le_antisymm bot_le (le_of_not_gt fun h => List.not_mem_nil (a := (⊥ : s)) ?_)⟩
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
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
⊢ Membership.mem (γ := List (↑s : Type)) [] ⊥
have bot : ⊥ ∈ t
Tactic: rwa [← List.maximum_eq_bot.1 hmax, hmt]
-- Lean 4 proof step from Mathlib.Logic.Denumerable (goal)
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
⊢ Membership.mem (γ := List (↑s : Type)) [] ⊥
have bot₁ : ⊥ < Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) x hx
Tactic: rwa [← List.maximum_eq_bot.1 hmax, hmt]