mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.map ((Finset.card ∘ support) ∘ fun l ↦ l.formPerm) p = m.toList

Tactic:
]

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.map ((Finset.card ∘ support) ∘ fun l ↦ l.formPerm) p = m.toList
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.map ((Finset.card ∘ support) ∘ fun l ↦ l.formPerm) p = List.map List.length p

Tactic:
]

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.map ((Finset.card ∘ support) ∘ fun l ↦ l.formPerm) p = List.map List.length p
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case pos.cons.refl.inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g✝ : G
w✝ : NormalWord d
h1✝ : w✝.head ∈ d.set { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ }
h2✝ :
  ∀ u' ∈ Option.map Prod.fst w✝.toList.head?,
    w✝.head ∈ toSubgroup A B { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } →
      { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } = u'
hcan : Cancels (-1) (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝)
a✝ :
  cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝ = w✝ →
    ReducedWord.prod φ
        (unitsSMulWithCancel φ (-1) (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝)
            hcan).toReducedWord =
      t ^ ↑(-1) *
        ReducedWord.prod φ
          (cons g✝ { val := -↑(-1), inv := -↑(-1)⁻¹, val_inv := ⋯, inv_val := ⋯ } w✝ h1✝ h2✝).toReducedWord
⊢ t⁻¹ * (of ↑⟨g✝, ⋯⟩ * (t * ReducedWord.prod φ w✝.toReducedWord)) =
    t⁻¹ * (of g✝ * (t * ReducedWord.prod φ w✝.toReducedWord))

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ x.toFinset.card = x.length

pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ ∀ (x_1 : α), x ≠ [x_1]

Tactic:
]

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ x.toFinset.card = x.length

case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ ∀ (x_1 : α), x ≠ [x_1]
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
x : List α
hx : x ∈ p
⊢ x.length = x.length

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg.inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels 1 w
⊢ of ↑(⋯.equiv w.head).1 *
      (of ((↑(⋯.equiv w.head).1)⁻¹ * w.head) * ((of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord)) =
    ReducedWord.prod φ w.toReducedWord

Tactic:
]

Goal state after:
case neg.inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels 1 w
⊢ of ↑(⋯.equiv w.head).1 *
      (of ((↑(⋯.equiv w.head).1)⁻¹ * w.head) * ((of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord)) =
    ReducedWord.prod φ w.toReducedWord
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg.inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels (-1) w
⊢ t⁻¹ * of ↑(⋯.equiv w.head).1 * t *
      (t⁻¹ * (of ((↑(⋯.equiv w.head).1)⁻¹ * w.head) * ((of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord))) =
    t⁻¹ * ReducedWord.prod φ w.toReducedWord

Tactic:
]

Goal state after:
case neg.inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels (-1) w
⊢ t⁻¹ * of ↑(⋯.equiv w.head).1 * t *
      (t⁻¹ * (of ((↑(⋯.equiv w.head).1)⁻¹ * w.head) * ((of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord))) =
    t⁻¹ * ReducedWord.prod φ w.toReducedWord
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.h2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.Pairwise (fun a b ↦ a.formPerm.Disjoint b.formPerm) p

Tactic:
]

Goal state after:
case h.h2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
⊢ List.Pairwise (fun a b ↦ a.formPerm.Disjoint b.formPerm) p
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
a b : List α
ha : a ∈ p
hb : b ∈ p
hab : a.Disjoint b
⊢ a.Disjoint b

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
a b : List α
ha : a ∈ p
hb : b ∈ p
hab : a.Disjoint b
⊢ a.Disjoint b
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case inv
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
x : HNNExtension G A B φ
ih : ∀ (w : NormalWord d), ReducedWord.prod φ (x • w).toReducedWord = x * ReducedWord.prod φ w.toReducedWord
w : NormalWord d
⊢ ReducedWord.prod φ (x • x⁻¹ • w).toReducedWord = x * (x⁻¹ * ReducedWord.prod φ w.toReducedWord)

Tactic:
]

