internlm/Lean-Github huggingface dataset:
Theorem: propagate_eq_of_carry_eq
Proof state before:
case zero.succ.zero
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
n✝ : ℕ
h₁ :
  (next_bit (propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ n✝) fun i => seq₁ i n✝).fst =
    init_carry
h₃ : ∀ (y : ℕ) (b : β), y = 0 → seq₁ b (Nat.succ n✝ + y) = seq₂ b y
this : ∀ (i : β), seq₁ i (Nat.succ n✝ + 0) = seq₂ i 0
⊢ (next_bit (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₁ n✝) fun i => seq₁ i n✝).fst
        fun j => seq₁ j (n✝ + 1)).snd =
    (next_bit init_carry fun i => seq₂ i 0).snd
Tactic:
dsimp at this
Proof state after:
case zero.succ.zero
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
n✝ : ℕ
h₁ :
  (next_bit (propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ n✝) fun i => seq₁ i n✝).fst =
    init_carry
h₃ : ∀ (y : ℕ) (b : β), y = 0 → seq₁ b (Nat.succ n✝ + y) = seq₂ b y
this : ∀ (i : β), seq₁ i (n✝ + 1) = seq₂ i 0
⊢ (next_bit (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₁ n✝) fun i => seq₁ i n✝).fst
        fun j => seq₁ j (n✝ + 1)).snd =
    (next_bit init_carry fun i => seq₂ i 0).snd
Theorem: propagate_eq_of_carry_eq
Proof state before:
case zero.succ.zero
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
n✝ : ℕ
h₁ :
  (next_bit (propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ n✝) fun i => seq₁ i n✝).fst =
    init_carry
h₃ : ∀ (y : ℕ) (b : β), y = 0 → seq₁ b (Nat.succ n✝ + y) = seq₂ b y
this : ∀ (i : β), seq₁ i (n✝ + 1) = seq₂ i 0
⊢ (next_bit (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₁ n✝) fun i => seq₁ i n✝).fst
        fun j => seq₁ j (n✝ + 1)).snd =
    (next_bit init_carry fun i => seq₂ i 0).snd
Tactic:
simp [this]
Proof state after:
case zero.succ.zero
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
n✝ : ℕ
h₁ :
  (next_bit (propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ n✝) fun i => seq₁ i n✝).fst =
    init_carry
h₃ : ∀ (y : ℕ) (b : β), y = 0 → seq₁ b (Nat.succ n✝ + y) = seq₂ b y
this : ∀ (i : β), seq₁ i (n✝ + 1) = seq₂ i 0
⊢ (next_bit (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₁ n✝) fun i => seq₁ i n✝).fst
        fun j => seq₂ j 0).snd =
    (next_bit init_carry fun j => seq₂ j 0).snd
Theorem: propagate_eq_of_carry_eq
Proof state before:
case zero.succ.zero
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
n✝ : ℕ
h₁ :
  (next_bit (propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ n✝) fun i => seq₁ i n✝).fst =
    init_carry
h₃ : ∀ (y : ℕ) (b : β), y = 0 → seq₁ b (Nat.succ n✝ + y) = seq₂ b y
this : ∀ (i : β), seq₁ i (n✝ + 1) = seq₂ i 0
⊢ (next_bit (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₁ n✝) fun i => seq₁ i n✝).fst
        fun j => seq₂ j 0).snd =
    (next_bit init_carry fun j => seq₂ j 0).snd
Tactic:
simp [h₁]
Proof state after:
no goals
Theorem: propagate_eq_of_carry_eq
Proof state before:
case zero.succ.succ
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
n✝¹ n✝ : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ (Nat.succ n✝¹) =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (Nat.succ n✝)
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.succ n✝¹ + y) = seq₂ b (Nat.succ n✝ + y)
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝¹ + Nat.zero) =
    propagate init_carry next_bit seq₂ (Nat.succ n✝ + Nat.zero)
Tactic:
rw [propagate_succ2, h₁, propagate_succ2]
Proof state after:
case zero.succ.succ
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
n✝¹ n✝ : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ (Nat.succ n✝¹) =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (Nat.succ n✝)
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.succ n✝¹ + y) = seq₂ b (Nat.succ n✝ + y)
⊢ (next_bit (propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (Nat.succ n✝)) fun j =>
        seq₁ j (n✝¹ + 1)).snd =
    (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₂ (n✝ + 1)) fun j => seq₂ j (n✝ + 1)).snd
