Theorem: fastCycleMin_eq_min_cycleAtTo (Controlbits/Cycles.lean)

State before:
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
x : α
⊢ FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
Tactic:
induction' i with i hi generalizing x
State after:
case zero
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x : α
⊢ FastCycleMin 0 π x = (CycleAtTo π (2 ^ 0) x).min' ⋯

case succ
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
⊢ FastCycleMin (i + 1) π x = (CycleAtTo π (2 ^ (i + 1)) x).min' ⋯

State before:
case zero
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
x : α
⊢ FastCycleMin 0 π x = (CycleAtTo π (2 ^ 0) x).min' ⋯
Tactic:
simp_rw [fastCycleMin_zero_eq, pow_zero, cycleAtTo_one, min'_singleton]
State after:
no goals

State before:
case succ
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
⊢ FastCycleMin (i + 1) π x = (CycleAtTo π (2 ^ (i + 1)) x).min' ⋯
Tactic:
simp_rw [fastCycleMin_succ_eq, hi, le_antisymm_iff, le_min_iff, Finset.le_min'_iff, min_le_iff,
  mem_cycleAtTo_iff, Nat.pow_succ', Nat.two_mul, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂, ← forall_and, ← Equiv.Perm.mul_apply, ← pow_add, imp_and]
State after:
case succ
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
⊢ ∀ (x_1 : ℕ),
    (x_1 < 2 ^ i + 2 ^ i →
        (CycleAtTo π (2 ^ i) x).min' ⋯ ≤ (π ^ x_1) x ∨ (CycleAtTo π (2 ^ i) ((π ^ 2 ^ i) x)).min' ⋯ ≤ (π ^ x_1) x) ∧
      (x_1 < 2 ^ i → (CycleAtTo π (2 ^ i + 2 ^ i) x).min' ⋯ ≤ (π ^ x_1) x) ∧
        (x_1 < 2 ^ i → (CycleAtTo π (2 ^ i + 2 ^ i) x).min' ⋯ ≤ (π ^ (x_1 + 2 ^ i)) x)

State before:
case succ
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
⊢ ∀ (x_1 : ℕ),
    (x_1 < 2 ^ i + 2 ^ i →
        (CycleAtTo π (2 ^ i) x).min' ⋯ ≤ (π ^ x_1) x ∨ (CycleAtTo π (2 ^ i) ((π ^ 2 ^ i) x)).min' ⋯ ≤ (π ^ x_1) x) ∧
      (x_1 < 2 ^ i → (CycleAtTo π (2 ^ i + 2 ^ i) x).min' ⋯ ≤ (π ^ x_1) x) ∧
        (x_1 < 2 ^ i → (CycleAtTo π (2 ^ i + 2 ^ i) x).min' ⋯ ≤ (π ^ (x_1 + 2 ^ i)) x)
Tactic:
refine' fun b => And.intro (fun h => (lt_or_le b (2^i)).imp _ _) (And.intro _ _) <;>
refine' fun hb => min'_le _ _ _
State after:
case succ.refine'_1
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
b : ℕ
h : b < 2 ^ i + 2 ^ i
hb : b < 2 ^ i
⊢ (π ^ b) x ∈ CycleAtTo π (2 ^ i) x

case succ.refine'_2
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
b : ℕ
h : b < 2 ^ i + 2 ^ i
hb : 2 ^ i ≤ b
⊢ (π ^ b) x ∈ CycleAtTo π (2 ^ i) ((π ^ 2 ^ i) x)

case succ.refine'_3
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
b : ℕ
hb : b < 2 ^ i
⊢ (π ^ b) x ∈ CycleAtTo π (2 ^ i + 2 ^ i) x

case succ.refine'_4
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
b : ℕ
hb : b < 2 ^ i
⊢ (π ^ (b + 2 ^ i)) x ∈ CycleAtTo π (2 ^ i + 2 ^ i) x

State before:
case succ.refine'_1
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
b : ℕ
h : b < 2 ^ i + 2 ^ i
hb : b < 2 ^ i
⊢ (π ^ b) x ∈ CycleAtTo π (2 ^ i) x
Tactic:
exact apply_pow_mem_cycleAtTo_of_lt hb
State after:
no goals

State before:
case succ.refine'_2
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
b : ℕ
h : b < 2 ^ i + 2 ^ i
hb : 2 ^ i ≤ b
⊢ (π ^ b) x ∈ CycleAtTo π (2 ^ i) ((π ^ 2 ^ i) x)
Tactic:
exact apply_pow_mem_cycleAtTo_apply_pow_of_ge_of_lt h hb
State after:
no goals

State before:
case succ.refine'_3
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
b : ℕ
hb : b < 2 ^ i
⊢ (π ^ b) x ∈ CycleAtTo π (2 ^ i + 2 ^ i) x
Tactic:
exact apply_pow_mem_cycleAtTo_of_lt (lt_of_lt_of_le hb le_self_add)
State after:
no goals

State before:
case succ.refine'_4
α : Type u
inst✝² : DecidableEq α
π : Perm α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
i : ℕ
hi : ∀ {x : α}, FastCycleMin i π x = (CycleAtTo π (2 ^ i) x).min' ⋯
x : α
b : ℕ
hb : b < 2 ^ i
⊢ (π ^ (b + 2 ^ i)) x ∈ CycleAtTo π (2 ^ i + 2 ^ i) x
Tactic:
exact apply_pow_mem_cycleAtTo_of_lt ((add_lt_add_iff_right _).mpr hb)
State after:
no goals