Goal state after:
case inv
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
x : HNNExtension G A B φ
ih : ∀ (w : NormalWord d), ReducedWord.prod φ (x • w).toReducedWord = x * ReducedWord.prod φ w.toReducedWord
w : NormalWord d
⊢ ReducedWord.prod φ (x • x⁻¹ • w).toReducedWord = x * (x⁻¹ * ReducedWord.prod φ w.toReducedWord)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
k_mem : k ∈ centralizer {g}
c_mem : c ∈ g.cycleFactorsFinset
this : ↑g.cycleFactorsFinset = ConjAct.toConjAct k • ↑g.cycleFactorsFinset
⊢ ConjAct.toConjAct k • c ∈ ConjAct.toConjAct k • ↑g.cycleFactorsFinset

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
k_mem : k ∈ centralizer {g}
c_mem : c ∈ g.cycleFactorsFinset
this : ↑g.cycleFactorsFinset = ConjAct.toConjAct k • ↑g.cycleFactorsFinset
⊢ ConjAct.toConjAct k • c ∈ ConjAct.toConjAct k • ↑g.cycleFactorsFinset
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
k_mem : k ∈ centralizer {g}
c_mem : c ∈ g.cycleFactorsFinset
this : (g * (k * k⁻¹)).cycleFactorsFinset = ConjAct.toConjAct k • g.cycleFactorsFinset
⊢ ↑g.cycleFactorsFinset = ConjAct.toConjAct k • ↑g.cycleFactorsFinset

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
k_mem : k ∈ centralizer {g}
c_mem : c ∈ g.cycleFactorsFinset
this : (g * (k * k⁻¹)).cycleFactorsFinset = ConjAct.toConjAct k • g.cycleFactorsFinset
⊢ ↑g.cycleFactorsFinset = ConjAct.toConjAct k • ↑g.cycleFactorsFinset
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
k_mem : k ∈ centralizer {g}
c_mem : c ∈ g.cycleFactorsFinset
this : (ConjAct.toConjAct k • g).cycleFactorsFinset = ConjAct.toConjAct k • g.cycleFactorsFinset
⊢ ↑g.cycleFactorsFinset = ConjAct.toConjAct k • ↑g.cycleFactorsFinset

Tactic:
rw [ConjAct.toConjAct_smul, mem_centralizer_singleton_iff.mp k_mem, mul_assoc] at this

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
k_mem : k ∈ centralizer {g}
c_mem : c ∈ g.cycleFactorsFinset
this : (g * (k * k⁻¹)).cycleFactorsFinset = ConjAct.toConjAct k • g.cycleFactorsFinset
⊢ ↑g.cycleFactorsFinset = ConjAct.toConjAct k • ↑g.cycleFactorsFinset
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ (g •
      if h : Cancels u w then unitsSMulWithCancel φ u w h
      else
        let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯) =
    cons g u w h1 h2

Tactic:
]

Goal state after:
case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ (g •
      if h : Cancels u w then unitsSMulWithCancel φ u w h
      else
        let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯) =
    cons g u w h1 h2
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
c : ↥g.cycleFactorsFinset
⊢ ↑(1 • c) = ↑c

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
c : ↥g.cycleFactorsFinset
⊢ ↑(1 • c) = ↑c
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ (g •
      let g' := unitsSMulGroup φ d u w.head;
      cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯) =
    cons g u w h1 h2

Tactic:
]

Goal state after:
case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ (g •
      let g' := unitsSMulGroup φ d u w.head;
      cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯) =
    cons g u w h1 h2
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : Equiv.swap a b ∈ M
hbc : Equiv.swap b c ∈ M
hab' : a ≠ b
hac : a ≠ c
⊢ Equiv.swap b c * Equiv.swap a b * Equiv.swap b c ∈ M

Tactic:
]

