awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
x y : { x : α // p x ∨ q x }
⊢ Eq.{u_1 + 1} (α := { x : α // p x } ⊕ { x : α // q x })
      (if h : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑x : α) h)
      else Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑x : α) ⋯))
      (if h : p (↑y : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑y : α) h)
      else Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑y : α) ⋯)) →
    x = y
have pos : ∀ (h : p (↑x : α)) (h_1 : p (↑y : α)),
  Eq (α := { x : α // p x } ⊕ { x : α // q x }) (Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑x : α) h))
      (Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑y : α) h_1)) →
    x = y
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
x y : { x : α // p x ∨ q x }
pos :
  ∀ (h : p (↑x : α)) (h_1 : p (↑y : α)),
    Eq (α := { x : α // p x } ⊕ { x : α // q x }) (Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑x : α) h))
        (Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑y : α) h_1)) →
      x = y
⊢ Eq.{u_1 + 1} (α := { x : α // p x } ⊕ { x : α // q x })
      (if h : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑x : α) h)
      else Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑x : α) ⋯))
      (if h : p (↑y : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑y : α) h)
      else Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑y : α) ⋯)) →
    x = y
have neg : p (↑x : α) → ¬p (↑y : α) → False → x = y
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
x y : { x : α // p x ∨ q x }
pos :
  ∀ (h : p (↑x : α)) (h_1 : p (↑y : α)),
    Eq (α := { x : α // p x } ⊕ { x : α // q x }) (Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑x : α) h))
        (Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑y : α) h_1)) →
      x = y
neg : p (↑x : α) → ¬p (↑y : α) → False → x = y
⊢ Eq.{u_1 + 1} (α := { x : α // p x } ⊕ { x : α // q x })
      (if h : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑x : α) h)
      else Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑x : α) ⋯))
      (if h : p (↑y : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑y : α) h)
      else Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑y : α) ⋯)) →
    x = y
have pos₁ : ¬p (↑x : α) → p (↑y : α) → False → x = y
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Embedding.Basic (goal)
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
x y : { x : α // p x ∨ q x }
pos :
  ∀ (h : p (↑x : α)) (h_1 : p (↑y : α)),
    Eq (α := { x : α // p x } ⊕ { x : α // q x }) (Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑x : α) h))
        (Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑y : α) h_1)) →
      x = y
neg : p (↑x : α) → ¬p (↑y : α) → False → x = y
pos₁ : ¬p (↑x : α) → p (↑y : α) → False → x = y
⊢ Eq.{u_1 + 1} (α := { x : α // p x } ⊕ { x : α // q x })
      (if h : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑x : α) h)
      else Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑x : α) ⋯))
      (if h : p (↑y : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ p x) (↑y : α) h)
      else Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑y : α) ⋯)) →
    x = y