Theorem: propagate_eq_of_carry_eq
Proof state before:
case zero.succ.succ
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
n✝¹ n✝ : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ (Nat.succ n✝¹) =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (Nat.succ n✝)
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.succ n✝¹ + y) = seq₂ b (Nat.succ n✝ + y)
⊢ (next_bit (propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (Nat.succ n✝)) fun j =>
        seq₁ j (n✝¹ + 1)).snd =
    (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₂ (n✝ + 1)) fun j => seq₂ j (n✝ + 1)).snd
Tactic:
have := h₃ 0
Proof state after:
case zero.succ.succ
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
n✝¹ n✝ : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ (Nat.succ n✝¹) =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (Nat.succ n✝)
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.succ n✝¹ + y) = seq₂ b (Nat.succ n✝ + y)
this : ∀ (b : β), 0 ≤ Nat.zero → seq₁ b (Nat.succ n✝¹ + 0) = seq₂ b (Nat.succ n✝ + 0)
⊢ (next_bit (propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (Nat.succ n✝)) fun j =>
        seq₁ j (n✝¹ + 1)).snd =
    (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₂ (n✝ + 1)) fun j => seq₂ j (n✝ + 1)).snd
Theorem: propagate_eq_of_carry_eq
Proof state before:
case zero.succ.succ
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
n✝¹ n✝ : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ (Nat.succ n✝¹) =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (Nat.succ n✝)
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.succ n✝¹ + y) = seq₂ b (Nat.succ n✝ + y)
this : ∀ (b : β), 0 ≤ Nat.zero → seq₁ b (Nat.succ n✝¹ + 0) = seq₂ b (Nat.succ n✝ + 0)
⊢ (next_bit (propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (Nat.succ n✝)) fun j =>
        seq₁ j (n✝¹ + 1)).snd =
    (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₂ (n✝ + 1)) fun j => seq₂ j (n✝ + 1)).snd
Tactic:
simp [*] at *
Proof state after:
no goals
Theorem: propagate_eq_of_carry_eq
Proof state before:
case succ
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
m n : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ m =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n
n✝ : ℕ
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.succ n✝ → seq₁ b (m + y) = seq₂ b (n + y)
⊢ propagate init_carry next_bit seq₁ (m + Nat.succ n✝) = propagate init_carry next_bit seq₂ (n + Nat.succ n✝)
Tactic:
erw [Nat.add_succ, propagate_succ2, propagate_succ2, Nat.add_eq, Nat.add_eq]
Proof state after:
case succ
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
m n : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ m =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n
n✝ : ℕ
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.succ n✝ → seq₁ b (m + y) = seq₂ b (n + y)
⊢ (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₁ (m + n✝ + 1)) fun j =>
        seq₁ j (m + n✝ + 1)).snd =
    (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₂ (n + n✝ + 1)) fun j =>
        seq₂ j (n + n✝ + 1)).snd
Theorem: propagate_eq_of_carry_eq
Proof state before:
case succ
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
m n : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ m =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n
n✝ : ℕ
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.succ n✝ → seq₁ b (m + y) = seq₂ b (n + y)
⊢ (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₁ (m + n✝ + 1)) fun j =>
        seq₁ j (m + n✝ + 1)).snd =
    (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₂ (n + n✝ + 1)) fun j =>
        seq₂ j (n + n✝ + 1)).snd
Tactic:
simp [← Nat.succ_eq_add_one, ← Nat.add_succ, h₃ _ _ (le_refl _)]
Proof state after:
case succ
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
m n : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ m =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n
n✝ : ℕ
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.succ n✝ → seq₁ b (m + y) = seq₂ b (n + y)
⊢ (next_bit
        (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₁ (m + n✝)) fun i =>
            seq₁ i (m + n✝)).fst
        fun j => seq₂ j (n + Nat.succ n✝)).snd =
    (next_bit
        (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₂ (n + n✝)) fun i =>
            seq₂ i (n + n✝)).fst
        fun j => seq₂ j (n + Nat.succ n✝)).snd
