awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih :
  R (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f)) (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a' f'))
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f)).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g
h₁ :
  (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a' f')).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g'
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ a = a'
have h₃ : (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f)).dest.fst (β := fun (x : P.A) ↦ P.B x → P.M) =
  Sigma.fst (β := fun (x : P.A) ↦ P.B x → P.M) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g)
Tactic: replace h₀ := congr_arg Sigma.fst h₀
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih :
  R (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f)) (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a' f'))
a'' : P.A
g g' : P.B a'' → P.M
h₁ :
  (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a' f')).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g'
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
h₀ :
  (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f)).dest.fst (β := fun (x : P.A) ↦ P.B x → P.M) =
    Sigma.fst (β := fun (x : P.A) ↦ P.B x → P.M) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g)
⊢ a = a'
have h₃ : (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a' f')).dest.fst (β := fun (x : P.A) ↦ P.B x → P.M) =
  Sigma.fst (β := fun (x : P.A) ↦ P.B x → P.M) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g')
Tactic: replace h₁ := congr_arg Sigma.fst h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih :
  R (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f)) (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a' f'))
a'' : P.A
g g' : P.B a'' → P.M
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
h₀ : a = a''
h₁ : a' = a''
⊢ a = a'
have head : a'' = a'
Tactic: rw [h₀, h₁]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih :
  R (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f)) (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a' f'))
