awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun (a : β) ↦ g a = true
hf : ∀ (a : α), p a ↔ (fun (a : β) ↦ g a = true) (f a)
⊢ Computable (σ := Bool) fun (a : α) ↦ decide ((fun (a : α) ↦ ((fun (a : β) ↦ g a = true) (f a) : Prop)) a)

Tactic:
simpa using hg.comp c

Premises used: Computable.comp
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α → Prop
f : α → β
c : Computable f
g : β → Bool
hg : Computable g
h₂ : ComputablePred fun (a : β) ↦ g a = true
hf : ∀ (a : α), p a ↔ (fun (a : β) ↦ g a = true) (f a)
⊢ ComputablePred fun (a : α) ↦ (fun (a : β) ↦ g a = true) (f a)

Tactic:
exact ⟨by infer_instance, by simpa using hg.comp c⟩
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α → Prop
q : β → Prop
h : p ≤₁ q
⊢ ComputablePred q → ComputablePred p

Tactic:
computable_of_manyOneReducible h.to_many_one

Premises used: OneOneReducible.to_many_one, ComputablePred.computable_of_manyOneReducible
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
⊢ ManyOneEquiv p p

Tactic:
⟨manyOneReducible_refl _, manyOneReducible_refl _⟩

Premises used: ManyOneEquiv, manyOneReducible_refl, And.intro
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α → Prop
q : β → Prop
⊢ ManyOneEquiv p q → ManyOneEquiv q p

Tactic:
And.symm

Premises used: ManyOneEquiv, And.symm
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
inst : Primcodable α
⊢ Equivalence.{u_1 + 1} (α := α → Prop) ManyOneEquiv

Tactic:
⟨manyOneEquiv_refl, fun {_ _} => ManyOneEquiv.symm, fun {_ _ _} => ManyOneEquiv.trans⟩

Premises used: ManyOneEquiv.symm, manyOneEquiv_refl, Equivalence.mk, ManyOneEquiv.trans
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
⊢ OneOneEquiv p p

Tactic:
⟨oneOneReducible_refl _, oneOneReducible_refl _⟩

Premises used: OneOneEquiv, oneOneReducible_refl, And.intro
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α → Prop
q : β → Prop
⊢ OneOneEquiv p q → OneOneEquiv q p

Tactic:
And.symm

Premises used: OneOneEquiv, And.symm
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
inst : Primcodable α
⊢ Equivalence.{u_1 + 1} (α := α → Prop) OneOneEquiv

Tactic:
⟨oneOneEquiv_refl, fun {_ _} => OneOneEquiv.symm, fun {_ _ _} => OneOneEquiv.trans⟩

Premises used: OneOneEquiv.symm, oneOneEquiv_refl, OneOneEquiv.trans, Equivalence.mk
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
e : α ≃ β
⊢ e.Computable → e.symm.Computable

Tactic:
And.symm

Premises used: Equiv.Computable, And.symm
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
inst : Denumerable α
⊢ (Denumerable.eqv α).Computable

Tactic:
⟨Computable.encode, Computable.ofNat _⟩

Premises used: Computable.encode, Computable.ofNat, Equiv.Computable, And.intro
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Denumerable α
inst_1 : Denumerable β
⊢ (Denumerable.equiv₂ α β).Computable

Tactic:
(Computable.eqv _).trans (Computable.eqv _).symm

Premises used: Denumerable.equiv₂, Equiv.Computable.symm, Computable.eqv, Equiv.Computable.trans
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
e : α ≃ β
h : e.Computable
p : β → Prop
⊢ OneOneEquiv.{u_1, u_2} (α := α) (p ∘ (⇑e : (a : α) → β)) p

Tactic:
⟨OneOneReducible.of_equiv _ h.1, OneOneReducible.of_equiv_symm _ h.2⟩

Premises used: OneOneReducible.of_equiv, OneOneReducible.of_equiv_symm, OneOneEquiv, And.right, And.left, And.intro
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
e : α ≃ β
h : e.Computable
p : β → Prop
⊢ ManyOneEquiv.{u_1, u_2} (α := α) (p ∘ (⇑e : (a : α) → β)) p

Tactic:
(OneOneEquiv.of_equiv h).to_many_one

Premises used: OneOneEquiv.to_many_one, OneOneEquiv.of_equiv
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
h : ManyOneEquiv p q
⊢ p ≤₀ r ↔ q ≤₀ r

Tactic:
⟨h.2.trans, h.1.trans⟩

Premises used: ManyOneReducible.trans, And.right, And.left, Iff.intro
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
h : ManyOneEquiv q r
⊢ p ≤₀ q ↔ p ≤₀ r

Tactic:
⟨fun h' => h'.trans h.1, fun h' => h'.trans h.2⟩

Premises used: ManyOneReducible.trans, And.right, And.left, Iff.intro
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
h : OneOneEquiv p q
⊢ p ≤₁ r ↔ q ≤₁ r

Tactic:
⟨h.2.trans, h.1.trans⟩

Premises used: OneOneReducible.trans, And.right, And.left, Iff.intro
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
h : OneOneEquiv q r
⊢ p ≤₁ q ↔ p ≤₁ r

Tactic:
⟨fun h' => h'.trans h.1, fun h' => h'.trans h.2⟩

Premises used: OneOneReducible.trans, And.right, And.left, Iff.intro
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
h : ManyOneEquiv p q
⊢ ManyOneEquiv p r ↔ ManyOneEquiv q r

Tactic:
and_congr h.le_congr_left h.le_congr_right

Premises used: ManyOneEquiv.le_congr_right, ManyOneEquiv, ManyOneEquiv.le_congr_left, and_congr
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
h : ManyOneEquiv q r
⊢ ManyOneEquiv p q ↔ ManyOneEquiv p r

Tactic:
and_congr h.le_congr_right h.le_congr_left

Premises used: ManyOneEquiv.le_congr_right, ManyOneEquiv, ManyOneEquiv.le_congr_left, and_congr
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
h : OneOneEquiv p q
⊢ OneOneEquiv p r ↔ OneOneEquiv q r

Tactic:
and_congr h.le_congr_left h.le_congr_right

Premises used: OneOneEquiv.le_congr_left, OneOneEquiv, OneOneEquiv.le_congr_right, and_congr
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
h : OneOneEquiv q r
⊢ OneOneEquiv p q ↔ OneOneEquiv p r

Tactic:
and_congr h.le_congr_right h.le_congr_left

Premises used: OneOneEquiv.le_congr_left, OneOneEquiv, OneOneEquiv.le_congr_right, and_congr
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
inst : Primcodable α
⊢ Equiv.Computable (β := ULower α) (equiv α)

Tactic:
⟨Primrec.ulower_down.to_comp, Primrec.ulower_up.to_comp⟩

Premises used: Primrec.to_comp, Equiv.Computable, Primrec.ulower_up, And.intro, Primrec.ulower_down
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
⊢ ManyOneEquiv (α := ULower α) (p ∘ ULower.up) p

Tactic:
ManyOneEquiv.of_equiv ULower.down_computable.symm

Premises used: ULower.up, ULower.down_computable, ManyOneEquiv.of_equiv, Equiv.Computable.symm
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α → Prop
q : β → Prop
⊢ p ≤₁ p ⊕' q

Tactic:
⟨Sum.inl, Computable.sumInl, fun _ _ => Sum.inl.inj_iff.1, fun _ => Iff.rfl⟩

Premises used: OneOneReducible, Iff.rfl, Sum.inl, Computable.sumInl, And.intro, Exists.intro, Iff.mp, Sum.inl.inj_iff
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α → Prop
q : β → Prop
⊢ q ≤₁ p ⊕' q

Tactic:
⟨Sum.inr, Computable.sumInr, fun _ _ => Sum.inr.inj_iff.1, fun _ => Iff.rfl⟩

Premises used: OneOneReducible, Iff.rfl, Computable.sumInr, Sum.inr, And.intro, Sum.inr.inj_iff, Exists.intro, Iff.mp
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → γ
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ r (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
x : α ⊕ β
inl : ∀ (val : α), (p ⊕' q) (Sum.inl val) ↔ r ((f ⊕' g) (Sum.inl val))
inr : ∀ (val : β), (p ⊕' q) (Sum.inr val) ↔ r ((f ⊕' g) (Sum.inr val))
⊢ (p ⊕' q) x ↔ r ((f ⊕' g) x)

Tactic:
cases x
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → γ
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ r (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
val : α
⊢ (p ⊕' q) (Sum.inl val) ↔ r ((f ⊕' g) (Sum.inl val))

Tactic:
apply h₁
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → γ
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ r (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
val : β
⊢ (p ⊕' q) (Sum.inr val) ↔ r ((f ⊕' g) (Sum.inr val))

Tactic:
apply h₂
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → γ
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ r (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
x : α ⊕ β
inl : ∀ (val : α), (p ⊕' q) (Sum.inl val) ↔ r ((f ⊕' g) (Sum.inl val))
inr : ∀ (val : β), (p ⊕' q) (Sum.inr val) ↔ r ((f ⊕' g) (Sum.inr val))
inl₁ : ∀ (val : α), (p ⊕' q) (Sum.inl val) ↔ r ((f ⊕' g) (Sum.inl val))
inr₁ : ∀ (val : β), (p ⊕' q) (Sum.inr val) ↔ r ((f ⊕' g) (Sum.inr val))
⊢ (p ⊕' q) x ↔ r ((f ⊕' g) x)

Tactic:
cases x <;> [apply h₁; apply h₂]
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
⊢ p ⊕' q ≤₀ r ↔ p ≤₀ r ∧ q ≤₀ r

Tactic:
⟨fun h =>
    ⟨OneOneReducible.disjoin_left.to_many_one.trans h,
      OneOneReducible.disjoin_right.to_many_one.trans h⟩,
    fun ⟨h₁, h₂⟩ => disjoin_manyOneReducible h₁ h₂⟩

Premises used: OneOneReducible.to_many_one, ManyOneReducible.trans, OneOneReducible.disjoin_left, _private.0.disjoin_le.match_1, ManyOneReducible, disjoin_manyOneReducible, And.intro, Iff.intro, OneOneReducible.disjoin_right, Sum.elim
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
p : Set α
⊢ toNat p ≤₀ p

Tactic:
⟨fun n => (Encodable.decode (α := α) n).getD default,
    Computable.option_getD Computable.decode (Computable.const _), fun _ => Iff.rfl⟩

Premises used: Inhabited.default, Computable.option_getD, Computable.decode, Iff.rfl, Option.getD, ManyOneReducible, And.intro, Exists.intro, Encodable.decode, Computable.const
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
p : Set α
⊢ ∀ (a : α), p a ↔ toNat p (Encodable.encode a)

Tactic:
simp [toNat, setOf]

Premises used: setOf, toNat
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
β : Type v
inst_2 : Primcodable β
inst_3 : Inhabited β
p : Set α
q : Set β
⊢ toNat p ≤₀ toNat q ↔ p ≤₀ q

Tactic:
⟨fun h => manyOneReducible_toNat.trans (h.trans toNat_manyOneReducible), fun h =>
    toNat_manyOneReducible.trans (h.trans manyOneReducible_toNat)⟩

Premises used: ManyOneReducible.trans, manyOneReducible_toNat, Iff.intro, toNat_manyOneReducible
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
p : Set α
⊢ ManyOneEquiv (toNat p) p

Tactic:
simp [ManyOneEquiv]

