Theorem: exists_repeat_carry (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 : β → ℕ → Bool
⊢ ∃ n m, propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m ∧ n < m
Tactic:
by_contra h
State after:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
h : ¬∃ n m, propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m ∧ n < m
⊢ False

State before:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
h : ¬∃ n m, propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m ∧ n < m
⊢ False
Tactic:
haveI := Classical.decEq α
State after:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
h : ¬∃ n m, propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m ∧ n < m
this : DecidableEq α
⊢ False

State before:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
h : ¬∃ n m, propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m ∧ n < m
this : DecidableEq α
⊢ False
Tactic:
push_neg at h
State after:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
this : DecidableEq α
h :
  ∀ (n m : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m → m ≤ n
⊢ False

State before:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
this : DecidableEq α
h :
  ∀ (n m : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m → m ≤ n
⊢ False
Tactic:
have := λ a b hab => (le_antisymm (h a b hab) (h b a hab.symm)).symm
State after:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
this✝ : DecidableEq α
h :
  ∀ (n m : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m → m ≤ n
this :
  ∀ (a b : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑a = propagateCarry2 init_carry next_carry seq ↑b → a = b
⊢ False

State before:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
this✝ : DecidableEq α
h :
  ∀ (n m : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m → m ≤ n
this :
  ∀ (a b : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑a = propagateCarry2 init_carry next_carry seq ↑b → a = b
⊢ False
Tactic:
have := Fintype.card_le_of_injective _ this
State after:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
this✝¹ : DecidableEq α
h :
  ∀ (n m : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m → m ≤ n
this✝ :
  ∀ (a b : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑a = propagateCarry2 init_carry next_carry seq ↑b → a = b
this : card (Fin (2 ^ card α + 1)) ≤ card (α → Bool)
⊢ False

State before:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
this✝¹ : DecidableEq α
h :
  ∀ (n m : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑n = propagateCarry2 init_carry next_carry seq ↑m → m ≤ n
this✝ :
  ∀ (a b : Fin (2 ^ card α + 1)),
    propagateCarry2 init_carry next_carry seq ↑a = propagateCarry2 init_carry next_carry seq ↑b → a = b
this : card (Fin (2 ^ card α + 1)) ≤ card (α → Bool)
⊢ False
Tactic:
simp at this
State after:
no goals