awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Encodable.Basic
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
rw : (some n).isSome = true
⊢ (decode₂ α x).isSome = true

Tactic:
rw [← hn, encodek₂]

Premises used: Encodable.encodek₂
-- Module: Mathlib.Logic.Encodable.Basic
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
⊢ (some n).isSome = true

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Encodable.Basic
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
⊢ (some n).isSome = true

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Encodable α
n : (↑(Set.range.{0, u_3 + 1} (ι := α) encode) : Type)
obtain : ∀ (x : α) (hx : encode x = (↑n : ℕ)), (decode₂ α (↑n : ℕ)).isSome = true
⊢ (decode₂ α (↑n : ℕ)).isSome = true

Tactic:
obtain ⟨x, hx⟩ := n.2

Premises used: Subtype.property
-- Module: Mathlib.Logic.Encodable.Basic
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 : ℕ)
rw : (some x).isSome = true
⊢ (decode₂ α (↑n : ℕ)).isSome = true

Tactic:
rw [← hx, encodek₂]

Premises used: Encodable.encodek₂
-- Module: Mathlib.Logic.Encodable.Basic
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 : ℕ)
⊢ (some x).isSome = true

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Encodable.Basic
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 : ℕ)
⊢ (some x).isSome = true

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Encodable α
x : α
dsimp : (decode₂ α (encode x)).get ⋯ = 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

Tactic:
dsimp
-- Module: Mathlib.Logic.Encodable.Basic
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
rw₂ rw₃ : some x = some x
⊢ (decode₂ α (encode x)).get ⋯ = x

Tactic:
rw [← Option.some_inj, Option.some_get, encodek₂]

Premises used: Option.some_get, Encodable.encodek₂, Option.some_inj
-- Module: Mathlib.Logic.Encodable.Basic
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))
inr :
  ∀ (val : β), Eq (α := Option (α ⊕ β)) (decodeSum (encodeSum.{u_1, u_2} (α := α) (Sum.inr val))) (some (Sum.inr val))
⊢ decodeSum (encodeSum s) = some s

Tactic:
cases s
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
val : α
⊢ Eq (α := Option (α ⊕ β)) (decodeSum (encodeSum.{u_1, u_2} (β := β) (Sum.inl val))) (some (Sum.inl val))

Tactic:
simp [encodeSum, div2_val, decodeSum, encodek]

Premises used: Encodable.decodeSum, Nat.div2_val, Encodable.encodek, Encodable.encodeSum
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
val : β
⊢ Eq (α := Option (α ⊕ β)) (decodeSum (encodeSum.{u_1, u_2} (α := α) (Sum.inr val))) (some (Sum.inr val))

Tactic:
simp [encodeSum, div2_val, decodeSum, encodek]

Premises used: Encodable.decodeSum, Nat.div2_val, Encodable.encodek, Encodable.encodeSum
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
a : α
⊢ encode (α := α ⊕ β) (Sum.inl a) = 2 * encode a

Tactic:
rfl

Premises used: Encodable.encodeSum, rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
b : β
⊢ encode (α := α ⊕ β) (Sum.inr b) = 2 * encode b + 1

Tactic:
rfl

