Theorem: cycleAt_cmtr_card_le_card_univ_div_two (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
⊢ orderOf (⁅x, y⁆.cycleOf q) ≤ Finset.univ.card / 2
Tactic:
rw [cycleAt_card_eq_orderOf_cycleOf, Nat.le_div_iff_mul_le (zero_lt_two), mul_comm, two_mul]
State after:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (CycleAt ⁅x, y⁆ q).card + (CycleAt ⁅x, y⁆ q).card ≤ Finset.univ.card

State before:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (CycleAt ⁅x, y⁆ q).card + (CycleAt ⁅x, y⁆ q).card ≤ Finset.univ.card
Tactic:
nth_rewrite 2 [← Finset.card_image_of_injective _ (y.injective)]
State after:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (CycleAt ⁅x, y⁆ q).card + (Finset.image (⇑y) (CycleAt ⁅x, y⁆ q)).card ≤ Finset.univ.card

State before:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (CycleAt ⁅x, y⁆ q).card + (Finset.image (⇑y) (CycleAt ⁅x, y⁆ q)).card ≤ Finset.univ.card
Tactic:
rw [← Finset.card_union_of_disjoint (cycleAt_cmtr_disjoint_image hxy hy)]
State after:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (CycleAt ⁅x, y⁆ q ∪ Finset.image (⇑y) (CycleAt ⁅x, y⁆ q)).card ≤ Finset.univ.card

State before:
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ (CycleAt ⁅x, y⁆ q ∪ Finset.image (⇑y) (CycleAt ⁅x, y⁆ q)).card ≤ Finset.univ.card
Tactic:
exact Finset.card_le_card (Finset.subset_univ _)
State after:
no goals