Goal state after:
case inr.inr
α : Type u_2
inst✝² : DecidableEq α
a b c : α
C : Type u_3
inst✝¹ : SetLike C (Equiv.Perm α)
inst✝ : SubmonoidClass C (Equiv.Perm α)
M : C
hab : Equiv.swap a b ∈ M
hbc : Equiv.swap b c ∈ M
hab' : a ≠ b
hac : a ≠ c
⊢ Equiv.swap b c * Equiv.swap a b * Equiv.swap b c ∈ M
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a✝ b✝ : Perm ↥g.cycleFactorsFinset
hσ : ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset), #(↑(a✝ ⟨a, b⟩)).support = #a.support
hτ : ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset), #(↑(b✝ ⟨a, b⟩)).support = #a.support
c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ #c.support = #c.support

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x✝ : Perm ↥g.cycleFactorsFinset
hσ : ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset), #(↑(x✝ ⟨a, b⟩)).support = #a.support
c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ #(↑(x✝ ⟨↑(x✝⁻¹ ⟨c, hc⟩), ⋯⟩)).support = #c.support

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x✝ : Perm ↥g.cycleFactorsFinset
hσ : ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset), #(↑(x✝ ⟨a, b⟩)).support = #a.support
c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ #(↑(x✝ ⟨↑(x✝⁻¹ ⟨c, hc⟩), ⋯⟩)).support = #c.support
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_4
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
a : α
ha : a ∈ {x | Equiv.swap x y ∈ closure S}
z w : α
hzw : z ≠ w
hσ : Equiv.swap z w ∈ S
hσa : Equiv.swap z w • a ∉ {x | Equiv.swap x y ∈ closure S}
this : a = z ∨ a = w
⊢ False

Tactic:
]

Goal state after:
case refine_4
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
a : α
ha : a ∈ {x | Equiv.swap x y ∈ closure S}
z w : α
hzw : z ≠ w
hσ : Equiv.swap z w ∈ S
hσa : Equiv.swap z w • a ∉ {x | Equiv.swap x y ∈ closure S}
this : a = z ∨ a = w
⊢ False
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : ↥g.cycleFactorsFinset
h : a c = a d
⊢ ↑c = ↑d

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : ↥g.cycleFactorsFinset
h : a c = a d
⊢ ↑c = ↑d
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
⊢ x ∉ Function.fixedPoints ⇑g → ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
⊢ x ∉ Function.fixedPoints ⇑g → ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x✝ y✝ : α
hf✝ : x✝ ∈ orbit (↥(closure S)) y✝
h : Equiv.swap x✝ y✝ ∉ closure S
x y : α
hf : Equiv.swap x y ∈ S
⊢ Equiv.swap x y ∈ S

Tactic:
]

Goal state after:
case refine_1
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x✝ y✝ : α
hf✝ : x✝ ∈ orbit (↥(closure S)) y✝
h : Equiv.swap x✝ y✝ ∉ closure S
x y : α
hf : Equiv.swap x y ∈ S
⊢ Equiv.swap x y ∈ S
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_3
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
⊢ Equiv.refl α ∈ closure S

Tactic:
]

Goal state after:
case refine_3
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
⊢ Equiv.refl α ∈ closure S
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ g.SameCycle x x ∧ g.cycleOf x ∈ g.cycleFactorsFinset

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ g.SameCycle x x ∧ g.cycleOf x ∈ g.cycleFactorsFinset
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
⊢ (g ^ n) (a c) = (g ^ Nat.find ⋯) (a ⟨g.cycleOf x, hx''⟩)

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
⊢ (g ^ n) (a c) = (g ^ Nat.find ⋯) (a ⟨g.cycleOf x, hx''⟩)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case e_6.e_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
⊢ g.cycleOf x = ↑⟨g.cycleOf x, hx''⟩

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
this : a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))
⊢ ↑n ≡ m [ZMOD ↑(#(↑(↑τ c)).support)]

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
this : a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))
⊢ ↑n ≡ m [ZMOD ↑(#(↑(↑τ c)).support)]
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
this : a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))
⊢ (g ^ ↑n) (a c) = (g ^ m) (a c)

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
this : a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))
⊢ (g ^ ↑n) (a c) = (g ^ m) (a c)
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case cons.refine_1
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
⊢ t ^ ↑a.1 * of a.2 * ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ } =
    ReducedWord.prod φ { head := 1, toList := a :: l, chain := chain }

Tactic:
]

Goal state after:
case cons.refine_1
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
⊢ t ^ ↑a.1 * of a.2 * ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ } =
    ReducedWord.prod φ { head := 1, toList := a :: l, chain := chain }
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
this : a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))
⊢ x = x

Tactic:
]

Goal state after: