internlm/Lean-Github huggingface dataset:
Theorem: propagate_eq_zero_iff
Proof 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
Proof 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
Theorem: propagate_eq_zero_iff
Proof 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] }
Proof 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
Theorem: propagate_eq_zero_iff
Proof 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] }
Proof state after:
no goals
Theorem: propagate_eq_zero_iff
Proof 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 _
Proof 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
Theorem: propagate_eq_zero_iff
Proof 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]
Proof state after:
no goals
Theorem: propagate_eq_zero_iff
Proof 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
Proof 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
Theorem: propagate_eq_zero_iff
Proof 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
Proof 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
Theorem: propagate_eq_zero_iff
Proof 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⟩
Proof 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
Theorem: propagate_eq_zero_iff
Proof 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]
Proof state after:
no goals
Theorem: eq_iff_xorSeq_eq_zero
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
⊢ (∀ (i : ℕ), seq₁ i = seq₂ i) ↔ ∀ (i : ℕ), xorSeq seq₁ seq₂ i = zeroSeq i
Tactic:
simp [Function.funext_iff, xorSeq, zeroSeq]
Proof state after:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : ℕ → Bool
⊢ (∀ (i : ℕ), seq₁ i = seq₂ i) ↔ ∀ (i : ℕ), _root_.xor (seq₁ i) (seq₂ i) = false
Theorem: eq_iff_xorSeq_eq_zero
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
⊢ (∀ (i : ℕ), seq₁ i = seq₂ i) ↔ ∀ (i : ℕ), _root_.xor (seq₁ i) (seq₂ i) = false
Tactic:
constructor
Proof state after:
case mp
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : ℕ → Bool
⊢ (∀ (i : ℕ), seq₁ i = seq₂ i) → ∀ (i : ℕ), _root_.xor (seq₁ i) (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 α'
seq₁ seq₂ : ℕ → Bool
⊢ (∀ (i : ℕ), _root_.xor (seq₁ i) (seq₂ i) = false) → ∀ (i : ℕ), seq₁ i = seq₂ i
Theorem: eq_iff_xorSeq_eq_zero
Proof state before:
case mp
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : ℕ → Bool
⊢ (∀ (i : ℕ), seq₁ i = seq₂ i) → ∀ (i : ℕ), _root_.xor (seq₁ i) (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 α'
seq₁ seq₂ : ℕ → Bool
⊢ (∀ (i : ℕ), _root_.xor (seq₁ i) (seq₂ i) = false) → ∀ (i : ℕ), seq₁ i = seq₂ i
Tactic:
{ intro i _; simp [*] }
Proof state after:
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : ℕ → Bool
⊢ (∀ (i : ℕ), _root_.xor (seq₁ i) (seq₂ i) = false) → ∀ (i : ℕ), seq₁ i = seq₂ i
Theorem: eq_iff_xorSeq_eq_zero
Proof state before:
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : ℕ → Bool
⊢ (∀ (i : ℕ), _root_.xor (seq₁ i) (seq₂ i) = false) → ∀ (i : ℕ), seq₁ i = seq₂ i
Tactic:
{ intro h a
  specialize h a
  revert h
  cases (seq₁ a) <;> cases (seq₂ a) <;> simp [*] at * }
Proof state after:
no goals
Theorem: eq_iff_xorSeq_eq_zero
Proof state before:
case mp
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : ℕ → Bool
⊢ (∀ (i : ℕ), seq₁ i = seq₂ i) → ∀ (i : ℕ), _root_.xor (seq₁ i) (seq₂ i) = false
Tactic:
intro i _
Proof state after:
case mp
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : ℕ → Bool
i : ∀ (i : ℕ), seq₁ i = seq₂ i
i✝ : ℕ
⊢ _root_.xor (seq₁ i✝) (seq₂ i✝) = false
Theorem: eq_iff_xorSeq_eq_zero
Proof state before:
case mp
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : ℕ → Bool
i : ∀ (i : ℕ), seq₁ i = seq₂ i
i✝ : ℕ
⊢ _root_.xor (seq₁ i✝) (seq₂ i✝) = false
Tactic:
simp [*]
Proof state after:
no goals
Theorem: eq_iff_xorSeq_eq_zero
Proof state before:
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : ℕ → Bool
⊢ (∀ (i : ℕ), _root_.xor (seq₁ i) (seq₂ i) = false) → ∀ (i : ℕ), seq₁ i = seq₂ i
Tactic:
intro h a
Proof state after:
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : ℕ → Bool
h : ∀ (i : ℕ), _root_.xor (seq₁ i) (seq₂ i) = false
a : ℕ
⊢ seq₁ a = seq₂ a
Theorem: eq_iff_xorSeq_eq_zero
Proof state before:
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : ℕ → Bool
h : ∀ (i : ℕ), _root_.xor (seq₁ i) (seq₂ i) = false
a : ℕ
⊢ seq₁ a = seq₂ a
Tactic:
specialize h a
Proof state after:
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : ℕ → Bool
a : ℕ
h : _root_.xor (seq₁ a) (seq₂ a) = false
⊢ seq₁ a = seq₂ a
Theorem: eq_iff_xorSeq_eq_zero
Proof state before:
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : ℕ → Bool
a : ℕ
h : _root_.xor (seq₁ a) (seq₂ a) = false
⊢ seq₁ a = seq₂ a
Tactic:
revert h
Proof state after:
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : ℕ → Bool
a : ℕ
⊢ _root_.xor (seq₁ a) (seq₂ a) = false → seq₁ a = seq₂ a
Theorem: eq_iff_xorSeq_eq_zero
Proof state before:
case mpr
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq₁ seq₂ : ℕ → Bool
a : ℕ
⊢ _root_.xor (seq₁ a) (seq₂ a) = false → seq₁ a = seq₂ a
Tactic:
cases (seq₁ a) <;> cases (seq₂ a) <;> simp [*] at *
Proof state after:
no goals
Theorem: eval_eq_iff_xorSeq_eq_zero
Proof 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]
Proof 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
Theorem: eval_eq_iff_xorSeq_eq_zero
Proof 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
Proof 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
Theorem: eval_eq_iff_xorSeq_eq_zero
Proof 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 }
Proof 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
Theorem: eval_eq_iff_xorSeq_eq_zero
Proof 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) _ }
Proof state after:
no goals
Theorem: eval_eq_iff_xorSeq_eq_zero
Proof 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
Proof 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
Theorem: eval_eq_iff_xorSeq_eq_zero
Proof 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
Proof 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