Premises used: ManyOneEquiv
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
β : Type v
inst_2 : Primcodable β
inst_3 : Inhabited β
p : Set α
q : Set β
⊢ ManyOneEquiv (toNat p) (toNat q) ↔ ManyOneEquiv p q

Tactic:
simp [ManyOneEquiv]

Premises used: ManyOneEquiv
-- Module: Mathlib.Computability.Reduce
Goal:
C : ManyOneDegree → Prop
d : ManyOneDegree
h : ∀ (p : Set ℕ), C (of p)
⊢ C d

Tactic:
Quotient.inductionOn' d h

Premises used: Quotient.inductionOn'
-- Module: Mathlib.Computability.Reduce
Goal:
φ : Sort u_1
p : Set ℕ
f : Set ℕ → φ
h : ∀ (p q : ℕ → Prop), ManyOneEquiv p q → f p = f q
⊢ (of p).liftOn f h = f p

Tactic:
rfl

Premises used: Quotient.liftOn', setOf, Option.getD, toNat, rfl
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
β : Type v
inst_2 : Primcodable β
inst_3 : Inhabited β
φ : Sort u_1
d₁ d₂ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p : Set ℕ
x x_1 : ℕ → Prop
hq : ManyOneEquiv x x_1
⊢ ManyOneEquiv p p

Tactic:
rfl
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
β : Type v
inst_2 : Primcodable β
inst_3 : Inhabited β
φ : Sort u_1
d₁ d₂ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
hp : ManyOneEquiv p₁ p₂
h₁ :
  ∀ (p : Set ℕ),
    Eq.{u_1} (α := φ) ((fun (p_1 : Set ℕ) ↦ (of p).liftOn (f p_1) ⋯) p₁)
      ((fun (p_1 : Set ℕ) ↦ (of p).liftOn (f p_1) ⋯) p₂)
⊢ Eq.{u_1} (α := φ) ((fun (p : Set ℕ) ↦ d₂.liftOn (f p) ⋯) p₁) ((fun (p : Set ℕ) ↦ d₂.liftOn (f p) ⋯) p₂)

Tactic:
induction d₂ using ManyOneDegree.ind_on
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
β : Type v
inst_2 : Primcodable β
inst_3 : Inhabited β
φ : Sort u_1
d₁ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
hp : ManyOneEquiv p₁ p₂
p : Set ℕ
h₁ : ManyOneEquiv p₁ p₂
h₂ : ManyOneEquiv (toNat p) (toNat p)
⊢ Eq.{u_1} (α := φ) ((fun (p_1 : Set ℕ) ↦ (of p).liftOn (f p_1) ⋯) p₁)
    ((fun (p_1 : Set ℕ) ↦ (of p).liftOn (f p_1) ⋯) p₂)

Tactic:
apply h
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
β : Type v
inst_2 : Primcodable β
inst_3 : Inhabited β
φ : Sort u_1
d₁ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
hp : ManyOneEquiv p₁ p₂
p : Set ℕ
⊢ ManyOneEquiv p₁ p₂

Tactic:
assumption
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
β : Type v
inst_2 : Primcodable β
inst_3 : Inhabited β
φ : Sort u_1
d₁ : ManyOneDegree
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
p₁ p₂ : ℕ → Prop
hp : ManyOneEquiv p₁ p₂
p : Set ℕ
⊢ ManyOneEquiv (toNat p) (toNat p)

Tactic:
rfl
-- Module: Mathlib.Computability.Reduce
Goal:
φ : Sort u_1
p q : Set ℕ
f : Set ℕ → Set ℕ → φ
h : ∀ (p₁ p₂ q₁ q₂ : ℕ → Prop), ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂
⊢ (of p).liftOn₂ (of q) f h = f p q

Tactic:
rfl

