awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
pos : ∀ (hp : P), (if P ∧ Q then a else b) = if P then if Q then a else b else b
neg : ∀ (hp : ¬P), (if P ∧ Q then a else b) = if P then if Q then a else b else b
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
by_cases hp : P
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : P
pos : ∀ (hq : Q), (if P ∧ Q then a else b) = if P then if Q then a else b else b
neg : ∀ (hq : ¬Q), (if P ∧ Q then a else b) = if P then if Q then a else b else b
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
by_cases hq : Q
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : ¬P
pos : ∀ (hq : Q), (if P ∧ Q then a else b) = if P then if Q then a else b else b
neg : ∀ (hq : ¬Q), (if P ∧ Q then a else b) = if P then if Q then a else b else b
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
by_cases hq : Q
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : P
hq : Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
simp [hp, hq]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : P
hq : ¬Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
simp [hp, hq]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : ¬P
hq : Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
simp [hp, hq]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : ¬P
hq : ¬Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
simp [hp, hq]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
pos : ∀ (hp : P), (if P ∨ Q then a else b) = if P then a else if Q then a else b
neg : ∀ (hp : ¬P), (if P ∨ Q then a else b) = if P then a else if Q then a else b
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
by_cases hp : P
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : P
pos : ∀ (hq : Q), (if P ∨ Q then a else b) = if P then a else if Q then a else b
neg : ∀ (hq : ¬Q), (if P ∨ Q then a else b) = if P then a else if Q then a else b
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
by_cases hq : Q
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : ¬P
pos : ∀ (hq : Q), (if P ∨ Q then a else b) = if P then a else if Q then a else b
neg : ∀ (hq : ¬Q), (if P ∨ Q then a else b) = if P then a else if Q then a else b
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
by_cases hq : Q
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : P
hq : Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
simp [hp, hq]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : P
hq : ¬Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
simp [hp, hq]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : ¬P
hq : Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
simp [hp, hq]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : ¬P
hq : ¬Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
simp [hp, hq]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
A : P → α
inst_1 : Decidable Q
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
⊢ Eq.{u_1} (α := α) (if p : P then A p else if q : Q then B q else C p q)
    (if q : Q then B q else if p : P then A p else C p q)

Tactic:
grind
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b c : α
inst_1 : Decidable Q
h : P → ¬Q
⊢ (if P then a else if Q then b else c) = if Q then b else if P then a else c

Tactic:
dite_dite_comm P Q h

Premises used: dite_dite_comm, ite
-- Module: Mathlib.Logic.Basic
Goal:
P Q R : Prop
inst : Decidable P
pos : ∀ (p : P), (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R
neg : ∀ (p : ¬P), (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R

Tactic:
by_cases p : P
-- Module: Mathlib.Logic.Basic
Goal:
P Q R : Prop
inst : Decidable P
p : P
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R

Tactic:
simp [p]
-- Module: Mathlib.Logic.Basic
Goal:
P Q R : Prop
inst : Decidable P
p : ¬P
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R

Tactic:
simp [p]
-- Module: Mathlib.Logic.Basic
Goal:
P : Prop
inst : Decidable P
Q : P → Prop
R : ¬P → Prop
pos : ∀ (h : P), dite P Q R ↔ (∃ (p : P), Q p) ∨ ∃ (p : ¬P), R p
neg : ∀ (h : ¬P), dite P Q R ↔ (∃ (p : P), Q p) ∨ ∃ (p : ¬P), R p
⊢ dite P Q R ↔ (∃ (p : P), Q p) ∨ ∃ (p : ¬P), R p

Tactic:
by_cases h : P
-- Module: Mathlib.Logic.Basic
Goal:
P : Prop
inst : Decidable P
Q : P → Prop
R : ¬P → Prop
h : P
⊢ dite P Q R ↔ (∃ (p : P), Q p) ∨ ∃ (p : ¬P), R p

Tactic:
simp [h, exists_prop_of_false, exists_prop_of_true]

Premises used: exists_prop_of_false, exists_prop_of_true
-- Module: Mathlib.Logic.Basic
Goal:
P : Prop
inst : Decidable P
Q : P → Prop
R : ¬P → Prop
h : ¬P
⊢ dite P Q R ↔ (∃ (p : P), Q p) ∨ ∃ (p : ¬P), R p

Tactic:
simp [h, exists_prop_of_false, exists_prop_of_true]

Premises used: exists_prop_of_false, exists_prop_of_true
-- Module: Mathlib.Logic.Basic
Goal:
P Q R : Prop
inst : Decidable P
pos : ∀ (p : P), (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)
neg : ∀ (p : ¬P), (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)

Tactic:
by_cases p : P
-- Module: Mathlib.Logic.Basic
Goal:
P Q R : Prop
inst : Decidable P
p : P
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)

Tactic:
simp [p]
-- Module: Mathlib.Logic.Basic
Goal:
P Q R : Prop
inst : Decidable P
p : ¬P
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)

