awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
pF : Nat.Partrec f
⊢ Nat.RecursiveIn O f
have zero : Nat.RecursiveIn O (pure 0)
Tactic: induction pF with
  | zero | succ | left | right => constructor
  | pair _ _ ih₁ ih₂ => exact .pair ih₁ ih₂
  | comp _ _ ih₁ ih₂ => exact .comp ih₁ ih₂
  | prec _ _ ih₁ ih₂ => exact .prec ih₁ ih₂
  | rfind _ ih => exact .rfind ih
Cleared hypotheses: pF
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
pF : Nat.Partrec f
zero : Nat.RecursiveIn O (pure 0)
⊢ Nat.RecursiveIn O f
have succ : Nat.RecursiveIn O (↑Nat.succ : ℕ →. ℕ)
Tactic: induction pF with
  | zero | succ | left | right => constructor
  | pair _ _ ih₁ ih₂ => exact .pair ih₁ ih₂
  | comp _ _ ih₁ ih₂ => exact .comp ih₁ ih₂
  | prec _ _ ih₁ ih₂ => exact .prec ih₁ ih₂
  | rfind _ ih => exact .rfind ih
Cleared hypotheses: pF
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
pF : Nat.Partrec f
zero : Nat.RecursiveIn O (pure 0)
succ : Nat.RecursiveIn O (↑Nat.succ : ℕ →. ℕ)
⊢ Nat.RecursiveIn O f
have left : Nat.RecursiveIn O (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
Tactic: induction pF with
  | zero | succ | left | right => constructor
  | pair _ _ ih₁ ih₂ => exact .pair ih₁ ih₂
  | comp _ _ ih₁ ih₂ => exact .comp ih₁ ih₂
  | prec _ _ ih₁ ih₂ => exact .prec ih₁ ih₂
  | rfind _ ih => exact .rfind ih
Cleared hypotheses: pF
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
pF : Nat.Partrec f
zero : Nat.RecursiveIn O (pure 0)
succ : Nat.RecursiveIn O (↑Nat.succ : ℕ →. ℕ)
left : Nat.RecursiveIn O (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
⊢ Nat.RecursiveIn O f
have right : Nat.RecursiveIn O (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
Tactic: induction pF with
  | zero | succ | left | right => constructor
  | pair _ _ ih₁ ih₂ => exact .pair ih₁ ih₂
  | comp _ _ ih₁ ih₂ => exact .comp ih₁ ih₂
  | prec _ _ ih₁ ih₂ => exact .prec ih₁ ih₂
  | rfind _ ih => exact .rfind ih
Cleared hypotheses: pF
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
pF : Nat.Partrec f
zero : Nat.RecursiveIn O (pure 0)
succ : Nat.RecursiveIn O (↑Nat.succ : ℕ →. ℕ)
left : Nat.RecursiveIn O (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
right : Nat.RecursiveIn O (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
⊢ Nat.RecursiveIn O f
have pair : ∀ {f g : ℕ →. ℕ},
  Nat.Partrec f →
    Nat.Partrec g →
      ∀ (ih₁ : Nat.RecursiveIn O f) (ih₂ : Nat.RecursiveIn O g),
        Nat.RecursiveIn O fun (n : ℕ) ↦ Nat.pair <$> f n <*> g n
Tactic: induction pF with
  | zero | succ | left | right => constructor
  | pair _ _ ih₁ ih₂ => exact .pair ih₁ ih₂
  | comp _ _ ih₁ ih₂ => exact .comp ih₁ ih₂
  | prec _ _ ih₁ ih₂ => exact .prec ih₁ ih₂
  | rfind _ ih => exact .rfind ih
Cleared hypotheses: pF
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
pF : Nat.Partrec f
zero : Nat.RecursiveIn O (pure 0)
succ : Nat.RecursiveIn O (↑Nat.succ : ℕ →. ℕ)
left : Nat.RecursiveIn O (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
right : Nat.RecursiveIn O (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
pair :
  ∀ {f g : ℕ →. ℕ},
    Nat.Partrec f →
      Nat.Partrec g →
        ∀ (ih₁ : Nat.RecursiveIn O f) (ih₂ : Nat.RecursiveIn O g),
          Nat.RecursiveIn O fun (n : ℕ) ↦ Nat.pair <$> f n <*> g n
⊢ Nat.RecursiveIn O f
have comp : ∀ {f g : ℕ →. ℕ},
  Nat.Partrec f →
    Nat.Partrec g → ∀ (ih₁ : Nat.RecursiveIn O f) (ih₂ : Nat.RecursiveIn O g), Nat.RecursiveIn O fun (n : ℕ) ↦ g n >>= f
Tactic: induction pF with
  | zero | succ | left | right => constructor
  | pair _ _ ih₁ ih₂ => exact .pair ih₁ ih₂
  | comp _ _ ih₁ ih₂ => exact .comp ih₁ ih₂
  | prec _ _ ih₁ ih₂ => exact .prec ih₁ ih₂
  | rfind _ ih => exact .rfind ih
Cleared hypotheses: pF
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
pF : Nat.Partrec f
zero : Nat.RecursiveIn O (pure 0)
succ : Nat.RecursiveIn O (↑Nat.succ : ℕ →. ℕ)
left : Nat.RecursiveIn O (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
right : Nat.RecursiveIn O (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
pair :
  ∀ {f g : ℕ →. ℕ},
    Nat.Partrec f →
      Nat.Partrec g →
        ∀ (ih₁ : Nat.RecursiveIn O f) (ih₂ : Nat.RecursiveIn O g),
          Nat.RecursiveIn O fun (n : ℕ) ↦ Nat.pair <$> f n <*> g n
comp :
  ∀ {f g : ℕ →. ℕ},
    Nat.Partrec f →
      Nat.Partrec g →
        ∀ (ih₁ : Nat.RecursiveIn O f) (ih₂ : Nat.RecursiveIn O g), Nat.RecursiveIn O fun (n : ℕ) ↦ g n >>= f
⊢ Nat.RecursiveIn O f
have prec : ∀ {f g : ℕ →. ℕ},
  Nat.Partrec f →
    Nat.Partrec g →
      ∀ (ih₁ : Nat.RecursiveIn O f) (ih₂ : Nat.RecursiveIn O g),
        Nat.RecursiveIn O
          (unpaired fun (a n : ℕ) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (f a)
              (fun (y : ℕ) (IH : Part ℕ) ↦ do
                let i ← IH
                g (Nat.pair a (Nat.pair y i)))
              n)
Tactic: induction pF with
  | zero | succ | left | right => constructor
  | pair _ _ ih₁ ih₂ => exact .pair ih₁ ih₂
  | comp _ _ ih₁ ih₂ => exact .comp ih₁ ih₂
  | prec _ _ ih₁ ih₂ => exact .prec ih₁ ih₂
  | rfind _ ih => exact .rfind ih
Cleared hypotheses: pF
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
Goal:
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
pF : Nat.Partrec f
zero : Nat.RecursiveIn O (pure 0)
succ : Nat.RecursiveIn O (↑Nat.succ : ℕ →. ℕ)
left : Nat.RecursiveIn O (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
right : Nat.RecursiveIn O (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
pair :
  ∀ {f g : ℕ →. ℕ},
    Nat.Partrec f →
      Nat.Partrec g →
        ∀ (ih₁ : Nat.RecursiveIn O f) (ih₂ : Nat.RecursiveIn O g),
          Nat.RecursiveIn O fun (n : ℕ) ↦ Nat.pair <$> f n <*> g n
comp :
  ∀ {f g : ℕ →. ℕ},
    Nat.Partrec f →
      Nat.Partrec g →
        ∀ (ih₁ : Nat.RecursiveIn O f) (ih₂ : Nat.RecursiveIn O g), Nat.RecursiveIn O fun (n : ℕ) ↦ g n >>= f
prec :
  ∀ {f g : ℕ →. ℕ},
    Nat.Partrec f →
      Nat.Partrec g →
        ∀ (ih₁ : Nat.RecursiveIn O f) (ih₂ : Nat.RecursiveIn O g),
          Nat.RecursiveIn O
            (unpaired fun (a n : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (f a)
                (fun (y : ℕ) (IH : Part ℕ) ↦ do
                  let i ← IH
                  g (Nat.pair a (Nat.pair y i)))
                n)
⊢ Nat.RecursiveIn O f
have rfind : ∀ {f : ℕ →. ℕ},
  Nat.Partrec f →
    ∀ (ih : Nat.RecursiveIn O f),
      Nat.RecursiveIn O fun (a : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> f (Nat.pair a n)
Tactic: induction pF with
  | zero | succ | left | right => constructor
  | pair _ _ ih₁ ih₂ => exact .pair ih₁ ih₂
  | comp _ _ ih₁ ih₂ => exact .comp ih₁ ih₂
  | prec _ _ ih₁ ih₂ => exact .prec ih₁ ih₂
  | rfind _ ih => exact .rfind ih
Cleared hypotheses: pF
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
Goal:
O : Set (ℕ →. ℕ)
g : ℕ →. ℕ
hg : g ∈ O
⊢ RecursiveIn O g
have rw : Nat.RecursiveIn O g
Tactic: rw [iff_nat]
-- Lean 4 proof step from Mathlib.Computability.RecursiveIn (goal)
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ
s : Part ℕ
hf : RecursiveIn {fun (x : ℕ) ↦ s} f
g : ℕ →. ℕ
hg : Membership.mem (γ := Set (ℕ →. ℕ)) {fun (x : ℕ) ↦ s} g
⊢ Partrec g
have rw : Partrec (α := ℕ) (σ := ℕ) fun (x : ℕ) ↦ s
Tactic: rw [Set.mem_singleton_iff.mp hg]
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
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 ↔ q (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : r ((g ∘ f) a)
⊢ p a
have rwa : q (f a)
Tactic: rwa [h₁, h₂]
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
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 ↔ q (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : r ((g ∘ f) a)
rwa : q (f a)
⊢ p a
have rwa₁ : r (g (f a))
Tactic: rwa [h₁, h₂]
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
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
i₁ : Injective f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
i₂ : Injective g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : r ((g ∘ f) a)
⊢ p a
have rwa : q (f a)
Tactic: rwa [h₁, h₂]
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
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
i₁ : Injective f
h₁ : ∀ (a : α), p a ↔ q (f a)
g : β → γ
c₂ : Computable g
i₂ : Injective g
h₂ : ∀ (a : β), q a ↔ r (g a)
a : α
h : r ((g ∘ f) a)
rwa : q (f a)
⊢ p a
have rwa₁ : r (g (f a))
Tactic: rwa [h₁, h₂]
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable.{u_2, u_1} (α := β) (σ := α) (⇑e.symm : (a : β) → α)
⊢ OneOneReducible.{u_2, u_1} (β := α) q (q ∘ (⇑e : (a : α) → β))
have h₁ : q = comp.{u_2 + 1, u_1 + 1, 1} (β := α) (q ∘ (⇑e : (a : α) → β)) (⇑e.symm : (a : β) → α)
Tactic: convert! OneOneReducible.of_equiv _ h
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable.{u_2, u_1} (α := β) (σ := α) (⇑e.symm : (a : β) → α)
⊢ q = comp.{u_2 + 1, u_1 + 1, 1} (β := α) (q ∘ (⇑e : (a : α) → β)) (⇑e.symm : (a : β) → α)
have h₁ : ∀ (x : β), q x = comp.{u_2 + 1, u_1 + 1, 1} (β := α) (q ∘ (⇑e : (a : α) → β)) (⇑e.symm : (a : β) → α) x
Tactic: funext
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α → Prop
q : β → Prop
h₁ : p ≤₀ q
h₂ : ComputablePred q
⊢ ComputablePred p
have rcases : ∀ (f : α → β) (c : Computable f) (hf : ∀ (a : α), p a ↔ q (f a)), ComputablePred p
Tactic: rcases h₁ with ⟨f, c, hf⟩
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred p
have rw : ComputablePred fun (a : α) ↦ q (f a)
Tactic: rw [show p = fun a => q (f a) from Set.ext hf]
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
p : α → Prop
q : β → Prop
h₂ : ComputablePred q
f : α → β
c : Computable f
hf : ∀ (a : α), p a ↔ q (f a)
⊢ ComputablePred fun (a : α) ↦ q (f a)
have rcases : ∀ (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: rcases computable_iff.1 h₂ with ⟨g, hg, rfl⟩
Cleared hypotheses: q, h₂, hf
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
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 : α ⊕ β
⊢ (p ⊕' q) x ↔ r ((f ⊕' g) x)
have inl : ∀ (val : α), (p ⊕' q) (Sum.inl val) ↔ r ((f ⊕' g) (Sum.inl val))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
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))
⊢ (p ⊕' q) x ↔ r ((f ⊕' g) x)
have inr : ∀ (val : β), (p ⊕' q) (Sum.inr val) ↔ r ((f ⊕' g) (Sum.inr val))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
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 : α ⊕ β
⊢ (p ⊕' q) x ↔ r ((f ⊕' g) x)
have inl : ∀ (val : α), (p ⊕' q) (Sum.inl val) ↔ r ((f ⊕' g) (Sum.inl val))
Tactic: cases x <;> [apply h₁; apply h₂]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
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))
⊢ (p ⊕' q) x ↔ r ((f ⊕' g) x)
have inr : ∀ (val : β), (p ⊕' q) (Sum.inr val) ↔ r ((f ⊕' g) (Sum.inr val))
Tactic: cases x <;> [apply h₁; apply h₂]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
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₂
⊢ Eq.{u_1} (α := φ) ((fun (p : Set ℕ) ↦ d₂.liftOn (f p) ⋯) p₁) ((fun (p : Set ℕ) ↦ d₂.liftOn (f p) ⋯) p₂)
have h₁ : ∀ (p : Set ℕ),
  Eq.{u_1} (α := φ) ((fun (p_1 : Set ℕ) ↦ (of p).liftOn (f p_1) sorry) p₁)
    ((fun (p_1 : Set ℕ) ↦ (of p).liftOn (f p_1) sorry) p₂)
Tactic: induction d₂ using ManyOneDegree.ind_on
Cleared hypotheses: d₂
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
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₂
⊢ 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₂)
have h₂ : ManyOneEquiv (toNat p) (toNat p)
Tactic: apply h
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
Goal:
α : Type u
inst : Primcodable α
inst_1 : Inhabited α
β : Type v
inst_2 : Primcodable β
inst_3 : Inhabited β
p : α → Prop
q : β → Prop
⊢ of p = of q ↔ ManyOneEquiv p q
have rw : ({ r := ManyOneEquiv, iseqv := _proof_1 } : Set ℕ → Set ℕ → Prop) (toNat p) (toNat q) ↔ ManyOneEquiv p q
Tactic: rw [of, of, Quotient.eq'']
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
Goal:
d : ManyOneDegree
⊢ d ≤ d
have h : ∀ (p : Set ℕ), of p ≤ of p
Tactic: induction d using ManyOneDegree.ind_on
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
Goal:
p : Set ℕ
⊢ of p ≤ of p
have h : p ≤₀ p
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
Goal:
d₁ d₂ : ManyOneDegree
⊢ d₁ ≤ d₂ → d₂ ≤ d₁ → d₁ = d₂
have h : ∀ (p : Set ℕ), of p ≤ d₂ → d₂ ≤ of p → of p = d₂
Tactic: induction d₁ using ManyOneDegree.ind_on
Cleared hypotheses: d₁
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
Goal:
d₂ : ManyOneDegree
p : Set ℕ
⊢ of p ≤ d₂ → d₂ ≤ of p → of p = d₂
have h : ∀ (p_1 : Set ℕ), of p ≤ of p_1 → of p_1 ≤ of p → of p = of p_1
Tactic: induction d₂ using ManyOneDegree.ind_on
Cleared hypotheses: d₂
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
Goal:
d₁ d₂ d₃ : ManyOneDegree
⊢ d₁ ≤ d₂ → d₂ ≤ d₃ → d₁ ≤ d₃
have h : ∀ (p : Set ℕ), of p ≤ d₂ → d₂ ≤ d₃ → of p ≤ d₃
Tactic: induction d₁ using ManyOneDegree.ind_on
Cleared hypotheses: d₁
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
Goal:
d₂ d₃ : ManyOneDegree
p : Set ℕ
⊢ of p ≤ d₂ → d₂ ≤ d₃ → of p ≤ d₃
have h : ∀ (p_1 : Set ℕ), of p ≤ of p_1 → of p_1 ≤ d₃ → of p ≤ d₃
Tactic: induction d₂ using ManyOneDegree.ind_on
Cleared hypotheses: d₂
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
Goal:
d₃ : ManyOneDegree
p p_1 : Set ℕ
⊢ of p ≤ of p_1 → of p_1 ≤ d₃ → of p ≤ d₃
have h : ∀ (p_2 : Set ℕ), of p ≤ of p_1 → of p_1 ≤ of p_2 → of p ≤ of p_2
Tactic: induction d₃ using ManyOneDegree.ind_on
Cleared hypotheses: d₃
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
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
⊢ Eq (α := ManyOneDegree) ((fun (a b : Set ℕ) ↦ of (a ⊕' b)) a c) ((fun (a b : Set ℕ) ↦ of (a ⊕' b)) b d)
have rw : ManyOneEquiv (a ⊕' c) (b ⊕' d)
Tactic: rw [of_eq_of]
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
Goal:
d₁ d₂ d₃ : ManyOneDegree
⊢ d₁ + d₂ ≤ d₃ ↔ d₁ ≤ d₃ ∧ d₂ ≤ d₃
have h : ∀ (p : Set ℕ), of p + d₂ ≤ d₃ ↔ of p ≤ d₃ ∧ d₂ ≤ d₃
Tactic: induction d₁ using ManyOneDegree.ind_on
Cleared hypotheses: d₁
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
Goal:
d₂ d₃ : ManyOneDegree
p : Set ℕ
⊢ of p + d₂ ≤ d₃ ↔ of p ≤ d₃ ∧ d₂ ≤ d₃
have h : ∀ (p_1 : Set ℕ), of p + of p_1 ≤ d₃ ↔ of p ≤ d₃ ∧ of p_1 ≤ d₃
Tactic: induction d₂ using ManyOneDegree.ind_on
Cleared hypotheses: d₂
-- Lean 4 proof step from Mathlib.Computability.Reduce (goal)
Goal:
d₃ : ManyOneDegree
p p_1 : Set ℕ
⊢ of p + of p_1 ≤ d₃ ↔ of p ≤ d₃ ∧ of p_1 ≤ d₃
have h : ∀ (p_2 : Set ℕ), of p + of p_1 ≤ of p_2 ↔ of p ≤ of p_2 ∧ of p_1 ≤ of p_2
Tactic: induction d₃ using ManyOneDegree.ind_on
Cleared hypotheses: d₃
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
⊢ rmatch 0 x = false
have nil : rmatch.{u_1} (α := α) 0 [] = false
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
nil : rmatch.{u_1} (α := α) 0 [] = false
⊢ rmatch 0 x = false
have cons : ∀ (head : α) (tail : List α), rmatch 0 tail = false → rmatch 0 (head :: tail) = false
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
⊢ rmatch 1 x = true ↔ x = []
have nil : rmatch.{u_1} (α := α) 1 [] = true ↔ Eq.{u_1 + 1} (α := List α) [] []
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
nil : rmatch.{u_1} (α := α) 1 [] = true ↔ Eq.{u_1 + 1} (α := List α) [] []
⊢ rmatch 1 x = true ↔ x = []
have cons : ∀ (head : α) (tail : List α), (rmatch 1 tail = true ↔ tail = []) → (rmatch 1 (head :: tail) = true ↔ head :: tail = [])
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
⊢ (char a).rmatch x = true ↔ x = [a]
have nil : (char a).rmatch [] = true ↔ [] = [a]
Tactic: rcases x with - | ⟨_, x⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
nil : (char a).rmatch [] = true ↔ [] = [a]
⊢ (char a).rmatch x = true ↔ x = [a]
have cons : ∀ (head : α) (x : List α), (char a).rmatch (head :: x) = true ↔ head :: x = [a]
Tactic: rcases x with - | ⟨_, x⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
x : List α
⊢ (char a).rmatch (head :: x) = true ↔ head :: x = [a]
have cons : (char a).rmatch [head] = true ↔ [head] = [a]
Tactic: rcases x with - | ⟨head, tail⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
x : List α
cons : (char a).rmatch [head] = true ↔ [head] = [a]
⊢ (char a).rmatch (head :: x) = true ↔ head :: x = [a]
have cons₁ : ∀ (head_1 : α) (tail : List α), (char a).rmatch (head :: head_1 :: tail) = true ↔ head :: head_1 :: tail = [a]
Tactic: rcases x with - | ⟨head, tail⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
⊢ (char a).rmatch [head] = true ↔ [head] = [a]
have cons : rmatch.{u_1} (α := α) (if a = head then 1 else 0) [] = true ↔ head = a
Tactic: rw [rmatch, deriv, List.singleton_inj]
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
⊢ rmatch.{u_1} (α := α) (if a = head then 1 else 0) [] = true ↔ head = a
have cons : a = head → (rmatch.{u_1} (α := α) 1 [] = true ↔ head = a)
Tactic: split
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
cons : a = head → (rmatch.{u_1} (α := α) 1 [] = true ↔ head = a)
⊢ rmatch.{u_1} (α := α) (if a = head then 1 else 0) [] = true ↔ head = a
have cons₁ : ¬a = head → (rmatch.{u_1} (α := α) 0 [] = true ↔ head = a)
Tactic: split
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
h : a = head
⊢ rmatch.{u_1} (α := α) 1 [] = true ↔ head = a
have cons : rmatch.{u_1} (α := α) 1 [] = true → head = a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
h : a = head
cons : rmatch.{u_1} (α := α) 1 [] = true → head = a
⊢ rmatch.{u_1} (α := α) 1 [] = true ↔ head = a
have cons₁ : head = a → rmatch.{u_1} (α := α) 1 [] = true
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
h : ¬a = head
⊢ rmatch.{u_1} (α := α) 0 [] = true ↔ head = a
have cons : rmatch.{u_1} (α := α) 0 [] = true → head = a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head : α
h : ¬a = head
cons : rmatch.{u_1} (α := α) 0 [] = true → head = a
⊢ rmatch.{u_1} (α := α) 0 [] = true ↔ head = a
have cons₁ : head = a → rmatch.{u_1} (α := α) 0 [] = true
Tactic: tauto
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head_1 head : α
tail : List α
⊢ (char a).rmatch (head_1 :: head :: tail) = true ↔ head_1 :: head :: tail = [a]
have cons : (deriv (if a = head_1 then 1 else 0) head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = []
Tactic: rw [rmatch, rmatch, deriv, cons.injEq]
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head_1 head : α
tail : List α
⊢ (deriv (if a = head_1 then 1 else 0) head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = []
have cons : a = head_1 → ((deriv 1 head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = [])
Tactic: split
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head_1 head : α
tail : List α
cons : a = head_1 → ((deriv 1 head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = [])
⊢ (deriv (if a = head_1 then 1 else 0) head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = []
have cons₁ : ¬a = head_1 → ((deriv 0 head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = [])
Tactic: split
-- Lean 4 proof step from Mathlib.Computability.RegularExpressions (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a head_1 head : α
tail : List α
h : a = head_1
⊢ (deriv 1 head).rmatch tail = true ↔ head_1 = a ∧ head :: tail = []
have cons : rmatch 0 tail = true ↔ head_1 = a ∧ head :: tail = []
Tactic: simp_rw [deriv_one, zero_rmatch, reduceCtorEq, and_false]