Theorem: cmtr_pow_mul_unfix (Controlbits/Commutator.lean)

State before:
α : Type u
x y : Perm α
q : α
k : ℕ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ ^ k * y) q ≠ q
Tactic:
induction' k using Nat.twoStepInduction with k IH
State after:
case H1
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ ^ 0 * y) q ≠ q

case H2
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ ^ 1 * y) q ≠ q

case H3
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (⁅x, y⁆ ^ k * y) q ≠ q
_IH2✝ : ∀ (q : α), (⁅x, y⁆ ^ k.succ * y) q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ ^ k.succ.succ * y) q ≠ q

State before:
case H1
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ ^ 0 * y) q ≠ q
Tactic:
rw [pow_zero, one_mul]
State after:
case H1
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), y q ≠ q

State before:
case H1
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), y q ≠ q
Tactic:
exact hy
State after:
no goals

State before:
case H2
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ ^ 1 * y) q ≠ q
Tactic:
rw [pow_one]
State after:
case H2
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ * y) q ≠ q

State before:
case H2
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ * y) q ≠ q
Tactic:
exact cmtr_mul_unfix_of_unfix hy
State after:
no goals

State before:
case H3
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (⁅x, y⁆ ^ k * y) q ≠ q
_IH2✝ : ∀ (q : α), (⁅x, y⁆ ^ k.succ * y) q ≠ q
⊢ ∀ (q : α), (⁅x, y⁆ ^ k.succ.succ * y) q ≠ q
Tactic:
intros q h
State after:
case H3
α : Type u
x y : Perm α
q✝ : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (⁅x, y⁆ ^ k * y) q ≠ q
_IH2✝ : ∀ (q : α), (⁅x, y⁆ ^ k.succ * y) q ≠ q
q : α
h : (⁅x, y⁆ ^ k.succ.succ * y) q = q
⊢ False

State before:
case H3
α : Type u
x y : Perm α
q✝ : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (⁅x, y⁆ ^ k * y) q ≠ q
_IH2✝ : ∀ (q : α), (⁅x, y⁆ ^ k.succ * y) q ≠ q
q : α
h : (⁅x, y⁆ ^ k.succ.succ * y) q = q
⊢ False
Tactic:
simp_rw [pow_succ (n := k.succ), pow_succ' (n := k), mul_assoc,
  cmtr_mul_eq_mul_inv_cmtr_inv, hxy, Perm.mul_apply,
  ← Perm.eq_inv_iff_eq (f := ⁅x, y⁆)] at h
State after:
case H3
α : Type u
x y : Perm α
q✝ : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (⁅x, y⁆ ^ k * y) q ≠ q
_IH2✝ : ∀ (q : α), (⁅x, y⁆ ^ k.succ * y) q ≠ q
q : α
h : (⁅x, y⁆ ^ k) (y (⁅x, y⁆⁻¹ q)) = ⁅x, y⁆⁻¹ q
⊢ False

State before:
case H3
α : Type u
x y : Perm α
q✝ : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
k : ℕ
IH : ∀ (q : α), (⁅x, y⁆ ^ k * y) q ≠ q
_IH2✝ : ∀ (q : α), (⁅x, y⁆ ^ k.succ * y) q ≠ q
q : α
h : (⁅x, y⁆ ^ k) (y (⁅x, y⁆⁻¹ q)) = ⁅x, y⁆⁻¹ q
⊢ False
Tactic:
exact IH (⁅x, y⁆⁻¹ q) h
State after:
no goals