internlm/Lean-Github huggingface dataset:
Theorem: propagateCarry2_eq_of_seq_eq_lt
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
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
i✝ : ℕ
h✝ : ∀ (b : β) (j : ℕ), j < i✝ → seq₁ b j = seq₂ b j
i : ℕ
ih :
  (∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j) →
    propagateCarry2 init_carry next_carry seq₁ i = propagateCarry2 init_carry next_carry seq₂ i
h : ∀ (b : β) (j : ℕ), j < Nat.succ i → seq₁ b j = seq₂ b j
⊢ (next_carry (propagateCarry2 init_carry next_carry seq₁ i) fun i_1 => seq₂ i_1 i) =
    next_carry (propagateCarry2 init_carry next_carry seq₂ i) fun i_1 => seq₂ i_1 i
Tactic:
rw [ih]
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
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
i✝ : ℕ
h✝ : ∀ (b : β) (j : ℕ), j < i✝ → seq₁ b j = seq₂ b j
i : ℕ
ih :
  (∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j) →
    propagateCarry2 init_carry next_carry seq₁ i = propagateCarry2 init_carry next_carry seq₂ i
h : ∀ (b : β) (j : ℕ), j < Nat.succ i → seq₁ b j = seq₂ b j
⊢ ∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j
Theorem: propagateCarry2_eq_of_seq_eq_lt
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
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
i✝ : ℕ
h✝ : ∀ (b : β) (j : ℕ), j < i✝ → seq₁ b j = seq₂ b j
i : ℕ
ih :
  (∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j) →
    propagateCarry2 init_carry next_carry seq₁ i = propagateCarry2 init_carry next_carry seq₂ i
h : ∀ (b : β) (j : ℕ), j < Nat.succ i → seq₁ b j = seq₂ b j
⊢ ∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j
Tactic:
exact λ b j hj => h b j (Nat.lt_succ_of_lt hj)
Proof state after:
no goals
Theorem: propagate_eq_of_seq_eq_le
Proof 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
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
i : ℕ
h : ∀ (b : β) (j : ℕ), j ≤ i → seq₁ b j = seq₂ b j
⊢ propagate init_carry next_bit seq₁ i = propagate init_carry next_bit seq₂ i
Tactic:
cases i
Proof 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
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
h : ∀ (b : β) (j : ℕ), j ≤ Nat.zero → seq₁ b j = seq₂ b j
⊢ propagate init_carry next_bit seq₁ Nat.zero = propagate init_carry next_bit seq₂ 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
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
n✝ : ℕ
h : ∀ (b : β) (j : ℕ), j ≤ Nat.succ n✝ → seq₁ b j = seq₂ b j
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝) = propagate init_carry next_bit seq₂ (Nat.succ n✝)
Theorem: propagate_eq_of_seq_eq_le
Proof 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
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
h : ∀ (b : β) (j : ℕ), j ≤ Nat.zero → seq₁ b j = seq₂ b j
⊢ propagate init_carry next_bit seq₁ Nat.zero = propagate init_carry next_bit seq₂ 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
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
n✝ : ℕ
h : ∀ (b : β) (j : ℕ), j ≤ Nat.succ n✝ → seq₁ b j = seq₂ b j
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝) = propagate init_carry next_bit seq₂ (Nat.succ n✝)
Tactic:
{ simp [propagate_zero, h _ 0 (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
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
n✝ : ℕ
h : ∀ (b : β) (j : ℕ), j ≤ Nat.succ n✝ → seq₁ b j = seq₂ b j
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝) = propagate init_carry next_bit seq₂ (Nat.succ n✝)
Theorem: propagate_eq_of_seq_eq_le
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
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
n✝ : ℕ
h : ∀ (b : β) (j : ℕ), j ≤ Nat.succ n✝ → seq₁ b j = seq₂ b j
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝) = propagate init_carry next_bit seq₂ (Nat.succ n✝)
Tactic:
{ simp only [propagate_succ2, propagate_succ2, h _ _ (le_refl _)]
  congr 2
  apply propagateCarry2_eq_of_seq_eq_lt
  exact λ b j hj => h b j (le_of_lt hj) }
Proof state after:
no goals
Theorem: propagate_eq_of_seq_eq_le
Proof 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
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
h : ∀ (b : β) (j : ℕ), j ≤ Nat.zero → seq₁ b j = seq₂ b j
⊢ propagate init_carry next_bit seq₁ Nat.zero = propagate init_carry next_bit seq₂ Nat.zero
Tactic:
simp [propagate_zero, h _ 0 (le_refl _)]
Proof state after:
no goals
Theorem: propagate_eq_of_seq_eq_le
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
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
n✝ : ℕ
h : ∀ (b : β) (j : ℕ), j ≤ Nat.succ n✝ → seq₁ b j = seq₂ b j
⊢ propagate init_carry next_bit seq₁ (Nat.succ n✝) = propagate init_carry next_bit seq₂ (Nat.succ n✝)
Tactic:
simp only [propagate_succ2, propagate_succ2, 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
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
n✝ : ℕ
h : ∀ (b : β) (j : ℕ), j ≤ Nat.succ n✝ → seq₁ b j = seq₂ b j
⊢ (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₁ (n✝ + 1)) fun j =>
        seq₂ j (Nat.succ n✝)).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_seq_eq_le
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
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
n✝ : ℕ
h : ∀ (b : β) (j : ℕ), j ≤ Nat.succ n✝ → seq₁ b j = seq₂ b j
⊢ (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₁ (n✝ + 1)) fun j =>
        seq₂ j (Nat.succ n✝)).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:
