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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A

Tactic:
let B := ⋂ (g : G) (_ : a ∈ g • A), g • A
  suffices b ∉ B by
    rw [Set.mem_iInter] at this
    simpa only [Set.mem_iInter, not_forall, exists_prop] using this
  suffices B = {a} by rw [this]; rw [Set.mem_singleton_iff]; exact Ne.symm h
  -- B is a block hence is a trivial block
  rcases isTrivialBlock_of_isBlock (G := G) (IsBlock.of_subset a hfA) with hyp | hyp
  · -- B.subsingleton
    apply Set.Subsingleton.eq_singleton_of_mem hyp
    rw [Set.mem_iInter]; intro g; simp only [Set.mem_iInter, imp_self]
  · -- B = Set.univ: contradiction
    change B = Set.univ at hyp
    exfalso; apply hA'
    suffices ∃ g : G, a ∈ g • A by
      obtain ⟨g, hg⟩ := this
      have : B ⊆ g • A := Set.biInter_subset_of_mem hg
      rw [hyp, Set.univ_subset_iff, ← eq_inv_smul_iff] at this
      rw [this, Set.smul_set_univ]
    -- ∃ (g : M), a ∈ g • A
    obtain ⟨x, hx⟩ := hA
    obtain ⟨g, hg⟩ := MulAction.exists_smul_eq G x a
    use g, x

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Nat.card α ≤ 2
⊢ alternatingGroup α = ⊥

