[GOAL]
⊢ DecidableRel fun x x_1 => x ≤ x_1
[PROOFSTEP]
infer_instance
[GOAL]
⊢ DecidableEq ℤ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ DecidableRel fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance
[GOAL]
a b : ℤ
h : a * b = 0
hlt₁ : 0 < a
hlt₂ : 0 < b
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
have : 0 < a * b := Int.mul_pos hlt₁ hlt₂
[GOAL]
a b : ℤ
h : a * b = 0
hlt₁ : 0 < a
hlt₂ : 0 < b
this : 0 < a * b
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
rw [h] at this
[GOAL]
a b : ℤ
h : a * b = 0
hlt₁ : 0 < a
hlt₂ : 0 < b
this : 0 < 0
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
exact absurd this (lt_irrefl _)
[GOAL]
a b : ℤ
h : a * b = 0
hlt₁ : 0 < a
hgt₂ : b < 0
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
have : 0 > a * b := Int.mul_neg_of_pos_of_neg hlt₁ hgt₂
[GOAL]
a b : ℤ
h : a * b = 0
hlt₁ : 0 < a
hgt₂ : b < 0
this : 0 > a * b
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
rw [h] at this
[GOAL]
a b : ℤ
h : a * b = 0
hlt₁ : 0 < a
hgt₂ : b < 0
this : 0 > 0
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
exact absurd this (lt_irrefl _)
[GOAL]
a b : ℤ
h : a * b = 0
hgt₁ : a < 0
hlt₂ : 0 < b
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
have : 0 > a * b := Int.mul_neg_of_neg_of_pos hgt₁ hlt₂
[GOAL]
a b : ℤ
h : a * b = 0
hgt₁ : a < 0
hlt₂ : 0 < b
this : 0 > a * b
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
rw [h] at this
[GOAL]
a b : ℤ
h : a * b = 0
hgt₁ : a < 0
hlt₂ : 0 < b
this : 0 > 0
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
exact absurd this (lt_irrefl _)
[GOAL]
a b : ℤ
h : a * b = 0
hgt₁ : a < 0
hgt₂ : b < 0
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
have : 0 < a * b := Int.mul_pos_of_neg_of_neg hgt₁ hgt₂
[GOAL]
a b : ℤ
h : a * b = 0
hgt₁ : a < 0
hgt₂ : b < 0
this : 0 < a * b
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
rw [h] at this
[GOAL]
a b : ℤ
h : a * b = 0
hgt₁ : a < 0
hgt₂ : b < 0
this : 0 < 0
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
exact absurd this (lt_irrefl _)


[GOAL]
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ run (f <$> x) = Option.map f <$> run x
[PROOFSTEP]
rw [← bind_pure_comp _ x.run]
[GOAL]
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ run (f <$> x) = do
    let a ← run x
    pure (Option.map f a)
[PROOFSTEP]
change
  x.run >>=
      (fun
        | some a => OptionT.run (pure (f a))
        | none => pure none) =
    _
[GOAL]
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ (do
      let x ← run x
      match x with
        | some a => run (pure (f a))
        | none => pure none) =
    do
    let a ← run x
    pure (Option.map f a)
[PROOFSTEP]
apply bind_congr
[GOAL]
case h
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ ∀ (a : Option α),
    (match a with
      | some a => run (pure (f a))
      | none => pure none) =
      pure (Option.map f a)
[PROOFSTEP]
intro a
[GOAL]
case h
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
a : Option α
⊢ (match a with
    | some a => run (pure (f a))
    | none => pure none) =
    pure (Option.map f a)
[PROOFSTEP]
cases a
[GOAL]
case h.none
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
⊢ (match none with
    | some a => run (pure (f a))
    | none => pure none) =
    pure (Option.map f none)
[PROOFSTEP]
simp [Option.map, Option.bind]
[GOAL]
case h.some
α β : Type u
m : Type u → Type v
x : OptionT m α
inst✝¹ : Monad m
f : α → β
inst✝ : LawfulMonad m
val✝ : α
⊢ (match some val✝ with
    | some a => run (pure (f a))
    | none => pure none) =
    pure (Option.map f (some val✝))