congr 2
Proof state after:
case succ.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
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
n✝ : ℕ
h : ∀ (b : β) (j : ℕ), j ≤ Nat.succ n✝ → seq₁ b j = seq₂ b j
⊢ propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₁ (n✝ + 1) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₂ (n✝ + 1)
Theorem: propagate_eq_of_seq_eq_le
Proof state before:
case succ.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
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
n✝ : ℕ
h : ∀ (b : β) (j : ℕ), j ≤ Nat.succ n✝ → seq₁ b j = seq₂ b j
⊢ propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₁ (n✝ + 1) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq₂ (n✝ + 1)
Tactic:
apply propagateCarry2_eq_of_seq_eq_lt
Proof state after:
case succ.e_self.e__carry.h
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
n✝ : ℕ
h : ∀ (b : β) (j : ℕ), j ≤ Nat.succ n✝ → seq₁ b j = seq₂ b j
⊢ ∀ (b : β) (j : ℕ), j < n✝ + 1 → seq₁ b j = seq₂ b j
Theorem: propagate_eq_of_seq_eq_le
Proof state before:
case succ.e_self.e__carry.h
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : β → ℕ → Bool
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
n✝ : ℕ
h : ∀ (b : β) (j : ℕ), j ≤ Nat.succ n✝ → seq₁ b j = seq₂ b j
⊢ ∀ (b : β) (j : ℕ), j < n✝ + 1 → seq₁ b j = seq₂ b j
Tactic:
exact λ b j hj => h b j (le_of_lt hj)
Proof state after:
no goals
Theorem: propagateCarry2_eq_of_carry_eq
Proof 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)
⊢ 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)
Tactic:
induction' x with x ih generalizing seq₁ seq₂
Proof 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
x : ℕ
h₃✝ : ∀ (y : ℕ) (b : β), y ≤ x → seq₁✝ b (m + y) = seq₂✝ b (n + y)
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.zero → seq₁ b (m + y) = seq₂ b (n + y)
⊢ propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ (m + Nat.zero) =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) 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
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 + Nat.succ x) =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (n + Nat.succ x)
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)
⊢ propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ (m + Nat.succ x) =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (n + Nat.succ x)
Tactic:
{ simp only [propagateCarry2, Nat.add_eq, h₃ x _ (Nat.le_succ _)] at *
  rw [ih]
  assumption
  exact λ y b h => h₃ y b (Nat.le_succ_of_le h) }
Proof state after:
no goals
Theorem: propagateCarry2_eq_of_carry_eq
Proof 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
x : ℕ
h₃✝ : ∀ (y : ℕ) (b : β), y ≤ x → seq₁✝ b (m + y) = seq₂✝ b (n + y)
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.zero → seq₁ b (m + y) = seq₂ b (n + y)
⊢ propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ (m + Nat.zero) =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (n + Nat.zero)
Tactic:
simp [*] at *
Proof state after:
no goals
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)
⊢ propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₁ (m + Nat.succ x) =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq₂ (n + Nat.succ x)
Tactic:
simp only [propagateCarry2, Nat.add_eq, h₃ x _ (Nat.le_succ _)] at *
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
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
Theorem: propagateCarry2_eq_of_carry_eq
Proof state before:
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)
Tactic:
exact λ y b h => h₃ y b (Nat.le_succ_of_le h)
Proof state after:
no goals
Theorem: propagate_eq_of_carry_eq
Proof 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
Proof 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✝)