Theorem: propagateCarry2_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
x✝ : ℕ
h₃✝ : ∀ (y : ℕ) (b : β), y ≤ x✝ → seq₁✝ b (m + y) = seq₂✝ b (n + y)
x : ℕ
ih :
  ∀ (seq₁ seq₂ : β → ℕ → Bool),
    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 →
      (∀ (y : ℕ) (b : β), y ≤ x → seq₁ b (m + y) = seq₂ b (n + y)) →
        propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ (m + x) =
          propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (n + x)
seq₁ seq₂ : β → ℕ → Bool
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
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.succ x → seq₁ b (m + y) = seq₂ b (n + y)
⊢ (next_bit (propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ (m + x)) fun i =>
        seq₂ i (n + x)).fst =
    (next_bit (propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (n + x)) fun i =>
        seq₂ i (n + x)).fst
Tactic:
rw [ih]
Proof state after:
case succ.h₁
α β α' β' : 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
x✝ : ℕ
h₃✝ : ∀ (y : ℕ) (b : β), y ≤ x✝ → seq₁✝ b (m + y) = seq₂✝ b (n + y)
x : ℕ
ih :
  ∀ (seq₁ seq₂ : β → ℕ → Bool),
    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 →
      (∀ (y : ℕ) (b : β), y ≤ x → seq₁ b (m + y) = seq₂ b (n + y)) →
        propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ (m + x) =
          propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (n + x)
seq₁ seq₂ : β → ℕ → Bool
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
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.succ x → seq₁ b (m + y) = seq₂ b (n + y)
⊢ 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

case succ.h₃
α β α' β' : 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
x✝ : ℕ
h₃✝ : ∀ (y : ℕ) (b : β), y ≤ x✝ → seq₁✝ b (m + y) = seq₂✝ b (n + y)
x : ℕ
ih :
  ∀ (seq₁ seq₂ : β → ℕ → Bool),
    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 →
      (∀ (y : ℕ) (b : β), y ≤ x → seq₁ b (m + y) = seq₂ b (n + y)) →
        propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ (m + x) =
          propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (n + x)
seq₁ seq₂ : β → ℕ → Bool
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
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.succ x → seq₁ b (m + y) = seq₂ b (n + y)
⊢ ∀ (y : ℕ) (b : β), y ≤ x → seq₁ b (m + y) = seq₂ b (n + y)