Premises used: Quotient.liftOn', setOf, Option.getD, toNat, rfl
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
β : Type v
inst_2 : Primcodable β
inst_3 : Inhabited β
p : α → Prop
q : β → Prop
rw : ({ r := ManyOneEquiv, iseqv := _proof_1 } : Set ℕ → Set ℕ → Prop) (toNat p) (toNat q) ↔ ManyOneEquiv p q
⊢ of p = of q ↔ ManyOneEquiv p q

Tactic:
rw [of, of, Quotient.eq'']

Premises used: Quotient.eq'', ManyOneDegree.of
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
β : Type v
inst_2 : Primcodable β
inst_3 : Inhabited β
p : α → Prop
q : β → Prop
⊢ ({ r := ManyOneEquiv, iseqv := _proof_1 } : Set ℕ → Set ℕ → Prop) (toNat p) (toNat q) ↔ ManyOneEquiv p q

Tactic:
simp
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
β : Type v
inst_2 : Primcodable β
inst_3 : Inhabited β
p : α → Prop
q : β → Prop
⊢ of p ≤ of q ↔ p ≤₀ q

Tactic:
manyOneReducible_toNat_toNat

Premises used: Quotient.liftOn', manyOneReducible_toNat_toNat, ManyOneReducible
-- Module: Mathlib.Computability.Reduce
Goal:
d : ManyOneDegree
h : ∀ (p : Set ℕ), of p ≤ of p
⊢ d ≤ d

Tactic:
induction d using ManyOneDegree.ind_on
-- Module: Mathlib.Computability.Reduce
Goal:
p : Set ℕ
h : p ≤₀ p
⊢ of p ≤ of p

Tactic:
simp
-- Module: Mathlib.Computability.Reduce
Goal:
p : Set ℕ
⊢ p ≤₀ p

Tactic:
rfl
-- Module: Mathlib.Computability.Reduce
Goal:
d₁ d₂ : ManyOneDegree
h : ∀ (p : Set ℕ), of p ≤ d₂ → d₂ ≤ of p → of p = d₂
⊢ d₁ ≤ d₂ → d₂ ≤ d₁ → d₁ = d₂

Tactic:
induction d₁ using ManyOneDegree.ind_on
-- Module: Mathlib.Computability.Reduce
Goal:
d₂ : ManyOneDegree
p : Set ℕ
h : ∀ (p_1 : Set ℕ), of p ≤ of p_1 → of p_1 ≤ of p → of p = of p_1
⊢ of p ≤ d₂ → d₂ ≤ of p → of p = d₂

Tactic:
induction d₂ using ManyOneDegree.ind_on
-- Module: Mathlib.Computability.Reduce
Goal:
p p_1 : Set ℕ
hp : of p ≤ of p_1
hq : of p_1 ≤ of p
⊢ of p = of p_1

Tactic:
simp_all only [ManyOneEquiv, of_le_of, of_eq_of, true_and]

Premises used: ManyOneEquiv, ManyOneDegree.of_eq_of, ManyOneDegree.of_le_of, true_and
-- Module: Mathlib.Computability.Reduce
Goal:
d₁ d₂ d₃ : ManyOneDegree
h : ∀ (p : Set ℕ), of p ≤ d₂ → d₂ ≤ d₃ → of p ≤ d₃
⊢ d₁ ≤ d₂ → d₂ ≤ d₃ → d₁ ≤ d₃

Tactic:
induction d₁ using ManyOneDegree.ind_on
-- Module: Mathlib.Computability.Reduce
Goal:
d₂ d₃ : ManyOneDegree
p : Set ℕ
h : ∀ (p_1 : Set ℕ), of p ≤ of p_1 → of p_1 ≤ d₃ → of p ≤ d₃
⊢ of p ≤ d₂ → d₂ ≤ d₃ → of p ≤ d₃

Tactic:
induction d₂ using ManyOneDegree.ind_on
-- Module: Mathlib.Computability.Reduce
Goal:
d₃ : ManyOneDegree
p p_1 : Set ℕ
h : ∀ (p_2 : Set ℕ), of p ≤ of p_1 → of p_1 ≤ of p_2 → of p ≤ of p_2
⊢ of p ≤ of p_1 → of p_1 ≤ d₃ → of p ≤ d₃

