m n : ℕ∞
P : ℕ∞ → Prop
a : ℕ∞
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
⊢ P a
m n : ℕ∞
P : ℕ∞ → Prop
a : ℕ∞
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
⊢ P a
have A : ∀ n : ℕ, P n := fun n => Nat.recOn n h0 hsuc
case none
m n : ℕ∞
P : ℕ∞ → Prop
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
⊢ P none

case some
m n : ℕ∞
P : ℕ∞ → Prop
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
val✝ : ℕ
⊢ P (some val✝)
m n : ℕ∞
P : ℕ∞ → Prop
a : ℕ∞
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
⊢ P a
cases a
case some
m n : ℕ∞
P : ℕ∞ → Prop
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
val✝ : ℕ
⊢ P (some val✝)
case none
m n : ℕ∞
P : ℕ∞ → Prop
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
⊢ P none

case some
m n : ℕ∞
P : ℕ∞ → Prop
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
val✝ : ℕ
⊢ P (some val✝)
. exact htop A
no goals
case some
m n : ℕ∞
P : ℕ∞ → Prop
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
val✝ : ℕ
⊢ P (some val✝)
. exact A _
no goals
case none
m n : ℕ∞
P : ℕ∞ → Prop
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
⊢ P none
exact htop A
no goals
case some
m n : ℕ∞
P : ℕ∞ → Prop
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
val✝ : ℕ
⊢ P (some val✝)
exact A _