mathlib-initiative/mathlib-tactics huggingface dataset:
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‖ ≤ δ
⊢ ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ <
    r

Tactic:
apply (opNorm_le_bound _ (by linarith) (fun v ↦ ?_)).trans_lt r'r

Goal state after:
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
⊢ ‖(Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
          Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x)
        v‖ ≤
    r' * ‖v‖
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
this : FreeGroup.lift a = (lift fun i ↦ FreeGroup.lift fun x ↦ a i).comp freeGroupEquivCoprodI.toMonoidHom
⊢ Function.Injective (⇑(lift fun i ↦ FreeGroup.lift fun x ↦ a i) ∘ ⇑freeGroupEquivCoprodI.toMonoidHom)

Tactic:
clear this

Goal state after:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
⊢ Function.Injective (⇑(lift fun i ↦ FreeGroup.lift fun x ↦ a i) ∘ ⇑freeGroupEquivCoprodI.toMonoidHom)
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : ↥S) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ ∏ a, Nat.card ↥(zpowers ↑a)
g : ↥S
x✝ : g ∈ Finset.univ
⊢ Nat.card ↥(zpowers ↑g) ∣ Monoid.exponent G

Tactic:
Nat.card_zpowers

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : ↥S) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ ∏ a, Nat.card ↥(zpowers ↑a)
g : ↥S
x✝ : g ∈ Finset.univ
⊢ orderOf ↑g ∣ Monoid.exponent G
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.focalSubgroupOf.Normal

Tactic:
rw [focalSubgroupOf_def, normal_subgroupOf_iff (focalSubgroup_le H)]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (h k : G), h ∈ H.focalSubgroup → k ∈ H → k * h * k⁻¹ ∈ H.focalSubgroup
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg.inl
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : k = 0
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime 1

Tactic:
apply Nat.coprime_one_right

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: case mp
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
hl : l = g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
⊢ (mk [w])⁻¹ • (fun m ↦ m • x) ⟨g, hg⟩ ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x}

Tactic:
match l with
    | [] => simp [← hl, startsWith] at hg
    | [a] =>
      simp_rw [h, ← hl, show a = w by simpa [← hl, startsWith] using hg, startsWith.smul_def,
        inv_smul_smul]
      exact Or.inr rfl
    | a :: b :: l =>
      have ha : a = w := by simpa [← hl, startsWith] using hg
      have h1 := isReduced_cons_cons.mp (hl ▸ isReduced_toWord)
      refine Or.inl (Set.mem_biUnion (x := b) (by grind) ?_)
      simp_rw [h, ← hl, ha, ← List.singleton_append (l := b :: l), ← mul_mk, startsWith.smul_def,
        mul_smul, inv_smul_smul]
      exact ⟨⟨mk (b :: l), by simp [startsWith, h1.2.reduce_eq]⟩, rfl⟩

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
x : X
hx : x ∈ B
key : (stabilizer G x).subgroupOf (stabilizer G B) = stabilizer (↥(stabilizer G B)) x
⊢ B.ncard = (orbit (↥(stabilizer G B)) x).ncard

Tactic:
hB.orbit_stabilizer_eq hx

Goal state after:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
x : X
hx : x ∈ B
key : (stabilizer G x).subgroupOf (stabilizer G B) = stabilizer (↥(stabilizer G B)) x
⊢ B.ncard = B.ncard
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ l.prod ∈ alternatingGroup α ↔ Even l.length

Tactic:
rw [mem_alternatingGroup, sign_prod_list_swap hl, neg_one_pow_eq_one_iff_even]
  decide

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
hNX : ∃ a, a ∉ fixedPoints (↥N) α
⊢ IsPretransitive (↥N) α

Tactic:
obtain ⟨a, ha⟩ := hNX

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
M : Type u_3
inst✝² : Group M
α : Type u_4
inst✝¹ : MulAction M α
inst✝ : IsPreprimitive M α
N : Subgroup M
x✝ : N.Normal
a : α
ha : a ∉ fixedPoints (↥N) α
⊢ IsPretransitive (↥N) α
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
a : α
⊢ ENat.card ↥(ofStabilizer G a) + 1 = ENat.card α

Tactic:
by
  dsimp only [ENat.card]
  rw [← Cardinal.mk_sum_compl {a}, map_add, add_comm, eq_comm]
  congr
  simp

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

Goal state before:
pp: case inl
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
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : (⋂ k, ⋂ (_ : a ∈ k • A), k • A).Subsingleton
⊢ B = {a}