a'' : P.A
g g' : P.B a'' → P.M
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
h₀ : a = a''
h₁ : a' = a''
head : a'' = a'
⊢ a = a'
have head₁ : a'' = a''
Tactic: rw [h₀, h₁]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih :
  R (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f)) (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f'))
i : P.B a
a'' : P.A
g g' : P.B a'' → P.M
h₀ :
  Eq (α := (↑P : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) P.M)
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g)
h₁ :
  Eq (α := (↑P : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) P.M)
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f') (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g')
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ R (f i) (f' i)
have tail : ∀ (g' : P.B a → P.M)
  (h₁ :
    Eq (α := (↑P : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) P.M)
      (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f') (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a g'))
  (h₂ : ∀ (i : P.B a), R (f i) (g' i)), R (f i) (f' i)
Tactic: cases h₀
Cleared hypotheses: a'', g, g', h₀, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih :
  R (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f)) (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f'))
i : P.B a
g' : P.B a → P.M
h₁ :
  Eq (α := (↑P : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) P.M)
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f') (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a g')
h₂ : ∀ (i : P.B a), R (f i) (g' i)
⊢ R (f i) (f' i)
have h₃ : ∀ (i : P.B a), R (f i) (f' i)
Tactic: cases h₁
Cleared hypotheses: g', h₁, h₂
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
⊢ f = M.corec g
have h : ∀ (x : α), f x = M.corec g x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
⊢ f x = M.corec g x
have apply : ∀ (x : α),
  (fun (x : α) ↦ True) x →
    ∃ (a : P.A) (f_1 : P.B a → P.M) (f' : P.B a → P.M),
      (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f_1 ∧
        (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧
          ∀ (i : P.B a), ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
Tactic: apply bisim' (fun _ => True) _ _ _ _ trivial
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
⊢ ∃ (a : P.A) (f_1 : P.B a → P.M) (f' : P.B a → P.M),
    (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f_1 ∧
      (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧
        ∀ (i : P.B a), ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
have rcases : ∀ (a : P.A) (f' : P.B a → α) (gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'),
  ∃ (a : P.A) (f_1 : P.B a → P.M) (f' : P.B a → P.M),
    (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f_1 ∧
      (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧
        ∀ (i : P.B a), ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
Tactic: rcases gxeq : g x with ⟨a, f'⟩
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
⊢ (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
have rw : P.map f (g x) = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
Tactic: rw [hyp, gxeq, PFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
rw : P.map f (g x) = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
⊢ (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
have rw₁ : P.map f (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f') = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
Tactic: rw [hyp, gxeq, PFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
rw : P.map f (g x) = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
rw₁ : P.map f (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f') = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
⊢ (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
have rw₂ : Eq (α := (↑P : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) P.M)
  (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f'))
Tactic: rw [hyp, gxeq, PFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
⊢ ∃ (a : P.A) (f_1 : P.B a → P.M) (f' : P.B a → P.M),
    (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f_1 ∧
      (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧
        ∀ (i : P.B a), ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
have h₀ : (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
Tactic: have h₀ : M.dest (f x) = ⟨a, f ∘ f'⟩ := by rw [hyp, gxeq, PFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
h₀ : (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
⊢ (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')
have rw : P.map (M.corec g) (g x) = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')
Tactic: rw [dest_corec, gxeq, PFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
h₀ : (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
rw : P.map (M.corec g) (g x) = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')
⊢ (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')
have rw₁ : P.map (M.corec g) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f') =
  Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')
Tactic: rw [dest_corec, gxeq, PFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
h₀ : (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
rw : P.map (M.corec g) (g x) = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')
rw₁ :
  P.map (M.corec g) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f') =
    Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')
⊢ (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')
have rw₂ : Eq (α := (↑P : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) P.M)
  (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f'))
  (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f'))
Tactic: rw [dest_corec, gxeq, PFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
h₀ : (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
⊢ ∃ (a : P.A) (f_1 : P.B a → P.M) (f' : P.B a → P.M),
    (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f_1 ∧
      (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧
        ∀ (i : P.B a), ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
have h₁ : (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')
Tactic: have h₁ : M.dest (M.corec g x) = ⟨a, M.corec g ∘ f'⟩ := by rw [dest_corec, gxeq, PFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
h₀ : (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
h₁ : (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')
⊢ ∃ (a : P.A) (f_1 : P.B a → P.M) (f' : P.B a → P.M),
    (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f_1 ∧
      (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧
        ∀ (i : P.B a), ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
have refine : ∀ (i : P.B a), ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'
Tactic: refine ⟨_, _, _, h₀, h₁, ?_⟩
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
n : ℕ+
⊢ 1 + n.natPred = (↑n : ℕ)
have rw : 1 + ((↑n : ℕ) - 1) = (↑n : ℕ)
Tactic: rw [natPred, add_tsub_cancel_iff_le.mpr <| show 1 ≤ (n : ℕ) from n.2]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
n : ℕ+
rw : 1 + ((↑n : ℕ) - 1) = (↑n : ℕ)
⊢ 1 + n.natPred = (↑n : ℕ)
have rw₁ : (↑n : ℕ) = (↑n : ℕ)
Tactic: rw [natPred, add_tsub_cancel_iff_le.mpr <| show 1 ≤ (n : ℕ) from n.2]
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
⊢ p a
have apply : (k : ℕ+) → ((m : ℕ+) → m < k → p m) → p k
Tactic: apply strongInductionOn a
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < k
hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) k kprop → p m
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) k kprop)
have zero : (kprop : LT.lt (α := ℕ) 0 0) →
  (hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 kprop → p m) →
    p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 kprop)
Tactic: rcases k with - | k
Cleared hypotheses: k, kprop, hk
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < k
hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) k kprop → p m
zero :
  (kprop : LT.lt (α := ℕ) 0 0) →
    (hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 kprop → p m) →
      p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 kprop)
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) k kprop)
have succ : (k : ℕ) →
  (kprop : 0 < k + 1) →
    (hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (k + 1) kprop → p m) →
      p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (k + 1) kprop)
Tactic: rcases k with - | k
Cleared hypotheses: k, kprop, hk
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < k + 1
hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (k + 1) kprop → p m
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (k + 1) kprop)
have succ : (kprop : 0 < HAdd.hAdd (α := ℕ) 0 1) →
  (hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (HAdd.hAdd (α := ℕ) 0 1) kprop → p m) →
    p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (HAdd.hAdd (α := ℕ) 0 1) kprop)
Tactic: rcases k with - | k
Cleared hypotheses: k, kprop, hk
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < k + 1
hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (k + 1) kprop → p m
succ :
  (kprop : 0 < HAdd.hAdd (α := ℕ) 0 1) →
    (hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (HAdd.hAdd (α := ℕ) 0 1) kprop → p m) →
      p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (HAdd.hAdd (α := ℕ) 0 1) kprop)
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (k + 1) kprop)
have succ₁ : (k : ℕ) →
  (kprop : 0 < k + 1 + 1) →
    (hk : (m : ℕ+) → m < Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (k + 1 + 1) kprop → p m) →
      p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (k + 1 + 1) kprop)
Tactic: rcases k with - | k
Cleared hypotheses: k, kprop, hk
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
n : ℕ+
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
⊢ p n
have rcases : (n : ℕ) → (h : 0 < n) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)
Tactic: rcases n with ⟨n, h⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
IH : (h : 0 < n) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)
h : 0 < n + 1
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h)
have succ₁ : (IH : (h : LT.lt (α := ℕ) 0 0) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h)) →
  (h : 0 < HAdd.hAdd (α := ℕ) 0 1) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (HAdd.hAdd (α := ℕ) 0 1) h)
Tactic: rcases n with - | n
Cleared hypotheses: n, IH, h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
IH : (h : 0 < n) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)
h : 0 < n + 1
succ₁ :
  (IH : (h : LT.lt (α := ℕ) 0 0) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h)) →
    (h : 0 < HAdd.hAdd (α := ℕ) 0 1) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (HAdd.hAdd (α := ℕ) 0 1) h)
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h)
have succ₂ : (n : ℕ) →
  (IH : (h : 0 < n + 1) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h)) →
    (h : 0 < n + 1 + 1) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1 + 1) h)
Tactic: rcases n with - | n
Cleared hypotheses: n, IH, h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)
have zero : (h : LT.lt (α := ℕ) 0 0) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h)
Tactic: induction n with
  | zero => exact absurd h (by decide)
  | succ n IH =>
    rcases n with - | n
    · exact one
    · exact succ _ (IH n.succ_pos)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
zero : (h : LT.lt (α := ℕ) 0 0) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h)
⊢ p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)
have succ₁ : (n : ℕ) →
  (IH : (h : 0 < n) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)) →
    (h : 0 < n + 1) → p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h)
Tactic: induction n with
  | zero => exact absurd h (by decide)
  | succ n IH =>
    rcases n with - | n
    · exact one
    · exact succ _ (IH n.succ_pos)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
n : ℕ+
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
⊢ (n + 1).recOn (p := p) one succ = succ n (n.recOn (p := p) one succ)
have obtain : ∀ (n : ℕ) (h : 0 < n),
  Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h + 1))
    ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h + 1).recOn (p := p) one succ)
    (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)
      (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h) (p := p) one succ))
Tactic: obtain ⟨n, h⟩ := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
⊢ Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h + 1))
    ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h + 1).recOn (p := p) one succ)
    (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)
      (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h) (p := p) one succ))
have zero : ∀ (h : LT.lt (α := ℕ) 0 0),
  Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h + 1))
    ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h + 1).recOn (p := p) one succ)
    (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h)
      (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h) (p := p) one succ))
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
zero :
  ∀ (h : LT.lt (α := ℕ) 0 0),
    Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h + 1))
      ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h + 1).recOn (p := p) one succ)
      (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h)
        (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h) (p := p) one succ))
