Theorem: 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 α'
seq₁ seq₂ : ℕ → Bool
⊢ (∀ (i : ℕ), seq₁ i = seq₂ i) ↔ ∀ (i : ℕ), xorSeq seq₁ seq₂ i = zeroSeq i
Tactic:
simp [Function.funext_iff, xorSeq, zeroSeq]
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

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

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 [*] }
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

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 * }
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 α'
seq₁ seq₂ : ℕ → Bool
⊢ (∀ (i : ℕ), seq₁ i = seq₂ i) → ∀ (i : ℕ), _root_.xor (seq₁ i) (seq₂ i) = false
Tactic:
intro 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 α'
seq₁ seq₂ : ℕ → Bool
i : ∀ (i : ℕ), seq₁ i = seq₂ i
i✝ : ℕ
⊢ _root_.xor (seq₁ i✝) (seq₂ 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 α'
seq₁ seq₂ : ℕ → Bool
i : ∀ (i : ℕ), seq₁ i = seq₂ i
i✝ : ℕ
⊢ _root_.xor (seq₁ i✝) (seq₂ i✝) = false
Tactic:
simp [*]
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 α'
seq₁ seq₂ : ℕ → Bool
⊢ (∀ (i : ℕ), _root_.xor (seq₁ i) (seq₂ i) = false) → ∀ (i : ℕ), seq₁ i = seq₂ i
Tactic:
intro h a
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

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

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

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