-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Power2.lean
theorem isPowerOfTwo_nextPowerOfTwo (n : Nat) : n.nextPowerOfTwo.isPowerOfTwo

Proof state:
n : Nat
x✝ : (power : Nat) ×' (_ : power > 0) ×' power.isPowerOfTwo
a✝² :
  ∀ (y : (power : Nat) ×' (_ : power > 0) ×' power.isPowerOfTwo),
    (invImage (fun x => PSigma.casesOn x fun power h₁ => PSigma.casesOn h₁ fun h₁ h₂ => n - power)
            instWellFoundedRelationOfSizeOf).1
        y x✝ →
      (nextPowerOfTwo.go n y.1 ⋯).isPowerOfTwo
power : Nat
h₁✝ : (_ : power > 0) ×' power.isPowerOfTwo
a✝¹ :
  ∀ (y : (power : Nat) ×' (_ : power > 0) ×' power.isPowerOfTwo),
    (invImage (fun x => PSigma.casesOn x fun power h₁ => PSigma.casesOn h₁ fun h₁ h₂ => n - power)
            instWellFoundedRelationOfSizeOf).1
        y ⟨power, h₁✝⟩ →
      (nextPowerOfTwo.go n y.1 ⋯).isPowerOfTwo
h₁ : power > 0
h₂ : power.isPowerOfTwo
a✝ :
  ∀ (y : (power : Nat) ×' (_ : power > 0) ×' power.isPowerOfTwo),
    (invImage (fun x => PSigma.casesOn x fun power h₁ => PSigma.casesOn h₁ fun h₁ h₂ => n - power)
            instWellFoundedRelationOfSizeOf).1
        y ⟨power, ⟨h₁, h₂⟩⟩ →
      (nextPowerOfTwo.go n y.1 ⋯).isPowerOfTwo
h✝ : power < n
⊢ n - power * 2 < n - power

Tactic:
apply nextPowerOfTwo_dec <;> assumption

Result:
no goals

Proof state:
n : Nat
⊢ n.nextPowerOfTwo.isPowerOfTwo

Tactic:
apply isPowerOfTwo_go

Result:
case h₂
n : Nat
⊢ isPowerOfTwo 1

Proof state:
case isTrue
n power : Nat
h₁ : power > 0
h₂ : power.isPowerOfTwo
h✝ : power < n
⊢ (nextPowerOfTwo.go n (power * 2) ⋯).isPowerOfTwo

case isFalse
n power : Nat
h₁ : power > 0
h₂ : power.isPowerOfTwo
h✝ : ¬power < n
⊢ power.isPowerOfTwo

Tactic:
. exact isPowerOfTwo_go (power*2) (Nat.mul_pos h₁ (by decide)) (Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₂)

Result:
case isFalse
n power : Nat
h₁ : power > 0
h₂ : power.isPowerOfTwo
h✝ : ¬power < n
⊢ power.isPowerOfTwo

Proof state:
n power : Nat
h₁ : power > 0
h₂ : power.isPowerOfTwo
⊢ (nextPowerOfTwo.go n power h₁).isPowerOfTwo

Tactic:
unfold nextPowerOfTwo.go

Result:
n power : Nat
h₁ : power > 0
h₂ : power.isPowerOfTwo
⊢ (if power < n then nextPowerOfTwo.go n (power * 2) ⋯ else power).isPowerOfTwo

Proof state:
case isFalse
n power : Nat
h₁ : power > 0
h₂ : power.isPowerOfTwo
h✝ : ¬power < n
⊢ power.isPowerOfTwo

Tactic:
. assumption

Result:
no goals

Proof state:
case h₂
n : Nat
⊢ isPowerOfTwo 1

Tactic:
apply one_isPowerOfTwo

Result:
no goals

Proof state:
n power : Nat
h₁ : power > 0
h₂ : power.isPowerOfTwo
⊢ (if power < n then nextPowerOfTwo.go n (power * 2) ⋯ else power).isPowerOfTwo

Tactic:
split

Result:
case isTrue
n power : Nat
h₁ : power > 0
h₂ : power.isPowerOfTwo
h✝ : power < n
⊢ (nextPowerOfTwo.go n (power * 2) ⋯).isPowerOfTwo

case isFalse
n power : Nat
h₁ : power > 0
h₂ : power.isPowerOfTwo
h✝ : ¬power < n
⊢ power.isPowerOfTwo

Proof state:
n power : Nat
h₁ : power > 0
h₂ : power.isPowerOfTwo
h✝ : power < n
⊢ 2 > 0

Tactic:
decide

Result:
no goals

Proof state:
case isFalse
n power : Nat
h₁ : power > 0
h₂ : power.isPowerOfTwo
h✝ : ¬power < n
⊢ power.isPowerOfTwo

Tactic:
assumption

Result:
no goals

Proof state:
case isTrue
n power : Nat
h₁ : power > 0
h₂ : power.isPowerOfTwo
h✝ : power < n
⊢ (nextPowerOfTwo.go n (power * 2) ⋯).isPowerOfTwo

Tactic:
exact isPowerOfTwo_go (power*2) (Nat.mul_pos h₁ (by decide)) (Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₂)

Result:
no goals