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

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✝ : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u u' : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F n s u
hu'u : u' ⊆ u
x : M
⊢ x ∈ u' → ⊤ ≤ Submodule.span 𝕜 (Set.range fun x_1 ↦ s x_1 x)

Tactic:
hx

Goal state after:
𝕜 : 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✝ : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u u' : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F n s u
hu'u : u' ⊆ u
x : M
hx : x ∈ u'
⊢ ⊤ ≤ Submodule.span 𝕜 (Set.range fun x_1 ↦ s x_1 x)
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

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
n : ℕ∞ω
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✝³ : FiberBundle F V
inst✝² : VectorBundle 𝕜 F V
inst✝¹ : ContMDiffVectorBundle n F V I
ι : Type u_7
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
b : Basis ι 𝕜 F
x : M
⊢ x ∈ e.baseSet → LinearIndependent 𝕜 fun x_1 ↦ e.localFrame b x_1 x

Tactic:
hx

Goal state after:
𝕜 : 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
n : ℕ∞ω
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✝³ : FiberBundle F V
inst✝² : VectorBundle 𝕜 F V
inst✝¹ : ContMDiffVectorBundle n F V I
ι : Type u_7
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
b : Basis ι 𝕜 F
x : M
hx : x ∈ e.baseSet
⊢ LinearIndependent 𝕜 fun x_1 ↦ e.localFrame b x_1 x
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

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
n : ℕ∞ω
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✝³ : FiberBundle F V
inst✝² : VectorBundle 𝕜 F V
inst✝¹ : ContMDiffVectorBundle n F V I
ι : Type u_7
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
b : Basis ι 𝕜 F
x : M
⊢ x ∈ e.baseSet → ⊤ ≤ Submodule.span 𝕜 (Set.range fun x_1 ↦ e.localFrame b x_1 x)

Tactic:
hx