Tactic:
nontriviality α

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : Nat.card α ≤ 2
a✝ : Nontrivial α
⊢ alternatingGroup α = ⊥
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < r' ^ 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
hgx : ((g x) v) v = ((g' x) w) w
hgy : ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) = ((g' y) w) w
⊢ (1 + δ * C) * ((g' x) w) w ≤ r' ^ 2 * ((g' x) w) w

Tactic:
by
      gcongr
      rw [← hgx, ← hg, real_inner_self_eq_norm_sq]
      positivity

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
H : Type u_3
β : Type u_4
inst✝¹ : Group H
inst✝ : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Injective ⇑f
⊢ Injective ⇑(mulActionHom_embedding ι hf)

Tactic:
intro _ _ hxy
  ext
  apply hf
  simp only [← hf.mulActionHom_embedding_apply, hxy]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
⊢ G = alternatingGroup α

Tactic:
nontriviality α

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
⊢ G = alternatingGroup α
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
φ : Perm α ≃* Perm α
⊢ comap φ.toMonoidHom (alternatingGroup α) = alternatingGroup α

Tactic:
nontriviality α

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
φ : Perm α ≃* Perm α
a✝ : Nontrivial α
⊢ comap φ.toMonoidHom (alternatingGroup α) = alternatingGroup α
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case hα
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
⊢ k + 1 ≤ Nat.card α

Tactic:
rw [← hs, ← Set.ncard_univ]
        exact ncard_le_ncard s.subset_univ finite_univ

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
x✝ : ↥(fixingSubgroup M s)
x : α
c : M
hc : c ∈ fixingSubgroup M s
⊢ x ∈ sᶜ → ⟨c, hc⟩ • x ∈ sᶜ

Tactic:
rw [← Subgroup.inv_mem_iff] at hc
    simp only [Set.mem_compl_iff, not_imp_not]
    intro hcx
    rwa [← one_smul M x, ← inv_mul_cancel c, mul_smul, (mem_fixingSubgroup_iff M).mp hc (c • x) hcx]

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
⊢ ↑m ∈ fixingSubgroup M s

Tactic:
let hm := m.prop

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
hm : ↑m ∈ fixingSubgroup M (s ∪ t) := Subtype.prop m
⊢ ↑m ∈ fixingSubgroup M s
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
⊢ ⟨↑m, ⋯⟩ ∈ fixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)

Tactic:
let hm := m.prop

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
hm : ↑m ∈ fixingSubgroup M (s ∪ t) := Subtype.prop m
⊢ ⟨↑m, ⋯⟩ ∈ fixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
s : Set α
hMk : IsMultiplyPretransitive G α s.ncard
⊢ s.ncard ≤ univ.ncard

Tactic:
exact ncard_le_ncard (subset_univ s)

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ IsMultiplyPretransitive (Perm α) α n

Tactic:
isMultiplyPretransitive_iff

Goal state after:
α : Type u_1
n : ℕ
⊢ ∀ (x y : Fin n ↪ α), ∃ g, g • x = y
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hM : stabilizer M s ≠ ⊤
⊢ IsPretransitive M α

Tactic:
suffices ∃ (a b : α) (g : M), a ∈ s ∧ b ∈ sᶜ ∧ g • a = b by
    obtain ⟨a, b, g, ha, hb, hgab⟩ := this
    rw [isPretransitive_iff_base a]
    intro x
    by_cases hx : x ∈ s
    · exact hs a ha x hx
    · rw [← Set.mem_compl_iff] at hx
      obtain ⟨k, hk⟩ := hs' b hb x hx
      use k * g
      rw [mul_smul, hgab, hk]

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hM : stabilizer M s ≠ ⊤
⊢ ∃ a b g, a ∈ s ∧ b ∈ sᶜ ∧ g • a = b
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s B : Set α
G : Subgroup M
inst✝ : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
hB : IsBlock (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
⊢ IsTrivialBlock (Subtype.val ⁻¹' B)

Tactic:
suffices IsPreprimitive (stabilizer G s) s by
    apply this.isTrivialBlock_of_isBlock
    -- `IsBlock (Subtype.val ⁻¹' B : Set s)`
    let φ' : stabilizer G s → G := Subtype.val
    let f' : s →ₑ[φ'] α := {
      toFun := Subtype.val
      map_smul' _ _ := rfl }
    apply MulAction.IsBlock.preimage f' hB

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s B : Set α
G : Subgroup M
inst✝ : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
hB : IsBlock (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
⊢ IsPreprimitive ↥(stabilizer (↥G) s) ↑s
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
s : Set α
inst✝¹ : Finite α
inst✝ : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
x : α
hx' : x ∈ sᶜ
this : ∃ k, k • b = x
⊢ x ∈ B

Tactic:
by
    obtain ⟨⟨k, hk⟩, rfl⟩ := this
    suffices k • B = B from this.le (smul_mem_smul_set hb)
    -- `k • B = B`
    apply isBlock_iff_smul_eq_of_nonempty.mp hB (g := ⟨k, ?_⟩)
    · refine ⟨a, ?_, ha⟩
      rw [mem_fixingSubgroup_iff] at hk
      rw [← hk a ha']
      exact Set.smul_mem_smul_set ha
    · -- `k ∈ G`
      apply hG
      exact MulAction.fixingSubgroup_le_stabilizer _ _ hk

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

Goal state before:
pp: α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝¹ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this✝ : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
this : sᶜ ⊆ B
⊢ B = univ

Tactic:
by
    apply hB.eq_univ_of_card_lt
    have : sᶜ.ncard ≤ B.ncard := ncard_le_ncard this
    rw [← Set.ncard_add_ncard_compl s]
    lia

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α < 3
⊢ G = ⊤

Tactic:
Nat.lt_succ_iff

Goal state after:
case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≤ 2
⊢ G = ⊤
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case inr
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)

Tactic:
have : IsPretransitive (alternatingGroup α) (powersetCard α (Nat.card α - n)) := by
      apply this hα
      grind

Goal state after:
case inr
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this✝ :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
this : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α (Nat.card α - n))
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α < 4
⊢ alternatingGroup α ≤ G

Tactic:
Nat.lt_succ_iff

Goal state after:
case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
⊢ alternatingGroup α ≤ G
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case inr
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)

pp: α✝ : Type u_2
n✝ : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)

Tactic:
· have : IsPretransitive (alternatingGroup α) (powersetCard α (Nat.card α - n)) := by
      apply this hα
      grind
    by_cases hn' : n ≤ Nat.card α
    · apply IsPretransitive.of_surjective_map
        (mulActionHom_compl_bijective (alternatingGroup α) α _).surjective this
      aesop
    · suffices Subsingleton (powersetCard α n) by infer_instance
      rw [not_le] at hn'
      rw [← Finite.card_le_one_iff_subsingleton, powersetCard.card,
        Nat.choose_eq_zero_iff.mpr hn']
      simp

Goal state after:
α✝ : Type u_2
n✝ : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
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⁻¹
⊢ motive x

Tactic:
let S : Subgroup (HNNExtension G A B φ) :=
    { carrier := Set.ofPred motive
      one_mem' := by simpa using of 1
      mul_mem' := mul _ _
      inv_mem' := inv _ }

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' := ⋯ }
⊢ motive x
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
a : α
i : ι
h : f a = i
⊢ stabilizerEquiv_invFun g a = ↑((g i) ⟨a, h⟩)

Tactic:
by subst h; rfl

Goal state after:
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
⊢ of ↑(φ.symm ⟨g✝, ⋯⟩) * ReducedWord.prod φ w✝.toReducedWord = t⁻¹ * (of g✝ * (t * ReducedWord.prod φ w✝.toReducedWord))

Tactic:
erw [equiv_symm_eq_conj, mul_assoc, mul_assoc]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsSwap
⊢ (fixedBy α σ)ᶜ.Finite

Tactic:
by
  obtain ⟨x, y, -, rfl⟩ := h
  exact finite_compl_fixedBy_swap

Goal state after:
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✝ ∈ {τ | ∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support}
hτ : b✝ ∈ {τ | ∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support}
⊢ ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset), #(↑(a✝ (b✝ ⟨a, b⟩))).support = #a.support

Tactic:
simp only [Subtype.forall, Set.mem_ofPred_eq] at hσ hτ

Goal state after:
α : 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
⊢ ∀ (a : Perm α) (b : a ∈ g.cycleFactorsFinset), #(↑(a✝ (b✝ ⟨a, b⟩))).support = #a.support
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: α : 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
⊢ False

Tactic:
have := exists_smul_notMem_of_subset_orbit_closure S {x | swap x y ∈ closure S}
    (fun f hf ↦ ?_) (fun z hz ↦ ?_) h ⟨y, ?_⟩

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
this : ∃ σ ∈ S, ∃ a ∈ {x | Equiv.swap x y ∈ closure S}, σ • a ∉ {x | Equiv.swap x y ∈ closure S}
⊢ False

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
f : Equiv.Perm α
hf : f ∈ S
⊢ f⁻¹ ∈ S

case refine_2
α : 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
z : α
hz : z ∈ {x | Equiv.swap x y ∈ closure S}
⊢ z ∈ orbit (↥(closure S)) x

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
⊢ y ∈ {x | Equiv.swap x y ∈ closure S}
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
⊢ a.ofPermHomFun τ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Tactic:
rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | ⟨d, hd, m, hm⟩)

Goal state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ Function.fixedPoints ⇑g
⊢ a.ofPermHomFun τ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d).support
m : ℤ
hm : (g ^ m) (a d) = x
⊢ a.ofPermHomFun τ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑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
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ a (↑τ c) ∈ (↑(↑τ c)).support

Tactic:
apply mem_support_self

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ (∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support) ↔
    (fun c ↦ #(↑c).support) ∘ ⇑τ = fun c ↦ #(↑c).support

Tactic:
funext_iff

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ (∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support) ↔
    ∀ (x : ↥g.cycleFactorsFinset), ((fun c ↦ #(↑c).support) ∘ ⇑τ) x = #(↑x).support
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f : (i : ι) → G i →* K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
g : H
⊢ (lift f k hf) ((base φ) g) = k g

Tactic:
by
  delta PushoutI lift base
  simp only [MonoidHom.coe_comp, Con.coe_mk', comp_apply, Con.lift_coe, lift_apply_inr]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' :
  ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∈
    ((Finset.univ.erase ⟨g.cycleOf x, hx⟩).noncommProd (fun i ↦ ↑((u, v).2 i)) ⋯).support
a : ↥g.cycleFactorsFinset
ha1 : ¬↑a = g.cycleOf x
key : ∀ ⦃a_1 : α⦄, a_1 ∈ (↑a).support → a_1 ∉ (g.cycleOf x).support
k✝ : ℤ
hk✝ : ↑a ^ k✝ = ↑(v a)
ha2 : ↑((u, v).2 ⟨g.cycleOf x, hx⟩) x ∉ (g.cycleOf x).support
k : ℤ
hk : ↑⟨g.cycleOf x, hx⟩ ^ k = ↑(v ⟨g.cycleOf x, hx⟩)
⊢ x ∈ Function.fixedPoints ⇑g

Tactic:
rwa [← hk, zpow_apply_mem_support, notMem_support, cycleOf_apply_self] at ha2

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
⊢ ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head

Tactic:
Word.equivPair_head

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
⊢ ↑(⋯.equiv (if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1)).2 =
    if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i then ⋯ ▸ (w.toList.head ⋯).snd else 1