Theorem: eval_eq_iff_xorSeq_eq_zero (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 α'
t₁ t₂ : Term
⊢ eval t₁ = eval t₂ ↔ evalFin (Term.xor t₁ t₂) = fun x => zeroSeq
Tactic:
simp only [Function.funext_iff, Term.eval, Term.evalFin,
  ← eq_iff_xorSeq_eq_zero, ← evalFin_eq_eval]
State after:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
⊢ (∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1) ↔
    ∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
      evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
        evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i

State before:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
⊢ (∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1) ↔
    ∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
      evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
        evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i
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 α'
t₁ t₂ : Term
⊢ (∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1) →
    ∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
      evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
        evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i

case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
⊢ (∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
      evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
        evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i) →
    ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1

State before:
case mp
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
⊢ (∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1) →
    ∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
      evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
        evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i

case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
⊢ (∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
      evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
        evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i) →
    ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1
Tactic:
{ intro h seq n
  have := h (λ j => if hj : j < (arity (t₁.xor t₂)) then seq ⟨j, hj⟩ else λ _ => false) n
  simp at this
  convert this }
State after:
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
⊢ (∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
      evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
        evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i) →
    ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1

State before:
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
⊢ (∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
      evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
        evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i) →
    ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1
Tactic:
{ intro h seq m
  exact h (λ j => seq j) _ }
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 α'
t₁ t₂ : Term
⊢ (∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1) →
    ∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
      evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
        evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i
Tactic:
intro h seq n
State after:
case mp
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
h : ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1
seq : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool
n : ℕ
⊢ evalFin t₁ (fun i => seq (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n =
    evalFin t₂ (fun i => seq (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n

State before:
case mp
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
h : ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1
seq : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool
n : ℕ
⊢ evalFin t₁ (fun i => seq (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n =
    evalFin t₂ (fun i => seq (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n
Tactic:
have := h (λ j => if hj : j < (arity (t₁.xor t₂)) then seq ⟨j, hj⟩ else λ _ => false) n
State after:
case mp
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
h : ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1
seq : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool
n : ℕ
this :
  evalFin t₁ (fun i => if hj : ↑i < arity (Term.xor t₁ t₂) then seq { val := ↑i, isLt := hj } else fun x => false) n =
    evalFin t₂ (fun i => if hj : ↑i < arity (Term.xor t₁ t₂) then seq { val := ↑i, isLt := hj } else fun x => false) n
⊢ evalFin t₁ (fun i => seq (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n =
    evalFin t₂ (fun i => seq (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n

State before:
case mp
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
h : ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1
seq : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool
n : ℕ
this :
  evalFin t₁ (fun i => if hj : ↑i < arity (Term.xor t₁ t₂) then seq { val := ↑i, isLt := hj } else fun x => false) n =
    evalFin t₂ (fun i => if hj : ↑i < arity (Term.xor t₁ t₂) then seq { val := ↑i, isLt := hj } else fun x => false) n
⊢ evalFin t₁ (fun i => seq (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n =
    evalFin t₂ (fun i => seq (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n
Tactic:
simp at this
State after:
case mp
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
h : ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1
seq : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool
n : ℕ
this :
  evalFin t₁ (fun i => seq { val := ↑i, isLt := (_ : ↑i < arity (Term.xor t₁ t₂)) }) n =
    evalFin t₂ (fun i => seq { val := ↑i, isLt := (_ : ↑i < arity (Term.xor t₁ t₂)) }) n
⊢ evalFin t₁ (fun i => seq (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n =
    evalFin t₂ (fun i => seq (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n

State before:
case mp
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
h : ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1
seq : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool
n : ℕ
this :
  evalFin t₁ (fun i => seq { val := ↑i, isLt := (_ : ↑i < arity (Term.xor t₁ t₂)) }) n =
    evalFin t₂ (fun i => seq { val := ↑i, isLt := (_ : ↑i < arity (Term.xor t₁ t₂)) }) n
⊢ evalFin t₁ (fun i => seq (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n =
    evalFin t₂ (fun i => seq (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) n
Tactic:
convert this
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 α'
t₁ t₂ : Term
⊢ (∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
      evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
        evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i) →
    ∀ (a : ℕ → ℕ → Bool) (a_1 : ℕ), evalFin t₁ (fun i => a ↑i) a_1 = evalFin t₂ (fun i => a ↑i) a_1
Tactic:
intro h seq m
State after:
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
h :
  ∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
    evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
      evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i
seq : ℕ → ℕ → Bool
m : ℕ
⊢ evalFin t₁ (fun i => seq ↑i) m = evalFin t₂ (fun i => seq ↑i) m

State before:
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
t₁ t₂ : Term
h :
  ∀ (a : Fin (arity (Term.xor t₁ t₂)) → ℕ → Bool) (i : ℕ),
    evalFin t₁ (fun i => a (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i =
      evalFin t₂ (fun i => a (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)) i
seq : ℕ → ℕ → Bool
m : ℕ
⊢ evalFin t₁ (fun i => seq ↑i) m = evalFin t₂ (fun i => seq ↑i) m
Tactic:
exact h (λ j => seq j) _
State after:
no goals