Theorem: Equiv.Perm.pow_apply_injOn_Iio_orderOf_cycleOf (Controlbits/Cycles.lean)

State before:
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
⊢ Set.InjOn (fun t => (π ^ t) x) (Set.Iio (orderOf (π.cycleOf x)))
Tactic:
rintro a ha b hb hab
State after:
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
⊢ a = b

State before:
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
⊢ a = b
Tactic:
refine' pow_injOn_Iio_orderOf ha hb (ext (fun y => _))
State after:
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
⊢ ((fun x_1 => π.cycleOf x ^ x_1) a) y = ((fun x_1 => π.cycleOf x ^ x_1) b) y

State before:
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
⊢ ((fun x_1 => π.cycleOf x ^ x_1) a) y = ((fun x_1 => π.cycleOf x ^ x_1) b) y
Tactic:
simp_rw [cycleOf_pow_apply]
State after:
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
⊢ (if π.SameCycle x y then (π ^ a) y else y) = if π.SameCycle x y then (π ^ b) y else y

State before:
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
⊢ (if π.SameCycle x y then (π ^ a) y else y) = if π.SameCycle x y then (π ^ b) y else y
Tactic:
by_cases h : SameCycle π x y
State after:
case pos
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
h : π.SameCycle x y
⊢ (if π.SameCycle x y then (π ^ a) y else y) = if π.SameCycle x y then (π ^ b) y else y

case neg
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
h : ¬π.SameCycle x y
⊢ (if π.SameCycle x y then (π ^ a) y else y) = if π.SameCycle x y then (π ^ b) y else y

State before:
case pos
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
h : π.SameCycle x y
⊢ (if π.SameCycle x y then (π ^ a) y else y) = if π.SameCycle x y then (π ^ b) y else y
Tactic:
simp_rw [h, ite_true]
State after:
case pos
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
h : π.SameCycle x y
⊢ (π ^ a) y = (π ^ b) y

State before:
case pos
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
h : π.SameCycle x y
⊢ (π ^ a) y = (π ^ b) y
Tactic:
rcases h with ⟨c, rfl⟩
State after:
case pos.intro
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
c : ℤ
⊢ (π ^ a) ((π ^ c) x) = (π ^ b) ((π ^ c) x)

State before:
case pos.intro
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
c : ℤ
⊢ (π ^ a) ((π ^ c) x) = (π ^ b) ((π ^ c) x)
Tactic:
simp_rw [← zpow_natCast, zpow_apply_comm, zpow_natCast, hab]
State after:
no goals

State before:
case neg
α : Type u_1
π✝ : Perm α
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
π : Perm α
x : α
a : ℕ
ha : a ∈ Set.Iio (orderOf (π.cycleOf x))
b : ℕ
hb : b ∈ Set.Iio (orderOf (π.cycleOf x))
hab : (fun t => (π ^ t) x) a = (fun t => (π ^ t) x) b
y : α
h : ¬π.SameCycle x y
⊢ (if π.SameCycle x y then (π ^ a) y else y) = if π.SameCycle x y then (π ^ b) y else y
Tactic:
simp_rw [h, ite_false]
State after:
no goals