case h₂
n : Nat
⊢ isPowerOfTwo 1
n : Nat
⊢ isPowerOfTwo (nextPowerOfTwo n)
apply isPowerOfTwo_go
no goals
case h₂
n : Nat
⊢ isPowerOfTwo 1
apply one_isPowerOfTwo
n power : Nat
h₁ : power > 0
h₂ : isPowerOfTwo power
⊢ isPowerOfTwo (if power < n then nextPowerOfTwo.go n (power * 2) (_ : power * 2 > 0) else power)
n power : Nat
h₁ : power > 0
h₂ : isPowerOfTwo power
⊢ isPowerOfTwo (nextPowerOfTwo.go n power h₁)
unfold nextPowerOfTwo.go
case inl
n power : Nat
h₁ : power > 0
h₂ : isPowerOfTwo power
h✝ : power < n
⊢ isPowerOfTwo (nextPowerOfTwo.go n (power * 2) (_ : power * 2 > 0))

case inr
n power : Nat
h₁ : power > 0
h₂ : isPowerOfTwo power
h✝ : ¬power < n
⊢ isPowerOfTwo power
n power : Nat
h₁ : power > 0
h₂ : isPowerOfTwo power
⊢ isPowerOfTwo (if power < n then nextPowerOfTwo.go n (power * 2) (_ : power * 2 > 0) else power)
split
case inr
n power : Nat
h₁ : power > 0
h₂ : isPowerOfTwo power
h✝ : ¬power < n
⊢ isPowerOfTwo power
case inl
n power : Nat
h₁ : power > 0
h₂ : isPowerOfTwo power
h✝ : power < n
⊢ isPowerOfTwo (nextPowerOfTwo.go n (power * 2) (_ : power * 2 > 0))

case inr
n power : Nat
h₁ : power > 0
h₂ : isPowerOfTwo power
h✝ : ¬power < n
⊢ isPowerOfTwo power
. exact isPowerOfTwo_go (power*2) (Nat.mul_pos h₁ (by decide)) (Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₂)
no goals
case inr
n power : Nat
h₁ : power > 0
h₂ : isPowerOfTwo power
h✝ : ¬power < n
⊢ isPowerOfTwo power
. assumption
no goals
case inl
n power : Nat
h₁ : power > 0
h₂ : isPowerOfTwo power
h✝ : power < n
⊢ isPowerOfTwo (nextPowerOfTwo.go n (power * 2) (_ : power * 2 > 0))
exact isPowerOfTwo_go (power*2) (Nat.mul_pos h₁ (by decide)) (Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₂)
no goals
n power : Nat
h₁ : power > 0
h₂ : isPowerOfTwo power
h✝ : power < n
⊢ 2 > 0
decide
no goals
case inr
n power : Nat
h₁ : power > 0
h₂ : isPowerOfTwo power
h✝ : ¬power < n
⊢ isPowerOfTwo power
assumption
n : Nat
_x✝ : (power : Nat) ×' (_ : power > 0) ×' isPowerOfTwo power
a✝² :
  ∀ (y : (power : Nat) ×' (_ : power > 0) ×' isPowerOfTwo power),
    (invImage (fun a => PSigma.casesOn a fun p snd => PSigma.casesOn snd fun h₁ snd => n - p) instWellFoundedRelation).1
        y _x✝ →
      isPowerOfTwo (nextPowerOfTwo.go n y.1 (_ : y.1 > 0))
power : Nat
h₁✝ : (_ : power > 0) ×' isPowerOfTwo power
a✝¹ :
  ∀ (y : (power : Nat) ×' (_ : power > 0) ×' isPowerOfTwo power),
    (invImage (fun a => PSigma.casesOn a fun p snd => PSigma.casesOn snd fun h₁ snd => n - p) instWellFoundedRelation).1
        y { fst := power, snd := h₁✝ } →
      isPowerOfTwo (nextPowerOfTwo.go n y.1 (_ : y.1 > 0))
