Theorem: propagate_eq_of_carry_eq (Lean4bits/lemmas.lean)

State before:
α β α' β' : 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)
⊢ propagate init_carry next_bit seq₁ (m + x) = propagate init_carry next_bit seq₂ (n + x)
Tactic:
cases x
State after:
case zero
α β α' β' : 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
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (m + y) = seq₂ b (n + y)
⊢ propagate init_carry next_bit seq₁ (m + Nat.zero) = propagate init_carry next_bit seq₂ (n + Nat.zero)

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✝)

State before:
case zero
α β α' β' : 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
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (m + y) = seq₂ b (n + y)
⊢ propagate init_carry next_bit seq₁ (m + Nat.zero) = propagate init_carry next_bit seq₂ (n + Nat.zero)

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:
{ cases m
  { cases n
    { simp [h₃ 0 _ (le_refl _), propagateCarry2, *] at * }
    { simp [*, h₃ 0 _ (le_refl _), propagate_succ2] at *
      rw [← h₁] } }
  { cases n
    { simp [*, propagate_succ2] at *
      have := fun i => h₃ 0 i rfl
      dsimp at this
      simp [this]
      simp [h₁] }
    { rw [propagate_succ2, h₁, propagate_succ2]
      have := h₃ 0
      simp [*] at * } } }
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)
⊢ propagate init_carry next_bit seq₁ (m + Nat.succ n✝) = propagate init_carry next_bit seq₂ (n + Nat.succ n✝)

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]
  simp [← Nat.succ_eq_add_one, ← Nat.add_succ, h₃ _ _ (le_refl _)]
  congr
  . apply propagateCarry2_eq_of_carry_eq
    . assumption
    . exact λ y b h => h₃ y b (Nat.le_succ_of_le h)
  . funext i
    rw [h₃]
    exact Nat.le_succ _ }
State after:
no goals

State before:
case zero
α β α' β' : 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
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (m + y) = seq₂ b (n + y)
⊢ propagate init_carry next_bit seq₁ (m + Nat.zero) = propagate init_carry next_bit seq₂ (n + Nat.zero)
Tactic:
cases m
State after:
case zero.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₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ Nat.zero =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.zero + y) = seq₂ b (n + y)
⊢ propagate init_carry next_bit seq₁ (Nat.zero + Nat.zero) = propagate init_carry next_bit seq₂ (n + Nat.zero)

case zero.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₂ n
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.succ n✝ + y) = seq₂ b (n + y)
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝ + Nat.zero) = propagate init_carry next_bit seq₂ (n + Nat.zero)

State before:
case zero.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₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ Nat.zero =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.zero + y) = seq₂ b (n + y)
⊢ propagate init_carry next_bit seq₁ (Nat.zero + Nat.zero) = propagate init_carry next_bit seq₂ (n + Nat.zero)

case zero.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₂ n
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.succ n✝ + y) = seq₂ b (n + y)
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝ + Nat.zero) = propagate init_carry next_bit seq₂ (n + Nat.zero)
Tactic:
{ cases n
  { simp [h₃ 0 _ (le_refl _), propagateCarry2, *] at * }
  { simp [*, h₃ 0 _ (le_refl _), propagate_succ2] at *
    rw [← h₁] } }
State after:
case zero.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₂ n
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.succ n✝ + y) = seq₂ b (n + y)
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝ + Nat.zero) = propagate init_carry next_bit seq₂ (n + Nat.zero)

State before:
case zero.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₂ n
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.succ n✝ + y) = seq₂ b (n + y)
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝ + Nat.zero) = propagate init_carry next_bit seq₂ (n + Nat.zero)
Tactic:
{ cases n
  { simp [*, propagate_succ2] at *
    have := fun i => h₃ 0 i rfl
    dsimp at this
    simp [this]
    simp [h₁] }
  { rw [propagate_succ2, h₁, propagate_succ2]
    have := h₃ 0
    simp [*] at * } }
State after:
no goals

State before:
case zero.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₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ Nat.zero =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.zero + y) = seq₂ b (n + y)
⊢ propagate init_carry next_bit seq₁ (Nat.zero + Nat.zero) = propagate init_carry next_bit seq₂ (n + Nat.zero)
Tactic:
cases n
State after:
case zero.zero.zero
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ Nat.zero =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ Nat.zero
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.zero + y) = seq₂ b (Nat.zero + y)
⊢ propagate init_carry next_bit seq₁ (Nat.zero + Nat.zero) = propagate init_carry next_bit seq₂ (Nat.zero + Nat.zero)

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

State before:
case zero.zero.zero
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ Nat.zero =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ Nat.zero
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.zero + y) = seq₂ b (Nat.zero + y)
⊢ propagate init_carry next_bit seq₁ (Nat.zero + Nat.zero) = propagate init_carry next_bit seq₂ (Nat.zero + Nat.zero)