Tactic:
simp [p]
-- Module: Mathlib.Logic.Basic
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
neg : ∀ (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

Tactic:
by_cases h : P
-- Module: Mathlib.Logic.Basic
Goal:
P : Prop
inst : Decidable P
Q : P → Prop
R : ¬P → Prop
h : P
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h

Tactic:
simp [h, forall_prop_of_false, forall_prop_of_true]

Premises used: forall_prop_of_false, forall_prop_of_true
-- Module: Mathlib.Logic.Basic
Goal:
P : Prop
inst : Decidable P
Q : P → Prop
R : ¬P → Prop
h : ¬P
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h

Tactic:
simp [h, forall_prop_of_false, forall_prop_of_true]

Premises used: forall_prop_of_false, forall_prop_of_true
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
inst_1 : Decidable Q
x y u v : α
h_c : P ↔ Q
h_t : Q → x = u
h_e : ¬Q → y = v
⊢ (if P then x else y) = if Q then u else v

Tactic:
ite_congr h_c.eq h_t h_e

Premises used: ite_congr, Iff.eq
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
inst_1 : Decidable Q
x y u v : α
h_c : P ↔ Q
h_t : x = u
h_e : y = v
⊢ (if P then x else y) = if Q then u else v

Tactic:
if_ctx_congr h_c (fun _ ↦ h_t) (fun _ ↦ h_e)

Premises used: if_ctx_congr
-- Module: Mathlib.Logic.Basic
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
inr : ∀ (hx : ¬p x), x = y
⊢ x = y

Tactic:
rcases em (p x) with (hx | hx)

Premises used: em
-- Module: Mathlib.Logic.Basic
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
inl₁ : ∀ (hy : ¬p y), x = y
⊢ x = y

Tactic:
rcases em (p y) with (hy | hy)

Premises used: em
-- Module: Mathlib.Logic.Basic
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
inr₁ : ∀ (hy : ¬p y), x = y
⊢ x = y

Tactic:
rcases em (p y) with (hy | hy)

Premises used: em
-- Module: Mathlib.Logic.Basic
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
hy : p y
⊢ x = y

Tactic:
grind
-- Module: Mathlib.Logic.Basic
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
hy : ¬p y
⊢ x = y

Tactic:
grind
-- Module: Mathlib.Logic.Basic
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
hy : p y
⊢ x = y

Tactic:
grind
-- Module: Mathlib.Logic.Basic
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
hy : ¬p y
⊢ x = y

Tactic:
grind
-- Module: Mathlib.Logic.Basic
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
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
⊢ 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
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Membership α β
p : Prop
inst_1 : Decidable p
a : α
s : p → β
t : ¬p → β
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:
simp [h]
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Membership α β
p : Prop
inst_1 : Decidable p
a : α
s : p → β
t : ¬p → β
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:
simp [h]
-- Module: Mathlib.Logic.Basic
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
neg : ∀ (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

Tactic:
by_cases h : p
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Membership α β
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
s : β
h : p
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s

Tactic:
simp [h]
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Membership α β
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
s : β
h : ¬p
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s

Tactic:
simp [h]
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Membership α β
p : Prop
inst_1 : Decidable p
a : α
s t : β
⊢ (a ∈ if p then s else t) ↔ (p → a ∈ s) ∧ (¬p → a ∈ t)

Tactic:
mem_dite

Premises used: mem_dite, ite
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Membership α β
p : Prop
inst_1 : Decidable p
a b : α
s : β
⊢ (if p then a else b) ∈ s ↔ (p → a ∈ s) ∧ (¬p → b ∈ s)

Tactic:
dite_mem

Premises used: dite_mem, ite
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
inst : BEq α
inst_1 : LawfulBEq α
a b : α
ne : a ≠ b
⊢ ¬(a == b) = true

Tactic:
fun h => ne (eq_of_beq h)

Premises used: LawfulBEq.eq_of_beq, Not
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
β : Type u_2
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
a₁ a₂ : α
b₁ b₂ : β
rw : ((a₁ == a₂) = true ↔ (b₁ == b₂) = true) ↔ (a₁ = a₂ ↔ b₁ = b₂)
⊢ (a₁ == a₂) = (b₁ == b₂) ↔ (a₁ = a₂ ↔ b₁ = b₂)

Tactic:
rw [Bool.eq_iff_iff]

Premises used: Bool.eq_iff_iff
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
β : Type u_2
inst : BEq α
inst_1 : LawfulBEq α
inst_2 : BEq β
inst_3 : LawfulBEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ ((a₁ == a₂) = true ↔ (b₁ == b₂) = true) ↔ (a₁ = a₂ ↔ b₁ = b₂)

Tactic:
simp
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
inst1 inst2 : BEq α
h : ∀ (x y : α), (x == y) = (x == y)
have : ∀ (beq1 : α → α → Bool) (h : ∀ (x y : α), (x == y) = (x == y)), { beq := beq1 : BEq α } = inst2
⊢ inst1 = inst2

Tactic:
have ⟨beq1⟩ := inst1
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
inst1 inst2 : BEq α
beq1 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
e_beq : beq1 = BEq.beq
⊢ { beq := beq1 : BEq α } = inst2

Tactic:
congr
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
inst1 inst2 : BEq α
beq1 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
e_beq : ∀ (x y : α), beq1 x y = (x == y)
⊢ beq1 = BEq.beq

Tactic:
funext x y
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
inst1 inst2 : BEq α
beq1 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
x y : α
⊢ beq1 x y = (x == y)

Tactic:
h x y
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
inst1 inst2 : BEq α
beq1 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
x y : α
⊢ beq1 x y = (x == y)

Tactic:
exact h x y
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
inst1 inst2 : BEq α
inst : LawfulBEq α
inst_1 : LawfulBEq α
h : ∀ (x y : α), (x == y) = (x == y)
⊢ inst1 = inst2

Tactic:
ext
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
inst1 inst2 : BEq α
inst : LawfulBEq α
inst_1 : LawfulBEq α
x y : α
⊢ (x == y) = (x == y)

Tactic:
simp
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_3
inst : Denumerable α
n : ℕ
⊢ Option.isSome.{u_3} (α := α) (decode n) = true

Tactic:
Option.isSome_iff_exists.2 <| (decode_inv n).imp fun _ => And.left

Premises used: Iff.mpr, Exists.imp, Option.isSome_iff_exists, And.left, Denumerable.decode_inv
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_3
inst : Denumerable α
n : ℕ
⊢ decode n = some (ofNat α n)

Tactic:
Option.eq_some_of_isSome _

Premises used: Option.eq_some_of_isSome, Denumerable.ofNat
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
inst : Denumerable α
n : ℕ
b : α
h : decode n = some b
⊢ ofNat α n = b

Tactic:
simpa using h
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
inst : Denumerable α
n : ℕ
obtain : ∀ (a : α) (h : Membership.mem (γ := Option α) (decode n) a) (e : encode a = n), encode (ofNat α n) = n
⊢ encode (ofNat α n) = n

Tactic:
obtain ⟨a, h, e⟩ := decode_inv (α := α) n

Premises used: Denumerable.decode_inv
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
inst : Denumerable α
n : ℕ
a : α
h : Membership.mem (γ := Option α) (decode n) a
e rwa rwa₁ rwa₂ rwa₃ : encode a = n
⊢ encode (ofNat α n) = n

Tactic:
rwa [ofNat_of_decode h]

Premises used: Denumerable.ofNat_of_decode
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
inst : Denumerable α
a : α
⊢ ofNat α (encode a) = a

Tactic:
ofNat_of_decode (encodek _)

Premises used: Encodable.encodek, Denumerable.ofNat_of_decode
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
⊢ Infinite α

Tactic:
Infinite.of_surjective _ (eqv α).surjective

Premises used: Denumerable.eqv, Equiv.surjective, Infinite.of_surjective
-- Module: Mathlib.Logic.Denumerable
Goal:
α_1 : Type u_1
β_1 : Type u_2
inst : Denumerable α_1
inst_1 : Denumerable β_1
α : Type u_3
β : Type u_4
inst_2 : Denumerable α
e : β ≃ α
n : ℕ
⊢ ∃ (a : β), Membership.mem (γ := Option β) (decode n) a ∧ encode a = n

Tactic:
simp [decode_ofEquiv, encode_ofEquiv]

Premises used: Encodable.decode_ofEquiv, Encodable.encode_ofEquiv
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_3
β : Type u_4
inst : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ ofNat β n = (e.symm : (a : α) → β) (ofNat α n)

Tactic:
ofNat_of_decode ?_

Premises used: Denumerable.ofNat_of_decode
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_3
β : Type u_4
inst : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
refine : Eq.{u_4 + 1} (α := Option β) (decode n : Option β) (some ((e.symm : (a : α) → β) (ofNat α n)) : Option β)
⊢ ofNat β n = (e.symm : (a : α) → β) (ofNat α n)

Tactic:
refine ofNat_of_decode ?_

Premises used: Denumerable.ofNat_of_decode
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_3
β : Type u_4
inst : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
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 β)
⊢ Eq.{u_4 + 1} (α := Option β) (decode n : Option β) (some ((e.symm : (a : α) → β) (ofNat α n)) : Option β)

Tactic:
rw [decode_ofEquiv e]

Premises used: Encodable.decode_ofEquiv
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_3
β : Type u_4
inst : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ 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:
simp
-- Module: Mathlib.Logic.Denumerable
Goal:
n : ℕ
⊢ ofNat ℕ n = n

Tactic:
rfl

Premises used: rfl, Denumerable.ofNat
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
⊢ ∃ (a : Option α), Membership.mem (γ := Option (Option α)) (decode 0) a ∧ encode a = 0

Tactic:
⟨none, ?_, encode_none⟩

Premises used: Option.none, And.intro, Exists.intro, Encodable.encode_none
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
zero : Membership.mem (γ := Option (Option α)) (decode 0) none
⊢ ∃ (a : Option α), Membership.mem (γ := Option (Option α)) (decode 0) a ∧ encode a = 0

Tactic:
refine ⟨none, ?_, encode_none⟩
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
zero : Membership.mem (γ := Option (Option α)) (some none) none
zero₁ zero₂ : Eq.{u_1 + 1} (α := Option (Option α)) (some none) (some none)
⊢ Membership.mem (γ := Option (Option α)) (decode 0) none

Tactic:
rw [decode_option_zero, Option.mem_def]

Premises used: Encodable.decode_option_zero, Option.mem_def
-- Module: Mathlib.Logic.Denumerable
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

Tactic:
⟨some (ofNat α n), ?_, ?_⟩

Premises used: Option.some, And.intro, Exists.intro, Denumerable.ofNat
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
succ : Membership.mem (γ := Option (Option α)) (decode (n + 1)) (some (ofNat α n))
succ₁ : encode (some (ofNat α n)) = n + 1
⊢ ∃ (a : Option α), Membership.mem (γ := Option (Option α)) (decode (n + 1)) a ∧ encode a = n + 1

Tactic:
refine ⟨some (ofNat α n), ?_, ?_⟩
-- Module: Mathlib.Logic.Denumerable
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))
succ₃ succ₄ : some (some (ofNat α n)) = some (some (ofNat α n))
⊢ Membership.mem (γ := Option (Option α)) (decode (n + 1)) (some (ofNat α n))