Tactic:
apply Set.Subsingleton.eq_singleton_of_mem hyp

Goal state after:
case inl
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
B : Set X := ⋯
hyp : (⋂ k, ⋂ (_ : a ∈ k • A), k • A).Subsingleton
⊢ a ∈ ⋂ k, ⋂ (_ : a ∈ k • A), k • A
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case mp
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a✝ : IsMultiplyPretransitive G α 2
a b : α
⊢ ∀ {c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d

Tactic:
c

Goal state after:
case mp
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a✝ : IsMultiplyPretransitive G α 2
a b c : α
⊢ ∀ {d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
⊢ IsTrivialBlock B

Tactic:
rcases B.subsingleton_or_nontrivial with h | h

Goal state after:
case inl
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
h : B.Subsingleton
⊢ IsTrivialBlock B

case inr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
h : B.Nontrivial
⊢ IsTrivialBlock B
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ ((alternatingGroup α).subtype.comp (ofSubtype s)).range =
    map (alternatingGroup α).subtype (Perm.ofSubtype.range.subgroupOf (alternatingGroup α))

Tactic:
ofSubtype_comp_subtype,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ (Perm.ofSubtype.comp (alternatingGroup ↥s).subtype).range =
    map (alternatingGroup α).subtype (Perm.ofSubtype.range.subgroupOf (alternatingGroup α))
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
⊢ Injective ⇑(map_ofFixingSubgroupUnion M s t)

pp: case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
⊢ Surjective ⇑(map_ofFixingSubgroupUnion M s t)

Tactic:
· intro a b h
    simpa only [← SetLike.coe_eq_coe] using! h

Goal state after:
case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
⊢ Surjective ⇑(map_ofFixingSubgroupUnion M s t)
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : 3 ≤ Nat.card α
⊢ IsPretransitive (↥(alternatingGroup α)) α

Tactic:
rw [← is_one_pretransitive_iff]
  let := isMultiplyPretransitive α
  apply isMultiplyPretransitive_of_le (n := Nat.card α - 2) _ (sub_le _ _)
  rwa [← add_le_add_iff_right 2, Nat.sub_add_cancel (le_trans (by norm_num) h)]

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

Goal state before:
pp: case inl
α : Type u_2
inst✝ : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
hα : Nat.card α ≠ 2 * s.ncard
h : s.ncard < sᶜ.ncard
⊢ IsCoatom (stabilizer (Perm α) s)

Tactic:
exact isCoatom_stabilizer_of_ncard_lt_ncard_compl hs_nonempty h

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

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
this : ∀ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ, ∃ k, x = k • a
⊢ IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)

Tactic:
isPretransitive_iff

Goal state after:
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left✝ : g a ≠ a
hgc : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
hs : ∀ (x : α), g • x ≠ x ↔ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ
this : ∀ x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ, ∃ k, x = k • a
⊢ ∀ (x y : ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)), ∃ g_1, g_1 • x = y
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 = ⊤

pp: case inr
α : 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:
· -- trivial case : Nat.card α ≤ 2
    rw [Nat.lt_succ_iff] at hα3
    apply Subgroup.eq_top_of_card_eq
    simp only [Nat.card_eq_fintype_card]
    apply le_antisymm (Fintype.card_subtype_le _)
    rw [← Nat.card_eq_fintype_card, Nat.card_perm]
    refine le_trans (Nat.factorial_le hα3) ?_
    rw [Nat.factorial_two]
    have : Nonempty G := One.instNonempty
    apply Nat.le_of_dvd Fintype.card_pos
    rw [← h2g.orderOf, orderOf_submonoid ⟨g, hg⟩]
    exact orderOf_dvd_card

Goal state after:
case inr
α : 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 = ⊤
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
⊢ ↑c₂ * a₁ ≤ ↑a₂ * c₁ ↔ ↑d₂ * b₁ ≤ ↑b₂ * d₁

Tactic:
obtain ⟨e, he⟩ := r_iff_exists.1 hab

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e : ↥s
he : ↑e * (↑(b₁, b₂).2 * (a₁, a₂).1) = ↑e * (↑(a₁, a₂).2 * (b₁, b₂).1)
⊢ ↑c₂ * a₁ ≤ ↑a₂ * c₁ ↔ ↑d₂ * b₁ ≤ ↑b₂ * d₁
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
⊢ ↑c₂ * a₁ < ↑a₂ * c₁ ↔ ↑d₂ * b₁ < ↑b₂ * d₁