⊢ Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h + 1))
    ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h + 1).recOn (p := p) one succ)
    (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)
      (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h) (p := p) one succ))
have succ₁ : ∀ (n : ℕ) (h : 0 < n + 1),
  Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h + 1))
    ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h + 1).recOn (p := p) one succ)
    (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h)
      (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h) (p := p) one succ))
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
⊢ Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h + 1))
    ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h + 1).recOn (p := p) one succ)
    (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)
      (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h) (p := p) one succ))
have zero : ∀ (h : LT.lt (α := ℕ) 0 0),
  Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h + 1))
    ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h + 1).recOn (p := p) one succ)
    (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h)
      (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h) (p := p) one succ))
Tactic: cases n <;> [exact absurd h (by decide); rfl]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
zero :
  ∀ (h : LT.lt (α := ℕ) 0 0),
    Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h + 1))
      ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h + 1).recOn (p := p) one succ)
      (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h)
        (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) 0 h) (p := p) one succ))
⊢ Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h + 1))
    ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h + 1).recOn (p := p) one succ)
    (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h)
      (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h) (p := p) one succ))
have succ₁ : ∀ (n : ℕ) (h : 0 < n + 1),
  Eq (α := p (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h + 1))
    ((Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h + 1).recOn (p := p) one succ)
    (succ (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h)
      (recOn (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (n + 1) h) (p := p) one succ))
Tactic: cases n <;> [exact absurd h (by decide); rfl]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
a b : ℕ+
⊢ (↑((↑a : ℕ) - (↑b : ℕ)).toPNat' : ℕ) = if b < a then (↑a : ℕ) - (↑b : ℕ) else 1
have pos : ∀ (h : b < a), (↑((↑a : ℕ) - (↑b : ℕ)).toPNat' : ℕ) = (↑a : ℕ) - (↑b : ℕ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.PNat.Basic (goal)
Goal:
a b : ℕ+
pos : ∀ (h : b < a), (↑((↑a : ℕ) - (↑b : ℕ)).toPNat' : ℕ) = (↑a : ℕ) - (↑b : ℕ)
⊢ (↑((↑a : ℕ) - (↑b : ℕ)).toPNat' : ℕ) = if b < a then (↑a : ℕ) - (↑b : ℕ) else 1
have neg : ∀ (h : ¬b < a), (↑((↑a : ℕ) - (↑b : ℕ)).toPNat' : ℕ) = 1
Tactic: split_ifs with h