Premises used: Encodable.encodeSum, rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
n : ℕ
⊢ Eq (α := Option (α ⊕ β)) (decode n) (decodeSum n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
⊢ encode true = 1

Tactic:
rfl

Premises used: Encodable.encodeSum, rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
⊢ encode false = 0

Tactic:
rfl

Premises used: Encodable.encodeSum, rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
⊢ decode 0 = some false

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
⊢ decode 1 = some true

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
n : ℕ
h : 2 ≤ n
this : Eq (α := Option (Unit ⊕ Unit)) (decodeSum n) none
rw :
  Eq (α := Option Bool)
    (Option.bind (α := Unit ⊕ Unit) none (some ∘ (⇑Equiv.boolEquivPUnitSumPUnit.symm : (a : Unit ⊕ Unit) → Bool))) none
⊢ Eq (α := Option Bool)
    (Option.bind (α := Unit ⊕ Unit) (decodeSum n)
      (some ∘ (⇑Equiv.boolEquivPUnitSumPUnit.symm : (a : Unit ⊕ Unit) → Bool)))
    none

Tactic:
rw [this]
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
n : ℕ
h : 2 ≤ n
this : Eq (α := Option (Unit ⊕ Unit)) (decodeSum n) none
⊢ Eq (α := Option Bool)
    (Option.bind (α := Unit ⊕ Unit) none (some ∘ (⇑Equiv.boolEquivPUnitSumPUnit.symm : (a : Unit ⊕ Unit) → Bool))) none

Tactic:
rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
n : ℕ
h : 2 ≤ n
suffices : Eq (α := Option (Unit ⊕ Unit)) (decodeSum n) none
⊢ Eq (α := Option Bool) (decode n) none

Tactic:
suffices decodeSum n = none by
    change (decodeSum n).bind _ = none
    rw [this]
    rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
n : ℕ
h : 2 ≤ n
rw : HMul.hMul (α := ℕ) 1 2 ≤ n
rw₁ : LT.lt (α := ℕ) 0 2
⊢ 1 ≤ n / 2

Tactic:
rw [Nat.le_div_iff_mul_le]

Premises used: Nat.le_div_iff_mul_le
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
n : ℕ
h : 2 ≤ n
⊢ HMul.hMul (α := ℕ) 1 2 ≤ n

Tactic:
h
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
n : ℕ
h : 2 ≤ n
⊢ LT.lt (α := ℕ) 0 2

Tactic:
decide
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
n : ℕ
h : 2 ≤ n
⊢ HMul.hMul (α := ℕ) 1 2 ≤ n

Tactic:
exacts [h, by decide]
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
n : ℕ
h : 2 ≤ n
⊢ 1 ≤ n / 2

Tactic:
have : 1 ≤ n / 2 := by
    rw [Nat.le_div_iff_mul_le]
    exacts [h, by decide]
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
obtain : ∀ (m : ℕ) (e : n / 2 = m.succ), Eq (α := Option (Unit ⊕ Unit)) (decodeSum n) none
⊢ Eq (α := Option (Unit ⊕ Unit)) (decodeSum n) none

Tactic:
obtain ⟨m, e⟩ := exists_eq_succ_of_ne_zero (_root_.ne_of_gt this)

Premises used: ne_of_gt, Nat.exists_eq_succ_of_ne_zero
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
false :
  Eq (α := Option (Unit ⊕ Unit))
    (match (motive := Bool → ℕ → Option (Unit ⊕ Unit)) Bool.false, n / 2 with
      | Bool.false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m) :
      Option (Unit ⊕ Unit))
    (none : Option (Unit ⊕ Unit))
true :
  Eq (α := Option (Unit ⊕ Unit))
    (match (motive := Bool → ℕ → Option (Unit ⊕ Unit)) Bool.true, n / 2 with
      | Bool.false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m) :
      Option (Unit ⊕ Unit))
    (none : Option (Unit ⊕ Unit))
⊢ Eq (α := Option (Unit ⊕ Unit))
    (match (motive := Bool → ℕ → Option (Unit ⊕ Unit)) n.bodd, n / 2 with
      | Bool.false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m) :
      Option (Unit ⊕ Unit))
    (none : Option (Unit ⊕ Unit))

Tactic:
cases bodd n

Premises used: Nat.bodd
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ Eq (α := Option (Unit ⊕ Unit))
    (match (motive := Bool → ℕ → Option (Unit ⊕ Unit)) false, n / 2 with
      | false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m) :
      Option (Unit ⊕ Unit))
    (none : Option (Unit ⊕ Unit))

Tactic:
simp [e]
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = m.succ
⊢ Eq (α := Option (Unit ⊕ Unit))
    (match (motive := Bool → ℕ → Option (Unit ⊕ Unit)) true, n / 2 with
      | false, m => Option.map Sum.inl (decode m)
      | x, m => Option.map Sum.inr (decode m) :
      Option (Unit ⊕ Unit))
    (none : Option (Unit ⊕ Unit))

Tactic:
simp [e]
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : α → Type u_3
inst : Encodable α
inst_1 : (a : α) → Encodable (γ a)
x : Sigma γ
a : α
b : γ a
⊢ decodeSigma (γ := γ) (encodeSigma (γ := γ) (Sigma.mk (β := γ) a b)) = some (Sigma.mk (β := γ) a b)