Tactic:
induction d₃ using ManyOneDegree.ind_on
-- Module: Mathlib.Computability.Reduce
Goal:
p p_1 p_2 : Set ℕ
⊢ of p ≤ of p_1 → of p_1 ≤ of p_2 → of p ≤ of p_2

Tactic:
apply ManyOneReducible.trans

Premises used: ManyOneReducible.trans
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
β : Type v
inst_2 : Primcodable β
inst_3 : Inhabited β
d₁ d₂ : ManyOneDegree
a b c d : ℕ → Prop
hl₁ : a ≤₀ b
hr₁ : b ≤₀ a
hl₂ : c ≤₀ d
hr₂ : d ≤₀ c
rw : ManyOneEquiv (a ⊕' c) (b ⊕' d)
⊢ Eq (α := ManyOneDegree) ((fun (a b : Set ℕ) ↦ of (a ⊕' b)) a c) ((fun (a b : Set ℕ) ↦ of (a ⊕' b)) b d)

Tactic:
rw [of_eq_of]

Premises used: ManyOneDegree.of_eq_of
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
β : Type v
inst_2 : Primcodable β
inst_3 : Inhabited β
d₁ d₂ : ManyOneDegree
a b c d : ℕ → Prop
hl₁ : a ≤₀ b
hr₁ : b ≤₀ a
hl₂ : c ≤₀ d
hr₂ : d ≤₀ c
⊢ ManyOneEquiv (a ⊕' c) (b ⊕' d)

Tactic:
⟨disjoin_manyOneReducible (hl₁.trans OneOneReducible.disjoin_left.to_many_one)
              (hl₂.trans OneOneReducible.disjoin_right.to_many_one),
            disjoin_manyOneReducible (hr₁.trans OneOneReducible.disjoin_left.to_many_one)
              (hr₂.trans OneOneReducible.disjoin_right.to_many_one)⟩

Premises used: OneOneReducible.to_many_one, ManyOneEquiv, ManyOneReducible.trans, OneOneReducible.disjoin_left, disjoin_manyOneReducible, And.intro, OneOneReducible.disjoin_right
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
β : Type v
inst_2 : Primcodable β
inst_3 : Inhabited β
d₁ d₂ : ManyOneDegree
a b c d : ℕ → Prop
hl₁ : a ≤₀ b
hr₁ : b ≤₀ a
hl₂ : c ≤₀ d
hr₂ : d ≤₀ c
⊢ ManyOneEquiv (a ⊕' c) (b ⊕' d)

Tactic:
exact
          ⟨disjoin_manyOneReducible (hl₁.trans OneOneReducible.disjoin_left.to_many_one)
              (hl₂.trans OneOneReducible.disjoin_right.to_many_one),
            disjoin_manyOneReducible (hr₁.trans OneOneReducible.disjoin_left.to_many_one)
              (hr₂.trans OneOneReducible.disjoin_right.to_many_one)⟩