Goal state after:
𝕜 : 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
n : ℕ∞ω
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✝³ : FiberBundle F V
inst✝² : VectorBundle 𝕜 F V
inst✝¹ : ContMDiffVectorBundle n F V I
ι : Type u_7
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
b : Basis ι 𝕜 F
x : M
hx : x ∈ e.baseSet
⊢ ⊤ ≤ Submodule.span 𝕜 (Set.range fun x_1 ↦ e.localFrame b x_1 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
s : Set M
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov : IsCovariantDerivativeOn F cov s
cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov' : IsCovariantDerivativeOn F cov' s
g : M → 𝕜
σ✝ : (x : M) → V x
g✝ : M → 𝕜
x✝ : M
hσ : MDiffAt (T% σ✝) x✝
hφ : MDiffAt g✝ x✝
hx : x✝ ∈ s
⊢ (g • cov (g✝ • σ✝) + (1 - g) • cov' (g✝ • σ✝)) x✝ =
    g✝ x✝ • (g • cov σ✝ + (1 - g) • cov' σ✝) x✝ + (d% g✝ x✝).smulRight (σ✝ x✝)

Tactic:
simp [hcov.leibniz hσ hφ, hcov'.leibniz hσ hφ]

Goal state after:
𝕜 : 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
s : Set M
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov : IsCovariantDerivativeOn F cov s
cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov' : IsCovariantDerivativeOn F cov' s
g : M → 𝕜
σ✝ : (x : M) → V x
g✝ : M → 𝕜
x✝ : M
hσ : MDiffAt (T% σ✝) x✝
hφ : MDiffAt g✝ x✝
hx : x✝ ∈ s
⊢ g x✝ • g✝ x✝ • cov σ✝ x✝ + g x✝ • (d% g✝ x✝).smulRight (σ✝ x✝) +
      ((1 - g x✝) • g✝ x✝ • cov' σ✝ x✝ + (1 - g x✝) • (d% g✝ x✝).smulRight (σ✝ x✝)) =
    g✝ x✝ • g x✝ • cov σ✝ x✝ + g✝ x✝ • (1 - g x✝) • cov' σ✝ x✝ + (d% g✝ x✝).smulRight (σ✝ x✝)
Module: Mathlib.Geometry.Manifold.WhitneyEmbedding

Goal state before:
pp: ι : Type uι
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
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
⊢ x ∈ s → ∀ ⦃x₂ : M⦄, x₂ ∈ s → f.embeddingPiTangent x = f.embeddingPiTangent x₂ → x = x₂

Tactic:
hx

Goal state after:
ι : Type uι
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
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ ∀ ⦃x₂ : M⦄, x₂ ∈ s → f.embeddingPiTangent x = f.embeddingPiTangent x₂ → x = x₂
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G

Tactic:
classical
  cases nonempty_fintype G
  simp [← sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype]

Goal state after:
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ Nat.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier = Nat.card G

Tactic:
by
  classical
  cases nonempty_fintype G
  rw [@Nat.card_eq_fintype_card G, ← sum_conjClasses_card_eq_card, ←
    Finset.sum_sdiff (ConjClasses.noncenter G).toFinset.subset_univ]
  simp only [Nat.card_eq_fintype_card, Set.toFinset_card]
  congr 1
  swap
  · convert! finsum_cond_eq_sum_of_cond_iff _ _
    simp [Set.mem_toFinset]
  calc
    Fintype.card (Subgroup.center G) = Fintype.card ((noncenter G)ᶜ : Set _) :=
      Fintype.card_congr ((mk_bijOn G).equiv _)
    _ = Finset.card (Finset.univ \ (noncenter G).toFinset) := by
      rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
    _ = _ := ?_
  rw [Finset.card_eq_sum_ones]
  refine Finset.sum_congr rfl ?_
  rintro ⟨g⟩ hg
  simp only [noncenter, Set.toFinset_ofPred, Finset.mem_univ, true_and,
             Finset.mem_sdiff, Finset.mem_filter, Set.not_nontrivial_iff] at hg
  rw [eq_comm, ← Set.toFinset_card, Finset.card_eq_one]
  exact ⟨g, Finset.coe_injective <| by simpa using hg.eq_singleton_of_mem mem_carrier_mk⟩

Goal state after:
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ Nat.card ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) = Nat.card ↥(_root_.commutator G)

Tactic:
rw [commutator_eq_closure G, ← image_commutatorSet_closureCommutatorRepresentatives, ←
    MonoidHom.map_closure, ← commutator_eq_closure]

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ Nat.card ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) =
    Nat.card
      ↥(map (closureCommutatorRepresentatives G).subtype (_root_.commutator ↥(closureCommutatorRepresentatives G)))
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inr.a
n : ℕ
hn : NeZero n
⊢ ∀ (g : DihedralGroup n), g ^ lcm n 2 = 1

Tactic:
rintro (m | m)

Goal state after:
case inr.a.r
n : ℕ
hn : NeZero n
m : ZMod n
⊢ r m ^ lcm n 2 = 1

case inr.a.sr
n : ℕ
hn : NeZero n
m : ZMod n
⊢ sr m ^ lcm n 2 = 1
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
⊢ commProb (DihedralGroup 3) * commProb (Product (reciprocalFactors (n / 2))) = 1 / ↑n

Tactic:
commProb_reciprocal (n / 2),

Goal state after:
case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
⊢ commProb (DihedralGroup 3) * (1 / ↑(n / 2)) = 1 / ↑n
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ commProb (DihedralGroup (n % 4 * n)) * (1 / ↑(n / 4 + 1)) = 1 / ↑n

Tactic:
rw [commProb_odd (hn.mul h2), div_mul_div_comm, div_eq_div_iff]

Goal state after:
case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ (↑(n % 4 * n) + 3) * 1 * ↑n = 1 * (4 * ↑(n % 4 * n) * ↑(n / 4 + 1))

case neg.inr.hb
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ 4 * ↑(n % 4 * n) * ↑(n / 4 + 1) ≠ 0

case neg.inr.hd
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ ↑n ≠ 0
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, w = cs.simple i) → cs.length w = 1

Tactic:
rintro ⟨i, rfl⟩

Goal state after:
case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.length (cs.simple i) = 1
Module: Mathlib.GroupTheory.Coxeter.Length

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

Tactic:
exact (cs.length_simple_mul w i).resolve_right (by lia)

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

Goal state before:
pp: case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD j' ((MulAut.conj (cs.simple i)) 1) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (i :: ω)[j' + 1]?).getD ((MulAut.conj (cs.simple i)) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹

Tactic:
rw [getD_map]

Goal state after:
case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (MulAut.conj (cs.simple i)) ((cs.leftInvSeq ω).getD j' 1) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (i :: ω)[j' + 1]?).getD ((MulAut.conj (cs.simple i)) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₁✝.toList
_w₂_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₂✝.toList
x : (i : ι) × M i
⊢ x ∈ _w₁✝.toList.getLast? → ∀ y ∈ _w₂✝.toList.head?, x.fst ≠ y.fst

Tactic:
hx

Goal state after:
case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₁✝.toList
_w₂_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₂✝.toList
x : (i : ι) × M i
hx : x ∈ _w₁✝.toList.getLast?
⊢ ∀ y ∈ _w₂✝.toList.head?, x.fst ≠ y.fst
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
h : G → ℝ
C : ℝ
H : ∀ (x y : G), |h (x * y) + h (x / y) - 2 * (h x + h y)| ≤ C
inst✝ : Northcott h
⊢ Finite ↥(torsion G)

Tactic:
by
  have H' x : 4 * h x - (h 1 + C) ≤ h (x ^ 2) := by grind [pow_two, div_self']
  exact finite_torsion_of_descent (b := 4) (by norm_num) H'

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : Type u_4
inst✝² : Group G
H : ι → Type u_5
inst✝¹ : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
i j k : ι
w : NeWord H i j
hhead : k ≠ i
hlast : k ≠ j
⊢ (lift f) w.prod ≠ 1