[PROOFSTEP]
simp [Option.map, Option.bind]
[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {α : Type u} (x : OptionT m α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ : Type u
x✝ : OptionT m α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
apply OptionT.ext
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ : Type u
x✝ : OptionT m α✝
⊢ OptionT.run (id <$> x✝) = OptionT.run x✝
[PROOFSTEP]
simp only [OptionT.run_map]
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ : Type u
x✝ : OptionT m α✝
⊢ Option.map id <$> OptionT.run x✝ = OptionT.run x✝
[PROOFSTEP]
rw [map_congr, id_map]
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ : Type u
x✝ : OptionT m α✝
⊢ ∀ (a : Option α✝), Option.map id a = id a
[PROOFSTEP]
intro a
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ : Type u
x✝ : OptionT m α✝
a : Option α✝
⊢ Option.map id a = id a
[PROOFSTEP]
cases a
[GOAL]
case h.none
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ : Type u
x✝ : OptionT m α✝
⊢ Option.map id none = id none
[PROOFSTEP]
rfl
[GOAL]
case h.some
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ : Type u
x✝ : OptionT m α✝
val✝ : α✝
⊢ Option.map id (some val✝) = id (some val✝)
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {α β : Type u} (x : α) (f : α → OptionT m β), pure x >>= f = f x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ : Type u
x✝ : α✝
f✝ : α✝ → OptionT m β✝
⊢ pure x✝ >>= f✝ = f✝ x✝
[PROOFSTEP]
apply OptionT.ext
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ : Type u
x✝ : α✝
f✝ : α✝ → OptionT m β✝
⊢ OptionT.run (pure x✝ >>= f✝) = OptionT.run (f✝ x✝)
[PROOFSTEP]
simp
[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {α β γ : Type u} (x : OptionT m α) (f : α → OptionT m β) (g : β → OptionT m γ),
    x >>= f >>= g = x >>= fun x => f x >>= g
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ γ✝ : Type u
x✝ : OptionT m α✝
f✝ : α✝ → OptionT m β✝
g✝ : β✝ → OptionT m γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
apply OptionT.ext
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ γ✝ : Type u
x✝ : OptionT m α✝
f✝ : α✝ → OptionT m β✝
g✝ : β✝ → OptionT m γ✝
⊢ OptionT.run (x✝ >>= f✝ >>= g✝) = OptionT.run (x✝ >>= fun x => f✝ x >>= g✝)
[PROOFSTEP]
simp only [OptionT.run_bind, bind_assoc]
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ γ✝ : Type u
x✝ : OptionT m α✝
f✝ : α✝ → OptionT m β✝
g✝ : β✝ → OptionT m γ✝
⊢ (do
      let x ← OptionT.run x✝
      let x ←
        match x with
          | some a => OptionT.run (f✝ a)
          | none => pure none
      match x with
        | some a => OptionT.run (g✝ a)
        | none => pure none) =
    do
    let x ← OptionT.run x✝
    match x with
      | some a => do
        let x ← OptionT.run (f✝ a)
        match x with
          | some a => OptionT.run (g✝ a)
          | none => pure none
      | none => pure none
[PROOFSTEP]
rw [bind_congr]
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ γ✝ : Type u
x✝ : OptionT m α✝
f✝ : α✝ → OptionT m β✝
g✝ : β✝ → OptionT m γ✝
⊢ ∀ (a : Option α✝),
    (do
        let x ←
          match a with
            | some a => OptionT.run (f✝ a)
            | none => pure none
        match x with
          | some a => OptionT.run (g✝ a)
          | none => pure none) =
      match a with
      | some a => do
        let x ← OptionT.run (f✝ a)
        match x with
          | some a => OptionT.run (g✝ a)
          | none => pure none
      | none => pure none
[PROOFSTEP]
intro a
[GOAL]
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ γ✝ : Type u
x✝ : OptionT m α✝
f✝ : α✝ → OptionT m β✝
g✝ : β✝ → OptionT m γ✝
a : Option α✝
⊢ (do
      let x ←
        match a with
          | some a => OptionT.run (f✝ a)
          | none => pure none
      match x with
        | some a => OptionT.run (g✝ a)
        | none => pure none) =
    match a with
    | some a => do
      let x ← OptionT.run (f✝ a)
      match x with
        | some a => OptionT.run (g✝ a)
        | none => pure none
    | none => pure none
[PROOFSTEP]
cases a
[GOAL]
case h.none
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ γ✝ : Type u
x✝ : OptionT m α✝
f✝ : α✝ → OptionT m β✝
g✝ : β✝ → OptionT m γ✝
⊢ (do
      let x ←
        match none with
          | some a => OptionT.run (f✝ a)
          | none => pure none
      match x with
        | some a => OptionT.run (g✝ a)
        | none => pure none) =
    match none with
    | some a => do
      let x ← OptionT.run (f✝ a)
      match x with
        | some a => OptionT.run (g✝ a)
        | none => pure none
    | none => pure none
[PROOFSTEP]
simp
[GOAL]
case h.some
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α✝ β✝ γ✝ : Type u
x✝ : OptionT m α✝
f✝ : α✝ → OptionT m β✝
g✝ : β✝ → OptionT m γ✝
val✝ : α✝
⊢ (do
      let x ←
        match some val✝ with
          | some a => OptionT.run (f✝ a)
          | none => pure none
      match x with
        | some a => OptionT.run (g✝ a)
        | none => pure none) =
    match some val✝ with
    | some a => do
      let x ← OptionT.run (f✝ a)
      match x with
        | some a => OptionT.run (g✝ a)
        | none => pure none
    | none => pure none
[PROOFSTEP]
simp


[GOAL]
a : ℤ
h₁ : a ≠ 0
h₂ : -a = 0
⊢ False
[PROOFSTEP]
have : -a = -0 := by rwa [Int.neg_zero]
[GOAL]
a : ℤ
h₁ : a ≠ 0
h₂ : -a = 0
⊢ -a = -0
[PROOFSTEP]
rwa [Int.neg_zero]
[GOAL]
a : ℤ
h₁ : a ≠ 0
h₂ : -a = 0
this : -a = -0
⊢ False
[PROOFSTEP]
have : a = 0 := Int.neg_eq_neg this
[GOAL]
a : ℤ
h₁ : a ≠ 0
h₂ : -a = 0
this✝ : -a = -0
this : a = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
a b : ℤ
h₁ : 0 < a
h₂ : 0 < b
h : -a = b
⊢ False
[PROOFSTEP]
rw [← h] at h₂
[GOAL]
a b : ℤ
h₁ : 0 < a
h₂ : 0 < -a
h : -a = b
⊢ False
[PROOFSTEP]
exact absurd (le_of_lt h₁) (not_le_of_gt (Int.neg_of_neg_pos h₂))
[GOAL]
n : ℕ
⊢ 0 + ↑n = ofNat n
[PROOFSTEP]
rw [Int.zero_add, Int.coe_nat_eq]
[GOAL]
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
h✝ : natAbs a ≠ natAbs b
h : a = b
⊢ False
[PROOFSTEP]
have : (natAbs a : ℤ) = natAbs b := by rwa [ofNat_natAbs_eq_of_nonneg _ ha, ofNat_natAbs_eq_of_nonneg _ hb]
[GOAL]
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
h✝ : natAbs a ≠ natAbs b
h : a = b
⊢ ↑(natAbs a) = ↑(natAbs b)
[PROOFSTEP]
rwa [ofNat_natAbs_eq_of_nonneg _ ha, ofNat_natAbs_eq_of_nonneg _ hb]
[GOAL]
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
h✝ : natAbs a ≠ natAbs b
h : a = b
this : ↑(natAbs a) = ↑(natAbs b)
⊢ False
[PROOFSTEP]
injection this
[GOAL]
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
h✝ : natAbs a ≠ natAbs b
h : a = b
a_eq✝ : natAbs a = natAbs b
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
a b : ℤ
n m : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
e1 : natAbs a = n
e2 : natAbs b = m
h : n ≠ m
⊢ natAbs a ≠ natAbs b
[PROOFSTEP]
rwa [e1, e2]
[GOAL]
n m : ℕ
x✝¹ : 0 ≤ ofNat n
x✝ : 0 ≤ ofNat m
⊢ natAbs (ofNat n + ofNat m) = natAbs (ofNat n) + natAbs (ofNat m)
[PROOFSTEP]
simp [natAbs_ofNat_core]
[GOAL]
n m : ℕ
x✝¹ : -[n+1] < 0
x✝ : -[m+1] < 0
⊢ natAbs (-[n+1] + -[m+1]) = natAbs -[n+1] + natAbs -[m+1]
[PROOFSTEP]
simp [natAbs_of_negSucc, Nat.succ_add, Nat.add_succ]
[GOAL]
a : ℤ
n : ℕ
h : natAbs a = n
⊢ natAbs (bit0 a) = bit0 n
[PROOFSTEP]
rw [← h]
[GOAL]
a : ℤ
n : ℕ
h : natAbs a = n
⊢ natAbs (bit0 a) = bit0 (natAbs a)
[PROOFSTEP]
apply Int.natAbs_bit0
[GOAL]
a : ℤ
h : 0 ≤ a
⊢ natAbs (bit0 a + 1) = bit0 (natAbs a) + natAbs 1
[PROOFSTEP]
rw [Int.natAbs_add_nonneg (Int.bit0_nonneg h) (le_of_lt Int.zero_lt_one), Int.natAbs_bit0]
[GOAL]
a : ℤ
n : ℕ
h₁ : 0 ≤ a
h₂ : natAbs a = n
⊢ natAbs (bit1 a) = bit1 n
[PROOFSTEP]
rw [← h₂]
[GOAL]
a : ℤ
n : ℕ
h₁ : 0 ≤ a
h₂ : natAbs a = n
⊢ natAbs (bit1 a) = bit1 (natAbs a)
[PROOFSTEP]
apply Int.natAbs_bit1_nonneg h₁


[GOAL]
x y : ℕ
⊢ gcd x y = if x = 0 then y else gcd (y % x) x
[PROOFSTEP]
cases x
[GOAL]
case zero
y : ℕ
⊢ gcd zero y = if zero = 0 then y else gcd (y % zero) zero
[PROOFSTEP]
simp [Nat.gcd_succ]
[GOAL]
case succ
y n✝ : ℕ
⊢ gcd (succ n✝) y = if succ n✝ = 0 then y else gcd (y % succ n✝) (succ n✝)
[PROOFSTEP]
simp [Nat.gcd_succ]


[GOAL]
α : Type u
β : Type v
γ : Type w
p : α → Prop
a : α
l : List α
x✝ : ∃ x, x ∈ a :: l ∧ p x
x : α
h : x ∈ a :: l
px : p x
⊢ p a ∨ ∃ x, x ∈ l ∧ p x
[PROOFSTEP]
simp only [find?, mem_cons] at h
[GOAL]
α : Type u
β : Type v
γ : Type w
p : α → Prop
a : α
l : List α
x✝ : ∃ x, x ∈ a :: l ∧ p x
x : α
px : p x
h : x = a ∨ x ∈ l
⊢ p a ∨ ∃ x, x ∈ l ∧ p x
[PROOFSTEP]
cases' h with h h
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
p : α → Prop
a : α
l : List α
x✝ : ∃ x, x ∈ a :: l ∧ p x
x : α
px : p x
h : x = a
⊢ p a ∨ ∃ x, x ∈ l ∧ p x
[PROOFSTEP]
cases h
[GOAL]
case inl.refl
α : Type u
β : Type v
γ : Type w
p : α → Prop
a : α
l : List α
x✝ : ∃ x, x ∈ a :: l ∧ p x
px : p a
⊢ p a ∨ ∃ x, x ∈ l ∧ p x
[PROOFSTEP]
exact Or.inl px
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
p : α → Prop
a : α
l : List α
x✝ : ∃ x, x ∈ a :: l ∧ p x
x : α
px : p x
h : x ∈ l
⊢ p a ∨ ∃ x, x ∈ l ∧ p x
[PROOFSTEP]
exact Or.inr ⟨x, h, px⟩


[GOAL]
a b c d : Prop
p : ?m.25026
h : Decidable True
⊢ decide True = true
[PROOFSTEP]
simp
[GOAL]
a b c d : Prop
p : ?m.25099
h : Decidable False
⊢ decide False = false
[PROOFSTEP]
simp
[GOAL]
a b c d p : Prop
h : Decidable p
h₁ : p → Sort u
h₂ : ¬p → Sort u
h₃ : p
h₄ : h₁ h₃
⊢ h₁ h₃ = Decidable.recOn h h₂ h₁
[PROOFSTEP]
match h with
| .isTrue _ => rfl
[GOAL]
a b c d p : Prop
h : Decidable p
h₁ : p → Sort u
h₂ : ¬p → Sort u
h₃ : p
h₄ : h₁ h₃
h✝ : p
⊢ h₁ h₃ = Decidable.recOn (isTrue h✝) h₂ h₁
[PROOFSTEP]
rfl
[GOAL]
a b c d p : Prop
h : Decidable p
h₁ : p → Sort u
h₂ : ¬p → Sort u
h₃ : ¬p
h₄ : h₂ h₃
⊢ h₂ h₃ = Decidable.recOn h h₂ h₁
[PROOFSTEP]
match h with
| .isFalse _ => rfl
[GOAL]
a b c d p : Prop
h : Decidable p
h₁ : p → Sort u
h₂ : ¬p → Sort u
h₃ : ¬p
h₄ : h₂ h₃
h✝ : ¬p
⊢ h₂ h₃ = Decidable.recOn (isFalse h✝) h₂ h₁
[PROOFSTEP]
rfl
[GOAL]
a b c d : Prop
p✝ : ?m.26639
α : Sort u
p : α → α → Bool
h₁ : IsDecEq p
h₂ : IsDecRefl p
x y : α
hp : ¬p x y = true
hxy : x = y
⊢ ¬p y y = true
[PROOFSTEP]
rwa [hxy] at hp
[GOAL]
a b c✝ d : Prop
p : ?m.27547
c t e : Prop
inst✝ : Decidable c
h : if c then t else e
hc : c
⊢ t
[PROOFSTEP]
have := if_pos hc ▸ h
[GOAL]
a b c✝ d : Prop
p : ?m.27547
c t e : Prop
inst✝ : Decidable c
h : if c then t else e
hc : c
this : t
⊢ t
[PROOFSTEP]
exact this
[GOAL]
a b c✝ d : Prop
p : ?m.27609
c t e : Prop
inst✝ : Decidable c
h : if c then t else e
hnc : ¬c
⊢ e
[PROOFSTEP]
have := if_neg hnc ▸ h
[GOAL]
a b c✝ d : Prop
p : ?m.27609
c t e : Prop
inst✝ : Decidable c
h : if c then t else e
hnc : ¬c
this : e
⊢ e
[PROOFSTEP]
exact this
[GOAL]
a b✝ c d : Prop
p : ?m.29900
α : Sort v
β : α → Sort u
a₁ a₂ : α
b : (x : α) → β x
h : a₁ = a₂
⊢ HEq
    (let x := a₁;
    b x)
    (let x := a₂;
    b x)
[PROOFSTEP]
cases h
[GOAL]
case refl
a b✝ c d : Prop
p : ?m.29900
α : Sort v
β : α → Sort u
a₁ : α
b : (x : α) → β x
⊢ HEq
    (let x := a₁;
    b x)
    (let x := a₁;
    b x)
[PROOFSTEP]
rfl
[GOAL]
a✝ b c d : Prop
p : ?m.30034
α : Sort v
β : α → Sort u
a : α
b₁ b₂ : (x : α) → β x
h : ∀ (x : α), b₁ x = b₂ x
⊢ (let x := a;
    b₁ x) =
    let x := a;
    b₂ x
[PROOFSTEP]
exact h _ ▸ rfl
[GOAL]
a b c d : Prop
p : ?m.30108
α : Sort v
β : Sort u
a₁ a₂ : α
b₁ b₂ : α → β
h₁ : a₁ = a₂
h₂ : ∀ (x : α), b₁ x = b₂ x
⊢ (let x := a₁;
    b₁ x) =
    let x := a₂;
    b₂ x
[PROOFSTEP]
simp [h₁, h₂]


[GOAL]
a b : ℕ
h : 0 < b
⊢ a + 0 < a + b
[PROOFSTEP]
apply Nat.add_lt_add_left
[GOAL]
case h
a b : ℕ
h : 0 < b
⊢ 0 < b
[PROOFSTEP]
assumption
[GOAL]
a : ℕ
this : 0 < a + 1
⊢ 0 < 1 + a
[PROOFSTEP]
simp [Nat.add_comm]
[GOAL]
a : ℕ
this : 0 < a + 1
⊢ 0 < a + 1
[PROOFSTEP]
assumption


[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed K
f : k →+* K
p : k[X]
h : Separable p
⊢ Splits f p
[PROOFSTEP]
convert IsSepClosed.splits_of_separable (p.map f) (Separable.map h)
[GOAL]
case a
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed K
f : k →+* K
p : k[X]
h : Separable p
⊢ Splits f p ↔ Splits (RingHom.id K) (map f p)
[PROOFSTEP]
simp [splits_map_iff]
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
⊢ ∃ z, z ^ n = x
[PROOFSTEP]
have hn' : 0 < n :=
  Nat.pos_of_ne_zero <| fun h => by
    rw [h, Nat.cast_zero] at hn
    exact hn.out rfl
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
h : n = 0
⊢ False
[PROOFSTEP]
rw [h, Nat.cast_zero] at hn
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero 0
h : n = 0
⊢ False
[PROOFSTEP]
exact hn.out rfl
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
⊢ ∃ z, z ^ n = x
[PROOFSTEP]
have : degree (X ^ n - C x) ≠ 0 := by
  rw [degree_X_pow_sub_C hn' x]
  exact (WithBot.coe_lt_coe.2 hn').ne'
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
⊢ degree (X ^ n - ↑C x) ≠ 0
[PROOFSTEP]
rw [degree_X_pow_sub_C hn' x]
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
⊢ ↑n ≠ 0
[PROOFSTEP]
exact (WithBot.coe_lt_coe.2 hn').ne'
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
⊢ ∃ z, z ^ n = x
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
hx : x = 0
⊢ ∃ z, z ^ n = x
[PROOFSTEP]
exact ⟨0, by rw [hx, pow_eq_zero_iff hn']⟩
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
hx : x = 0
⊢ 0 ^ n = x
[PROOFSTEP]
rw [hx, pow_eq_zero_iff hn']
[GOAL]
case neg
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
hx : ¬x = 0
⊢ ∃ z, z ^ n = x
[PROOFSTEP]
obtain ⟨z, hz⟩ := exists_root _ this <| separable_X_pow_sub_C x hn.out hx
[GOAL]
case neg.intro
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
hx : ¬x = 0
z : k
hz : IsRoot (X ^ n - ↑C x) z
⊢ ∃ z, z ^ n = x
[PROOFSTEP]
use z
[GOAL]
case h
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : degree (X ^ n - ↑C x) ≠ 0
hx : ¬x = 0
z : k
hz : IsRoot (X ^ n - ↑C x) z
⊢ z ^ n = x
[PROOFSTEP]
simpa [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def, sub_eq_zero] using hz
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
x : k
h2 : NeZero 2
⊢ ∃ z, x = z * z
[PROOFSTEP]
rcases exists_pow_nat_eq x 2 with ⟨z, rfl⟩
[GOAL]
case intro
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
h2 : NeZero 2
z : k
⊢ ∃ z_1, z ^ 2 = z_1 * z_1
[PROOFSTEP]
exact ⟨z, sq z⟩
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
p : k[X]
hsep : Separable p
⊢ roots p = 0 ↔ p = ↑C (coeff p 0)
[PROOFSTEP]
refine' ⟨fun h => _, fun hp => by rw [hp, roots_C]⟩
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
p : k[X]
hsep : Separable p
hp : p = ↑C (coeff p 0)
⊢ roots p = 0
[PROOFSTEP]
rw [hp, roots_C]
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
p : k[X]
hsep : Separable p
h : roots p = 0
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
cases' le_or_lt (degree p) 0 with hd hd
[GOAL]
case inl
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
p : k[X]
hsep : Separable p
h : roots p = 0
hd : degree p ≤ 0
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
exact eq_C_of_degree_le_zero hd
[GOAL]
case inr
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
p : k[X]
hsep : Separable p
h : roots p = 0
hd : 0 < degree p
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
obtain ⟨z, hz⟩ := IsSepClosed.exists_root p hd.ne' hsep
[GOAL]
case inr.intro
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
p : k[X]
hsep : Separable p
h : roots p = 0
hd : 0 < degree p
z : k
hz : IsRoot p z
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
rw [← mem_roots (ne_zero_of_degree_gt hd), h] at hz
[GOAL]
case inr.intro
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed k
p : k[X]
hsep : Separable p
h : roots p = 0
hd : 0 < degree p
z : k
hz : z ∈ 0
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
simp at hz
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed K
f : k →+* K
p : k[X]
hp : degree p ≠ 0
hsep : Separable p
⊢ degree (map f p) ≠ 0
[PROOFSTEP]
rwa [degree_map_eq_of_injective f.injective]
[GOAL]
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed K
f : k →+* K
p : k[X]
hp : degree p ≠ 0
hsep : Separable p
x : K
hx : IsRoot (map f p) x
⊢ eval₂ f x p = 0
[PROOFSTEP]
rwa [eval₂_eq_eval_map, ← IsRoot]
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
⊢ IsSepClosed k
[PROOFSTEP]
refine ⟨fun p hsep ↦ Or.inr ?_⟩
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
⊢ ∀ {g : k[X]}, Irreducible g → g ∣ map (RingHom.id k) p → degree g = 1
[PROOFSTEP]
intro q hq hdvd
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
q : k[X]
hq : Irreducible q
hdvd : q ∣ map (RingHom.id k) p
⊢ degree q = 1
[PROOFSTEP]
simp only [map_id] at hdvd
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
⊢ degree q = 1
[PROOFSTEP]
have hlc : IsUnit (leadingCoeff q)⁻¹ := IsUnit.inv <| Ne.isUnit <| leadingCoeff_ne_zero.2 <| Irreducible.ne_zero hq
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit (leadingCoeff q)⁻¹
⊢ degree q = 1
[PROOFSTEP]
have hsep' : Separable (q * C (leadingCoeff q)⁻¹) :=
  Separable.mul (Separable.of_dvd hsep hdvd) ((separable_C _).2 hlc)
    (by simpa only [← isCoprime_mul_unit_right_right (isUnit_C.2 hlc) q 1, one_mul] using isCoprime_one_right (x := q))
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit (leadingCoeff q)⁻¹
⊢ IsCoprime q (↑C (leadingCoeff q)⁻¹)
[PROOFSTEP]
simpa only [← isCoprime_mul_unit_right_right (isUnit_C.2 hlc) q 1, one_mul] using isCoprime_one_right (x := q)
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit (leadingCoeff q)⁻¹
hsep' : Separable (q * ↑C (leadingCoeff q)⁻¹)
⊢ degree q = 1
[PROOFSTEP]
have hirr' := hq
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit (leadingCoeff q)⁻¹
hsep' : Separable (q * ↑C (leadingCoeff q)⁻¹)
hirr' : Irreducible q
⊢ degree q = 1
[PROOFSTEP]
rw [← irreducible_mul_isUnit (isUnit_C.2 hlc)] at hirr'
[GOAL]
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit (leadingCoeff q)⁻¹
hsep' : Separable (q * ↑C (leadingCoeff q)⁻¹)
hirr' : Irreducible (q * ↑C (leadingCoeff q)⁻¹)
⊢ degree q = 1
[PROOFSTEP]
obtain ⟨x, hx⟩ := H (q * C (leadingCoeff q)⁻¹) (monic_mul_leadingCoeff_inv hq.ne_zero) hirr' hsep'
[GOAL]
case intro
k : Type u
inst✝¹ : Field k
K : Type v
inst✝ : Field K
H : ∀ (p : k[X]), Monic p → Irreducible p → Separable p → ∃ x, eval x p = 0
p : k[X]
hsep : Separable p
q : k[X]
hq : Irreducible q
hdvd : q ∣ p
hlc : IsUnit (leadingCoeff q)⁻¹
hsep' : Separable (q * ↑C (leadingCoeff q)⁻¹)
hirr' : Irreducible (q * ↑C (leadingCoeff q)⁻¹)
x : k
hx : eval x (q * ↑C (leadingCoeff q)⁻¹) = 0
⊢ degree q = 1
[PROOFSTEP]
exact degree_mul_leadingCoeff_inv q hq.ne_zero ▸ degree_eq_one_of_irreducible_of_root hirr' hx
[GOAL]
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : IsSeparable k K
⊢ Function.Surjective ↑(algebraMap k K)
[PROOFSTEP]
refine fun x => ⟨-(minpoly k x).coeff 0, ?_⟩
[GOAL]
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : IsSeparable k K
x : K
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
[PROOFSTEP]
have hq : (minpoly k x).leadingCoeff = 1 := minpoly.monic (IsSeparable.isIntegral k x)
[GOAL]
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
[PROOFSTEP]
have hsep : (minpoly k x).Separable := IsSeparable.separable k x
[GOAL]
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
hsep : Separable (minpoly k x)
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
[PROOFSTEP]
have h : (minpoly k x).degree = 1 :=
  degree_eq_one_of_irreducible k (minpoly.irreducible (IsSeparable.isIntegral k x)) hsep
[GOAL]
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
hsep : Separable (minpoly k x)
h : degree (minpoly k x) = 1
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
[PROOFSTEP]
have : aeval x (minpoly k x) = 0 := minpoly.aeval k x
[GOAL]
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
hsep : Separable (minpoly k x)
h : degree (minpoly k x) = 1
this : ↑(aeval x) (minpoly k x) = 0
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
[PROOFSTEP]
rw [eq_X_add_C_of_degree_eq_one h, hq, C_1, one_mul, aeval_add, aeval_X, aeval_C, add_eq_zero_iff_eq_neg] at this
[GOAL]
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : IsSeparable k K
x : K
hq : leadingCoeff (minpoly k x) = 1
hsep : Separable (minpoly k x)
h : degree (minpoly k x) = 1
this : x = -↑(algebraMap k K) (coeff (minpoly k x) 0)
⊢ ↑(algebraMap k K) (-coeff (minpoly k x) 0) = x
[PROOFSTEP]
exact (RingHom.map_neg (algebraMap k K) ((minpoly k x).coeff 0)).symm ▸ this.symm
[GOAL]
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsSepClosure k K
x : K
⊢ IsAlgebraic k x
[PROOFSTEP]
apply IsIntegral.isAlgebraic
[GOAL]
case a
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsSepClosure k K
x : K
⊢ IsIntegral k x
[PROOFSTEP]
exact IsSepClosure.separable.isIntegral' x
[GOAL]
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsSepClosure k K
x : K
⊢ Separable (minpoly k x)
[PROOFSTEP]
have : IsSeparable k K := IsSepClosure.separable
[GOAL]
k : Type u
inst✝³ : Field k
K : Type v
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsSepClosure k K
x : K
this : IsSeparable k K
⊢ Separable (minpoly k x)
[PROOFSTEP]
exact IsSeparable.separable k x


[GOAL]
n : ℕ
⊢ bodd (succ n) = !bodd n
[PROOFSTEP]
simp only [bodd, boddDiv2]
[GOAL]
n : ℕ
⊢ (match boddDiv2 n with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).fst =
    !(boddDiv2 n).fst
[PROOFSTEP]
let ⟨b, m⟩ := boddDiv2 n
[GOAL]
n : ℕ
b : Bool
m : ℕ
⊢ (match (b, m) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).fst =
    !(b, m).fst
[PROOFSTEP]
cases b
[GOAL]
case false
n m : ℕ
⊢ (match (false, m) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).fst =
    !(false, m).fst
[PROOFSTEP]
rfl
[GOAL]
case true
n m : ℕ
⊢ (match (true, m) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).fst =
    !(true, m).fst
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
⊢ bodd (m + n) = bxor (bodd m) (bodd n)
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
m : ℕ
⊢ bodd (m + zero) = bxor (bodd m) (bodd zero)
[PROOFSTEP]
simp
[GOAL]
case succ
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ bodd (m + succ n) = bxor (bodd m) (bodd (succ n))
[PROOFSTEP]
simp [add_succ, IH]
[GOAL]
case succ
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ (!bxor (bodd m) (bodd n)) = bxor (bodd m) !bodd n
[PROOFSTEP]
cases bodd m
[GOAL]
case succ.false
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ (!bxor false (bodd n)) = bxor false !bodd n
[PROOFSTEP]
cases bodd n
[GOAL]
case succ.true
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ (!bxor true (bodd n)) = bxor true !bodd n
[PROOFSTEP]
cases bodd n
[GOAL]
case succ.false.false
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ (!bxor false false) = bxor false !false
[PROOFSTEP]
rfl
[GOAL]
case succ.false.true
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ (!bxor false true) = bxor false !true
[PROOFSTEP]
rfl
[GOAL]
case succ.true.false
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ (!bxor true false) = bxor true !false
[PROOFSTEP]
rfl
[GOAL]
case succ.true.true
m n : ℕ
IH : bodd (m + n) = bxor (bodd m) (bodd n)
⊢ (!bxor true true) = bxor true !true
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
⊢ bodd (m * n) = (bodd m && bodd n)
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
m : ℕ
⊢ bodd (m * zero) = (bodd m && bodd zero)
[PROOFSTEP]
simp
[GOAL]
case succ
m n : ℕ
IH : bodd (m * n) = (bodd m && bodd n)
⊢ bodd (m * succ n) = (bodd m && bodd (succ n))
[PROOFSTEP]
simp [mul_succ, IH]
[GOAL]
case succ
m n : ℕ
IH : bodd (m * n) = (bodd m && bodd n)
⊢ bxor (bodd m && bodd n) (bodd m) = (bodd m && !bodd n)
[PROOFSTEP]
cases bodd m
[GOAL]
case succ.false
m n : ℕ
IH : bodd (m * n) = (bodd m && bodd n)
⊢ bxor (false && bodd n) false = (false && !bodd n)
[PROOFSTEP]
cases bodd n
[GOAL]
case succ.true
m n : ℕ
IH : bodd (m * n) = (bodd m && bodd n)
⊢ bxor (true && bodd n) true = (true && !bodd n)
[PROOFSTEP]
cases bodd n
[GOAL]
case succ.false.false
m n : ℕ
IH : bodd (m * n) = (bodd m && bodd n)
⊢ bxor (false && false) false = (false && !false)
[PROOFSTEP]
rfl
[GOAL]
case succ.false.true
m n : ℕ
IH : bodd (m * n) = (bodd m && bodd n)
⊢ bxor (false && true) false = (false && !true)
[PROOFSTEP]
rfl
[GOAL]
case succ.true.false
m n : ℕ
IH : bodd (m * n) = (bodd m && bodd n)
⊢ bxor (true && false) true = (true && !false)
[PROOFSTEP]
rfl
[GOAL]
case succ.true.true
m n : ℕ
IH : bodd (m * n) = (bodd m && bodd n)
⊢ bxor (true && true) true = (true && !true)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ n % 2 = bif bodd n then 1 else 0
[PROOFSTEP]
have := congr_arg bodd (mod_add_div n 2)
[GOAL]
n : ℕ
this : bodd (n % 2 + 2 * (n / 2)) = bodd n
⊢ n % 2 = bif bodd n then 1 else 0
[PROOFSTEP]
simp [not] at this
[GOAL]
n : ℕ
this : bodd (n % 2) = bodd n
⊢ n % 2 = bif bodd n then 1 else 0
[PROOFSTEP]
have _ : ∀ b, and false b = false := by
  intro b
  cases b <;> rfl
[GOAL]
n : ℕ
this : bodd (n % 2) = bodd n
⊢ ∀ (b : Bool), (false && b) = false
[PROOFSTEP]
intro b
[GOAL]
n : ℕ
this : bodd (n % 2) = bodd n
b : Bool
⊢ (false && b) = false
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
this : bodd (n % 2) = bodd n
⊢ (false && false) = false
[PROOFSTEP]
rfl
[GOAL]
case true
n : ℕ
this : bodd (n % 2) = bodd n
⊢ (false && true) = false
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
this : bodd (n % 2) = bodd n
x✝ : ∀ (b : Bool), (false && b) = false
⊢ n % 2 = bif bodd n then 1 else 0
[PROOFSTEP]
have _ : ∀ b, bxor b false = b := by
  intro b
  cases b <;> rfl
[GOAL]
n : ℕ
this : bodd (n % 2) = bodd n
x✝ : ∀ (b : Bool), (false && b) = false
⊢ ∀ (b : Bool), bxor b false = b
[PROOFSTEP]
intro b
[GOAL]
n : ℕ
this : bodd (n % 2) = bodd n
x✝ : ∀ (b : Bool), (false && b) = false
b : Bool
⊢ bxor b false = b
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
this : bodd (n % 2) = bodd n
x✝ : ∀ (b : Bool), (false && b) = false
⊢ bxor false false = false
[PROOFSTEP]
rfl
[GOAL]
case true
n : ℕ
this : bodd (n % 2) = bodd n
x✝ : ∀ (b : Bool), (false && b) = false
⊢ bxor true false = true
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
this : bodd (n % 2) = bodd n
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), bxor b false = b
⊢ n % 2 = bif bodd n then 1 else 0
[PROOFSTEP]
rw [← this]
[GOAL]
n : ℕ
this : bodd (n % 2) = bodd n
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), bxor b false = b
⊢ n % 2 = bif bodd (n % 2) then 1 else 0
[PROOFSTEP]
cases' mod_two_eq_zero_or_one n with h h
[GOAL]
case inl
n : ℕ
this : bodd (n % 2) = bodd n
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), bxor b false = b
h : n % 2 = 0
⊢ n % 2 = bif bodd (n % 2) then 1 else 0
[PROOFSTEP]
rw [h]
[GOAL]
case inr
n : ℕ
this : bodd (n % 2) = bodd n
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), bxor b false = b
h : n % 2 = 1
⊢ n % 2 = bif bodd (n % 2) then 1 else 0
[PROOFSTEP]
rw [h]
[GOAL]
case inl
n : ℕ
this : bodd (n % 2) = bodd n
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), bxor b false = b
h : n % 2 = 0
⊢ 0 = bif bodd 0 then 1 else 0
[PROOFSTEP]
rfl
[GOAL]
case inr
n : ℕ
this : bodd (n % 2) = bodd n
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), bxor b false = b
h : n % 2 = 1
⊢ 1 = bif bodd 1 then 1 else 0
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ div2 (succ n) = bif bodd n then succ (div2 n) else div2 n
[PROOFSTEP]
simp only [bodd, boddDiv2, div2]
[GOAL]
n : ℕ
⊢ (match boddDiv2 n with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (boddDiv2 n).fst then succ (boddDiv2 n).snd else (boddDiv2 n).snd
[PROOFSTEP]
cases' boddDiv2 n with fst snd
[GOAL]
case mk
n : ℕ
fst : Bool
snd : ℕ
⊢ (match (fst, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (fst, snd).fst then succ (fst, snd).snd else (fst, snd).snd
[PROOFSTEP]
cases fst
[GOAL]
case mk.false
n snd : ℕ
⊢ (match (false, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (false, snd).fst then succ (false, snd).snd else (false, snd).snd
case mk.true
n snd : ℕ
⊢ (match (true, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (true, snd).fst then succ (true, snd).snd else (true, snd).snd
[PROOFSTEP]
case mk.false => simp
[GOAL]
n snd : ℕ
⊢ (match (false, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (false, snd).fst then succ (false, snd).snd else (false, snd).snd
[PROOFSTEP]
case mk.false => simp
[GOAL]
n snd : ℕ
⊢ (match (false, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (false, snd).fst then succ (false, snd).snd else (false, snd).snd
[PROOFSTEP]
simp
[GOAL]
case mk.true
n snd : ℕ
⊢ (match (true, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (true, snd).fst then succ (true, snd).snd else (true, snd).snd
[PROOFSTEP]
case mk.true => simp
[GOAL]
n snd : ℕ
⊢ (match (true, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (true, snd).fst then succ (true, snd).snd else (true, snd).snd
[PROOFSTEP]
case mk.true => simp
[GOAL]
n snd : ℕ
⊢ (match (true, snd) with
      | (false, m) => (true, m)
      | (true, m) => (false, succ m)).snd =
    bif (true, snd).fst then succ (true, snd).snd else (true, snd).snd
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ (bif bodd (succ n) then 1 else 0) + 2 * div2 (succ n) = succ n
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ (bif bodd n then 0 else 1) + (bif bodd n then succ (div2 n) else div2 n) * 2 = succ n
[PROOFSTEP]
refine' Eq.trans _ (congr_arg succ (bodd_add_div2 n))
[GOAL]
n : ℕ
⊢ (bif bodd n then 0 else 1) + (bif bodd n then succ (div2 n) else div2 n) * 2 =
    succ ((bif bodd n then 1 else 0) + 2 * div2 n)
[PROOFSTEP]
cases bodd n
[GOAL]
case false
n : ℕ
⊢ (bif false then 0 else 1) + (bif false then succ (div2 n) else div2 n) * 2 =
    succ ((bif false then 1 else 0) + 2 * div2 n)
[PROOFSTEP]
simp [cond, not]
[GOAL]
case true
n : ℕ
⊢ (bif true then 0 else 1) + (bif true then succ (div2 n) else div2 n) * 2 =
    succ ((bif true then 1 else 0) + 2 * div2 n)
[PROOFSTEP]
simp [cond, not]
[GOAL]
case false
n : ℕ
⊢ 1 + div2 n * 2 = succ (div2 n * 2)
[PROOFSTEP]
rw [Nat.add_comm, Nat.add_succ]
[GOAL]
case true
n : ℕ
⊢ succ (div2 n) * 2 = succ (1 + div2 n * 2)
[PROOFSTEP]
rw [succ_mul, Nat.add_comm 1, Nat.add_succ]
[GOAL]
n : ℕ
⊢ div2 n = n / 2
[PROOFSTEP]
refine' Nat.eq_of_mul_eq_mul_left (by decide) (Nat.add_left_cancel (Eq.trans _ (Nat.mod_add_div n 2).symm))
[GOAL]
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ n % 2 + 2 * div2 n = n
[PROOFSTEP]
rw [mod_two_of_bodd, bodd_add_div2]
[GOAL]
n : ℕ
⊢ n + n = 0 + n + n
[PROOFSTEP]
rw [Nat.zero_add]
[GOAL]
b : Bool
n : ℕ
⊢ bit b n = 2 * n + bif b then 1 else 0
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
⊢ bit false n = 2 * n + bif false then 1 else 0
case true n : ℕ ⊢ bit true n = 2 * n + bif true then 1 else 0
[PROOFSTEP]
apply bit0_val
[GOAL]
case true
n : ℕ
⊢ bit true n = 2 * n + bif true then 1 else 0
[PROOFSTEP]
apply bit1_val
[GOAL]
⊢ ∀ (n : ℕ), shiftr 0 n = 0
[PROOFSTEP]
intro n
[GOAL]
n : ℕ
⊢ shiftr 0 n = 0
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
⊢ shiftr 0 zero = 0
case succ n : ℕ IH : shiftr 0 n = 0 ⊢ shiftr 0 (succ n) = 0
[PROOFSTEP]
case zero => rw [shiftr]
[GOAL]
⊢ shiftr 0 zero = 0
[PROOFSTEP]
case zero => rw [shiftr]
[GOAL]
⊢ shiftr 0 zero = 0
[PROOFSTEP]
rw [shiftr]
[GOAL]
case succ
n : ℕ
IH : shiftr 0 n = 0
⊢ shiftr 0 (succ n) = 0
[PROOFSTEP]
case succ =>
  rw [shiftr, div2, IH]
  rfl
[GOAL]
n : ℕ
IH : shiftr 0 n = 0
⊢ shiftr 0 (succ n) = 0
[PROOFSTEP]
case succ =>
  rw [shiftr, div2, IH]
  rfl
[GOAL]
n : ℕ
IH : shiftr 0 n = 0
⊢ shiftr 0 (succ n) = 0
[PROOFSTEP]
rw [shiftr, div2, IH]
[GOAL]
n : ℕ
IH : shiftr 0 n = 0
⊢ (boddDiv2 0).snd = 0
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
h : n ≠ 0
⊢ div2 n < n
[PROOFSTEP]
rw [div2_val]
[GOAL]
n : ℕ
h : n ≠ 0
⊢ n / 2 < n
[PROOFSTEP]
apply (div_lt_iff_lt_mul <| succ_pos 1).2
[GOAL]
n : ℕ
h : n ≠ 0
⊢ n < n * succ 1
[PROOFSTEP]
have := Nat.mul_lt_mul_of_pos_left (lt_succ_self 1) (lt_of_le_of_ne n.zero_le h.symm)
[GOAL]
n : ℕ
h : n ≠ 0
this : n * 1 < n * succ 1
⊢ n < n * succ 1
[PROOFSTEP]
rwa [Nat.mul_one] at this
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
n0 : n = 0
⊢ C n
[PROOFSTEP]
simp [n0]
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
n0 : n = 0
⊢ C 0
[PROOFSTEP]
exact z
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
n0 : ¬n = 0
⊢ C n
[PROOFSTEP]
let n' := div2 n
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
n0 : ¬n = 0
n' : ℕ := div2 n
⊢ C n
[PROOFSTEP]
have _x : bit (bodd n) n' = n := by apply bit_decomp n
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
n0 : ¬n = 0
n' : ℕ := div2 n
⊢ bit (bodd n) n' = n
[PROOFSTEP]
apply bit_decomp n
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
n0 : ¬n = 0
n' : ℕ := div2 n
_x : bit (bodd n) n' = n
⊢ C n
[PROOFSTEP]
rw [← _x]
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
n : ℕ
n0 : ¬n = 0
n' : ℕ := div2 n
_x : bit (bodd n) n' = n
⊢ C (bit (bodd n) n')
[PROOFSTEP]
exact f (bodd n) n' (binaryRec z f n')
[GOAL]
n : ℕ
n0 : ¬n = 0
n' : ℕ := div2 n
_x : bit (bodd n) n' = n
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n' n
[PROOFSTEP]
exact binaryRec_decreasing n0
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
⊢ binaryRec z f 0 = z
[PROOFSTEP]
rw [binaryRec]
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
⊢ (if n0 : 0 = 0 then Eq.mpr (_ : C 0 = C 0) z
    else
      let n' := div2 0;
      let_fun _x := (_ : bit (bodd 0) (div2 0) = 0);
      Eq.mpr (_ : C 0 = C (bit (bodd 0) n')) (f (bodd 0) n' (binaryRec z f n'))) =
    z
[PROOFSTEP]
rfl
[GOAL]
b : Bool
n : ℕ
⊢ bodd (bit b n) = b
[PROOFSTEP]
rw [bit_val]
[GOAL]
b : Bool
n : ℕ
⊢ bodd (2 * n + bif b then 1 else 0) = b
[PROOFSTEP]
simp
[GOAL]
b : Bool
n : ℕ
⊢ bodd (bif b then 1 else 0) = b
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
⊢ bodd (bif false then 1 else 0) = false
[PROOFSTEP]
cases bodd n
[GOAL]
case true
n : ℕ
⊢ bodd (bif true then 1 else 0) = true
[PROOFSTEP]
cases bodd n
[GOAL]
case false.false
n : ℕ
⊢ bodd (bif false then 1 else 0) = false
[PROOFSTEP]
rfl
[GOAL]
case false.true
n : ℕ
⊢ bodd (bif false then 1 else 0) = false
[PROOFSTEP]
rfl
[GOAL]
case true.false
n : ℕ
⊢ bodd (bif true then 1 else 0) = true
[PROOFSTEP]
rfl
[GOAL]
case true.true
n : ℕ
⊢ bodd (bif true then 1 else 0) = true
[PROOFSTEP]
rfl
[GOAL]
b : Bool
n : ℕ
⊢ div2 (bit b n) = n
[PROOFSTEP]
rw [bit_val, div2_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
[GOAL]
b : Bool
n : ℕ
⊢ (bif b then 1 else 0) < 2
[PROOFSTEP]
cases b
[GOAL]
case H
b : Bool
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
cases b
[GOAL]
case false
n : ℕ
⊢ (bif false then 1 else 0) < 2
[PROOFSTEP]
exact by decide
[GOAL]
n : ℕ
⊢ (bif false then 1 else 0) < 2
[PROOFSTEP]
decide
[GOAL]
case true
n : ℕ
⊢ (bif true then 1 else 0) < 2
[PROOFSTEP]
exact by decide
[GOAL]
n : ℕ
⊢ (bif true then 1 else 0) < 2
[PROOFSTEP]
decide
[GOAL]
case H.false
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
exact by decide
[GOAL]
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
case H.true
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
exact by decide
[GOAL]
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftl' b m (n + 1 - (k + 1)) = shiftr (shiftl' b m (n + 1)) (k + 1)
[PROOFSTEP]
simp [shiftl']
[GOAL]
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftl' b m (n - k) = shiftr (bit b (shiftl' b m n)) (k + 1)
[PROOFSTEP]
rw [Nat.add_comm, shiftr_add]
[GOAL]
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftl' b m (n - k) = shiftr (shiftr (bit b (shiftl' b m n)) 1) k
[PROOFSTEP]
simp [shiftr, div2_bit]
[GOAL]
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftl' b m (n - k) = shiftr (shiftl' b m n) k
[PROOFSTEP]
simp [shiftl'_sub, (Nat.le_of_succ_le_succ h)]
[GOAL]
m : ℕ
b : Bool
n : ℕ
⊢ testBit (bit b n) (succ m) = testBit n m
[PROOFSTEP]
have : bodd (shiftr (shiftr (bit b n) 1) m) = bodd (shiftr n m) :=
  by
  dsimp [shiftr]
  rw [div2_bit]
[GOAL]
m : ℕ
b : Bool
n : ℕ
⊢ bodd (shiftr (shiftr (bit b n) 1) m) = bodd (shiftr n m)
[PROOFSTEP]
dsimp [shiftr]
[GOAL]
m : ℕ
b : Bool
n : ℕ
⊢ bodd (shiftr (div2 (bit b n)) m) = bodd (shiftr n m)
[PROOFSTEP]
rw [div2_bit]
[GOAL]
m : ℕ
b : Bool
n : ℕ
this : bodd (shiftr (shiftr (bit b n) 1) m) = bodd (shiftr n m)
⊢ testBit (bit b n) (succ m) = testBit n m
[PROOFSTEP]
rw [← shiftr_add, Nat.add_comm] at this
[GOAL]
m : ℕ
b : Bool
n : ℕ
this : bodd (shiftr (bit b n) (m + 1)) = bodd (shiftr n m)
⊢ testBit (bit b n) (succ m) = testBit n m
[PROOFSTEP]
exact this
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h : f false 0 z = z
b : Bool
n : ℕ
⊢ binaryRec z f (bit b n) = f b n (binaryRec z f n)
[PROOFSTEP]
rw [binaryRec]
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h : f false 0 z = z
b : Bool
n : ℕ
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
by_cases h :
  bit b n =
    0
      -- Note: this renames the original `h : f false 0 z = z` to `h'` and leaves `h : bit b n = 0`
[GOAL]
case pos
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h✝ : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
case neg
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h✝ : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
case pos h' =>
  simp [dif_pos h]
  generalize binaryRec z f (bit b n) = e
  revert e
  have bf := bodd_bit b n
  have n0 := div2_bit b n
  rw [h] at bf n0
  simp at bf n0
  subst bf n0
  rw [binaryRec_zero]
  intros
  rw [h']
  rfl
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
case pos h' =>
  simp [dif_pos h]
  generalize binaryRec z f (bit b n) = e
  revert e
  have bf := bodd_bit b n
  have n0 := div2_bit b n
  rw [h] at bf n0
  simp at bf n0
  subst bf n0
  rw [binaryRec_zero]
  intros
  rw [h']
  rfl
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
simp [dif_pos h]
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
⊢ Eq.mpr (_ : C (bit b n) = C 0) z = f b n (binaryRec z f n)
[PROOFSTEP]
generalize binaryRec z f (bit b n) = e
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
e : C (bit b n)
⊢ Eq.mpr (_ : C (bit b n) = C 0) z = f b n (binaryRec z f n)
[PROOFSTEP]
revert e
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
⊢ C (bit b n) → Eq.mpr (_ : C (bit b n) = C 0) z = f b n (binaryRec z f n)
[PROOFSTEP]
have bf := bodd_bit b n
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
bf : bodd (bit b n) = b
⊢ C (bit b n) → Eq.mpr (_ : C (bit b n) = C 0) z = f b n (binaryRec z f n)
[PROOFSTEP]
have n0 := div2_bit b n
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
bf : bodd (bit b n) = b
n0 : div2 (bit b n) = n
⊢ C (bit b n) → Eq.mpr (_ : C (bit b n) = C 0) z = f b n (binaryRec z f n)
[PROOFSTEP]
rw [h] at bf n0
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
bf : bodd 0 = b
n0 : div2 0 = n
⊢ C (bit b n) → Eq.mpr (_ : C (bit b n) = C 0) z = f b n (binaryRec z f n)
[PROOFSTEP]
simp at bf n0
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : bit b n = 0
bf : false = b
n0 : 0 = n
⊢ C (bit b n) → Eq.mpr (_ : C (bit b n) = C 0) z = f b n (binaryRec z f n)
[PROOFSTEP]
subst bf n0
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
h : bit false 0 = 0
⊢ C (bit false 0) → Eq.mpr (_ : C (bit false 0) = C 0) z = f false 0 (binaryRec z f 0)
[PROOFSTEP]
rw [binaryRec_zero]
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
h : bit false 0 = 0
⊢ C (bit false 0) → Eq.mpr (_ : C (bit false 0) = C 0) z = f false 0 z
[PROOFSTEP]
intros
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
h : bit false 0 = 0
e✝ : C (bit false 0)
⊢ Eq.mpr (_ : C (bit false 0) = C 0) z = f false 0 z
[PROOFSTEP]
rw [h']
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
h : bit false 0 = 0
e✝ : C (bit false 0)
⊢ Eq.mpr (_ : C (bit false 0) = C 0) z = z
[PROOFSTEP]
rfl
[GOAL]
case neg
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h✝ : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
case neg h' =>
  simp [dif_neg h]
  generalize
    @id (C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n))))
      (Eq.symm (bit_decomp (bit b n)) ▸ Eq.refl (C (bit b n))) =
    e
  revert e
  rw [bodd_bit, div2_bit]
  intros; rfl
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
case neg h' =>
  simp [dif_neg h]
  generalize
    @id (C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n))))
      (Eq.symm (bit_decomp (bit b n)) ▸ Eq.refl (C (bit b n))) =
    e
  revert e
  rw [bodd_bit, div2_bit]
  intros; rfl
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
⊢ (if n0 : bit b n = 0 then Eq.mpr (_ : C (bit b n) = C 0) z
    else
      let n' := div2 (bit b n);
      let_fun _x := (_ : bit (bodd (bit b n)) (div2 (bit b n)) = bit b n);
      Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) n')) (f (bodd (bit b n)) n' (binaryRec z f n'))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
simp [dif_neg h]
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
⊢ Eq.mpr (_ : C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n))))
      (f (bodd (bit b n)) (div2 (bit b n)) (binaryRec z f (div2 (bit b n)))) =
    f b n (binaryRec z f n)
[PROOFSTEP]
generalize
  @id (C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n))))
    (Eq.symm (bit_decomp (bit b n)) ▸ Eq.refl (C (bit b n))) =
  e
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
e : C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n)))
⊢ Eq.mpr e (f (bodd (bit b n)) (div2 (bit b n)) (binaryRec z f (div2 (bit b n)))) = f b n (binaryRec z f n)
[PROOFSTEP]
revert e
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
⊢ ∀ (e : C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n)))),
    Eq.mpr e (f (bodd (bit b n)) (div2 (bit b n)) (binaryRec z f (div2 (bit b n)))) = f b n (binaryRec z f n)
[PROOFSTEP]
rw [bodd_bit, div2_bit]
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
⊢ ∀ (e : C (bit b n) = C (bit b n)), Eq.mpr e (f b n (binaryRec z f n)) = f b n (binaryRec z f n)
[PROOFSTEP]
intros
[GOAL]
C : ℕ → Sort u
z : C 0
f : (b : Bool) → (n : ℕ) → C n → C (bit b n)
h' : f false 0 z = z
b : Bool
n : ℕ
h : ¬bit b n = 0
e✝ : C (bit b n) = C (bit b n)
⊢ Eq.mpr e✝ (f b n (binaryRec z f n)) = f b n (binaryRec z f n)
[PROOFSTEP]
rfl
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
⊢ (binaryRec (bif f true false then bit false 0 else 0) fun b n x => bit (f false b) (bif f false true then n else 0)) =
    fun n => bif f false true then n else 0
[PROOFSTEP]
funext n
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
n : ℕ
⊢ binaryRec (bif f true false then bit false 0 else 0) (fun b n x => bit (f false b) (bif f false true then n else 0))
      n =
    bif f false true then n else 0
[PROOFSTEP]
apply bitCasesOn n
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    binaryRec (bif f true false then bit false 0 else 0) (fun b n x => bit (f false b) (bif f false true then n else 0))
        (bit b n) =
      bif f false true then bit b n else 0
[PROOFSTEP]
intro b n
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ binaryRec (bif f true false then bit false 0 else 0) (fun b n x => bit (f false b) (bif f false true then n else 0))
      (bit b n) =
    bif f false true then bit b n else 0
[PROOFSTEP]
rw [binaryRec_eq]
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ bit (f false b) (bif f false true then n else 0) = bif f false true then bit b n else 0
[PROOFSTEP]
cases b
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit (f false false) (bif f false true then n else 0) = bif f false true then bit false n else 0
[PROOFSTEP]
try rw [h] <;> induction' fft : f false true <;> simp [cond]
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit (f false false) (bif f false true then n else 0) = bif f false true then bit false n else 0
[PROOFSTEP]
rw [h]
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit false (bif f false true then n else 0) = bif f false true then bit false n else 0
[PROOFSTEP]
induction' fft : f false true
[GOAL]
case h.false.false
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
x✝ : Bool
fft✝ : f false true = x✝
fft : f false true = false
⊢ bit false (bif false then n else 0) = bif false then bit false n else 0
[PROOFSTEP]
simp [cond]
[GOAL]
case h.false.true
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
x✝ : Bool
fft✝ : f false true = x✝
fft : f false true = true
⊢ bit false (bif true then n else 0) = bif true then bit false n else 0
[PROOFSTEP]
simp [cond]
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit (f false true) (bif f false true then n else 0) = bif f false true then bit true n else 0
[PROOFSTEP]
try rw [h] <;> induction' fft : f false true <;> simp [cond]
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit (f false true) (bif f false true then n else 0) = bif f false true then bit true n else 0
[PROOFSTEP]
rw [h]
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit (f false true) (bif f false true then n else 0) = bif f false true then bit true n else 0
[PROOFSTEP]
cases f false true
[GOAL]
case h.true.false
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit false (bif false then n else 0) = bif false then bit true n else 0
case h.true.true
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit true (bif true then n else 0) = bif true then bit true n else 0
[PROOFSTEP]
case h.true.false => simp
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit false (bif false then n else 0) = bif false then bit true n else 0
[PROOFSTEP]
case h.true.false => simp
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit false (bif false then n else 0) = bif false then bit true n else 0
[PROOFSTEP]
simp
[GOAL]
case h.true.true
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit true (bif true then n else 0) = bif true then bit true n else 0
[PROOFSTEP]
case h.true.true => simp
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit true (bif true then n else 0) = bif true then bit true n else 0
[PROOFSTEP]
case h.true.true => simp
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
n✝ n : ℕ
⊢ bit true (bif true then n else 0) = bif true then bit true n else 0
[PROOFSTEP]
simp
[GOAL]
case h.h
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ bit (f false false) (bif f false true then 0 else 0) = bif f true false then bit false 0 else 0
[PROOFSTEP]
rw [h, show cond (f false true) 0 0 = 0 by cases f false true <;> rfl,
  show cond (f true false) (bit false 0) 0 = 0 by cases f true false <;> rfl]
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ (bif f false true then 0 else 0) = 0
[PROOFSTEP]
cases f false true
[GOAL]
case false
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ (bif false then 0 else 0) = 0
[PROOFSTEP]
rfl
[GOAL]
case true
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ (bif true then 0 else 0) = 0
[PROOFSTEP]
rfl
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ (bif f true false then bit false 0 else 0) = 0
[PROOFSTEP]
cases f true false
[GOAL]
case false
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ (bif false then bit false 0 else 0) = 0
[PROOFSTEP]
rfl
[GOAL]
case true
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ (bif true then bit false 0 else 0) = 0
[PROOFSTEP]
rfl
[GOAL]
case h.h
f : Bool → Bool → Bool
h : f false false = false
n✝ : ℕ
b : Bool
n : ℕ
⊢ bit false 0 = 0
[PROOFSTEP]
rfl
[GOAL]
f : Bool → Bool → Bool
n : ℕ
⊢ bitwise' f 0 n = bif f false true then n else 0
[PROOFSTEP]
unfold bitwise'
[GOAL]
f : Bool → Bool → Bool
n : ℕ
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) 0 n =
    bif f false true then n else 0
[PROOFSTEP]
rw [binaryRec_zero]
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ bitwise' f m 0 = bif f true false then m else 0
[PROOFSTEP]
unfold bitwise'
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    bif f true false then m else 0
[PROOFSTEP]
apply bitCasesOn m
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit b n) 0 =
      bif f true false then bit b n else 0
[PROOFSTEP]
intros
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b✝ : Bool
n✝ : ℕ
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit b✝ n✝) 0 =
    bif f true false then bit b✝ n✝ else 0
[PROOFSTEP]
rw [binaryRec_eq, binaryRec_zero]
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b✝ : Bool
n✝ : ℕ
⊢ (binaryRec (bif f true false then bit false 0 else 0) fun b n x => bit (f false b) (bif f false true then n else 0)) =
    fun n => bif f false true then n else 0
[PROOFSTEP]
exact bitwise'_bit_aux h
[GOAL]
f : Bool → Bool → Bool
⊢ bitwise' f 0 0 = 0
[PROOFSTEP]
rw [bitwise'_zero_left]
[GOAL]
f : Bool → Bool → Bool
⊢ (bif f false true then 0 else 0) = 0
[PROOFSTEP]
cases f false true
[GOAL]
case false
f : Bool → Bool → Bool
⊢ (bif false then 0 else 0) = 0
[PROOFSTEP]
rfl
[GOAL]
case true
f : Bool → Bool → Bool
⊢ (bif true then 0 else 0) = 0
[PROOFSTEP]
rfl
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
⊢ bitwise' f (bit a m) (bit b n) = bit (f a b) (bitwise' f m n)
[PROOFSTEP]
unfold bitwise'
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit a m)
      (bit b n) =
    bit (f a b)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m n)