case zero.zero.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✝ : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ Nat.zero =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (Nat.succ n✝)
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.zero + y) = seq₂ b (Nat.succ n✝ + y)
⊢ propagate init_carry next_bit seq₁ (Nat.zero + Nat.zero) = propagate init_carry next_bit seq₂ (Nat.succ n✝ + Nat.zero)
Tactic:
{ simp [h₃ 0 _ (le_refl _), propagateCarry2, *] at * }
State after:
case zero.zero.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✝ : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ Nat.zero =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (Nat.succ n✝)
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.zero + y) = seq₂ b (Nat.succ n✝ + y)
⊢ propagate init_carry next_bit seq₁ (Nat.zero + Nat.zero) = propagate init_carry next_bit seq₂ (Nat.succ n✝ + Nat.zero)

State before:
case zero.zero.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✝ : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ Nat.zero =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (Nat.succ n✝)
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.zero + y) = seq₂ b (Nat.succ n✝ + y)
⊢ propagate init_carry next_bit seq₁ (Nat.zero + Nat.zero) = propagate init_carry next_bit seq₂ (Nat.succ n✝ + Nat.zero)
Tactic:
{ simp [*, h₃ 0 _ (le_refl _), propagate_succ2] at *
  rw [← h₁] }
State after:
no goals

State before:
case zero.zero.zero
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ Nat.zero =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ Nat.zero
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.zero + y) = seq₂ b (Nat.zero + y)
⊢ propagate init_carry next_bit seq₁ (Nat.zero + Nat.zero) = propagate init_carry next_bit seq₂ (Nat.zero + Nat.zero)
Tactic:
simp [h₃ 0 _ (le_refl _), propagateCarry2, *] at *
State after:
no goals

State before:
case zero.zero.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✝ : ℕ
h₁ :
  propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ Nat.zero =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (Nat.succ n✝)
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.zero + y) = seq₂ b (Nat.succ n✝ + y)
⊢ propagate init_carry next_bit seq₁ (Nat.zero + Nat.zero) = propagate init_carry next_bit seq₂ (Nat.succ n✝ + Nat.zero)
Tactic:
simp [*, h₃ 0 _ (le_refl _), propagate_succ2] at *
State after:
case zero.zero.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✝ : ℕ
h₁ :
  init_carry =
    (next_bit (propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n✝) fun i => seq₂ i n✝).fst
h₃ : ∀ (y : ℕ) (b : β), y = 0 → seq₁ b y = seq₂ b (Nat.succ n✝ + y)
⊢ (next_bit init_carry fun i => seq₂ i (Nat.succ n✝)).snd =
    (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

State before:
case zero.zero.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✝ : ℕ
h₁ :
  init_carry =
    (next_bit (propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ n✝) fun i => seq₂ i n✝).fst
h₃ : ∀ (y : ℕ) (b : β), y = 0 → seq₁ b y = seq₂ b (Nat.succ n✝ + y)
⊢ (next_bit init_carry fun i => seq₂ i (Nat.succ n✝)).snd =
    (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
Tactic:
rw [← h₁]
State after:
no goals

State before:
case zero.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₂ n
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.succ n✝ + y) = seq₂ b (n + y)
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝ + Nat.zero) = propagate init_carry next_bit seq₂ (n + Nat.zero)
Tactic:
cases n
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₁ :
  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.zero
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.succ n✝ + y) = seq₂ b (Nat.zero + y)
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝ + Nat.zero) = propagate init_carry next_bit seq₂ (Nat.zero + Nat.zero)

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)

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₁ :
  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.zero
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.succ n✝ + y) = seq₂ b (Nat.zero + y)
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝ + Nat.zero) = propagate init_carry next_bit seq₂ (Nat.zero + Nat.zero)

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:
{ simp [*, propagate_succ2] at *
  have := fun i => h₃ 0 i rfl
  dsimp at this
  simp [this]
  simp [h₁] }
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)
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝¹ + Nat.zero) =
    propagate init_carry next_bit seq₂ (Nat.succ n✝ + Nat.zero)

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]
  have := h₃ 0
  simp [*] at * }
State after:
no goals

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₁ :
  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.zero
h₃ : ∀ (y : ℕ) (b : β), y ≤ Nat.zero → seq₁ b (Nat.succ n✝ + y) = seq₂ b (Nat.zero + y)
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝ + Nat.zero) = propagate init_carry next_bit seq₂ (Nat.zero + Nat.zero)
Tactic:
simp [*, propagate_succ2] at *
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
⊢ (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

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
⊢ (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:
have := fun i => h₃ 0 i rfl
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 (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

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
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

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]
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

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₁]
State after:
no goals

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]
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

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
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

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 *
State after:
no goals

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]
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

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 _)]
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

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
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✝)

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)
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✝)

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 _
State after:
no goals