Theorem: cycleAt_cmtr_disjoint_image (Controlbits/CommutatorCycles.lean)

State before:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ Disjoint (CycleAt ⁅x, y⁆ q) (Finset.image (⇑y) (CycleAt ⁅x, y⁆ q))
Tactic:
simp_rw [Finset.disjoint_iff_ne, Finset.mem_image, mem_cycleAt_iff]
State after:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (a : α), ⁅x, y⁆.SameCycle q a → ∀ (b : α), (∃ a, ⁅x, y⁆.SameCycle q a ∧ y a = b) → a ≠ b

State before:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (a : α), ⁅x, y⁆.SameCycle q a → ∀ (b : α), (∃ a, ⁅x, y⁆.SameCycle q a ∧ y a = b) → a ≠ b
Tactic:
rintro _ ⟨j, rfl⟩ _ ⟨_, ⟨⟨_, rfl⟩, rfl⟩⟩
State after:
case intro.intro.intro.intro
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
j w✝ : ℤ
⊢ (⁅x, y⁆ ^ j) q ≠ y ((⁅x, y⁆ ^ w✝) q)

State before:
case intro.intro.intro.intro
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
j w✝ : ℤ
⊢ (⁅x, y⁆ ^ j) q ≠ y ((⁅x, y⁆ ^ w✝) q)
Tactic:
exact cmtr_zpow_apply_ne_apply_cmtr_pow_apply hxy hy
State after:
no goals