[PROOFSTEP]
rw [binaryRec_eq, binaryRec_eq]
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif f true false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif f true false then bit a m else 0
[PROOFSTEP]
induction' ftf : f true false
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif false then bit a m else 0
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif true then bit a m else 0
[PROOFSTEP]
rw [show f a false = false by cases a <;> assumption]
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ f a false = false
[PROOFSTEP]
cases a
[GOAL]
case false
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ f false false = false
[PROOFSTEP]
assumption
[GOAL]
case true
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ f true false = false
[PROOFSTEP]
assumption
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ bit false
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif false then bit a m else 0
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif true then bit a m else 0
[PROOFSTEP]
apply @congr_arg _ _ _ 0 (bit false)
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    0
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif true then bit a m else 0
[PROOFSTEP]
swap
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ bit (f a false)
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif true then bit a m else 0
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    0
[PROOFSTEP]
rw [show f a false = a by cases a <;> assumption]
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ f a false = a
[PROOFSTEP]
cases a
[GOAL]
case false
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ f false false = false
[PROOFSTEP]
assumption
[GOAL]
case true
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ f true false = true
[PROOFSTEP]
assumption
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ bit a
      (binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0) =
    bif true then bit a m else 0
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    0
[PROOFSTEP]
apply congr_arg (bit a)
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    m
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    0
[PROOFSTEP]
all_goals {
  apply bitCasesOn m
  intro a m
  rw [binaryRec_eq, binaryRec_zero]
  · rfl
  · rw [← bitwise'_bit_aux h, ftf]
}
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    m
[PROOFSTEP]
{ apply bitCasesOn m
  intro a m
  rw [binaryRec_eq, binaryRec_zero]
  · rfl
  · rw [← bitwise'_bit_aux h, ftf]
}
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    m
[PROOFSTEP]
apply bitCasesOn m
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
⊢ ∀ (b : Bool) (n : ℕ),
    binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit b n) 0 =
      bit b n
[PROOFSTEP]
intro a m
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a✝ : Bool
m✝ : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
a : Bool
m : ℕ
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif true then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit a m) 0 =
    bit a m
