internlm/Lean-Github huggingface dataset:
Theorem: exists_repeat
Proof state before:
case neg
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Tactic:
rcases exists_repeat_carry
  (propagateCarry2 init_carry (λ c b => (next_bit c b).1) seq
    (n - 2 ^ card α))
  (λ carry bits => (next_bit  carry bits).1)
  (λ b i => seq b (i + (n - 2^ (card α)))) with ⟨a, b, h₁, h₂⟩
Proof state after:
case neg.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₁ :
  propagateCarry2 (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (n - 2 ^ card α))
      (fun carry bits => (next_bit carry bits).fst) (fun b i => seq b (i + (n - 2 ^ card α))) ↑a =
    propagateCarry2 (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (n - 2 ^ card α))
      (fun carry bits => (next_bit carry bits).fst) (fun b i => seq b (i + (n - 2 ^ card α))) ↑b
h₂ : a < b
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Theorem: exists_repeat
Proof state before:
case neg.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₁ :
  propagateCarry2 (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (n - 2 ^ card α))
      (fun carry bits => (next_bit carry bits).fst) (fun b i => seq b (i + (n - 2 ^ card α))) ↑a =
    propagateCarry2 (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (n - 2 ^ card α))
      (fun carry bits => (next_bit carry bits).fst) (fun b i => seq b (i + (n - 2 ^ card α))) ↑b
h₂ : a < b
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Tactic:
simp only [propagateCarry_propagateCarry_add] at h₁
Proof state after:
case neg.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Theorem: exists_repeat
Proof state before:
case neg.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Tactic:
rcases have _wf : n - (b - a) < n :=
   Nat.sub_lt (lt_of_lt_of_le (pow_pos (by norm_num) _) (le_of_not_lt hn2)) (Nat.sub_pos_of_lt h₂)
  exists_repeat (λ c i => if i < a + (n - 2 ^ card α) then seq c i else
    seq c (i + (b - a))) (n - (b - a)) with ⟨m, hmle, seq2, hm⟩
Proof state after:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
hm :
  propagate init_carry next_bit seq2 m =
    propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (n - (↑b - ↑a))
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Theorem: exists_repeat
Proof state before:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
hm :
  propagate init_carry next_bit seq2 m =
    propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (n - (↑b - ↑a))
⊢ ∃ m _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Tactic:
use m
Proof state after:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
hm :
  propagate init_carry next_bit seq2 m =
    propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (n - (↑b - ↑a))
⊢ ∃ _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Theorem: exists_repeat
Proof state before:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
hm :
  propagate init_carry next_bit seq2 m =
    propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (n - (↑b - ↑a))
⊢ ∃ _hm seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Tactic:
use hmle
Proof state after:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
hm :
  propagate init_carry next_bit seq2 m =
    propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (n - (↑b - ↑a))
⊢ ∃ seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Theorem: exists_repeat
Proof state before:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
hm :
  propagate init_carry next_bit seq2 m =
    propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (n - (↑b - ↑a))
⊢ ∃ seq2, propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Tactic:
use seq2
Proof state after:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
hm :
  propagate init_carry next_bit seq2 m =
    propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (n - (↑b - ↑a))
⊢ propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Theorem: exists_repeat
Proof state before:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
hm :
  propagate init_carry next_bit seq2 m =
    propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (n - (↑b - ↑a))
⊢ propagate init_carry next_bit seq2 m = propagate init_carry next_bit seq n
Tactic:
rw [hm]
Proof state after:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
hm :
  propagate init_carry next_bit seq2 m =
    propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (n - (↑b - ↑a))
⊢ propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (n - (↑b - ↑a)) =
    propagate init_carry next_bit seq n
Theorem: exists_repeat
Proof state before:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
hm :
  propagate init_carry next_bit seq2 m =
    propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (n - (↑b - ↑a))
⊢ propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (n - (↑b - ↑a)) =
    propagate init_carry next_bit seq n
Tactic:
clear hm
Proof state after:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
⊢ propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (n - (↑b - ↑a)) =
    propagate init_carry next_bit seq n
Theorem: exists_repeat
Proof state before:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
⊢ propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (n - (↑b - ↑a)) =
    propagate init_carry next_bit seq n
