Theorem: propagate_eq_zero_iff (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 α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
⊢ (∀ (seq : β → ℕ → Bool), propagate init_carry next_bit seq = zeroSeq) ↔
    ∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false
Tactic:
constructor
State after:
case mp
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
⊢ (∀ (seq : β → ℕ → Bool), propagate init_carry next_bit seq = zeroSeq) →
    ∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false

case mpr
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
⊢ (∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false) →
    ∀ (seq : β → ℕ → Bool), propagate init_carry next_bit seq = zeroSeq

State before:
case mp
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
⊢ (∀ (seq : β → ℕ → Bool), propagate init_carry next_bit seq = zeroSeq) →
    ∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false

case mpr
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
⊢ (∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false) →
    ∀ (seq : β → ℕ → Bool), propagate init_carry next_bit seq = zeroSeq
Tactic:
{ intro h i _
  simp [h, zeroSeq] }
State after:
case mpr
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
⊢ (∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false) →
    ∀ (seq : β → ℕ → Bool), propagate init_carry next_bit seq = zeroSeq

State before:
case mpr
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
⊢ (∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false) →
    ∀ (seq : β → ℕ → Bool), propagate init_carry next_bit seq = zeroSeq
Tactic:
{ intro h seq
  funext i
  rcases exists_repeat init_carry next_bit seq i with ⟨j, hj, seq2, hseq2⟩
  rw [← hseq2, h seq2 j hj, zeroSeq] }
State after:
no goals

State before:
case mp
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
⊢ (∀ (seq : β → ℕ → Bool), propagate init_carry next_bit seq = zeroSeq) →
    ∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false
Tactic:
intro h i _
State after:
case mp
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
h : ∀ (seq : β → ℕ → Bool), propagate init_carry next_bit seq = zeroSeq
i : β → ℕ → Bool
i✝ : ℕ
⊢ i✝ < 2 ^ card α → propagate init_carry next_bit i i✝ = false

State before:
case mp
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
h : ∀ (seq : β → ℕ → Bool), propagate init_carry next_bit seq = zeroSeq
i : β → ℕ → Bool
i✝ : ℕ
⊢ i✝ < 2 ^ card α → propagate init_carry next_bit i i✝ = false
Tactic:
simp [h, zeroSeq]
State after:
no goals

State before:
case mpr
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
⊢ (∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false) →
    ∀ (seq : β → ℕ → Bool), propagate init_carry next_bit seq = zeroSeq
Tactic:
intro h seq
State after:
case mpr
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
h : ∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false
seq : β → ℕ → Bool
⊢ propagate init_carry next_bit seq = zeroSeq

State before:
case mpr
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
h : ∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false
seq : β → ℕ → Bool
⊢ propagate init_carry next_bit seq = zeroSeq
Tactic:
funext i
State after:
case mpr.h
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
h : ∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false
seq : β → ℕ → Bool
i : ℕ
⊢ propagate init_carry next_bit seq i = zeroSeq i

State before:
case mpr.h
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
h : ∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false
seq : β → ℕ → Bool
i : ℕ
⊢ propagate init_carry next_bit seq i = zeroSeq i
Tactic:
rcases exists_repeat init_carry next_bit seq i with ⟨j, hj, seq2, hseq2⟩
State after:
case mpr.h.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
h : ∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false
seq : β → ℕ → Bool
i j : ℕ
hj : j < 2 ^ card α
seq2 : β → ℕ → Bool
hseq2 : propagate init_carry next_bit seq2 j = propagate init_carry next_bit seq i
⊢ propagate init_carry next_bit seq i = zeroSeq i

State before:
case mpr.h.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit✝ : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
h : ∀ (seq : β → ℕ → Bool) (i : ℕ), i < 2 ^ card α → propagate init_carry next_bit seq i = false
seq : β → ℕ → Bool
i j : ℕ
hj : j < 2 ^ card α
seq2 : β → ℕ → Bool
hseq2 : propagate init_carry next_bit seq2 j = propagate init_carry next_bit seq i
⊢ propagate init_carry next_bit seq i = zeroSeq i
Tactic:
rw [← hseq2, h seq2 j hj, zeroSeq]
State after:
no goals