Theorem: exists_repeat
Proof state before:
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)
Tactic:
{ have _h : ↑b + (n - 2 ^ card α) = (a + (n - 2 ^ card α)) + (b - a) := by
  { zify
    rw [Nat.cast_sub, Nat.cast_sub]
    ring_nf
    exact le_of_lt h₂
    exact le_of_not_lt hn2 }
  rw [← h₁]
  apply propagateCarry2_eq_of_seq_eq_lt
  simp (config := { contextual := true }) }
Proof state after:
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)