Tactic:
rw [decode_option_succ, decode_eq_ofNat, Option.map_some, Option.mem_def]

Premises used: Encodable.decode_option_succ, Denumerable.decode_eq_ofNat, Option.map_some, Option.mem_def
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
succ : (encode (ofNat α n)).succ = n + 1
succ₁ succ₂ : n.succ = n + 1
⊢ encode (some (ofNat α n)) = n + 1

Tactic:
rw [encode_some, encode_ofNat]

Premises used: Denumerable.encode_ofNat, Encodable.encode_some
-- Module: Mathlib.Logic.Denumerable
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
succ : ∀ (n : ℕ), ∃ (a : Option α), Membership.mem (γ := Option (Option α)) (decode (n + 1)) a ∧ encode a = n + 1
⊢ ∃ (a : Option α), Membership.mem (γ := Option (Option α)) (decode n) a ∧ encode a = n

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]

Premises used: Encodable.decode_option_zero, Denumerable.encode_ofNat, Encodable.decode_option_succ, Denumerable.decode_eq_ofNat, Option.map_some, Nat.zero, Nat.succ, Encodable.encode_some, Option.mem_def
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
this : ∃ (a : α ⊕ β), Membership.mem (γ := Option (α ⊕ β)) (decodeSum n) a ∧ encodeSum a = bit n.bodd n.div2
⊢ ∃ (a : α ⊕ β), Membership.mem (γ := Option (α ⊕ β)) (decode n) a ∧ encode a = n

Tactic:
simpa [bit_bodd_div2]

Premises used: Nat.bit_bodd_div2
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
suffices : ∃ (a : α ⊕ β), Membership.mem (γ := Option (α ⊕ β)) (decodeSum n) a ∧ encodeSum a = bit n.bodd n.div2
⊢ ∃ (a : α ⊕ β), Membership.mem (γ := Option (α ⊕ β)) (decode n) a ∧ encode a = n

Tactic:
suffices ∃ a ∈ @decodeSum α β _ _ n, encodeSum a = bit (bodd n) (div2 n) by
      simpa [bit_bodd_div2]
-- Module: Mathlib.Logic.Denumerable
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
n : ℕ
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
⊢ ∃ (a : α ⊕ β), Membership.mem (γ := Option (α ⊕ β)) (decodeSum n) a ∧ encodeSum a = bit n.bodd n.div2

Tactic:
simp only [decodeSum, decode_eq_ofNat, Option.map_some, Sum.exists]

Premises used: Encodable.decodeSum, Denumerable.decode_eq_ofNat, Sum.exists, Option.map_some