mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case right.hf
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
⊢ Function.Bijective ⇑g

Tactic:
constructor

Goal state after:
case right.hf.left
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⋯
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) := ⋯
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := ⋯
⊢ Function.Injective ⇑g

case right.hf.right
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⋯
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) := ⋯
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := ⋯
⊢ Function.Surjective ⇑g
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case h.inr.inr
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha✝ : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
hsgs_ne_top : s ∪ g • s ≠ ⊤
⊢ (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)

Tactic:
suffices IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) →
      IsMultiplyPretransitive G α 2 by
      refine ⟨this, fun hs_prim ↦ ?_⟩
      apply (hrec _ hmn hG htm htm').2
      exact IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
          hs_prim hsgs_ne_top

Goal state after:
case h.inr.inr
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha✝ : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
hsgs_ne_top : s ∪ g • s ≠ ⊤
⊢ IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
Module: Mathlib.GroupTheory.GroupAction.Support

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Group H
inst✝⁵ : SMul G α
inst✝⁴ : SMul G β
inst✝³ : MulAction H α
inst✝² : SMul H β
inst✝¹ : SMulCommClass G H β
inst✝ : SMulCommClass G H α
s : Set α
b : β
g : H
h : Supports G s b
⊢ Supports G (g • s) (g • b)

Tactic:
rintro g' hg'
  rw [smul_comm, h]
  rintro a ha
  have := Set.forall_mem_image.1 hg' ha
  rwa [smul_comm, smul_left_cancel_iff] at this

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : MulAction G α
n : ℕ
s✝ t : ↑(powersetCard α n)
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
g : G
s : ↑(powersetCard α n)
⊢ (compl hm) (g • s) = id g • (compl hm) s

Tactic:
ext

Goal state after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : MulAction G α
n : ℕ
s✝ t : ↑(powersetCard α n)
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
g : G
s : ↑(powersetCard α n)
a✝ : α
⊢ a✝ ∈ ↑((compl hm) (g • s)) ↔ a✝ ∈ ↑(id g • (compl hm) s)
Module: Mathlib.GroupTheory.MonoidLocalization.DivPairs

Goal state before:
pp: M : Type u_1
G : Type u_2
H : Type u_3
inst✝² : CommMonoid M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : ⊤.LocalizationMap G
g : ⊤.LocalizationMap H
s : Submonoid G
⊢ divPairs g (comap (g.mulEquivOfLocalizations f).toMonoidHom s) = divPairs f s

Tactic:
ext

Goal state after:
M : Type u_1
G : Type u_2
H : Type u_3
inst✝² : CommMonoid M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : ⊤.LocalizationMap G
g : ⊤.LocalizationMap H
s : Submonoid G
x✝ : M × M
⊢ x✝ ∈ divPairs g (comap (g.mulEquivOfLocalizations f).toMonoidHom s) ↔ x✝ ∈ divPairs f s
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive (HNNExtension.of g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := Set.ofPred motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
a : ↥A
⊢ ⟨HNNExtension.t, t⟩ * (HNNExtension.of.codRestrict S of) ↑a =
    (HNNExtension.of.codRestrict S of) ↑(φ a) * ⟨HNNExtension.t, t⟩

Tactic:
ext

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive (HNNExtension.of g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := ⋯
a : ↥A
⊢ ↑(⟨HNNExtension.t, t⟩ * (HNNExtension.of.codRestrict S of) ↑a) =
    ↑((HNNExtension.of.codRestrict S of) ↑(φ a) * ⟨HNNExtension.t, t⟩)
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive (HNNExtension.of g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := Set.ofPred motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
f : HNNExtension G A B φ →* ↥S := lift (HNNExtension.of.codRestrict S of) ⟨HNNExtension.t, t⟩ ⋯
⊢ (S.subtype.comp f).comp HNNExtension.of = (MonoidHom.id (HNNExtension G A B φ)).comp HNNExtension.of

Tactic:
ext

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
motive : HNNExtension G A B φ → Prop
x : HNNExtension G A B φ
of : ∀ (g : G), motive (HNNExtension.of g)
t : motive HNNExtension.t
mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)
inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹
S : Subgroup (HNNExtension G A B φ) := { carrier := Set.ofPred motive, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
f : HNNExtension G A B φ →* ↥S := lift (HNNExtension.of.codRestrict S of) ⟨HNNExtension.t, t⟩ ⋯
x✝ : G
⊢ ((S.subtype.comp f).comp HNNExtension.of) x✝ = ((MonoidHom.id (HNNExtension G A B φ)).comp HNNExtension.of) x✝
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
hN : H.IsSubnormal
H_ne : H ≠ ⊤
⊢ H = ⊤ ∨ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
grind only [iff_eq_top_or_exists, exists_normal_and_le_and_lt_top_of_ne]

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

Goal state before:
pp: case h
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ map length (map (map ⇑(Fintype.equivFin α).symm) l) = c ∧
    (∀ s ∈ map (map ⇑(Fintype.equivFin α).symm) l, s.Nodup) ∧ Pairwise Disjoint (map (map ⇑(Fintype.equivFin α).symm) l)

Tactic:
constructor

Goal state after:
case h.left
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ map length (map (map ⇑(Fintype.equivFin α).symm) l) = c

case h.right
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ (∀ s ∈ map (map ⇑(Fintype.equivFin α).symm) l, s.Nodup) ∧ Pairwise Disjoint (map (map ⇑(Fintype.equivFin α).symm) l)
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ f.range ≤ (f.noncommCoprod g comm).range ∧ g.range ≤ (f.noncommCoprod g comm).range

Tactic:
constructor

Goal state after:
case a.left
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ f.range ≤ (f.noncommCoprod g comm).range

case a.right
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ g.range ≤ (f.noncommCoprod g comm).range
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.right
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ (∀ s ∈ map (map ⇑(Fintype.equivFin α).symm) l, s.Nodup) ∧ Pairwise Disjoint (map (map ⇑(Fintype.equivFin α).symm) l)

Tactic:
constructor

Goal state after:
case h.right.left
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ ∀ s ∈ map (map ⇑(Fintype.equivFin α).symm) l, s.Nodup

case h.right.right
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ Pairwise Disjoint (map (map ⇑(Fintype.equivFin α).symm) l)
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (∃ g, g.cycleType = m) ↔ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (∃ g, g.cycleType = m) → m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) → ∃ g, g.cycleType = m
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
⊢ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

Tactic:
constructor

Goal state after:
case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
⊢ m.sum ≤ Fintype.card α

case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
⊢ ∀ a ∈ m, 2 ≤ a
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
⊢ m.toList.sum ≤ Fintype.card α

Tactic:
simp only [Multiset.sum_toList]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
⊢ m.sum ≤ Fintype.card α
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : ¬Cancels u w
⊢ ReducedWord.prod φ
      (let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯).toReducedWord =
    t ^ ↑u * ReducedWord.prod φ w.toReducedWord

Tactic:
simp only [unitsSMulGroup, SetLike.coe_sort_coe, prod_cons, prod_group_smul, map_mul, map_inv]

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : ¬Cancels u w
⊢ of ↑((toSubgroupEquiv φ u) (⋯.equiv w.head).1) *
      (t ^ ↑u * (of ↑(⋯.equiv w.head).2 * (of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord)) =
    t ^ ↑u * ReducedWord.prod φ w.toReducedWord
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
⊢ cons (g * ↑((toSubgroupEquiv φ u) ⟨1, ⋯⟩)) u w ⋯ ⋯ = cons g u w h1 h2

Tactic:
ext

Goal state after:
case cons.h1
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
⊢ (cons (g * ↑((toSubgroupEquiv φ u) ⟨1, ⋯⟩)) u w ⋯ ⋯).head = (cons g u w h1 h2).head

case h2
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
i✝ : ℕ
a✝ : ℤˣ × G
⊢ (cons (g * ↑((toSubgroupEquiv φ u) ⟨1, ⋯⟩)) u w ⋯ ⋯).toList[i✝]? = some a✝ ↔ (cons g u w h1 h2).toList[i✝]? = some a✝
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
⊢ Equiv.swap (Equiv.swap z w • a) a ∈ closure S

Tactic:
obtain rfl | rfl := this

Goal state after:
case refine_4.inl
α : 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}
w : α
hzw : a ≠ w
hσ : Equiv.swap a w ∈ S
hσa : Equiv.swap a w • a ∉ {x | Equiv.swap x y ∈ closure S}
⊢ Equiv.swap (Equiv.swap a w • a) a ∈ closure S

case refine_4.inr
α : 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 : α
hzw : z ≠ a
hσ : Equiv.swap z a ∈ S
hσa : Equiv.swap z a • a ∉ {x | Equiv.swap x y ∈ closure S}
⊢ Equiv.swap (Equiv.swap z a • a) a ∈ closure S
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
⊢ f = 1

Tactic:
ext

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
x✝ : α
⊢ f x✝ = 1 x✝
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ (g ^ m) (a (↑τ c)) ≠ (g ^ m) (a c) ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x

Tactic:
rw [(g ^ m).injective.ne_iff, a.injective.ne_iff, not_iff_comm]

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ (¬∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x) ↔ ↑τ c = c
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a b c : D ≀ᵣ Q
⊢ a * b * c = a * (b * c)

Tactic:
ext

Goal state after:
case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a b c : D ≀ᵣ Q
x✝ : Q
⊢ (a * b * c).left x✝ = (a * (b * c)).left x✝

case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a b c : D ≀ᵣ Q
⊢ (a * b * c).right = (a * (b * c)).right
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ 1 * a = a

Tactic:
ext

Goal state after:
case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
x✝ : Q
⊢ (1 * a).left x✝ = a.left x✝

case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ (1 * a).right = a.right
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ a * 1 = a

Tactic:
ext

Goal state after:
case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
x✝ : Q
⊢ (a * 1).left x✝ = a.left x✝

case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ (a * 1).right = a.right
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ a⁻¹ * a = 1

Tactic:
ext

Goal state after:
case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
x✝ : Q
⊢ (a⁻¹ * a).left x✝ = left 1 x✝

case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
a : D ≀ᵣ Q
⊢ (a⁻¹ * a).right = right 1
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
x✝¹ x✝ : Q
⊢ { left := 1, right := x✝¹ * x✝ } = { left := 1, right := x✝¹ } * { left := 1, right := x✝ }

Tactic:
ext

Goal state after:
case left
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
x✝² x✝¹ x✝ : Q
⊢ { left := 1, right := x✝² * x✝¹ }.left x✝ = ({ left := 1, right := x✝² } * { left := 1, right := x✝¹ }).left x✝

case right
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
x✝¹ x✝ : Q
⊢ { left := 1, right := x✝¹ * x✝ }.right = ({ left := 1, right := x✝¹ } * { left := 1, right := x✝ }).right
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
⊢ rightHom.comp inl = MonoidHom.id Q

Tactic:
ext

Goal state after:
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
x✝ : Q
⊢ (rightHom.comp inl) x✝ = (MonoidHom.id Q) x✝
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₁ ≀ᵣ Q₁
⊢ (fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right })
      ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right }) x) =
    x

Tactic:
ext

Goal state after:
case left
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₁ ≀ᵣ Q₁
x✝ : Q₁
⊢ ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right })
          ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right }) x)).left
      x✝ =
    x.left x✝

case right
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₁ ≀ᵣ Q₁
⊢ ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right })
        ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right }) x)).right =
    x.right
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₂ ≀ᵣ Q₂
⊢ (fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right })
      ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right }) x) =
    x

Tactic:
ext

Goal state after:
case left
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₂ ≀ᵣ Q₂
x✝ : Q₂
⊢ ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right })
          ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right }) x)).left
      x✝ =
    x.left x✝

case right
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x : D₂ ≀ᵣ Q₂
⊢ ((fun x ↦ { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right })
        ((fun x ↦ { left := (⇑f.symm ∘ x.left) ∘ ⇑g, right := g.symm x.right }) x)).right =
    x.right