mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

Goal state before:
pp: E : Type u_1
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
H✝ : Type u_2
inst✝¹² : TopologicalSpace H✝
I : ModelWithCorners ℝ E H✝
M : Type u_3
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H✝ M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → NormedAddCommGroup (V x)
inst✝⁵ : (x : M) → InnerProductSpace ℝ (V x)
inst✝⁴ : FiberBundle F V
cov : CovariantDerivative I F V
inst✝³ : VectorBundle ℝ F V
inst✝² : IsContMDiffRiemannianBundle I 1 F V
inst✝¹ : ContMDiffVectorBundle 1 F V I
inst✝ : FiniteDimensional ℝ F
hcov : cov.IsMetricCompatible
x : M
X : (x : M) → TangentSpace I x
σ τ : (x : M) → V x
hσ : MDiffAt (T% σ) x
hτ : MDiffAt (T% τ) x
H : (((cov.derivMetricTensor x) (σ x)) (τ x)) (X x) = (((0 x) (σ x)) (τ x)) (X x)
⊢ ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) =
    (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x + (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x

Tactic:
simp [derivMetricTensor_apply _ _ hσ hτ] at H

Goal state after:
E : Type u_1
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
H✝ : Type u_2
inst✝¹² : TopologicalSpace H✝
I : ModelWithCorners ℝ E H✝
M : Type u_3
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H✝ M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → NormedAddCommGroup (V x)
inst✝⁵ : (x : M) → InnerProductSpace ℝ (V x)
inst✝⁴ : FiberBundle F V
cov : CovariantDerivative I F V
inst✝³ : VectorBundle ℝ F V
inst✝² : IsContMDiffRiemannianBundle I 1 F V
inst✝¹ : ContMDiffVectorBundle 1 F V I
inst✝ : FiniteDimensional ℝ F
hcov : cov.IsMetricCompatible
x : M
X : (x : M) → TangentSpace I x
σ τ : (x : M) → V x
hσ : MDiffAt (T% σ) x
hτ : MDiffAt (T% τ) x
H : ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) - inner ℝ ((↑cov σ x) (X x)) (τ x) - inner ℝ (σ x) ((↑cov τ x) (X x)) = 0
⊢ ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) =
    (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x + (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
F : Type u_5
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → AddCommGroup (V x)
inst✝⁵ : (x : M) → Module 𝕜 (V x)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝² : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝¹ : FiberBundle F V
inst✝ : VectorBundle 𝕜 F V
cov : CovariantDerivative I F V
x : M
⊢ ↑cov 0 x = 0 x

Tactic:
simp [cov.isCovariantDerivativeOnUniv.zero]

Goal state after:
Module: Mathlib.Geometry.Manifold.WhitneyEmbedding

Goal state before:
pp: case intro
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
ι : Type u_1
inst✝ : Finite ι
f : SmoothBumpCovering ι I M
val✝ : Fintype ι
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ Injective e ∧ ∀ (x : M), Injective ⇑(mfderiv% e x)

Tactic:
set F := EuclideanSpace ℝ (Fin <| finrank ℝ (ι → E × ℝ))

Goal state after:
case intro
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
ι : Type u_1
inst✝ : Finite ι
f : SmoothBumpCovering ι I M
val✝ : Fintype ι
F : Type := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ Injective e ∧ ∀ (x : M), Injective ⇑(mfderiv% e x)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
fi : (i : ι) → M i →* N
x✝¹ x✝ : FreeMonoid ((i : ι) × M i)
⊢ Rel M x✝¹ x✝ ≤ (Con.ker (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd)) x✝¹ x✝

Tactic:
by
        simp_rw [Con.ker_rel]
        rintro (i | ⟨x, y⟩) <;> simp

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ (alternatingWord i' i (m + 1)).concat i' = (if Even (m + 1) then i' else i) :: alternatingWord i i' (m + 1)

Tactic:
ih i' i

Goal state after:
case succ
B : Type u_1
m : ℕ
ih : ∀ (i i' : B), alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m
i i' : B
⊢ ((if Even m then i else i') :: alternatingWord i' i m).concat i' =
    (if Even (m + 1) then i' else i) :: alternatingWord i i' (m + 1)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : ¬p.head = 1
⊢ (of ⟨i, p.head⟩.snd :: List.map (fun l ↦ of l.snd) p.tail.toList).prod = of p.head * p.tail.prod

Tactic:
List.prod_cons,

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : ¬p.head = 1
⊢ of ⟨i, p.head⟩.snd * (List.map (fun l ↦ of l.snd) p.tail.toList).prod = of p.head * p.tail.prod
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
i i' : B
m : ℕ
⊢ (alternatingWord i i' m).length = m

Tactic:
by
  induction m generalizing i i' with
  | zero => dsimp [alternatingWord]
  | succ m ih => simpa [alternatingWord] using ih i' i

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) + 1 = cs.length w → cs.length (cs.simple i * w) < cs.length w

Tactic:
· lia

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) = cs.length w + 1 → ¬cs.length (cs.simple i * w) < cs.length w

Tactic:
· lia

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) + 1 = cs.length w → cs.length (w * cs.simple i) < cs.length w

Tactic:
· lia

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) = cs.length w + 1 → ¬cs.length (w * cs.simple i) < cs.length w

Tactic:
· lia

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case smul
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
ih : w.prod • empty = w
⊢ (of m • w).prod • empty = of m • w

Tactic:
rw [prod_smul, mul_smul, ih]

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
H₁ H₂ : Subgroup G
⊢ { toFun := fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker,
          invFun := fun Φ ↦ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker,
          left_inv := ⋯, right_inv := ⋯ }
        H₁ ≤
      { toFun := fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker,
          invFun := fun Φ ↦ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker,
          left_inv := ⋯, right_inv := ⋯ }
        H₂ ↔
    H₁ ≤ H₂

Tactic:
by
    simp_rw [Equiv.coe_fn_mk, OrderDual.toDual_le_toDual,
      SetLike.le_def, mem_ker, domRestrictHom_apply, domRestrict_eq_one_iff]
    grind [forall_monoidHom_apply_eq_one_iff M H₂]

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hG : Group.FG G
inst✝ : H.FiniteIndex
this : Group.FG ↥H
⊢ Group.rank ↥H ≤ H.index * Group.rank G

Tactic:
obtain ⟨S, hS₀, hS⟩ := Group.rank_spec G

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hG : Group.FG G
inst✝ : H.FiniteIndex
this : Group.FG ↥H
S : Finset G
hS₀ : #S = Group.rank G
hS : closure ↑S = ⊤
⊢ Group.rank ↥H ≤ H.index * Group.rank G
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
⊢ ↑(⟨g⁻¹ * h * g, hconj⟩⁻¹ * ⟨h, hh⟩) ∈ H.focalSubgroup

Tactic:
apply subset_closure

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
⊢ ↑(⟨g⁻¹ * h * g, hconj⟩⁻¹ * ⟨h, hh⟩) ∈ {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg
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
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime (Nat.card (MulAut ↥↑P))

Tactic:
rcases eq_zero_or_pos k with h0 | h0

Goal state after:
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 (Nat.card (MulAut ↥↑P))

case neg.inr
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 : 0 < k
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime (Nat.card (MulAut ↥↑P))
Module: Mathlib.GroupTheory.Frattini

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
⊢ (frattini G).Characteristic

Tactic:
characteristic_iff_comap_eq

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
⊢ ∀ (ϕ : G ≃* G), comap ϕ.toMonoidHom (frattini G) = frattini G
Module: Mathlib.GroupTheory.Frattini

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
p_prime : Fact (Nat.Prime p)
P : Sylow p ↥(frattini G)
frattini_argument : normalizer ↑(map (frattini G).subtype ↑P) ⊔ frattini G = ⊤
normalizer_P : normalizer ↑(map (frattini G).subtype ↑P) = ⊤
P_normal_in_G : (map (frattini G).subtype ↑P).Normal
⊢ (↑P).Normal

Tactic:
exact P_normal_in_G.of_map_subtype

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
x✝ y : G
⊢ x✝ + y + -x✝ + -y = 0 ↔ y + x✝ = x✝ + y

Tactic:
add_neg_eq_zero,

Goal state after:
G : Type u_2
inst✝ : AddGroup G
x✝ y : G
⊢ x✝ + y + -x✝ = y ↔ y + x✝ = x✝ + y
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsDescendingCentralSeries H ∧ H n = ⊥) → ⊤.lowerCentralSeries n = ⊥

Tactic:
rintro n ⟨H, ⟨hH, hn⟩⟩
    rw [← le_bot_iff, ← hn]
    exact descending_central_series_ge_lower H hH n

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

Goal state before:
pp: case refine_1.cons.inr
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : c✝ ⟶ b✝
eT : Sum.inr e ∈ T b✝ c✝
⊢ inv (F'.map (of e)) = 1

Tactic:
inv_as_inv,

Goal state after:
case refine_1.cons.inr
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : c✝ ⟶ b✝
eT : Sum.inr e ∈ T b✝ c✝
⊢ (F'.map (of e))⁻¹ = 1
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: case mp
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := ⋯
H' : Subgroup H := ⋯
P : ↥I →* ↥G' := ⋯
Q : ↥I →* ↥H' := ⋯
I' : Subgroup (↥G' × ↥H') := ⋯
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : G
h : H
⊢ (g, h) ∈ I →
    (g, h) ∈ map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype) (P.prod Q).range

pp: case mpr
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := ⋯
H' : Subgroup H := ⋯
P : ↥I →* ↥G' := ⋯
Q : ↥I →* ↥H' := ⋯
I' : Subgroup (↥G' × ↥H') := ⋯
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : G
h : H
⊢ (g, h) ∈ map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype) (P.prod Q).range →
    (g, h) ∈ I

Tactic:
· intro hgh
      simpa only [G', H', mem_map, MonoidHom.mem_range, MonoidHom.prod_apply, Subtype.exists,
        Prod.exists, MonoidHom.coe_prodMap, coe_subtype, Prod.mk.injEq, Prod.map_apply,
        MonoidHom.coe_snd, exists_eq_right, exists_and_right, exists_eq_right_right,
        MonoidHom.coe_fst]
        using ⟨⟨h, hgh⟩, ⟨g, hgh⟩, g, h, hgh, ⟨rfl, rfl⟩⟩

Goal state after:
case mpr
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := ⋯
H' : Subgroup H := ⋯
P : ↥I →* ↥G' := ⋯
Q : ↥I →* ↥H' := ⋯
I' : Subgroup (↥G' × ↥H') := ⋯
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : G
h : H
⊢ (g, h) ∈ map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype) (P.prod Q).range →
    (g, h) ∈ I
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
⊢ nilpotencyClass G ≤ 1 ↔ IsMulCommutative G

Tactic:
rw [← upperCentralSeries_eq_top_iff_nilpotencyClass_le]
  exact upperCentralSeries_one_eq_top_iff

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ (upperCentralSeries G '' Set.Iic a).ncard = a + 1

Tactic:
by
  refine Set.ncard_eq_of_bijective (fun _ => upperCentralSeries G ·) ?_ ?_ ?_
  · grind
  · grind
  · intros i j hi hj
    refine (upperCentralSeries.StrictMonoOn G).injOn ?_ ?_ <;> grind

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

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsSimpleOrder ↑(Set.Ici (stabilizer G a)) ↔ IsSimpleOrder (BlockMem G a)

Tactic:
simp only [isSimpleOrder_iff_isCoatom_bot]

Goal state after:
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsCoatom ⊥ ↔ IsCoatom ⊥
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
a : α
ha : a ∉ fixedPoints (↥N) α
h : (orbit (↥N) a).Subsingleton
n : ↥N
this : orbit (↥N) a = {a}
⊢ n • a ∈ {a}

Tactic:
rw [← this]; use n

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Embedding

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : ↑s.ncard + ↑n ≤ ENat.card α
hα : Finite α
⊢ Nonempty (Fin n ↪ ↑sᶜ)

Tactic:
let _ : Fintype α := Fintype.ofFinite α

Goal state after:
case inl
α : Type u_1
n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : ↑s.ncard + ↑n ≤ ENat.card α
hα : Finite α
x✝ : Fintype α := Fintype.ofFinite α
⊢ Nonempty (Fin n ↪ ↑sᶜ)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
a b : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: b :: l, g.IsSwap
hn : (b :: l).length = 2 * n + 1
⊢ (a :: b :: l).prod ∈ closure {σ | σ.IsThreeCycle}

Tactic:
List.prod_cons,

Goal state after:
case succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
a b : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: b :: l, g.IsSwap
hn : (b :: l).length = 2 * n + 1
⊢ a * (b :: l).prod ∈ closure {σ | σ.IsThreeCycle}
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
a b : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: b :: l, g.IsSwap
hn : (b :: l).length = 2 * n + 1
⊢ a * (b :: l).prod ∈ closure {σ | σ.IsThreeCycle}

Tactic:
List.prod_cons,

Goal state after:
case succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
a b : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: b :: l, g.IsSwap
hn : (b :: l).length = 2 * n + 1
⊢ a * (b * l.prod) ∈ closure {σ | σ.IsThreeCycle}
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
m n : ℕ
inst✝¹ : IsMultiplyPreprimitive M α n
s : Set α
inst✝ : Finite ↑s
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = ↑m
t' : Set α := ⋯
htt' : t = Subtype.val ⁻¹' t'
⊢ (s ∪ t').encard + 1 = ↑n

Tactic:
Set.encard_union_eq _

Goal state after:
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
m n : ℕ
inst✝¹ : IsMultiplyPreprimitive M α n
s : Set α
inst✝ : Finite ↑s
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ s.encard + t'.encard + 1 = ↑n

M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
m n : ℕ
inst✝¹ : IsMultiplyPreprimitive M α n
s : Set α
inst✝ : Finite ↑s
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Disjoint s t'
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: 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
hn1 : 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 α := ⋯
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
this : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
hs_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ s.ncard + (g • s).ncard < Nat.card α

Tactic:
rwa [Set.ncard_smul_set, hsn, ← two_mul]

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

Goal state before:
pp: 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
hn1 : 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 α := ⋯
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
hs_trans : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ s.ncard + (g • s).ncard < Nat.card α

Tactic:
rwa [Set.ncard_smul_set, hsn, ← two_mul]

Goal state after:
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 : ∀ (a b : α) (g : M), a ∈ s → b ∈ sᶜ → g • a ≠ b
⊢ ∀ g ∈ ⊤, g • s ⊆ s

Tactic:
rintro g _ b ⟨a, ha, hgab⟩

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 : ∀ (a b : α) (g : M), a ∈ s → b ∈ sᶜ → g • a ≠ b
g : M
a✝ : g ∈ ⊤
b a : α
ha : a ∈ s
hgab : (fun x ↦ g • x) a = b
⊢ b ∈ s