[PROOFSTEP]
rw [binaryRec_eq, binaryRec_zero]
[GOAL]
case h.true
f : Bool → Bool → Bool
h : f false false = false
a✝ : Bool
m✝ : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
a : Bool
m : ℕ
⊢ (bif true then bit a m else 0) = bit a m
[PROOFSTEP]
rfl
[GOAL]
case h.true.h
f : Bool → Bool → Bool
h : f false false = false
a✝ : Bool
m✝ : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = true
a : Bool
m : ℕ
⊢ (binaryRec (bif true then bit false 0 else 0) fun b n x => bit (f false b) (bif f false true then n else 0)) =
    fun n => bif f false true then n else 0
[PROOFSTEP]
rw [← bitwise'_bit_aux h, ftf]
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    0
[PROOFSTEP]
{ apply bitCasesOn m
  intro a m
  rw [binaryRec_eq, binaryRec_zero]
  · rfl
  · rw [← bitwise'_bit_aux h, ftf]
}
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) m 0 =
    0
[PROOFSTEP]
apply bitCasesOn m
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
⊢ ∀ (b : Bool) (n : ℕ),
    binaryRec (fun n => bif f false true then n else 0)
        (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit b n) 0 =
      0
[PROOFSTEP]
intro a m
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a✝ : Bool
m✝ : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
a : Bool
m : ℕ
⊢ binaryRec (fun n => bif f false true then n else 0)
      (fun a m Ia => binaryRec (bif false then bit a m else 0) fun b n x => bit (f a b) (Ia n)) (bit a m) 0 =
    0
[PROOFSTEP]
rw [binaryRec_eq, binaryRec_zero]
[GOAL]
case h.false
f : Bool → Bool → Bool
h : f false false = false
a✝ : Bool
m✝ : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
a : Bool
m : ℕ
⊢ (bif false then bit a m else 0) = 0
[PROOFSTEP]
rfl
[GOAL]
case h.false.h
f : Bool → Bool → Bool
h : f false false = false
a✝ : Bool
m✝ : ℕ
b : Bool
n : ℕ
x✝ : Bool
ftf✝ : f true false = x✝
ftf : f true false = false
a : Bool
m : ℕ
⊢ (binaryRec (bif false then bit false 0 else 0) fun b n x => bit (f false b) (bif f false true then n else 0)) =
    fun n => bif f false true then n else 0
[PROOFSTEP]
rw [← bitwise'_bit_aux h, ftf]
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
a : Bool
m : ℕ
b : Bool
n : ℕ
⊢ (binaryRec (bif f true false then bit false 0 else 0) fun b n x => bit (f false b) (bif f false true then n else 0)) =
    fun n => bif f false true then n else 0
[PROOFSTEP]
exact bitwise'_bit_aux h
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
⊢ bitwise' (Function.swap f) = Function.swap (bitwise' f)
[PROOFSTEP]
funext m n
[GOAL]
case h.h
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
⊢ bitwise' (Function.swap f) m n = Function.swap (bitwise' f) m n
[PROOFSTEP]
revert n
[GOAL]
case h.h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ ∀ (n : ℕ), bitwise' (Function.swap f) m n = Function.swap (bitwise' f) m n
[PROOFSTEP]
dsimp [Function.swap]
[GOAL]
case h.h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ ∀ (n : ℕ), bitwise' (fun y x => f x y) m n = bitwise' f n m
[PROOFSTEP]
apply binaryRec _ _ m
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ ∀ (n : ℕ), bitwise' (fun y x => f x y) 0 n = bitwise' f n 0
[PROOFSTEP]
intro n
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    (∀ (n_1 : ℕ), bitwise' (fun y x => f x y) n n_1 = bitwise' f n_1 n) →
      ∀ (n_1 : ℕ), bitwise' (fun y x => f x y) (bit b n) n_1 = bitwise' f n_1 (bit b n)