Tactic:
simp [encodeSigma, decodeSigma, unpair_pair, encodek]

Premises used: Encodable.decodeSigma, Encodable.encodek, Encodable.encodeSigma, Nat.unpair_pair
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
γ : α → Type u_3
inst : Encodable α
inst_1 : (a : α) → Encodable (γ a)
n : ℕ
⊢ Eq (α := Option (Sigma γ)) (decode n)
    (Option.bind (decode (unpair n).1) fun (a : α) ↦ Option.map (Sigma.mk (β := γ) a) (decode (unpair n).2))

Tactic:
rfl

Premises used: Encodable.decodeSigma, rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
γ : α → Type u_3
inst : Encodable α
inst_1 : (a : α) → Encodable (γ a)
a : α
b : γ a
⊢ encode (Sigma.mk (β := γ) a b) = pair (encode a) (encode b)

Tactic:
rfl

Premises used: Nat.pair, Encodable.encodeSigma, rfl, ite
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
n : ℕ
simp :
  Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      (Option.bind (decode (unpair n).1) fun (a : α) ↦
        Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (decode (unpair n).2)))
    (Option.bind (decode (unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))
⊢ Eq (α := Option (α × β)) (decode n)
    (Option.bind (decode (unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))

Tactic:
simp only [decode_ofEquiv, Equiv.symm_symm, decode_sigma_val]

Premises used: Encodable.decode_sigma_val, Equiv.symm_symm, Encodable.decode_ofEquiv
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
n : ℕ
none :
  Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      (Option.bind Option.none fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (decode (unpair n).2)))
    (Option.bind Option.none fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))
some :
  ∀ (val : α),
    Eq (α := Option (α × β))
      (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
        ((Option.some val).bind fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (decode (unpair n).2)))
      ((Option.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))
⊢ Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      (Option.bind (decode (unpair n).1) fun (a : α) ↦
        Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (decode (unpair n).2)))
    (Option.bind (decode (unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))

Tactic:
cases (decode n.unpair.1 : Option α)

Premises used: Nat.unpair, Prod.fst, Encodable.decode
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
n : ℕ
none :
  Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      (Option.bind Option.none fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) Option.none))
    (Option.bind Option.none fun (a : α) ↦ Option.map (Prod.mk a) Option.none)
none₁ :
  ∀ (val : β),
    Eq (α := Option (α × β))
      (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
        (Option.bind Option.none fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (some val)))
      (Option.bind Option.none fun (a : α) ↦ Option.map (Prod.mk a) (some val))
⊢ Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      (Option.bind Option.none fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (decode (unpair n).2)))
    (Option.bind Option.none fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))

Tactic:
cases (decode n.unpair.2 : Option β)

Premises used: Nat.unpair, Encodable.decode, Prod.snd
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
n : ℕ
val : α
some :
  Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      ((Option.some val).bind fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) none))
    ((Option.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) none)
some₁ :
  ∀ (val_1 : β),
    Eq (α := Option (α × β))
      (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
        ((Option.some val).bind fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (Option.some val_1)))
      ((Option.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (Option.some val_1))
⊢ Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      ((Option.some val).bind fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (decode (unpair n).2)))
    ((Option.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (decode (unpair n).2))

Tactic:
cases (decode n.unpair.2 : Option β)

Premises used: Nat.unpair, Encodable.decode, Prod.snd
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
n : ℕ
⊢ Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      (Option.bind none fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) none))
    (Option.bind none fun (a : α) ↦ Option.map (Prod.mk a) none)

Tactic:
rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
n : ℕ
val : β
⊢ Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      (Option.bind none fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (some val)))
    (Option.bind none fun (a : α) ↦ Option.map (Prod.mk a) (some val))

Tactic:
rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
n : ℕ
val : α
⊢ Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      ((some val).bind fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) none))
    ((some val).bind fun (a : α) ↦ Option.map (Prod.mk a) none)