have neg₁ : ∀ (h : ¬p (↑x : α)) (h_1 : ¬p (↑y : α)),
  Eq (α := { x : α // p x } ⊕ { x : α // q x }) (Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑x : α) sorry))
      (Sum.inr (Subtype.mk (p := fun (x : α) ↦ q x) (↑y : α) sorry)) →
    x = y
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Logic.Embedding.Set (goal)
Goal:
α : Type u_1
s t : Set α
h_1 : s ⊆ t
x_1 x_2 : (↑s : Type u_1)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h :
  Eq.{u_1 + 1} (α := (↑t : Type u_1))
    ((fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx))
    ((fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy))
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx = Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy
have e_val : x = y
Tactic: congr
-- Lean 4 proof step from Mathlib.Logic.Embedding.Set (goal)
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
h : Disjoint p q
x : { x : α // q x }
⊢ Eq (α := { x : α // p x } ⊕ { x : α // q x })
    ((subtypeOrLeftEmbedding p q : (a : { x : α // p x ∨ q x }) → { x : α // p x } ⊕ { x : α // q x })
        (Sum.elim (α := { x : α // p x })
          (⇑(Subtype.impEmbedding p (fun (x : α) ↦ p x ∨ q x) ⋯) : (a : { x : α // p x }) → { x : α // p x ∨ q x })
          (⇑(Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) ⋯) : (a : { x : α // q x }) → { x : α // p x ∨ q x })
          (Sum.inr x)) :
      { x : α // p x } ⊕ { x : α // q x })
    (Sum.inr x : { x : α // p x } ⊕ { x : α // q x })
have inr : Eq (α := { x : α // p x } ⊕ { x : α // q x })
  ((subtypeOrLeftEmbedding p q : (a : { x : α // p x ∨ q x }) → { x : α // p x } ⊕ { x : α // q x })
      ((Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) sorry : (a : { x : α // q x }) → { x : α // p x ∨ q x }) x :
        { x : α // p x ∨ q x }) :
    { x : α // p x } ⊕ { x : α // q x })
  (Sum.inr x : { x : α // p x } ⊕ { x : α // q x })
Tactic: simp only [Sum.elim_inr]
-- Lean 4 proof step from Mathlib.Logic.Embedding.Set (goal)
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
h : Disjoint p q
x : { x : α // q x }
⊢ Eq (α := { x : α // p x } ⊕ { x : α // q x })
    ((subtypeOrLeftEmbedding p q : (a : { x : α // p x ∨ q x }) → { x : α // p x } ⊕ { x : α // q x })
        ((Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) ⋯ : (a : { x : α // q x }) → { x : α // p x ∨ q x }) x :
          { x : α // p x ∨ q x }) :
      { x : α // p x } ⊕ { x : α // q x })
    (Sum.inr x : { x : α // p x } ⊕ { x : α // q x })
have inr : Eq (α := { x : α // p x } ⊕ { x : α // q x })
  (Sum.inr
      (Subtype.mk (p := fun (x : α) ↦ q x)
        (↑((Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) sorry : (a : { x : α // q x }) → { x : α // p x ∨ q x }) x) :
          α)
        sorry) :
    { x : α // p x } ⊕ { x : α // q x })
  (Sum.inr x : { x : α // p x } ⊕ { x : α // q x })
Tactic: rw [subtypeOrLeftEmbedding_apply_right]
-- Lean 4 proof step from Mathlib.Logic.Embedding.Set (goal)
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
h : Disjoint p q
x : { x : α // q x }
inr :
  Eq (α := { x : α // p x } ⊕ { x : α // q x })
    (Sum.inr
        (Subtype.mk (p := fun (x : α) ↦ q x)
          (↑((Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) ⋯ : (a : { x : α // q x }) → { x : α // p x ∨ q x }) x) :
            α)
          ⋯) :
      { x : α // p x } ⊕ { x : α // q x })
    (Sum.inr x : { x : α // p x } ⊕ { x : α // q x })
⊢ Eq (α := { x : α // p x } ⊕ { x : α // q x })
    ((subtypeOrLeftEmbedding p q : (a : { x : α // p x ∨ q x }) → { x : α // p x } ⊕ { x : α // q x })
        ((Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) ⋯ : (a : { x : α // q x }) → { x : α // p x ∨ q x }) x :
          { x : α // p x ∨ q x }) :
      { x : α // p x } ⊕ { x : α // q x })
    (Sum.inr x : { x : α // p x } ⊕ { x : α // q x })
have inr₁ : ¬p (↑((Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) sorry : (a : { x : α // q x }) → { x : α // p x ∨ q x }) x) : α)
Tactic: rw [subtypeOrLeftEmbedding_apply_right]
-- Lean 4 proof step from Mathlib.Logic.Embedding.Set (goal)
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
h : Disjoint p q
x : { x : α // q x }
⊢ ¬p (↑((Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) ⋯ : (a : { x : α // q x }) → { x : α // p x ∨ q x }) x) : α)
have inr : ¬p (↑x : α)
Tactic: suffices ¬p x by simpa
-- Lean 4 proof step from Mathlib.Logic.Embedding.Set (goal)
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
h : Disjoint p q
x : { x : α // p x } ⊕ { x : α // q x }
⊢ (subtypeOrLeftEmbedding p q : (a : { x : α // p x ∨ q x }) → { x : α // p x } ⊕ { x : α // q x })
      (Sum.elim
        (⇑(Subtype.impEmbedding p (fun (x : α) ↦ p x ∨ q x) ⋯) : (a : { x : α // p x }) → { x : α // p x ∨ q x })
        (⇑(Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) ⋯) : (a : { x : α // q x }) → { x : α // p x ∨ q x }) x) =
    x
have inl : ∀ (x : { x : α // p x }),
  Eq (α := { x : α // p x } ⊕ { x : α // q x })
    ((subtypeOrLeftEmbedding p q : (a : { x : α // p x ∨ q x }) → { x : α // p x } ⊕ { x : α // q x })
        (Sum.elim (β := { x : α // q x })
          (⇑(Subtype.impEmbedding p (fun (x : α) ↦ p x ∨ q x) sorry) : (a : { x : α // p x }) → { x : α // p x ∨ q x })
          (⇑(Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) sorry) : (a : { x : α // q x }) → { x : α // p x ∨ q x })
          (Sum.inl x)) :
      { x : α // p x } ⊕ { x : α // q x })
    (Sum.inl x : { x : α // p x } ⊕ { x : α // q x })
Tactic: cases x with
    | inl x => grind
    | inr x =>
      simp only [Sum.elim_inr]
      rw [subtypeOrLeftEmbedding_apply_right]
      · grind
      · suffices ¬p x by simpa
        intro hp
        simpa using h.le_bot x ⟨hp, x.prop⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Logic.Embedding.Set (goal)
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
h : Disjoint p q
x : { x : α // p x } ⊕ { x : α // q x }
inl :
  ∀ (x : { x : α // p x }),
    Eq (α := { x : α // p x } ⊕ { x : α // q x })
      ((subtypeOrLeftEmbedding p q : (a : { x : α // p x ∨ q x }) → { x : α // p x } ⊕ { x : α // q x })
          (Sum.elim (β := { x : α // q x })
            (⇑(Subtype.impEmbedding p (fun (x : α) ↦ p x ∨ q x) ⋯) : (a : { x : α // p x }) → { x : α // p x ∨ q x })
            (⇑(Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) ⋯) : (a : { x : α // q x }) → { x : α // p x ∨ q x })
            (Sum.inl x)) :
        { x : α // p x } ⊕ { x : α // q x })
      (Sum.inl x : { x : α // p x } ⊕ { x : α // q x })
⊢ (subtypeOrLeftEmbedding p q : (a : { x : α // p x ∨ q x }) → { x : α // p x } ⊕ { x : α // q x })
      (Sum.elim
        (⇑(Subtype.impEmbedding p (fun (x : α) ↦ p x ∨ q x) ⋯) : (a : { x : α // p x }) → { x : α // p x ∨ q x })
        (⇑(Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) ⋯) : (a : { x : α // q x }) → { x : α // p x ∨ q x }) x) =
    x
have inr : ∀ (x : { x : α // q x }),
  Eq (α := { x : α // p x } ⊕ { x : α // q x })
    ((subtypeOrLeftEmbedding p q : (a : { x : α // p x ∨ q x }) → { x : α // p x } ⊕ { x : α // q x })
        (Sum.elim (α := { x : α // p x })
          (⇑(Subtype.impEmbedding p (fun (x : α) ↦ p x ∨ q x) sorry) : (a : { x : α // p x }) → { x : α // p x ∨ q x })
          (⇑(Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) sorry) : (a : { x : α // q x }) → { x : α // p x ∨ q x })
          (Sum.inr x)) :
      { x : α // p x } ⊕ { x : α // q x })
    (Sum.inr x : { x : α // p x } ⊕ { x : α // q x })
Tactic: cases x with
    | inl x => grind
    | inr x =>
      simp only [Sum.elim_inr]
      rw [subtypeOrLeftEmbedding_apply_right]
      · grind
      · suffices ¬p x by simpa
        intro hp
        simpa using h.le_bot x ⟨hp, x.prop⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Logic.Embedding.Set (goal)
Goal:
α : Type u_1
ι : Type u_2
s_1 t r : Set α
s : ι → Set α
h : Pairwise (Disjoint on s)
i : ι
x : α
hx : x ∈ s i
j : ι
hx' :
  (fun (x : (i : ι) × (↑(s i) : Type u_1)) ↦ (↑(x.snd (β := fun (i : ι) ↦ (↑(s i) : Type u_1))) : α))
      (Sigma.mk (β := fun (i : ι) ↦ (↑(s i) : Type u_1)) i (Subtype.mk (p := fun (x : α) ↦ x ∈ s i) x hx)) ∈
    s j
⊢ Eq (α := (i : ι) × (↑(s i) : Type u_1))
    (Sigma.mk (β := fun (i : ι) ↦ (↑(s i) : Type u_1)) i (Subtype.mk (p := fun (x : α) ↦ x ∈ s i) x hx))
    (Sigma.mk (β := fun (i : ι) ↦ (↑(s i) : Type u_1)) j
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s j)
        ((fun (x : (i : ι) × (↑(s i) : Type u_1)) ↦ (↑(x.snd (β := fun (i : ι) ↦ (↑(s i) : Type u_1))) : α))
          (Sigma.mk (β := fun (i : ι) ↦ (↑(s i) : Type u_1)) i (Subtype.mk (p := fun (x : α) ↦ x ∈ s i) x hx)))
        hx'))
have obtain : ∀
  (hx' :
    (fun (x : (i : ι) × (↑(s i) : Type u_1)) ↦ (↑(x.snd (β := fun (i : ι) ↦ (↑(s i) : Type u_1))) : α))
        (Sigma.mk (β := fun (i : ι) ↦ (↑(s i) : Type u_1)) i (Subtype.mk (p := fun (x : α) ↦ x ∈ s i) x hx)) ∈
      s i),
  Eq (α := (i : ι) × (↑(s i) : Type u_1))
    (Sigma.mk (β := fun (i : ι) ↦ (↑(s i) : Type u_1)) i (Subtype.mk (p := fun (x : α) ↦ x ∈ s i) x hx))
    (Sigma.mk (β := fun (i : ι) ↦ (↑(s i) : Type u_1)) i
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s i)
        ((fun (x : (i : ι) × (↑(s i) : Type u_1)) ↦ (↑(x.snd (β := fun (i : ι) ↦ (↑(s i) : Type u_1))) : α))
          (Sigma.mk (β := fun (i : ι) ↦ (↑(s i) : Type u_1)) i (Subtype.mk (p := fun (x : α) ↦ x ∈ s i) x hx)))
        hx'))
Tactic: obtain rfl : i = j := h.eq (not_disjoint_iff.2 ⟨_, hx, hx'⟩)
Cleared hypotheses: j, hx'
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
inst : Encodable α
x y : α
e : encode x = encode y
⊢ some x = some y
have rw : decode (encode x) = some y
Tactic: rw [← encodek, e, encodek]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
inst : Encodable α
x y : α
e : encode x = encode y
rw : decode (encode x) = some y
⊢ some x = some y
have rw₁ : decode (encode y) = some y
Tactic: rw [← encodek, e, encodek]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
inst : Encodable α
x y : α
e : encode x = encode y
rw : decode (encode x) = some y
rw₁ : decode (encode y) = some y
⊢ some x = some y
have rw₂ : some y = some y
Tactic: rw [← encodek, e, encodek]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_3
inst : Encodable α
d x : α
⊢ (fun (n : ℕ) ↦ Option.getD (decode n) d) (encode x) = x
have simp_rw : (some x).getD d = x
Tactic: simp_rw [Encodable.encodek]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Encodable α
e : β ≃ α
n : ℕ
⊢ Eq.{u_4 + 1} (α := Option β) (Option.bind.{u_3, u_4} (α := α) (decode n) (some ∘ (⇑e.symm : (a : α) → β)))
    (Option.map.{u_3, u_4} (α := α) (⇑e.symm : (a : α) → β) (decode n))
have rw : Eq.{u_4 + 1} (α := Option β) (Option.bind.{u_3, u_4} (α := α) (decode n) (some ∘ (⇑e.symm : (a : α) → β)))
  (Option.bind.{u_3, u_4} (α := α) (decode n) (some ∘ (⇑e.symm : (a : α) → β)))
Tactic: rw [Option.map_eq_bind]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
o : Option α
⊢ (fun (n : ℕ) ↦
        (Nat.casesOn (motive := fun (x : ℕ) ↦ Option (Option α)) n (some none) fun (m : ℕ) ↦
            Option.map some (decode m) :
          Option (Option α)))
      ((fun (o : Option α) ↦
          (Option.casesOn (motive := fun (x : Option α) ↦ ℕ) o zero fun (a : α) ↦ (encode a).succ : ℕ))
        o) =
    some o
have none : Eq.{u_3 + 1} (α := Option (Option α))
  ((fun (n : ℕ) ↦
      (Nat.casesOn (motive := fun (x : ℕ) ↦ Option (Option α)) n (some none) fun (m : ℕ) ↦ Option.map some (decode m) :
        Option (Option α)))
    ((fun (o : Option α) ↦ (Option.casesOn (motive := fun (x : Option α) ↦ ℕ) o zero fun (a : α) ↦ (encode a).succ : ℕ))
      none))
  (some none)
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
o : Option α
none :
  Eq.{u_3 + 1} (α := Option (Option α))
    ((fun (n : ℕ) ↦
        (Nat.casesOn (motive := fun (x : ℕ) ↦ Option (Option α)) n (some Option.none) fun (m : ℕ) ↦
            Option.map some (decode m) :
          Option (Option α)))
      ((fun (o : Option α) ↦
          (Option.casesOn (motive := fun (x : Option α) ↦ ℕ) o zero fun (a : α) ↦ (encode a).succ : ℕ))
        Option.none))
    (some Option.none)
⊢ (fun (n : ℕ) ↦
        (Nat.casesOn (motive := fun (x : ℕ) ↦ Option (Option α)) n (some Option.none) fun (m : ℕ) ↦
            Option.map some (decode m) :
          Option (Option α)))
      ((fun (o : Option α) ↦
          (Option.casesOn (motive := fun (x : Option α) ↦ ℕ) o zero fun (a : α) ↦ (encode a).succ : ℕ))
        o) =
    some o
have some : ∀ (val : α),
  (fun (n : ℕ) ↦
        (Nat.casesOn (motive := fun (x : ℕ) ↦ Option (Option α)) n (some Option.none) fun (m : ℕ) ↦
            Option.map some (decode m) :
          Option (Option α)))
      ((fun (o : Option α) ↦
          (Option.casesOn (motive := fun (x : Option α) ↦ ℕ) o zero fun (a : α) ↦ (encode a).succ : ℕ))
        (some val)) =
    some (some val)
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
inst : Encodable α
n : ℕ
⊢ decode₂ α n ≠ none ↔ n ∈ Set.range.{0, u_1 + 1} (ι := α) encode
have simp_rw : decode₂ α n ≠ none ↔ Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (y : α), encode y = x} n
Tactic: simp_rw [Set.range, Set.mem_setOf_eq, Ne, Option.eq_none_iff_forall_not_mem,
    Encodable.mem_decode₂, not_forall, not_not]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
inst : Encodable α
n : ℕ
simp_rw : decode₂ α n ≠ none ↔ Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (y : α), encode y = x} n
⊢ decode₂ α n ≠ none ↔ n ∈ Set.range.{0, u_1 + 1} (ι := α) encode
have simp_rw₁ : decode₂ α n ≠ none ↔ ∃ (y : α), encode y = n
Tactic: simp_rw [Set.range, Set.mem_setOf_eq, Ne, Option.eq_none_iff_forall_not_mem,
    Encodable.mem_decode₂, not_forall, not_not]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
inst : Encodable α
n : ℕ
simp_rw : decode₂ α n ≠ none ↔ Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (y : α), encode y = x} n
simp_rw₁ : decode₂ α n ≠ none ↔ ∃ (y : α), encode y = n
⊢ decode₂ α n ≠ none ↔ n ∈ Set.range.{0, u_1 + 1} (ι := α) encode
have simp_rw₂ : ¬decode₂ α n = none ↔ ∃ (y : α), encode y = n
Tactic: simp_rw [Set.range, Set.mem_setOf_eq, Ne, Option.eq_none_iff_forall_not_mem,
    Encodable.mem_decode₂, not_forall, not_not]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
inst : Encodable α
n : ℕ
simp_rw : decode₂ α n ≠ none ↔ Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (y : α), encode y = x} n
simp_rw₁ : decode₂ α n ≠ none ↔ ∃ (y : α), encode y = n
simp_rw₂ : ¬decode₂ α n = none ↔ ∃ (y : α), encode y = n
⊢ decode₂ α n ≠ none ↔ n ∈ Set.range.{0, u_1 + 1} (ι := α) encode
have simp_rw₃ : (¬∀ (a : α), a ∉ decode₂ α n) ↔ ∃ (y : α), encode y = n
Tactic: simp_rw [Set.range, Set.mem_setOf_eq, Ne, Option.eq_none_iff_forall_not_mem,
    Encodable.mem_decode₂, not_forall, not_not]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
inst : Encodable α
n : ℕ
simp_rw : decode₂ α n ≠ none ↔ Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (y : α), encode y = x} n
simp_rw₁ : decode₂ α n ≠ none ↔ ∃ (y : α), encode y = n
simp_rw₂ : ¬decode₂ α n = none ↔ ∃ (y : α), encode y = n
simp_rw₃ : (¬∀ (a : α), a ∉ decode₂ α n) ↔ ∃ (y : α), encode y = n
⊢ decode₂ α n ≠ none ↔ n ∈ Set.range.{0, u_1 + 1} (ι := α) encode
have simp_rw₄ : (¬∀ (a : α), ¬encode a = n) ↔ ∃ (y : α), encode y = n
Tactic: simp_rw [Set.range, Set.mem_setOf_eq, Ne, Option.eq_none_iff_forall_not_mem,
    Encodable.mem_decode₂, not_forall, not_not]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
inst : Encodable α
n : ℕ
simp_rw : decode₂ α n ≠ none ↔ Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (y : α), encode y = x} n
simp_rw₁ : decode₂ α n ≠ none ↔ ∃ (y : α), encode y = n
simp_rw₂ : ¬decode₂ α n = none ↔ ∃ (y : α), encode y = n
simp_rw₃ : (¬∀ (a : α), a ∉ decode₂ α n) ↔ ∃ (y : α), encode y = n
simp_rw₄ : (¬∀ (a : α), ¬encode a = n) ↔ ∃ (y : α), encode y = n
⊢ decode₂ α n ≠ none ↔ n ∈ Set.range.{0, u_1 + 1} (ι := α) encode
have simp_rw₅ : (∃ (x : α), ¬¬encode x = n) ↔ ∃ (y : α), encode y = n
Tactic: simp_rw [Set.range, Set.mem_setOf_eq, Ne, Option.eq_none_iff_forall_not_mem,
    Encodable.mem_decode₂, not_forall, not_not]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Encodable α
x : ℕ
h : (decode₂ α x).isSome = true
⊢ encode ((decode₂ α x).get h) = x
have rw : decode₂ α x = some ((decode₂ α x).get h)
Tactic: rw [← decode₂_isPartialInv (Option.get _ h), Option.some_get]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Encodable α
x : ℕ
h : (decode₂ α x).isSome = true
rw : decode₂ α x = some ((decode₂ α x).get h)
⊢ encode ((decode₂ α x).get h) = x
have rw₁ : decode₂ α x = decode₂ α x
Tactic: rw [← decode₂_isPartialInv (Option.get _ h), Option.some_get]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Encodable α
x : ℕ
h : (fun (x : ℕ) ↦ x ∈ Set.range.{0, u_3 + 1} (ι := α) encode) x
n : α
hn : encode n = x
⊢ (decode₂ α x).isSome = true
have rw : (some n).isSome = true
Tactic: rw [← hn, encodek₂]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Encodable α
n : (↑(Set.range.{0, u_3 + 1} (ι := α) encode) : Type)
⊢ (decode₂ α (↑n : ℕ)).isSome = true
have obtain : ∀ (x : α) (hx : encode x = (↑n : ℕ)), (decode₂ α (↑n : ℕ)).isSome = true
Tactic: obtain ⟨x, hx⟩ := n.2
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Encodable α
n : (↑(Set.range.{0, u_3 + 1} (ι := α) encode) : Type)
x : α
hx : encode x = (↑n : ℕ)
⊢ (decode₂ α (↑n : ℕ)).isSome = true
have rw : (some x).isSome = true
Tactic: rw [← hx, encodek₂]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Encodable α
x : α
⊢ (fun (n : (↑(Set.range.{0, u_3 + 1} (ι := α) encode) : Type)) ↦ (decode₂ α (↑n : ℕ)).get ⋯)
      ((fun (a : α) ↦ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.range.{0, u_3 + 1} (ι := α) encode) (encode a) ⋯) x) =
    x
have dsimp : (decode₂ α (encode x)).get sorry = x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Encodable α
x : α
⊢ (decode₂ α (encode x)).get ⋯ = x
have rw : some ((decode₂ α (encode x)).get sorry) = some x
Tactic: rw [← Option.some_inj, Option.some_get, encodek₂]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Encodable α
x : α
rw : some ((decode₂ α (encode x)).get ⋯) = some x
⊢ (decode₂ α (encode x)).get ⋯ = x
have rw₁ : decode₂ α (encode x) = some x
Tactic: rw [← Option.some_inj, Option.some_get, encodek₂]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Encodable α
x : α
rw : some ((decode₂ α (encode x)).get ⋯) = some x
rw₁ : decode₂ α (encode x) = some x
⊢ (decode₂ α (encode x)).get ⋯ = x
have rw₂ : some x = some x
Tactic: rw [← Option.some_inj, Option.some_get, encodek₂]
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
s : α ⊕ β
⊢ decodeSum (encodeSum s) = some s
have inl : ∀ (val : α), Eq (α := Option (α ⊕ β)) (decodeSum (encodeSum.{u_1, u_2} (β := β) (Sum.inl val))) (some (Sum.inl val))
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
s : α ⊕ β
inl :
  ∀ (val : α), Eq (α := Option (α ⊕ β)) (decodeSum (encodeSum.{u_1, u_2} (β := β) (Sum.inl val))) (some (Sum.inl val))
⊢ decodeSum (encodeSum s) = some s
have inr : ∀ (val : β), Eq (α := Option (α ⊕ β)) (decodeSum (encodeSum.{u_1, u_2} (α := α) (Sum.inr val))) (some (Sum.inr val))
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Logic.Encodable.Basic (goal)
Goal:
n : ℕ
h : 2 ≤ n
this : Eq (α := Option (Unit ⊕ Unit)) (decodeSum n) none
⊢ Eq (α := Option Bool)
    (Option.bind (α := Unit ⊕ Unit) (decodeSum n)
      (some ∘ (⇑Equiv.boolEquivPUnitSumPUnit.symm : (a : Unit ⊕ Unit) → Bool)))
    none
have rw : Eq (α := Option Bool)
  (Option.bind (α := Unit ⊕ Unit) none (some ∘ (⇑Equiv.boolEquivPUnitSumPUnit.symm : (a : Unit ⊕ Unit) → Bool))) none
Tactic: rw [this]