[PROOFSTEP]
intro n
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
⊢ bitwise' (fun y x => f x y) 0 n = bitwise' f n 0
[PROOFSTEP]
rw [bitwise'_zero_left, bitwise'_zero_right]
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
⊢ f false false = false
[PROOFSTEP]
exact h
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
⊢ ∀ (n_1 : ℕ),
    (∀ (n : ℕ), bitwise' (fun y x => f x y) n_1 n = bitwise' f n n_1) →
      ∀ (n_2 : ℕ), bitwise' (fun y x => f x y) (bit n n_1) n_2 = bitwise' f n_2 (bit n n_1)
[PROOFSTEP]
intros a ih m'
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
a : ℕ
ih : ∀ (n : ℕ), bitwise' (fun y x => f x y) a n = bitwise' f n a
m' : ℕ
⊢ bitwise' (fun y x => f x y) (bit n a) m' = bitwise' f m' (bit n a)
[PROOFSTEP]
apply bitCasesOn m'
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
a : ℕ
ih : ∀ (n : ℕ), bitwise' (fun y x => f x y) a n = bitwise' f n a
m' : ℕ
⊢ ∀ (b : Bool) (n_1 : ℕ), bitwise' (fun y x => f x y) (bit n a) (bit b n_1) = bitwise' f (bit b n_1) (bit n a)
[PROOFSTEP]
intro b n'
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
a : ℕ
ih : ∀ (n : ℕ), bitwise' (fun y x => f x y) a n = bitwise' f n a
m' : ℕ
b : Bool
n' : ℕ
⊢ bitwise' (fun y x => f x y) (bit n a) (bit b n') = bitwise' f (bit b n') (bit n a)
[PROOFSTEP]
rw [bitwise'_bit, bitwise'_bit, ih]
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
a : ℕ
ih : ∀ (n : ℕ), bitwise' (fun y x => f x y) a n = bitwise' f n a
m' : ℕ
b : Bool
n' : ℕ
⊢ f false false = false
[PROOFSTEP]
exact h
[GOAL]
case h
f : Bool → Bool → Bool
h : f false false = false
m : ℕ
n : Bool
a : ℕ
ih : ∀ (n : ℕ), bitwise' (fun y x => f x y) a n = bitwise' f n a
m' : ℕ
b : Bool
n' : ℕ
⊢ f false false = false
[PROOFSTEP]
exact h
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
m n k : ℕ
⊢ testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
[PROOFSTEP]
revert m n
[GOAL]
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
⊢ ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
[PROOFSTEP]
induction' k with k IH
[GOAL]
case zero
f : Bool → Bool → Bool
h : f false false = false
⊢ ∀ (m n : ℕ), testBit (bitwise' f m n) zero = f (testBit m zero) (testBit n zero)
[PROOFSTEP]
intros m n
[GOAL]
case succ
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
IH : ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
⊢ ∀ (m n : ℕ), testBit (bitwise' f m n) (succ k) = f (testBit m (succ k)) (testBit n (succ k))
[PROOFSTEP]
intros m n
[GOAL]
case zero
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
⊢ testBit (bitwise' f m n) zero = f (testBit m zero) (testBit n zero)
[PROOFSTEP]
apply bitCasesOn m
[GOAL]
case succ
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
IH : ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
m n : ℕ
⊢ testBit (bitwise' f m n) (succ k) = f (testBit m (succ k)) (testBit n (succ k))
[PROOFSTEP]
apply bitCasesOn m
[GOAL]
case zero
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
⊢ ∀ (b : Bool) (n_1 : ℕ), testBit (bitwise' f (bit b n_1) n) zero = f (testBit (bit b n_1) zero) (testBit n zero)
[PROOFSTEP]
intros a m'
[GOAL]
case succ
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
IH : ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
m n : ℕ
⊢ ∀ (b : Bool) (n_1 : ℕ),
    testBit (bitwise' f (bit b n_1) n) (succ k) = f (testBit (bit b n_1) (succ k)) (testBit n (succ k))
[PROOFSTEP]
intros a m'
[GOAL]
case zero
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
a : Bool
m' : ℕ
⊢ testBit (bitwise' f (bit a m') n) zero = f (testBit (bit a m') zero) (testBit n zero)
[PROOFSTEP]
apply bitCasesOn n
[GOAL]
case succ
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
IH : ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
m n : ℕ
a : Bool
m' : ℕ
⊢ testBit (bitwise' f (bit a m') n) (succ k) = f (testBit (bit a m') (succ k)) (testBit n (succ k))
[PROOFSTEP]
apply bitCasesOn n
[GOAL]
case zero
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
a : Bool
m' : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    testBit (bitwise' f (bit a m') (bit b n)) zero = f (testBit (bit a m') zero) (testBit (bit b n) zero)
[PROOFSTEP]
intros b n'
[GOAL]
case succ
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
IH : ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
m n : ℕ
a : Bool
m' : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    testBit (bitwise' f (bit a m') (bit b n)) (succ k) = f (testBit (bit a m') (succ k)) (testBit (bit b n) (succ k))
[PROOFSTEP]
intros b n'
[GOAL]
case zero
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
a : Bool
m' : ℕ
b : Bool
n' : ℕ
⊢ testBit (bitwise' f (bit a m') (bit b n')) zero = f (testBit (bit a m') zero) (testBit (bit b n') zero)
[PROOFSTEP]
rw [bitwise'_bit h]
[GOAL]
case succ
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
IH : ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
m n : ℕ
a : Bool
m' : ℕ
b : Bool
n' : ℕ
⊢ testBit (bitwise' f (bit a m') (bit b n')) (succ k) = f (testBit (bit a m') (succ k)) (testBit (bit b n') (succ k))
[PROOFSTEP]
rw [bitwise'_bit h]
[GOAL]
case zero
f : Bool → Bool → Bool
h : f false false = false
m n : ℕ
a : Bool
m' : ℕ
b : Bool
n' : ℕ
⊢ testBit (bit (f a b) (bitwise' f m' n')) zero = f (testBit (bit a m') zero) (testBit (bit b n') zero)
[PROOFSTEP]
simp [testBit_zero]
[GOAL]
case succ
f : Bool → Bool → Bool
h : f false false = false
k : ℕ
IH : ∀ (m n : ℕ), testBit (bitwise' f m n) k = f (testBit m k) (testBit n k)
m n : ℕ
a : Bool
m' : ℕ
b : Bool
n' : ℕ
⊢ testBit (bit (f a b) (bitwise' f m' n')) (succ k) = f (testBit (bit a m') (succ k)) (testBit (bit b n') (succ k))
[PROOFSTEP]
simp [testBit_succ, IH]


[GOAL]
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ IsNoetherian K V ↔ Module.rank K V < ℵ₀
[PROOFSTEP]
let b := Basis.ofVectorSpace K V
[GOAL]
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ IsNoetherian K V ↔ Module.rank K V < ℵ₀
[PROOFSTEP]
rw [← b.mk_eq_rank'', lt_aleph0_iff_set_finite]
[GOAL]
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ IsNoetherian K V ↔ Set.Finite (Basis.ofVectorSpaceIndex K V)
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ IsNoetherian K V → Set.Finite (Basis.ofVectorSpaceIndex K V)
[PROOFSTEP]
intro
[GOAL]
case mp
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
a✝ : IsNoetherian K V
⊢ Set.Finite (Basis.ofVectorSpaceIndex K V)
[PROOFSTEP]
exact finite_of_linearIndependent (Basis.ofVectorSpaceIndex.linearIndependent K V)
[GOAL]
case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ Set.Finite (Basis.ofVectorSpaceIndex K V) → IsNoetherian K V
[PROOFSTEP]
intro hbfinite
[GOAL]
case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hbfinite : Set.Finite (Basis.ofVectorSpaceIndex K V)
⊢ IsNoetherian K V
[PROOFSTEP]
refine' @isNoetherian_of_linearEquiv K (⊤ : Submodule K V) V _ _ _ _ _ (LinearEquiv.ofTop _ rfl) (id _)
[GOAL]
case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hbfinite : Set.Finite (Basis.ofVectorSpaceIndex K V)
⊢ IsNoetherian K { x // x ∈ ⊤ }
[PROOFSTEP]
refine' isNoetherian_of_fg_of_noetherian _ ⟨Set.Finite.toFinset hbfinite, _⟩
[GOAL]
case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
b : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hbfinite : Set.Finite (Basis.ofVectorSpaceIndex K V)
⊢ span K ↑(Set.Finite.toFinset hbfinite) = ⊤
[PROOFSTEP]
rw [Set.Finite.coe_toFinset, ← b.span_eq, Basis.coe_ofVectorSpace, Subtype.range_coe]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsNoetherian K V
⊢ ↑(Basis.ofVectorSpaceIndex K V) ≃ { x // x ∈ finsetBasisIndex K V }
[PROOFSTEP]
rw [coeSort_finsetBasisIndex]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsNoetherian K V
⊢ Set.range ↑(finsetBasis K V) = Basis.ofVectorSpaceIndex K V
[PROOFSTEP]
rw [finsetBasis, Basis.range_reindex, Basis.range_ofVectorSpace]
[GOAL]
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ IsNoetherian K V ↔ Module.Finite K V
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ IsNoetherian K V → Module.Finite K V
[PROOFSTEP]
intro h
[GOAL]
case mp
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : IsNoetherian K V
⊢ Module.Finite K V
[PROOFSTEP]
exact
  ⟨⟨finsetBasisIndex K V, by
      convert (finsetBasis K V).span_eq
      simp⟩⟩
[GOAL]
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : IsNoetherian K V
⊢ span K ↑(finsetBasisIndex K V) = ⊤
[PROOFSTEP]
convert (finsetBasis K V).span_eq
[GOAL]
case h.e'_2.h.e'_6
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : IsNoetherian K V
⊢ ↑(finsetBasisIndex K V) = Set.range ↑(finsetBasis K V)
[PROOFSTEP]
simp
[GOAL]
case mpr
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Module.Finite K V → IsNoetherian K V
[PROOFSTEP]
rintro ⟨s, hs⟩
[GOAL]
case mpr.mk.intro
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : span K ↑s = ⊤
⊢ IsNoetherian K V
[PROOFSTEP]
rw [IsNoetherian.iff_rank_lt_aleph0, ← rank_top, ← hs]
[GOAL]
case mpr.mk.intro
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : span K ↑s = ⊤
⊢ Module.rank K { x // x ∈ span K ↑s } < ℵ₀
[PROOFSTEP]
exact lt_of_le_of_lt (rank_span_le _) s.finite_toSet.lt_aleph0