Theorem: exists_repeat
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.refine'_2.e_a
α β α' β' : 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 : ℕ
c : β
_hc : y ≤ 2 ^ card α - ↑b
⊢ ↑↑a + (↑n - ↑(2 ^ card α)) + ↑y + (↑↑b - ↑↑a) = ↑↑b + (↑n - ↑(2 ^ card α)) + ↑y

case neg.intro.intro.intro.intro.intro.intro.refine'_2.e_a
α β α' β' : 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 : ℕ
c : β
_hc : y ≤ 2 ^ card α - ↑b
⊢ ↑a ≤ ↑b

case neg.intro.intro.intro.intro.intro.intro.refine'_2.e_a
α β α' β' : 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 : ℕ
c : β
_hc : y ≤ 2 ^ card α - ↑b
⊢ 2 ^ card α ≤ n
Tactic:
ring
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.refine'_2.e_a
α β α' β' : 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 : ℕ
c : β
_hc : y ≤ 2 ^ card α - ↑b
⊢ ↑a ≤ ↑b

case neg.intro.intro.intro.intro.intro.intro.refine'_2.e_a
α β α' β' : 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 : ℕ
c : β
_hc : y ≤ 2 ^ card α - ↑b
⊢ 2 ^ card α ≤ n