Tactic:
rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
n : ℕ
val : α
val_1 : β
⊢ Eq (α := Option (α × β))
    (Option.map (α := (_ : α) × β) (⇑(Equiv.sigmaEquivProd α β) : (a : (_ : α) × β) → α × β)
      ((some val).bind fun (a : α) ↦ Option.map (Sigma.mk (β := fun (x : α) ↦ β) a) (some val_1)))
    ((some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (some val_1))

Tactic:
rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Encodable β
a : α
b : β
⊢ encode (a, b) = pair (encode a) (encode b)

Tactic:
rfl

Premises used: Nat.pair, Encodable.encodeSigma, rfl, ite
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
P : α → Prop
encA : Encodable α
decP : DecidablePred P
x : { a : α // P a }
v : α
h : P v
⊢ decodeSubtype (P := P) (encodeSubtype (P := P) (Subtype.mk (p := fun (a : α) ↦ P a) v h)) =
    some (Subtype.mk (p := fun (a : α) ↦ P a) v h)

Tactic:
simp [encodeSubtype, decodeSubtype, encodek, h]

Premises used: Encodable.decodeSubtype, Encodable.encodek, Encodable.encodeSubtype
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
P : α → Prop
encA : Encodable α
decP : DecidablePred P
a : Subtype P
mk :
  ∀ (val : α) (property : P val),
    encode (Subtype.mk (p := P) val property) = encode (↑(Subtype.mk (p := P) val property) : α)
⊢ encode a = encode (↑a : α)

Tactic:
cases a
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
P : α → Prop
encA : Encodable α
decP : DecidablePred P
val : α
property : P val
⊢ encode (Subtype.mk (p := P) val property) = encode (↑(Subtype.mk (p := P) val property) : α)

Tactic:
rfl
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
⊢ Nonempty.{u_1 + 1} (Encodable α) ↔ Countable α

Tactic:
⟨fun ⟨h⟩ => @Encodable.countable α h, fun h => ⟨@ofCountable _ h⟩⟩

Premises used: _private.0.Encodable.nonempty_encodable.match_1, Nonempty.intro, Encodable.ofCountable, Iff.intro, Countable, Encodable.countable
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Countable α
⊢ Nonempty.{u_1 + 1} (Encodable α)

Tactic:
⟨Encodable.ofCountable _⟩

Premises used: Nonempty.intro, Encodable.ofCountable
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
⊢ Countable { n : ℕ // 0 < n }

Tactic:
infer_instance
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
⊢ DecidableEq (↑(Set.range.{0, u_1 + 1} (ι := α) Encodable.encode) : Type)

Tactic:
exact Encodable.decidableEqOfEncodable _

Premises used: Encodable.decidableEqOfEncodable
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
⊢ Encodable (↑(Set.range.{0, u_1 + 1} (ι := α) Encodable.encode) : Type)

Tactic:
infer_instance
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
a : ULower α
⊢ down a.up = a

Tactic:
Equiv.right_inv _ _

Premises used: Equiv.right_inv, ULower.up, ULower.down
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
a : α
⊢ up (down a) = a

Tactic:
simp [up, down, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, ULower.up, ULower.down
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
a b : ULower α
⊢ a.up = b.up ↔ a = b

Tactic:
Equiv.apply_eq_iff_eq _

Premises used: ULower.up, Equiv.apply_eq_iff_eq
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
a b : α
⊢ Eq (α := ULower α) (down a) (down b) ↔ a = b

Tactic:
Equiv.apply_eq_iff_eq _

Premises used: Equiv.apply_eq_iff_eq, ULower.down
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
a b : ULower α
⊢ a.up = b.up → a = b

Tactic:
up_eq_up.1

Premises used: Iff.mp, ULower.up_eq_up
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
p : α → Prop
inst : Encodable α
inst_1 : DecidablePred p
h : ∃ (x : α), p x
w : α
pw : p w
⊢ good p (decode (encode w))

Tactic:
simp [good, encodek, pw]

Premises used: _private.0.Encodable.good, Encodable.encodek
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
p : α → Prop
inst : Encodable α
inst_1 : DecidablePred p
h : ∃ (x : α), p x
⊢ p (choose (p := p) h)

Tactic:
(chooseX h).2

Premises used: Encodable.choose, Encodable.chooseX, Subtype.property
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : α → Type u_2
R : (x : α) → β x → Prop
inst : (a : α) → Encodable (β a)
inst_1 : (x : α) → (y : β x) → Decidable (R x y)
H : ∀ (x : α), ∃ (y : β x), R x y
⊢ ∃ (f : (a : α) → β a), ∀ (x : α), R x (f x)

Tactic:
⟨fun x => choose (H x), fun x => choose_spec (H x)⟩

Premises used: Encodable.choose, Encodable.choose_spec, Exists.intro
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : α → Type u_2
P : (x : α) → β x → Prop
inst : (a : α) → Encodable (β a)
inst_1 : (x : α) → (y : β x) → Decidable (P x y)
⊢ (∀ (x : α), ∃ (y : β x), P x y) ↔ ∃ (f : (a : α) → β a), ∀ (x : α), P x (f x)

Tactic:
⟨axiom_of_choice, fun ⟨_, H⟩ x => ⟨_, H x⟩⟩

Premises used: Encodable.axiom_of_choice, Exists, _private.0.Encodable.skolem.match_1, Iff.intro, Exists.intro
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
⊢ Std.Antisymm (α := α) ((⇑(encode' α) : (a : α) → ℕ) ⁻¹'o fun (x1 x2 : ℕ) ↦ x1 ≤ x2)

Tactic:
(RelEmbedding.preimage _ _).antisymm

Premises used: RelEmbedding.antisymm, RelEmbedding.preimage, Order.Preimage
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
inst : Encodable α
⊢ Std.Total (α := α) ((⇑(encode' α) : (a : α) → ℕ) ⁻¹'o fun (x1 x2 : ℕ) ↦ x1 ≤ x2)

Tactic:
(RelEmbedding.preimage _ _).total

Premises used: RelEmbedding.total, RelEmbedding.preimage, Order.Preimage
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
dsimp :
  r (f (Directed.sequence (r := r) f hf n))
    (f
      (match (motive := Option α → α) decode n with
      | none =>
        Classical.choose (p := fun (x : α) ↦
          r (f (Directed.sequence (r := r) f hf n)) (f x) ∧ r (f (Directed.sequence (r := r) f hf n)) (f x)) ⋯
      | some a =>
        Classical.choose (p := fun (x : α) ↦ r (f (Directed.sequence (r := r) f hf n)) (f x) ∧ r (f a) (f x)) ⋯))
⊢ r (f (Directed.sequence (r := r) f hf n)) (f (Directed.sequence (r := r) f hf (n + 1)))

Tactic:
dsimp [Directed.sequence]

Premises used: Directed.sequence
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
generalize :
  ∀ (p : α),
    r (f p)
      (f
        (match (motive := Option α → α) decode n with
        | none => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f p) (f x)) ⋯
        | some a => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f a) (f x)) ⋯))
⊢ r (f (Directed.sequence (r := r) f hf n))
    (f
      (match (motive := Option α → α) decode n with
      | none =>
        Classical.choose (p := fun (x : α) ↦
          r (f (Directed.sequence (r := r) f hf n)) (f x) ∧ r (f (Directed.sequence (r := r) f hf n)) (f x)) ⋯
      | some a =>
        Classical.choose (p := fun (x : α) ↦ r (f (Directed.sequence (r := r) f hf n)) (f x) ∧ r (f a) (f x)) ⋯))

Tactic:
generalize hf.sequence f n = p

Premises used: Directed.sequence
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
none :
  r (f p)
    (f
      (match (motive := Option α → α) Option.none with
      | Option.none => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f p) (f x)) ⋯
      | Option.some a => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f a) (f x)) ⋯))
some :
  ∀ (a : α),
    r (f p)
      (f
        (match (motive := Option α → α) Option.some a with
        | Option.none => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f p) (f x)) ⋯
        | Option.some a => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f a) (f x)) ⋯))
⊢ r (f p)
    (f
      (match (motive := Option α → α) decode n with
      | Option.none => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f p) (f x)) ⋯
      | Option.some a => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f a) (f x)) ⋯))

Tactic:
rcases (decode n : Option α) with - | a

Premises used: Encodable.decode