Tactic:
have h1 : n - (b - a) = (a + (n - 2 ^ (card α))) + (2 ^ card α - b) := by
{ zify
  rw [Nat.cast_sub, Nat.cast_sub, Nat.cast_sub, Nat.cast_sub]
  ring_nf
  exact Nat.le_of_lt_succ b.2
  simp [*] at *
  exact hn2
  exact le_of_lt h₂
  exact le_trans (Nat.sub_le _ _) (le_trans (Nat.le_of_lt_succ b.2)
    (le_of_not_lt hn2)) }
Proof state after:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
h1 : n - (↑b - ↑a) = ↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)
⊢ propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (n - (↑b - ↑a)) =
    propagate init_carry next_bit seq n
Theorem: exists_repeat
Proof state before:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
h1 : n - (↑b - ↑a) = ↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)
⊢ propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (n - (↑b - ↑a)) =
    propagate init_carry next_bit seq n
Tactic:
rw [h1]
Proof state after:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
h1 : n - (↑b - ↑a) = ↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)
⊢ propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)) =
    propagate init_carry next_bit seq n
Theorem: exists_repeat
Proof state before:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
h1 : n - (↑b - ↑a) = ↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)
⊢ propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)) =
    propagate init_carry next_bit seq n
Tactic:
have h2 : n = (b + (n - 2 ^ card α)) + (2 ^ card α - b) := by
{ zify
  rw [Nat.cast_sub, Nat.cast_sub]
  ring
  exact Nat.le_of_lt_succ b.2
  simp [*] at *
  exact hn2 }
Proof state after:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
h1 : n - (↑b - ↑a) = ↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)
h2 : n = ↑b + (n - 2 ^ card α) + (2 ^ card α - ↑b)
⊢ propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)) =
    propagate init_carry next_bit seq n
Theorem: exists_repeat
Proof state before:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
h1 : n - (↑b - ↑a) = ↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)
h2 : n = ↑b + (n - 2 ^ card α) + (2 ^ card α - ↑b)
⊢ propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)) =
    propagate init_carry next_bit seq n
Tactic:
conv_rhs => rw [h2]
Proof state after:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
h1 : n - (↑b - ↑a) = ↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)
h2 : n = ↑b + (n - 2 ^ card α) + (2 ^ card α - ↑b)
⊢ propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)) =
    propagate init_carry next_bit seq (↑b + (n - 2 ^ card α) + (2 ^ card α - ↑b))
Theorem: exists_repeat
Proof state before:
case neg.intro.intro.intro.intro.intro.intro
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
h1 : n - (↑b - ↑a) = ↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)
h2 : n = ↑b + (n - 2 ^ card α) + (2 ^ card α - ↑b)
⊢ propagate init_carry next_bit (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a)))
      (↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)) =
    propagate init_carry next_bit seq (↑b + (n - 2 ^ card α) + (2 ^ card α - ↑b))
Tactic:
refine' propagate_eq_of_carry_eq _ _ _ _ _ _ _ _ _
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.refine'_1
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
h1 : n - (↑b - ↑a) = ↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)
h2 : n = ↑b + (n - 2 ^ card α) + (2 ^ card α - ↑b)
⊢ propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst)
      (fun c i => if i < ↑a + (n - 2 ^ card α) then seq c i else seq c (i + (↑b - ↑a))) (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun carry bits => (next_bit carry bits).fst) seq (↑b + (n - 2 ^ card α))

case neg.intro.intro.intro.intro.intro.intro.refine'_2
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
seq : β → ℕ → Bool
n : ℕ
hn2 : ¬n < 2 ^ card α
a b : Fin (2 ^ card α + 1)
h₂ : a < b
h₁ :
  propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑a + (n - 2 ^ card α)) =
    propagateCarry2 init_carry (fun c b => (next_bit c b).fst) seq (↑b + (n - 2 ^ card α))
m : ℕ
hmle : m < 2 ^ card α
seq2 : β → ℕ → Bool
h1 : n - (↑b - ↑a) = ↑a + (n - 2 ^ card α) + (2 ^ card α - ↑b)
h2 : n = ↑b + (n - 2 ^ card α) + (2 ^ card α - ↑b)
⊢ ∀ (y : ℕ) (b_1 : β),
    y ≤ 2 ^ card α - ↑b →
      (if ↑a + (n - 2 ^ card α) + y < ↑a + (n - 2 ^ card α) then seq b_1 (↑a + (n - 2 ^ card α) + y)
        else seq b_1 (↑a + (n - 2 ^ card α) + y + (↑b - ↑a))) =
        seq b_1 (↑b + (n - 2 ^ card α) + y)