Theorem: propagate_eq_of_carry_eq
Proof state before:
case succ
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
m n : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ m =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n
n✝ : ℕ
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.succ n✝ → seq₁ b (m + y) = seq₂ b (n + y)
⊢ (next_bit
        (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₁ (m + n✝)) fun i =>
            seq₁ i (m + n✝)).fst
        fun j => seq₂ j (n + Nat.succ n✝)).snd =
    (next_bit
        (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₂ (n + n✝)) fun i =>
            seq₂ i (n + n✝)).fst
        fun j => seq₂ j (n + Nat.succ n✝)).snd
Tactic:
congr
Proof state after:
case succ.e_self.e__carry.e_self.e__carry
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
m n : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ m =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n
n✝ : ℕ
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.succ n✝ → seq₁ b (m + y) = seq₂ b (n + y)
⊢ propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₁ (m + n✝) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₂ (n + n✝)

case succ.e_self.e__carry.e_self.e__bits
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
m n : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ m =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n
n✝ : ℕ
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.succ n✝ → seq₁ b (m + y) = seq₂ b (n + y)
⊢ (fun i => seq₁ i (m + n✝)) = fun i => seq₂ i (n + n✝)
Theorem: propagate_eq_of_carry_eq
Proof state before:
case succ.e_self.e__carry.e_self.e__carry
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
m n : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ m =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n
n✝ : ℕ
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.succ n✝ → seq₁ b (m + y) = seq₂ b (n + y)
⊢ propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₁ (m + n✝) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₂ (n + n✝)

case succ.e_self.e__carry.e_self.e__bits
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
m n : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ m =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n
n✝ : ℕ
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.succ n✝ → seq₁ b (m + y) = seq₂ b (n + y)
⊢ (fun i => seq₁ i (m + n✝)) = fun i => seq₂ i (n + n✝)
Tactic:
. apply propagateCarry2_eq_of_carry_eq
  . assumption
  . exact λ y b h => h₃ y b (Nat.le_succ_of_le h)
Proof state after:
case succ.e_self.e__carry.e_self.e__bits
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
m n : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ m =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n
n✝ : ℕ
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.succ n✝ → seq₁ b (m + y) = seq₂ b (n + y)
⊢ (fun i => seq₁ i (m + n✝)) = fun i => seq₂ i (n + n✝)
Theorem: propagate_eq_of_carry_eq
Proof state before:
case succ.e_self.e__carry.e_self.e__bits
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
m n : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ m =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n
n✝ : ℕ
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.succ n✝ → seq₁ b (m + y) = seq₂ b (n + y)
⊢ (fun i => seq₁ i (m + n✝)) = fun i => seq₂ i (n + n✝)
Tactic:
. funext i
  rw [h₃]
  exact Nat.le_succ _
Proof state after:
no goals
Theorem: propagateCarry_propagateCarry_add
Proof state before:
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
x : β → ℕ → Bool
init_carry : α → Bool
_next_carry : (α → Bool) → (β → Bool) → α → Bool
⊢ propagateCarry2 (propagateCarry2 init_carry _next_carry x 0) _next_carry (fun b k => x b (k + 0)) 0 =
    propagateCarry2 init_carry _next_carry x (0 + 0)
Tactic:
simp [propagateCarry2]
Proof state after:
no goals
Theorem: propagateCarry_propagateCarry_add
Proof state before:
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
x : β → ℕ → Bool
init_carry : α → Bool
next_carr : (α → Bool) → (β → Bool) → α → Bool
n : ℕ
⊢ propagateCarry2 (propagateCarry2 init_carry next_carr x (n + 1)) next_carr (fun b k => x b (k + (n + 1))) 0 =
    propagateCarry2 init_carry next_carr x (0 + (n + 1))
Tactic:
simp [propagateCarry, propagateCarry2_succ]
Proof state after:
no goals
Theorem: propagateCarry_propagateCarry_add
Proof state before:
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry✝ : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
x : β → ℕ → Bool
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
n i : ℕ
⊢ propagateCarry2 (propagateCarry2 init_carry next_carry x n) next_carry (fun b k => x b (k + n)) (i + 1) =
    propagateCarry2 init_carry next_carry x (i + 1 + n)