-- Module: Mathlib.Computability.Reduce
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
β : Type v
inst_2 : Primcodable β
inst_3 : Inhabited β
p : Set α
q : Set β
⊢ of (p ⊕' q) = of p + of q

Tactic:
of_eq_of.mpr
    ⟨disjoin_manyOneReducible
        (manyOneReducible_toNat.trans OneOneReducible.disjoin_left.to_many_one)
        (manyOneReducible_toNat.trans OneOneReducible.disjoin_right.to_many_one),
      disjoin_manyOneReducible
        (toNat_manyOneReducible.trans OneOneReducible.disjoin_left.to_many_one)
        (toNat_manyOneReducible.trans OneOneReducible.disjoin_right.to_many_one)⟩

Premises used: Iff.mpr, OneOneReducible.to_many_one, Quotient.liftOn', ManyOneReducible.trans, OneOneReducible.disjoin_left, ManyOneDegree.of_eq_of, disjoin_manyOneReducible, manyOneReducible_toNat, And.intro, toNat_manyOneReducible, OneOneReducible.disjoin_right, ManyOneDegree.of
-- Module: Mathlib.Computability.Reduce
Goal:
d₁ d₂ d₃ : ManyOneDegree
h : ∀ (p : Set ℕ), of p + d₂ ≤ d₃ ↔ of p ≤ d₃ ∧ d₂ ≤ d₃
⊢ d₁ + d₂ ≤ d₃ ↔ d₁ ≤ d₃ ∧ d₂ ≤ d₃

Tactic:
induction d₁ using ManyOneDegree.ind_on
-- Module: Mathlib.Computability.Reduce
Goal:
d₂ d₃ : ManyOneDegree
p : Set ℕ
h : ∀ (p_1 : Set ℕ), of p + of p_1 ≤ d₃ ↔ of p ≤ d₃ ∧ of p_1 ≤ d₃
⊢ of p + d₂ ≤ d₃ ↔ of p ≤ d₃ ∧ d₂ ≤ d₃

Tactic:
induction d₂ using ManyOneDegree.ind_on
-- Module: Mathlib.Computability.Reduce
Goal:
d₃ : ManyOneDegree
p p_1 : Set ℕ
h : ∀ (p_2 : Set ℕ), of p + of p_1 ≤ of p_2 ↔ of p ≤ of p_2 ∧ of p_1 ≤ of p_2
⊢ of p + of p_1 ≤ d₃ ↔ of p ≤ d₃ ∧ of p_1 ≤ d₃

Tactic:
induction d₃ using ManyOneDegree.ind_on
-- Module: Mathlib.Computability.Reduce
Goal:
p p_1 p_2 : Set ℕ
⊢ of p + of p_1 ≤ of p_2 ↔ of p ≤ of p_2 ∧ of p_1 ≤ of p_2

Tactic:
simpa only [← add_of, of_le_of] using disjoin_le

Premises used: disjoin_le, ManyOneDegree.add_of, ManyOneDegree.of_le_of
-- Module: Mathlib.Computability.Reduce
Goal:
d₁ d₂ : ManyOneDegree
⊢ d₁ ≤ d₁ + d₂

Tactic:
(ManyOneDegree.add_le.1 (le_refl _)).1

Premises used: ManyOneDegree.add_le, And.left, Iff.mp, _private.0.ManyOneDegree.le_refl
-- Module: Mathlib.Computability.Reduce
Goal:
d₁ d₂ : ManyOneDegree
⊢ d₂ ≤ d₁ + d₂

Tactic:
(ManyOneDegree.add_le.1 (le_refl _)).2

Premises used: ManyOneDegree.add_le, And.right, Iff.mp, _private.0.ManyOneDegree.le_refl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := RegularExpression α) zero 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := RegularExpression α) epsilon 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
P Q : RegularExpression α
⊢ P.plus Q = P + Q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
P Q : RegularExpression α
⊢ P.comp Q = P * Q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Language α) (matches' 0) 0

Tactic:
rfl

Premises used: RegularExpression.matches', rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Language α) (matches' 1) 1

Tactic:
rfl

Premises used: RegularExpression.matches', rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
a : α
⊢ (char a).matches' = {[a]}

Tactic:
rfl

Premises used: RegularExpression.matches', rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
P Q : RegularExpression α
⊢ (P + Q).matches' = P.matches' + Q.matches'

Tactic:
rfl

Premises used: RegularExpression.matches', rfl
-- Module: Mathlib.Computability.RegularExpressions
Goal:
α : Type u_1
P Q : RegularExpression α
⊢ (P * Q).matches' = P.matches' * Q.matches'

Tactic:
rfl

Premises used: RegularExpression.matches', rfl