awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Embedding.Set
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 })
    ((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 })
⊢ 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 })

Tactic:
simp only [Sum.elim_inr]

Premises used: Sum.elim_inr
-- Module: Mathlib.Logic.Embedding.Set
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 })
inr₁ :
  ¬p (↑((Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) ⋯ : (a : { x : α // q x }) → { x : α // p x ∨ q x }) 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 })

Tactic:
rw [subtypeOrLeftEmbedding_apply_right]

Premises used: subtypeOrLeftEmbedding_apply_right
-- Module: Mathlib.Logic.Embedding.Set
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 })
    (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 })

Tactic:
grind
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
h : Disjoint p q
x : { x : α // q x }
this : ¬p (↑x : α)
⊢ ¬p (↑((Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) ⋯ : (a : { x : α // q x }) → { x : α // p x ∨ q x }) x) : α)

Tactic:
simpa
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
h : Disjoint p q
x : { x : α // q x }
inr : ¬p (↑x : α)
⊢ ¬p (↑((Subtype.impEmbedding q (fun (x : α) ↦ p x ∨ q x) ⋯ : (a : { x : α // q x }) → { x : α // p x ∨ q x }) x) : α)

Tactic:
suffices ¬p x by simpa
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
h : Disjoint p q
x : { x : α // q x }
hp : p (↑x : α)
⊢ False

Tactic:
simpa using h.le_bot x ⟨hp, x.prop⟩

Premises used: Disjoint.le_bot, Subtype.prop, And.intro, Subtype.val
-- Module: Mathlib.Logic.Embedding.Set
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 })
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) ⋯) : (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 })
⊢ (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

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⟩

Premises used: Sum.elim_inr, subtypeOrLeftEmbedding_apply_right
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
h : Disjoint p q
x : { x : α // p x }
⊢ Eq (α := { x : α // p x ∨ q x })
    (((subtypeOrEquiv p q h).symm : (a : { x : α // p x } ⊕ { x : α // q x }) → { x : α // p x ∨ q x }) (Sum.inl x) :
      { x : α // p x ∨ q x })
    (Subtype.mk (p := fun (x : α) ↦ p x ∨ q x) (↑x : α) ⋯ : { x : α // p x ∨ q x })

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
p q : α → Prop
inst : DecidablePred p
h : Disjoint p q
x : { x : α // q x }
⊢ Eq (α := { x : α // p x ∨ q x })
    (((subtypeOrEquiv p q h).symm : (a : { x : α // p x } ⊕ { x : α // q x }) → { x : α // p x ∨ q x }) (Sum.inr x) :
      { x : α // p x ∨ q x })
    (Subtype.mk (p := fun (x : α) ↦ p x ∨ q x) (↑x : α) ⋯ : { x : α // p x ∨ q x })

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Sum.elim (β := (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ t))
        (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha)) =
      Sum.elim (β := (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ t))
        (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb)) →
    Eq (α := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha))
      (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb))

Tactic:
simp
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ Sum.elim (β := (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ t))
        (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha)) =
      Sum.elim (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ t))
        (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) b hb)) →
    Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) = Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) b hb)

Tactic:
simpa using h.ne_of_mem ha hb

Premises used: Disjoint.ne_of_mem
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ t
b : α
hb : b ∈ s
⊢ Sum.elim (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ t))
        (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) a ha)) =
      Sum.elim (β := (↑t : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ t))
        (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb)) →
    Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) a ha) = Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) b hb)

Tactic:
simpa using h.symm.ne_of_mem ha hb

Premises used: Disjoint.symm, Disjoint.ne_of_mem
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
ι : Type u_2
s t r : Set α
h : Disjoint s t
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ Sum.elim (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ t))
        (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) a ha)) =
      Sum.elim (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ t))
        (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) b hb)) →
    Eq (α := (↑s : Type u_1) ⊕ (↑t : Type u_1)) (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) a ha))
      (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) b hb))