Tactic:
rw [propagateCarry2, add_assoc,
  propagateCarry_propagateCarry_add _ _ _ _ i]
Proof state after:
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry✝ : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
x : β → ℕ → Bool
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
n i : ℕ
⊢ (next_carry (propagateCarry2 init_carry next_carry x (i + n)) fun i_1 => x i_1 (i + n)) =
    propagateCarry2 init_carry next_carry x (i + (1 + n))
Theorem: propagateCarry_propagateCarry_add
Proof state before:
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry✝ : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
x : β → ℕ → Bool
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
n i : ℕ
⊢ (next_carry (propagateCarry2 init_carry next_carry x (i + n)) fun i_1 => x i_1 (i + n)) =
    propagateCarry2 init_carry next_carry x (i + (1 + n))
Tactic:
simp only [Nat.one_add, Nat.add_one, Nat.succ_add, Nat.add_succ,
  add_zero, propagateCarry2, zero_add]
Proof state after:
no goals
Theorem: exists_repeat
Proof state before:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Tactic:
by_cases hn2 : n < 2 ^ card α
Proof state after:
case pos
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : n < 2 ^ card α
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n

case neg
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Theorem: exists_repeat
Proof state before:
case pos
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : n < 2 ^ card α
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n

case neg
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Tactic:
{ exact ⟨n, hn2, seq, rfl⟩ }
Proof state after:
case neg
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Theorem: exists_repeat
Proof state before:
case neg
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Tactic:
{ rcases exists_repeat_carry
    (propagateCarry2 init_carry (λ c b => (next_bit c b).1) seq
      (n - 2 ^ card α))
    (λ carry bits => (next_bit  carry bits).1)
    (λ b i => seq b (i + (n - 2^ (card α)))) with ⟨a, b, h₁, h₂⟩
  simp only [propagateCarry_propagateCarry_add] at h₁
  rcases have _wf : n - (b - a) < n :=
     Nat.sub_lt (lt_of_lt_of_le (pow_pos (by norm_num) _) (le_of_not_lt hn2)) (Nat.sub_pos_of_lt h₂)
    exists_repeat (λ c i => if i < a + (n - 2 ^ card α) then seq c i else
      seq c (i + (b - a))) (n - (b - a)) with ⟨m, hmle, seq2, hm⟩
  use m; use hmle; use seq2
  rw [hm]; clear hm
  have h1 : n - (b - a) = (a + (n - 2 ^ (card α))) + (2 ^ card α - b) := by
  { zify
    rw [Nat.cast_sub, Nat.cast_sub, Nat.cast_sub, Nat.cast_sub]
    ring_nf
    exact Nat.le_of_lt_succ b.2
    simp [*] at *
    exact hn2
    exact le_of_lt h₂
    exact le_trans (Nat.sub_le _ _) (le_trans (Nat.le_of_lt_succ b.2)
      (le_of_not_lt hn2)) }
  rw [h1]
  have h2 : n = (b + (n - 2 ^ card α)) + (2 ^ card α - b) := by
  { zify
    rw [Nat.cast_sub, Nat.cast_sub]
    ring
    exact Nat.le_of_lt_succ b.2
    simp [*] at *
    exact hn2 }
  conv_rhs => rw [h2]
  refine' propagate_eq_of_carry_eq _ _ _ _ _ _ _ _ _
  { have _h : ↑b + (n - 2 ^ card α) = (a + (n - 2 ^ card α)) + (b - a) := by
    { zify
      rw [Nat.cast_sub, Nat.cast_sub]
      ring_nf
      exact le_of_lt h₂
      exact le_of_not_lt hn2 }
    rw [← h₁]
    apply propagateCarry2_eq_of_seq_eq_lt
    simp (config := { contextual := true }) }
  { intro y c _hc
    simp only [add_lt_iff_neg_left, not_lt_zero', if_false]
    congr 1
    zify
    rw [Nat.cast_sub, Nat.cast_sub]
    ring
    exact le_of_lt h₂
    exact le_of_not_lt hn2 } }
Proof state after:
no goals
Theorem: exists_repeat
Proof state before:
case pos
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : n < 2 ^ card α
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Tactic:
exact ⟨n, hn2, seq, rfl⟩
Proof state after:
no goals