h₁ : power > 0
h₂ : isPowerOfTwo power
a✝ :
  ∀ (y : (power : Nat) ×' (_ : power > 0) ×' isPowerOfTwo power),
    (invImage (fun a => PSigma.casesOn a fun p snd => PSigma.casesOn snd fun h₁ snd => n - p) instWellFoundedRelation).1
        y { fst := power, snd := { fst := h₁, snd := h₂ } } →
      isPowerOfTwo (nextPowerOfTwo.go n y.1 (_ : y.1 > 0))
h✝ : power < n
⊢ n - power * 2 < n - power
n : Nat
_x✝ : (power : Nat) ×' (_ : power > 0) ×' isPowerOfTwo power
a✝² :
  ∀ (y : (power : Nat) ×' (_ : power > 0) ×' isPowerOfTwo power),
    (invImage (fun a => PSigma.casesOn a fun p snd => PSigma.casesOn snd fun h₁ snd => n - p) instWellFoundedRelation).1
        y _x✝ →
      isPowerOfTwo (nextPowerOfTwo.go n y.1 (_ : y.1 > 0))
power : Nat
h₁✝ : (_ : power > 0) ×' isPowerOfTwo power
a✝¹ :
  ∀ (y : (power : Nat) ×' (_ : power > 0) ×' isPowerOfTwo power),
    (invImage (fun a => PSigma.casesOn a fun p snd => PSigma.casesOn snd fun h₁ snd => n - p) instWellFoundedRelation).1
        y { fst := power, snd := h₁✝ } →
      isPowerOfTwo (nextPowerOfTwo.go n y.1 (_ : y.1 > 0))
h₁ : power > 0
h₂ : isPowerOfTwo power
a✝ :
  ∀ (y : (power : Nat) ×' (_ : power > 0) ×' isPowerOfTwo power),
    (invImage (fun a => PSigma.casesOn a fun p snd => PSigma.casesOn snd fun h₁ snd => n - p) instWellFoundedRelation).1
        y { fst := power, snd := { fst := h₁, snd := h₂ } } →
      isPowerOfTwo (nextPowerOfTwo.go n y.1 (_ : y.1 > 0))
h✝ : power < n
⊢ (invImage (fun a => PSigma.casesOn a fun p snd => PSigma.casesOn snd fun h₁ snd => n - p) instWellFoundedRelation).1
    { fst := power * 2, snd := { fst := (_ : power * 2 > 0), snd := (_ : isPowerOfTwo (power * 2)) } }
    { fst := power, snd := { fst := h₁, snd := h₂ } }
simp_wf
no goals
n : Nat
_x✝ : (power : Nat) ×' (_ : power > 0) ×' isPowerOfTwo power
a✝² :
  ∀ (y : (power : Nat) ×' (_ : power > 0) ×' isPowerOfTwo power),
    (invImage (fun a => PSigma.casesOn a fun p snd => PSigma.casesOn snd fun h₁ snd => n - p) instWellFoundedRelation).1
        y _x✝ →
      isPowerOfTwo (nextPowerOfTwo.go n y.1 (_ : y.1 > 0))
power : Nat
h₁✝ : (_ : power > 0) ×' isPowerOfTwo power
a✝¹ :
  ∀ (y : (power : Nat) ×' (_ : power > 0) ×' isPowerOfTwo power),
    (invImage (fun a => PSigma.casesOn a fun p snd => PSigma.casesOn snd fun h₁ snd => n - p) instWellFoundedRelation).1
        y { fst := power, snd := h₁✝ } →
      isPowerOfTwo (nextPowerOfTwo.go n y.1 (_ : y.1 > 0))
h₁ : power > 0
h₂ : isPowerOfTwo power
a✝ :
  ∀ (y : (power : Nat) ×' (_ : power > 0) ×' isPowerOfTwo power),
    (invImage (fun a => PSigma.casesOn a fun p snd => PSigma.casesOn snd fun h₁ snd => n - p) instWellFoundedRelation).1
        y { fst := power, snd := { fst := h₁, snd := h₂ } } →
      isPowerOfTwo (nextPowerOfTwo.go n y.1 (_ : y.1 > 0))
h✝ : power < n
⊢ n - power * 2 < n - power
apply nextPowerOfTwo_dec <;> assumption