Tactic:
simp
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
⊢ Eq (α := (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
    (⇑(sumSet (s := s) (t := t) h) : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α)
    (Sum.elim (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ t)))

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
s t r : Set α
h : Disjoint s t
⊢ image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (preimage (β := (↑s : Type u_1) ⊕ (↑t : Type u_1)) Sum.inl
        ((⇑(sumSet (s := s) (t := t) h) : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α) ⁻¹' r)) =
    r ∩ s

Tactic:
simp [Set.ext_iff]

Premises used: Set.ext_iff
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
s t r : Set α
h : Disjoint s t
⊢ image (α := { x : α // x ∈ t }) (Subtype.val (p := fun (x : α) ↦ x ∈ t))
      (preimage (β := (↑s : Type u_1) ⊕ (↑t : Type u_1)) Sum.inr
        ((⇑(sumSet (s := s) (t := t) h) : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α) ⁻¹' r)) =
    r ∩ t

Tactic:
simp [Set.ext_iff]

Premises used: Set.ext_iff
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
⊢ range (ι := (↑s : Type u_1) ⊕ (↑t : Type u_1))
      (⇑(sumSet (s := s) (t := t) h) : (a : (↑s : Type u_1) ⊕ (↑t : Type u_1)) → α) =
    s ∪ t

Tactic:
simp [Set.ext_iff]

Premises used: Set.ext_iff
-- Module: Mathlib.Logic.Embedding.Set
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
⊢ i = j

Tactic:
h.eq (not_disjoint_iff.2 ⟨_, hx, hx'⟩)

Premises used: Iff.mpr, Pairwise.eq, Set.not_disjoint_iff, And.intro, Exists.intro
-- Module: Mathlib.Logic.Embedding.Set
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
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'))
⊢ 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'))

Tactic:
obtain rfl : i = j := h.eq (not_disjoint_iff.2 ⟨_, hx, hx'⟩)

Premises used: Iff.mpr, Pairwise.eq, Set.not_disjoint_iff, And.intro, Exists.intro, rfl
-- Module: Mathlib.Logic.Embedding.Set
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
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:
rfl
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
ι : Type u_2
s : ι → Set α
h : Pairwise (Disjoint on s)
⊢ Eq (α := (a : (i : ι) × (↑(s i) : Type u_1)) → α) (⇑(sigmaSet (s := s) h) : (a : (i : ι) × (↑(s i) : Type u_1)) → α)
    fun (x : (i : ι) × (↑(s i) : Type u_1)) ↦ (↑(x.snd (β := fun (i : ι) ↦ (↑(s i) : Type u_1))) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
ι : Type u_2
s : ι → Set α
h : Pairwise (Disjoint on s)
i : ι
r : Set α
⊢ image (α := { x : α // x ∈ s i }) (Subtype.val (p := fun (x : α) ↦ x ∈ s i))
      (preimage (β := (i : ι) × (↑(s i) : Type u_1)) (Sigma.mk (β := fun (i : ι) ↦ (↑(s i) : Type u_1)) i)
        ((⇑(sigmaSet (s := s) h) : (a : (i : ι) × (↑(s i) : Type u_1)) → α) ⁻¹' r)) =
    r ∩ s i

Tactic:
simp [Set.ext_iff]

Premises used: Set.ext_iff
-- Module: Mathlib.Logic.Embedding.Set
Goal:
α : Type u_1
ι : Type u_2
s : ι → Set α
h : Pairwise (Disjoint on s)
⊢ Eq.{u_1 + 1} (α := Set α)
    (range (ι := (i : ι) × (↑(s i) : Type u_1)) (⇑(sigmaSet (s := s) h) : (a : (i : ι) × (↑(s i) : Type u_1)) → α))
    (⋃ (i : ι), s i)

Tactic:
simp [Set.ext_iff]

Premises used: Set.ext_iff
-- Module: Mathlib.Logic.Encodable.Basic
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
rw₂ rw₃ : some y = some y
⊢ some x = some y

Tactic:
rw [← encodek, e, encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
a b : α
⊢ encode a = encode b ↔ a = b

Tactic:
encode_injective.eq_iff

Premises used: Function.Injective.eq_iff, Encodable.encode_injective
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_3
inst : Encodable α
d x : α
simp_rw : (some x).getD d = x
⊢ (fun (n : ℕ) ↦ Option.getD (decode n) d) (encode x) = x

Tactic:
simp_rw [Encodable.encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_3
inst : Encodable α
d x : α
⊢ (some x).getD d = x

Tactic:
rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_3
inst : Encodable α
inst_1 : Inhabited α
⊢ Surjective.{1, u_3 + 1} (β := α) fun (n : ℕ) ↦ Option.getD (decode n) default

Tactic:
surjective_decode_getD α default

Premises used: Inhabited.default, Encodable.surjective_decode_getD
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
f : β → α
finv : α → Option β
linv : ∀ (b : β), finv (f b) = some b
b : β
⊢ (fun (n : ℕ) ↦ Option.bind (decode n) finv) ((fun (b : β) ↦ encode (f b)) b) = some b

Tactic:
simp [Encodable.encodek, linv]

Premises used: Encodable.encodek
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Encodable α
e : β ≃ α
b : β
⊢ encode b = encode.{u_3} (α := α) ((e : (a : β) → α) b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_3
β : Type u_4
inst : Encodable α
e : β ≃ α
n : ℕ
rw 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 : α) → β)))
⊢ 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))

Tactic:
rw [Option.map_eq_bind]

Premises used: Option.map_eq_bind
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
n : ℕ
⊢ encode n = n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
n : ℕ
⊢ decode n = some n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
x : PUnit.{u_3 + 1}
⊢ (fun (n : ℕ) ↦
        (Nat.casesOn (motive := fun (x : ℕ) ↦ Option PUnit.{u_3 + 1}) n (some PUnit.unit) fun (x : ℕ) ↦ none :
          Option PUnit.{u_3 + 1}))
      ((fun (x : PUnit.{u_3 + 1}) ↦ (0 : ℕ)) x) =
    some x

Tactic:
simp
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
⊢ encode PUnit.unit = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
⊢ decode 0 = some PUnit.unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
n : ℕ
⊢ Eq.{u_3 + 1} (α := Option PUnit.{u_3 + 1}) (decode n.succ) none

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Encodable.Basic
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 (Option.some Option.none) fun (m : ℕ) ↦
            Option.map Option.some (decode m) :
          Option (Option α)))
      ((fun (o : Option α) ↦
          (Option.casesOn (motive := fun (x : Option α) ↦ ℕ) o zero fun (a : α) ↦ (encode a).succ : ℕ))
        Option.none))
    (Option.some Option.none)
some :
  ∀ (val : α),
    (fun (n : ℕ) ↦
          (Nat.casesOn (motive := fun (x : ℕ) ↦ Option (Option α)) n (Option.some Option.none) fun (m : ℕ) ↦
              Option.map Option.some (decode m) :
            Option (Option α)))
        ((fun (o : Option α) ↦
            (Option.casesOn (motive := fun (x : Option α) ↦ ℕ) o zero fun (a : α) ↦ (encode a).succ : ℕ))
          (Option.some val)) =
      Option.some (Option.some val)
⊢ (fun (n : ℕ) ↦
        (Nat.casesOn (motive := fun (x : ℕ) ↦ Option (Option α)) n (Option.some Option.none) fun (m : ℕ) ↦
            Option.map Option.some (decode m) :
          Option (Option α)))
      ((fun (o : Option α) ↦
          (Option.casesOn (motive := fun (x : Option α) ↦ ℕ) o zero fun (a : α) ↦ (encode a).succ : ℕ))
        o) =
    Option.some o

Tactic:
cases o
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
⊢ 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:
simp [encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
val : α
⊢ (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 : ℕ))
        (some val)) =
    some (some val)

Tactic:
simp [encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
⊢ encode.{u_1} (α := Option α) none = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
a : α
⊢ encode (some a) = (encode a).succ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
⊢ Eq.{u_1 + 1} (α := Option (Option α)) (decode 0) (some none)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
n : ℕ
⊢ Eq.{u_1 + 1} (α := Option (Option α)) (decode n.succ) (Option.map some (decode n))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
n : ℕ
a : α
⊢ a ∈ decode₂ α n ↔ Membership.mem (γ := Option α) (decode n) a ∧ encode a = n

Tactic:
simp [decode₂, Option.bind_eq_some_iff]

Premises used: Encodable.decode₂, Option.bind_eq_some_iff
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
n : ℕ
a : α
⊢ a ∈ decode₂ α n ↔ encode a = n

Tactic:
mem_decode₂'.trans (and_iff_right_of_imp fun e => e ▸ encodek _)

Premises used: Encodable.mem_decode₂', Eq.rec, Encodable.encodek, Iff.trans, and_iff_right_of_imp
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
n : ℕ
a : α
⊢ decode₂ α n = some a ↔ encode a = n

Tactic:
mem_decode₂

Premises used: Encodable.mem_decode₂
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
a : α
⊢ decode₂ α (encode a) = some a

Tactic:
simp [decode₂_eq_some]

Premises used: Encodable.decode₂_eq_some
-- Module: Mathlib.Logic.Encodable.Basic
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
simp_rw₅ : (∃ (x : α), ¬¬encode x = n) ↔ ∃ (y : α), encode y = n
⊢ decode₂ α n ≠ none ↔ n ∈ Set.range.{0, u_1 + 1} (ι := α) encode

Tactic:
simp_rw [Set.range, Set.mem_setOf_eq, Ne, Option.eq_none_iff_forall_not_mem,
    Encodable.mem_decode₂, not_forall, not_not]

Premises used: Encodable.mem_decode₂, Classical.not_not, Ne, Set.mem_setOf_eq, Set.range, Option.eq_none_iff_forall_not_mem, Classical.not_forall
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
⊢ IsPartialInv encode (decode₂ α)

Tactic:
fun _ _ =>
  mem_decode₂

Premises used: Encodable.mem_decode₂, Function.IsPartialInv
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
n : ℕ
a₁ a₂ : α
h₁ : a₁ ∈ decode₂ α n
h₂ : a₂ ∈ decode₂ α n
⊢ a₁ = a₂

Tactic:
encode_injective <| (mem_decode₂.1 h₁).trans (mem_decode₂.1 h₂).symm

Premises used: Encodable.mem_decode₂, Encodable.encode_injective, Iff.mp, Eq.symm, Eq.trans
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
a : α
⊢ decode₂ α (encode a) = some a

Tactic:
mem_decode₂.2 rfl

Premises used: Iff.mpr, Encodable.mem_decode₂, rfl
-- Module: Mathlib.Logic.Encodable.Basic
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)
rw₁ rw₂ : decode₂ α x = decode₂ α x
⊢ encode ((decode₂ α x).get h) = x

Tactic:
rw [← decode₂_isPartialInv (Option.get _ h), Option.some_get]

Premises used: Option.some_get, Option.get, Encodable.decode₂_isPartialInv