Theorem: mul_cmtr_pow_unfix (Controlbits/Commutator.lean)

State before:
α : Type u
x y : Perm α
q : α
k : ℕ
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (y * ⁅x, y⁆ ^ k) 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 : α), (y * ⁅x, y⁆ ^ 0) q ≠ q

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

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

State before:
case H1
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (y * ⁅x, y⁆ ^ 0) q ≠ q
Tactic:
rw [pow_zero, mul_one]
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 : α), (y * ⁅x, y⁆ ^ 1) 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 : α), (y * ⁅x, y⁆) q ≠ q

State before:
case H2
α : Type u
x y : Perm α
q : α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
⊢ ∀ (q : α), (y * ⁅x, y⁆) q ≠ q
Tactic:
exact mul_cmtr_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 : α), (y * ⁅x, y⁆ ^ k) q ≠ q
_IH2✝ : ∀ (q : α), (y * ⁅x, y⁆ ^ k.succ) q ≠ q
⊢ ∀ (q : α), (y * ⁅x, y⁆ ^ k.succ.succ) 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 : α), (y * ⁅x, y⁆ ^ k) q ≠ q
_IH2✝ : ∀ (q : α), (y * ⁅x, y⁆ ^ k.succ) q ≠ q
q : α
h : (y * ⁅x, y⁆ ^ k.succ.succ) 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 : α), (y * ⁅x, y⁆ ^ k) q ≠ q
_IH2✝ : ∀ (q : α), (y * ⁅x, y⁆ ^ k.succ) q ≠ q
q : α
h : (y * ⁅x, y⁆ ^ k.succ.succ) q = q
⊢ False
Tactic:
simp_rw [pow_succ (n := k.succ), pow_succ' (n := k), ← mul_assoc, ← hxy,
  ← cmtr_inv_mul_eq_mul_inv_cmtr, hxy, mul_assoc,
  Perm.mul_apply, Perm.inv_eq_iff_eq] 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 : α), (y * ⁅x, y⁆ ^ k) q ≠ q
_IH2✝ : ∀ (q : α), (y * ⁅x, y⁆ ^ k.succ) q ≠ q
q : α
h : y ((⁅x, y⁆ ^ k) (⁅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 : α), (y * ⁅x, y⁆ ^ k) q ≠ q
_IH2✝ : ∀ (q : α), (y * ⁅x, y⁆ ^ k.succ) q ≠ q
q : α
h : y ((⁅x, y⁆ ^ k) (⁅x, y⁆ q)) = ⁅x, y⁆ q
⊢ False
Tactic:
exact IH (⁅x, y⁆ q) h
State after:
no goals