Tactic:
obtain ⟨e, he⟩ := r_iff_exists.1 hab

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e : ↥s
he : ↑e * (↑(b₁, b₂).2 * (a₁, a₂).1) = ↑e * (↑(a₁, a₂).2 * (b₁, b₂).1)
⊢ ↑c₂ * a₁ < ↑a₂ * c₁ ↔ ↑d₂ * b₁ < ↑b₂ * d₁
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case h.refine_1
M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
inst✝ : UniqueFactorizationMonoid M
this : IsCancelMulZero N
n : N
m : M
s : ↥S
hn : ¬f (m, s).1 = 0
eq : n * f ↑(m, s).2 = f (m, s).1
p : M
hp : p ∈ factors m
hx : (∃ a ∈ factors m, f a = f p) ∧ ¬IsUnit (f p)
⊢ Prime (f p)

Tactic:
exact f.map_prime (prime_of_factor _ hp)
        (mt (fun h ↦ eq_zero_of_zero_dvd <| h ▸ map_dvd f (dvd_of_mem_factors hp)) hn) hx.2

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
| ↑(φ (⋯.equiv (↑g * w.head)).1)

Tactic:
IsComplement.equiv_mul_left

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
| ↑(φ (g * (⋯.equiv w.head).1, (⋯.equiv w.head).2).1)
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
| (↑(⋯.equiv (↑g * w.head)).2 * w.head⁻¹) • w

Tactic:
IsComplement.equiv_mul_left

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
| (↑(g * (⋯.equiv w.head).1, (⋯.equiv w.head).2).2 * w.head⁻¹) • w
Module: Mathlib.GroupTheory.Perm.ClosureSwap

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

Tactic:
simpa [Equiv.swap_comm] using subset_closure hσ

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

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

Tactic:
simpa [Equiv.swap_comm] using subset_closure hσ

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: 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)
hS : a.2 * w'.head ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
⊢ False

Tactic:
have hx' := congr_arg (Option.map Prod.fst) hx

Goal state after:
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)
hS : a.2 * w'.head ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
hx' : Option.map Prod.fst w'.toList.head? = Option.map Prod.fst (some (-a.1, x))
⊢ False
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ a.ofPermHomFun τ x ≠ x ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x

Tactic:
simp only [ofPermHomFun_apply_of_mem_fixedPoints a τ hx, ne_eq, not_true_eq_false, false_iff,
      ← mem_support]

Goal state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ¬∃ a ∈ (↑τ).support, x ∈ (↑a).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
i : ι
x' : H
⊢ (Con.ker (Coprod.lift (CoprodI.lift f) k)) (inl (CoprodI.of ((φ i) x'))) (inr x')

Tactic:
simp only [DFunLike.ext_iff, MonoidHom.coe_comp, comp_apply] at hf

Goal state after:
ι : 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
i : ι
x' : H
hf : ∀ (i : ι) (x : H), (f i) ((φ i) x) = k x
⊢ (Con.ker (Coprod.lift (CoprodI.lift f) k)) (inl (CoprodI.of ((φ i) x'))) (inr x')
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ #{g | (↑g).cycleType = m} =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
    else 0

Tactic:
split_ifs with hm
  · -- m is an even cycle_type
    rw [← Finset.card_map, map_subtype_of_cycleType, if_pos hm.2,
      Equiv.Perm.card_of_cycleType α m, if_pos hm.1, mul_assoc]
  · -- m does not correspond to a permutation, or to an odd one,
    rw [← Finset.card_map, map_subtype_of_cycleType]
    rw [apply_ite Finset.card, Finset.card_empty]
    split_ifs with hm'
    · rw [Equiv.Perm.card_of_cycleType, if_neg]
      obtain hm | hm := not_and_or.mp hm
      · exact hm
      · contradiction
    · rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↥(centralizer {g}) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
by
  rw [← (toPermHom g).ker.card_mul_index, index_ker, nat_card_range_toPermHom,
    ← kerParam_range_card, ← Nat.card_eq_fintype_card, kerParam_range_eq, card_subtype]

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: case ind
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
⊢ ∃ H, N.IsComplement' H

Tactic:
refine not_forall_not.mp fun h3 => ?_

Goal state after:
case ind
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
⊢ (toPermHom g) ⟨x, ⋯⟩ = 1

Tactic:
ext c : 2

Goal state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
c : ↥g.cycleFactorsFinset
⊢ ↑(((toPermHom g) ⟨x, ⋯⟩) c) = ↑(1 c)