Tactic:
by
  intro heq1
  have : X k ⊆ X i := by simpa [heq1] using lift_word_ping_pong f X hpp w hlast.symm
  obtain ⟨x, hx⟩ := hXnonempty k
  exact (hXdisj hhead).le_bot ⟨hx, this hx⟩

Goal state after:
Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Type u_2
N : Type u_3
inst✝¹ : Group H
inst✝ : Group N
f : G →* H
K : FiniteIndexNormalSubgroup H
⊢ (Subgroup.comap f K.toSubgroup).FiniteIndex

Tactic:
by
    let g : G →* (H ⧸ K.toSubgroup) := (QuotientGroup.mk' K.toSubgroup).comp f
    have hker : K.toSubgroup.comap f = g.ker := by
      simpa using MonoidHom.comap_ker (g := QuotientGroup.mk' K.toSubgroup) (f := f)
    simpa [hker] using (inferInstance : g.ker.FiniteIndex)

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ g ^ ((H.quotientEquivSigmaZMod g) ((H.quotientEquivSigmaZMod g).symm ⟨q, k⟩)).snd.cast *
      Quotient.out (Quotient.out ((H.quotientEquivSigmaZMod g) ((H.quotientEquivSigmaZMod g).symm ⟨q, k⟩)).fst) =
    g ^ k.cast * Quotient.out (Quotient.out q)

Tactic:
apply_symm_apply

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ g ^ ⟨q, k⟩.snd.cast * Quotient.out (Quotient.out ⟨q, k⟩.fst) = g ^ k.cast * Quotient.out (Quotient.out q)
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ ⊤ ≤ closure ((fun g ↦ ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) '' (R * S))

Tactic:
← map_subtype_le_map_subtype,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ map H.subtype ⊤ ≤ map H.subtype (closure ((fun g ↦ ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) '' (R * S)))
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Finite α
⊢ IsFinitelyPresented (FreeGroup α)

Tactic:
have ⟨n, _, f, hf_surj, hf_inj⟩ := Finite.exists_equiv_fin α

Goal state after:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Finite α
n : ℕ
toFun✝ : α → Fin n
f : Fin n → α
hf_surj : Function.LeftInverse f toFun✝
hf_inj : Function.RightInverse f toFun✝
⊢ IsFinitelyPresented (FreeGroup α)
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
⊢ (transferSylow P hP).ker.IsComplement' ↑P

Tactic:
have hf : Function.Bijective ((transferSylow P hP).domRestrict (P : Subgroup G)) :=
    (transferSylow_domRestrict_eq_pow P hP).symm ▸ (P.2.powEquiv' P.not_dvd_index).bijective
  rw [Function.Bijective, ← range_eq_top, domRestrict_range] at hf
  have := range_eq_top.mp (top_le_iff.mp (hf.2.ge.trans
    (map_le_range (transferSylow P hP) P)))
  rw [← (comap_injective this).eq_iff, comap_top, comap_map_eq, sup_comm, SetLike.ext'_iff,
    normal_mul, ← ker_eq_bot_iff, ← map_subtype_inj,
    ker_domRestrict, subgroupOf_map_subtype, Subgroup.map_bot, coe_top] at hf
  exact isComplement'_of_disjoint_and_mul_eq_univ (disjoint_iff.2 hf.1) hf.2

Goal state after:
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)
⊢ normalizer ↑P ≤ centralizer ↑P

Tactic:
have key := card_dvd_of_injective _ (QuotientGroup.kerLift_injective P.normalizerMonoidHom)

Goal state after:
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 : Nat.card (↥(normalizer ↑↑P) ⧸ (↑P).normalizerMonoidHom.ker) ∣ Nat.card (MulAut ↥↑P)
⊢ normalizer ↑P ≤ centralizer ↑P
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
⊢ x ∈ H (n + 1) → x ∈ upperCentralSeries G (n + 1)

Tactic:
hx

Goal state after:
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
hx : x ∈ H (n + 1)
⊢ x ∈ upperCentralSeries G (n + 1)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ
x : G
⊢ x ∈ upperCentralSeries G n → x ∈ upperCentralSeries G (n + 1)

Tactic:
hx

Goal state after:
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
⊢ x ∈ upperCentralSeries G (n + 1)
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: G A : Type u
inst✝² : Group G
inst✝¹ : IsFreeGroup G
inst✝ : MulAction G A
⊢ ∀ {X : Type u} [inst : Group X] (f : Labelling (Generators (ActionCategory G A)) X),
    ∃! F, ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), F.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g

Tactic:
by
    intro X _ f
    let f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e =>
      ⟨fun b => @f ⟨(), _⟩ ⟨(), b⟩ ⟨e, smul_inv_smul _ b⟩, IsFreeGroup.of e⟩
    rcases IsFreeGroup.unique_lift f' with ⟨F', hF', uF'⟩
    refine ⟨uncurry F' ?_, ?_, ?_⟩
    · suffices SemidirectProduct.rightHom.comp F' = MonoidHom.id _ by
        exact DFunLike.ext_iff.mp this
      apply IsFreeGroup.ext_hom (fun x ↦ ?_)
      rw [MonoidHom.comp_apply, hF']
      rfl
    · rintro ⟨⟨⟩, a : A⟩ ⟨⟨⟩, b⟩ ⟨e, h : IsFreeGroup.of e • a = b⟩
      change (F' (IsFreeGroup.of _)).left _ = _
      rw [hF']
      cases inv_smul_eq_iff.mpr h.symm
      rfl
    · intro E hE
      have : curry E = F' := by
        apply uF'
        intro e
        ext
        · convert! hE _ _ _
          rfl
        · rfl
      apply Functor.hext
      · intro
        apply Unit.ext
      · refine ActionCategory.cases ?_
        intros
        simp only [← this, uncurry_map, curry_apply_left, coe_back, homOfPair.val]
        rfl

Goal state after:
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
⊢ H.Normal

Tactic:
by_cases hG1 : Nat.card G = 1

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : Nat.card G = 1
⊢ H.Normal

case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
⊢ H.Normal
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
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
g : G
hg : a ∈ g • B'
x : X
⊢ x ∈ B' → x ∈ g • B'

Tactic:
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
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
⊢ x ∈ g • B'
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case mpr
M : Type u_3
inst✝³ : Group M
α : Type u_4
inst✝² : MulAction M α
N : Type u_5
β : Type u_6
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPreprimitive N β → IsPreprimitive M α

Tactic:
· intro _
    have := (isPretransitive_congr hφ hf).mpr toIsPretransitive
    exact {
      isTrivialBlock_of_isBlock {B} hB := by
        rw [← Set.preimage_image_eq B hf.injective]
        exact IsTrivialBlock.preimage hf.injective
          (isTrivialBlock_of_isBlock (hB.image f hφ hf.injective)) }

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

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

pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nat.card α ≤ 3
h✝ : Nontrivial α
⊢ IsCyclic ↥(alternatingGroup α)

Tactic:
· infer_instance

Goal state after:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nat.card α ≤ 3
h✝ : Nontrivial α
⊢ IsCyclic ↥(alternatingGroup α)