Theorem: propagateCarry2_eq_of_seq_eq_lt (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
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
i : ℕ
h : ∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j
⊢ propagateCarry2 init_carry next_carry seq₁ i = propagateCarry2 init_carry next_carry seq₂ i
Tactic:
induction' i with i ih
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_carry : (α → Bool) → (β → Bool) → α → Bool
i : ℕ
h✝ : ∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j
h : ∀ (b : β) (j : ℕ), j < Nat.zero → seq₁ b j = seq₂ b j
⊢ propagateCarry2 init_carry next_carry seq₁ Nat.zero = propagateCarry2 init_carry next_carry 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_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
⊢ propagateCarry2 init_carry next_carry seq₁ (Nat.succ i) = propagateCarry2 init_carry next_carry seq₂ (Nat.succ i)

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_carry : (α → Bool) → (β → Bool) → α → Bool
i : ℕ
h✝ : ∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j
h : ∀ (b : β) (j : ℕ), j < Nat.zero → seq₁ b j = seq₂ b j
⊢ propagateCarry2 init_carry next_carry seq₁ Nat.zero = propagateCarry2 init_carry next_carry 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_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
⊢ propagateCarry2 init_carry next_carry seq₁ (Nat.succ i) = propagateCarry2 init_carry next_carry seq₂ (Nat.succ i)
Tactic:
{ simp [propagateCarry2] }
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
⊢ propagateCarry2 init_carry next_carry seq₁ (Nat.succ i) = propagateCarry2 init_carry next_carry seq₂ (Nat.succ i)

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
⊢ propagateCarry2 init_carry next_carry seq₁ (Nat.succ i) = propagateCarry2 init_carry next_carry seq₂ (Nat.succ i)
Tactic:
{ simp only [propagateCarry2, h _ i (Nat.lt_succ_self i)]
  rw [ih]
  exact λ b j hj => h b j (Nat.lt_succ_of_lt hj) }
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
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
i : ℕ
h✝ : ∀ (b : β) (j : ℕ), j < i → seq₁ b j = seq₂ b j
h : ∀ (b : β) (j : ℕ), j < Nat.zero → seq₁ b j = seq₂ b j
⊢ propagateCarry2 init_carry next_carry seq₁ Nat.zero = propagateCarry2 init_carry next_carry seq₂ Nat.zero
Tactic:
simp [propagateCarry2]
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
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
⊢ propagateCarry2 init_carry next_carry seq₁ (Nat.succ i) = propagateCarry2 init_carry next_carry seq₂ (Nat.succ i)
Tactic:
simp only [propagateCarry2, h _ i (Nat.lt_succ_self i)]
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
⊢ (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

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

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