Theorem: cycleMin_cmtr_right_apply_eq_apply_cycleMin_cmtr (Controlbits/CommutatorCycles.lean)

State before:
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
⊢ CycleMin ⁅x, y⁆ (y q) = y (CycleMin ⁅x, y⁆ q)
Tactic:
rcases cycleMin_exists_pow_apply ⁅x, y⁆ q with ⟨j, hjq₂⟩
State after:
case intro
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
⊢ CycleMin ⁅x, y⁆ (y q) = y (CycleMin ⁅x, y⁆ q)

State before:
case intro
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
⊢ CycleMin ⁅x, y⁆ (y q) = y (CycleMin ⁅x, y⁆ q)
Tactic:
refine' eq_of_le_of_not_lt _ (fun h => _)
State after:
case intro.refine'_1
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
⊢ CycleMin ⁅x, y⁆ (y q) ≤ y (CycleMin ⁅x, y⁆ q)

case intro.refine'_2
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
h : CycleMin ⁅x, y⁆ (y q) < y (CycleMin ⁅x, y⁆ q)
⊢ False

State before:
case intro.refine'_1
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
⊢ CycleMin ⁅x, y⁆ (y q) ≤ y (CycleMin ⁅x, y⁆ q)
Tactic:
refine' cycleMin_le ⁅x, y⁆ (y q)  ⟨-j, _⟩
State after:
case intro.refine'_1
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
⊢ (⁅x, y⁆ ^ (-j)) (y q) = y (CycleMin ⁅x, y⁆ q)

State before:
case intro.refine'_1
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
⊢ (⁅x, y⁆ ^ (-j)) (y q) = y (CycleMin ⁅x, y⁆ q)
Tactic:
simp_rw [zpow_neg, ← Perm.mul_apply, cmtr_zpow_inv_mul_eq_mul_inv_cmtr_zpow, hxy,
  Perm.mul_apply, hjq₂]
State after:
no goals

State before:
case intro.refine'_2
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
h : CycleMin ⁅x, y⁆ (y q) < y (CycleMin ⁅x, y⁆ q)
⊢ False
Tactic:
rcases cycleMin_exists_pow_apply ⁅x, y⁆  (y q) with ⟨k, hkq₂⟩
State after:
case intro.refine'_2.intro
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
h : CycleMin ⁅x, y⁆ (y q) < y (CycleMin ⁅x, y⁆ q)
k : ℤ
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
⊢ False

State before:
case intro.refine'_2.intro
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
h : CycleMin ⁅x, y⁆ (y q) < y (CycleMin ⁅x, y⁆ q)
k : ℤ
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
⊢ False
Tactic:
rw [←hkq₂, ← hjq₂, ← Perm.mul_apply, cmtr_zpow_mul_eq_mul_inv_cmtr_zpow_inv, Perm.mul_apply,
  hxy, ← zpow_neg] at h
State after:
case intro.refine'_2.intro
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
k : ℤ
h : y ((⁅x, y⁆ ^ (-k)) q) < y ((⁅x, y⁆ ^ j) q)
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
⊢ False

State before:
case intro.refine'_2.intro
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
k : ℤ
h : y ((⁅x, y⁆ ^ (-k)) q) < y ((⁅x, y⁆ ^ j) q)
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
⊢ False
Tactic:
rcases lt_trichotomy ((⁅x, y⁆ ^ (-k)) q) ((⁅x, y⁆ ^ j) q) with H | H | H
State after:
case intro.refine'_2.intro.inl
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
k : ℤ
h : y ((⁅x, y⁆ ^ (-k)) q) < y ((⁅x, y⁆ ^ j) q)
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
H : (⁅x, y⁆ ^ (-k)) q < (⁅x, y⁆ ^ j) q
⊢ False

case intro.refine'_2.intro.inr.inl
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
k : ℤ
h : y ((⁅x, y⁆ ^ (-k)) q) < y ((⁅x, y⁆ ^ j) q)
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
H : (⁅x, y⁆ ^ (-k)) q = (⁅x, y⁆ ^ j) q
⊢ False

case intro.refine'_2.intro.inr.inr
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
k : ℤ
h : y ((⁅x, y⁆ ^ (-k)) q) < y ((⁅x, y⁆ ^ j) q)
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
H : (⁅x, y⁆ ^ j) q < (⁅x, y⁆ ^ (-k)) q
⊢ False

State before:
case intro.refine'_2.intro.inl
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
k : ℤ
h : y ((⁅x, y⁆ ^ (-k)) q) < y ((⁅x, y⁆ ^ j) q)
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
H : (⁅x, y⁆ ^ (-k)) q < (⁅x, y⁆ ^ j) q
⊢ False
Tactic:
exact (cycleMin_le ⁅x, y⁆ q ⟨-k, rfl⟩).not_lt (hjq₂.symm ▸ H)
State after:
no goals

State before:
case intro.refine'_2.intro.inr.inl
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
k : ℤ
h : y ((⁅x, y⁆ ^ (-k)) q) < y ((⁅x, y⁆ ^ j) q)
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
H : (⁅x, y⁆ ^ (-k)) q = (⁅x, y⁆ ^ j) q
⊢ False
Tactic:
exact False.elim (lt_irrefl _ (H ▸ h))
State after:
no goals

State before:
case intro.refine'_2.intro.inr.inr
α : Type u
inst✝² : Fintype α
inst✝¹ : DecidableEq α
x y : Perm α
q : α
inst✝ : LinearOrder α
hxy : ⁅x, y⁻¹⁆ = ⁅x, y⁆
hy : ∀ (q : α), y q ≠ q
hy₂ : ∀ {r q : α}, r < q → y q < y r → r = y q
j : ℤ
hjq₂ : (⁅x, y⁆ ^ j) q = CycleMin ⁅x, y⁆ q
k : ℤ
h : y ((⁅x, y⁆ ^ (-k)) q) < y ((⁅x, y⁆ ^ j) q)
hkq₂ : (⁅x, y⁆ ^ k) (y q) = CycleMin ⁅x, y⁆ (y q)
H : (⁅x, y⁆ ^ j) q < (⁅x, y⁆ ^ (-k)) q
⊢ False
Tactic:
exact cmtr_zpow_apply_ne_apply_cmtr_pow_apply hxy hy (hy₂ H h)
State after:
no goals