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

Goal state before:
pp: case append
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord G i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord G k✝ l✝
_w₁_ih✝ : _w₁✝.inv.prod = _w₁✝.prod⁻¹
_w₂_ih✝ : _w₂✝.inv.prod = _w₂✝.prod⁻¹
⊢ (_w₁✝.append _hne✝ _w₂✝).inv.prod = (_w₁✝.append _hne✝ _w₂✝).prod⁻¹

Tactic:
simp [inv, *]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case singleton
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j i✝ : ι
x✝ : G i✝
a✝ : x✝ ≠ 1
⊢ (singleton x✝ a✝).inv.head = (singleton x✝ a✝).last⁻¹

Tactic:
simp [inv, *]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord G i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord G k✝ l✝
_w₁_ih✝ : _w₁✝.inv.head = _w₁✝.last⁻¹
_w₂_ih✝ : _w₂✝.inv.head = _w₂✝.last⁻¹
⊢ (_w₁✝.append _hne✝ _w₂✝).inv.head = (_w₁✝.append _hne✝ _w₂✝).last⁻¹

Tactic:
simp [inv, *]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case singleton
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j i✝ : ι
x✝ : G i✝
a✝ : x✝ ≠ 1
⊢ (singleton x✝ a✝).inv.last = (singleton x✝ a✝).head⁻¹

Tactic:
simp [inv, *]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord G i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord G k✝ l✝
_w₁_ih✝ : _w₁✝.inv.last = _w₁✝.head⁻¹
_w₂_ih✝ : _w₂✝.inv.last = _w₂✝.head⁻¹
⊢ (_w₁✝.append _hne✝ _w₂✝).inv.last = (_w₁✝.append _hne✝ _w₂✝).head⁻¹

Tactic:
simp [inv, *]

Goal state after:
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‖ ≤ δ
⊢ 0 ≤ r'

Tactic:
linarith

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this :
  ((a + b).num * ↑a.den * ↑b.den * (↑↑s * ↑↑s)) • m =
    ((a.num * ↑b.den + b.num * ↑a.den) * ↑(a + b).den * (↑↑s * ↑↑s)) • m
⊢ ↑1 • ↑(⟨a.den, ⋯⟩ * s * (⟨b.den, ⋯⟩ * s)) • (a + b).num • m =
    ↑1 • ↑(⟨(a + b).den, ⋯⟩ * s) • (↑(⟨b.den, ⋯⟩ * s) • a.num • m + ↑(⟨a.den, ⋯⟩ * s) • b.num • m)

Tactic:
by
      convert! this using 1
      all_goals
      simp [← natCast_zsmul, smul_smul, ← add_smul]
      ring_nf

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
x : Quot ⇑(leftRel K)
y : G
hy : ⟦y⟧ = x
cover : ¬∃ i, y ∈ doubleCoset (out i) ↑H ↑K
⊢ ¬⋃ q, quotToDoubleCoset H K q = Set.univ

Tactic:
exact (Set.ne_univ_iff_exists_notMem _).mpr ⟨y, by simpa using! cover⟩

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
x : Quot ⇑(rightRel H)
y : G
hy : ⟦y⟧ = x
cover : ¬∃ i, y ∈ doubleCoset (out i) ↑H ↑K
⊢ ¬⋃ q, quotToDoubleCoset H K q = Set.univ

Tactic:
exact (Set.ne_univ_iff_exists_notMem _).mpr ⟨y, by simpa using! cover⟩

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : ↥H →* A
inst✝¹ : H.FiniteIndex
g : G
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ ∏ a,
      ∏ s,
        ϕ
          ⟨(↑(⋯.leftQuotientEquiv ((H.quotientEquivSigmaZMod g).symm ⟨a, s⟩)))⁻¹ *
              ↑(⋯.leftQuotientEquiv ((H.quotientEquivSigmaZMod g).symm ⟨a, s⟩)),
            ⋯⟩ =
    ∏ q, ϕ ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x ↦ g • x) q.out * Quotient.out q.out, ⋯⟩

Tactic:
refine Fintype.prod_congr _ _ (fun q => ?_)

Goal state after:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : ↥H →* A
inst✝¹ : H.FiniteIndex
g : G
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
⊢ ∏ s,
      ϕ
        ⟨(↑(⋯.leftQuotientEquiv ((H.quotientEquivSigmaZMod g).symm ⟨q, s⟩)))⁻¹ *
            ↑(⋯.leftQuotientEquiv ((H.quotientEquivSigmaZMod g).symm ⟨q, s⟩)),
          ⋯⟩ =
    ϕ
      ⟨(Quotient.out (Quotient.out q))⁻¹ * g ^ Function.minimalPeriod (fun x ↦ g • x) (Quotient.out q) *
          Quotient.out (Quotient.out q),
        ⋯⟩
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
hR : IsComplement (↑H) R₀
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
⊢ ∃ T, #T ≤ H.index * #S ∧ closure ↑T = ⊤

Tactic:
let R : Finset G := Set.toFinset R₀

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
hR : IsComplement (↑H) R₀
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
⊢ ∃ T, #T ≤ H.index * #S ∧ closure ↑T = ⊤
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' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
this : SemidirectProduct.rightHom.comp F' = MonoidHom.id G
⊢ ∀ (g : G), (F' g).right = g

Tactic:
by
        exact DFunLike.ext_iff.mp this

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ ∀ (i j : ℕ), i < a + 1 → j < a + 1 → upperCentralSeries G i = upperCentralSeries G j → i = j

Tactic:
intros i j hi hj
    refine (upperCentralSeries.StrictMonoOn G).injOn ?_ ?_ <;> grind

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
C : SubMulAction G X
B : Set ↥C
g₁ g₂ : G
⊢ g₁ • ⇑C.inclusion '' B ≠ g₂ • ⇑C.inclusion '' B → Disjoint (g₁ • ⇑C.inclusion '' B) (g₂ • ⇑C.inclusion '' B) ↔
    g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)

Tactic:
← image_smul_set,

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g₁ g₂ : G
⊢ ⇑C.inclusion '' (g₁ • B) ≠ g₂ • ⇑C.inclusion '' B → Disjoint (⇑C.inclusion '' (g₁ • B)) (g₂ • ⇑C.inclusion '' B) ↔
    g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g₁ g₂ : G
⊢ ⇑C.inclusion '' (g₁ • B) ≠ g₂ • ⇑C.inclusion '' B → Disjoint (⇑C.inclusion '' (g₁ • B)) (g₂ • ⇑C.inclusion '' B) ↔
    g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)

Tactic:
← image_smul_set,

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g₁ g₂ : G
⊢ ⇑C.inclusion '' (g₁ • B) ≠ ⇑C.inclusion '' (g₂ • B) → Disjoint (⇑C.inclusion '' (g₁ • B)) (⇑C.inclusion '' (g₂ • B)) ↔
    g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)

Tactic:
simp only [this]
    apply (hB.smul_eq_or_disjoint ⟨h, hH⟩).imp
    · intro; congr
    · exact Set.disjoint_image_of_injective (MulAction.injective g)

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
⊢ IsBlock G ↑s

Tactic:
simp only [IsBlock, disjoint_left]
  rintro a b hab _ ⟨c, hc, rfl⟩ ⟨d, hd, (hcd : b • d = a • c)⟩
  refine hab ?_
  rw [← smul_coe_set hc, ← smul_assoc, ← hcd, smul_assoc, smul_coe_set hc, smul_coe_set hd]

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
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g ∈ stabilizer G a
⊢ g • a ∈ g • B

Tactic:
smul_mem_smul_set_iff

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
a : X
ha : a ∈ B
g : G
hg : g ∈ stabilizer G a
⊢ a ∈ B
Module: Mathlib.GroupTheory.GroupAction.Iwasawa

Goal state before:
pp: case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints (↥N) α = Set.univ
n : M
hn : n ∈ N
x : α
⊢ n • x = 1 • x

Tactic:
one_smul

Goal state after:
case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints (↥N) α = Set.univ
n : M
hn : n ∈ N
x : α
⊢ n • x = x
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case h
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : Nontrivial X
a : X
h : ⊥ = ⊤
⊢ False

Tactic:
rw [← Subtype.coe_inj] at h

Goal state after:
case h
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : Nontrivial X
a : X
h : ↑⊥ = ↑⊤
⊢ False
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : ¬2 * (orbit G B).ncard ≤ B.ncard * (orbit G B).ncard
h : B.Nonempty
⊢ B.ncard < 2

Tactic:
← not_le

Goal state after:
case inr
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : ¬2 * (orbit G B).ncard ≤ B.ncard * (orbit G B).ncard
h : B.Nonempty
⊢ ¬2 ≤ B.ncard
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case inr
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
⊢ IsTrivialBlock B

Tactic:
· obtain ⟨g, hg⟩ := exists_smul_eq G b a
      rw [← IsTrivialBlock.smul_iff g]
      apply H _ (hB.translate g)
      rw [← hg]
      use b

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
⊢ (alternatingGroup α).index = 1

Tactic:
by
  rw [Subgroup.index_eq_one]; apply Subsingleton.elim

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : g • x (Fin.last n) = a
i : Fin n
this : (Fin.Embedding.init (g • x)) i = (g • x) i.castSucc
⊢ ¬(Fin.Embedding.init (g • x)) i = (g • x) (Fin.last n)

Tactic:
simp [this]

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ᶜ)

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

Tactic:
· let _ : Fintype α := Fintype.ofFinite α
    classical
    apply nonempty_of_card_le
    rwa [Fintype.card_fin, ← add_le_add_iff_left s.ncard,
      ← Nat.card_eq_fintype_card, Nat.card_coe_set_eq,
        ncard_add_ncard_compl, ← ENat.natCast_le_natCast,
        ← ENat.card_eq_coe_natCard, ENat.natCast_add]

Goal state after:
case inr
α : Type u_1
n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : ↑s.ncard + ↑n ≤ ENat.card α
hα : Infinite α
⊢ Nonempty (Fin n ↪ ↑sᶜ)
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
a₁✝ a₂✝ : ι ↪ α
hxy : (mulActionHom_embedding ι hf) a₁✝ = (mulActionHom_embedding ι hf) a₂✝
x✝ : ι
⊢ a₁✝ x✝ = a₂✝ x✝

Tactic:
apply hf

Goal state after:
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
a₁✝ a₂✝ : ι ↪ α
hxy : (mulActionHom_embedding ι hf) a₁✝ = (mulActionHom_embedding ι hf) a₂✝
x✝ : ι
⊢ f (a₁✝ x✝) = f (a₂✝ x✝)
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: case h₂
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 y : B
hy :
  ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ <
    2
A :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
      Trivialization.symmL ℝ (trivializationAt F E x) x =
    ContinuousLinearMap.id ℝ F
this :
  Trivialization.symmL ℝ (trivializationAt F E x) y =
    Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL ContinuousLinearMap.id ℝ F
⊢ ‖Trivialization.symmL ℝ (trivializationAt F E x) x‖ < 1 + ‖Trivialization.symmL ℝ (trivializationAt F E x) x‖

Tactic:
linarith

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this✝ : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j✝.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j < Fintype.card α - 1
this : i = j
⊢ (g • x) i = (k • x) i

Tactic:
by
          rw [← this, ← hi] at hj
          exact (lt_irrefl _ hj).elim

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hn : IsMultiplyPreprimitive M α n
m : ℕ
hmn : m ≤ n
hα : ↑n ≤ ENat.card α
⊢ IsMultiplyPreprimitive M α m

Tactic:
by
  induction n with
  | zero => rw [Nat.eq_zero_of_le_zero hmn]; exact hn
  | succ n hrec =>
    rcases Nat.eq_or_lt_of_le hmn with hmn | hmn'
    · rw [hmn]; exact hn
    · apply hrec
        (isMultiplyPreprimitive_of_isMultiplyPretransitive_succ M α hα)
        (Nat.lt_succ_iff.mp hmn')
      · refine le_trans ?_ hα; rw [ENat.natCast_le_natCast]; exact Nat.le_succ n

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

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
⊢ 1 • a = a

Tactic:
one_smul

Goal state after:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
⊢ a = a
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]
  contrapose! hM
  rw [eq_top_iff, le_stabilizer_iff_smul_le]
  rintro g _ b ⟨a, ha, hgab⟩
  by_contra hb
  exact hM a b g ha (Set.mem_compl hb) hgab

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = -1
x : ↑s
this : k ↑x = ↑x
⊢ ↑((toPerm ⟨⟨Perm.ofSubtype g * k, ⋯⟩, ⋯⟩) x) = ↑(g x)

Tactic:
simp [this]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
this : stabilizer (↥(alternatingGroup α)) s = ⊤
⊢ ∀ (g : ↥(alternatingGroup α)), g ∈ stabilizer (↥(alternatingGroup α)) s

Tactic:
simp [this]

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
⊢ sᶜ ⊆ B

Tactic:
have not_isBlock_sc : ¬ IsBlock G sᶜ := fun hsc ↦ by
    rcases lt_or_ge (Nat.card α) (sᶜ.ncard * 2) with hB' | hB'
    · apply h0.ne_empty
      rw [← compl_univ_iff]
      exact hsc.eq_univ_of_card_lt hB'
    · rw [← not_lt] at hB'
      apply hB'
      rwa [← Set.ncard_add_ncard_compl sᶜ, mul_two, add_lt_add_iff_left, compl_compl]

Goal state after:
α : 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
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
⊢ sᶜ ⊆ B
Module: Mathlib.GroupTheory.GroupExtension.Defs

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
n : N
⊢ S.rightHom (S.inl n) = 1

Tactic:
exact S.rightHom_inl n

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
inst✝ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
⊢ toPerm g = 1 ↔ toPerm g = 1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · contrapose h with h
    have : ∃ a, (g • a : α) ≠ a := by simpa [Equiv.ext_iff] using h
    obtain ⟨a, ha⟩ := this
    obtain ⟨s, has, has'⟩ := exists_mem_notMem hn hα (Ne.symm ha)
    rw [Equiv.ext_iff, not_forall]
    use s
    contrapose! has'
    simp only [toPerm_apply, coe_one, id_eq] at has'
    rw [← has']
    simpa only [coe_smul, smul_mem_smul_finset_iff, ← mem_coe_iff]
  · simp only [Equiv.ext_iff, toPerm_apply] at h ⊢
    simp [Subtype.ext_iff, Finset.ext_iff, mem_smul_finset, h]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
inst✝ : DecidableEq α
s : Finset α
hs : s ∈ powersetCard α n
⊢ Fintype.card ?m.29 = #?m.32

Tactic:
by rw [hs, Fintype.card_fin]

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

Goal state before:
pp: case inr.inl
α✝ : Type u_2
n : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * 1 ≤ Nat.card α
hn0 : 1 ≠ 0
⊢ IsPretransitive (↥(alternatingGroup α)) α

Tactic:
exact alternatingGroup.isPretransitive_of_three_le_card α 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
H : Type u_2
inst✝¹ : Group H
M : Type u_3
inst✝ : Monoid M
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
⊢ (g : G) → g ∈ toSubgroup A B u ∧ none = some (-u) → NormalWord d

Tactic:
tauto

Goal state after:
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : Monoid P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
mn : M × N
⊢ (f.noncommCoprod g comm) mn = g mn.2 * f mn.1

Tactic:
by
  rw [← comm, MonoidHom.noncommCoprod_apply]

Goal state after:
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
x : N
hx : x ∈ Multiset.filter (fun x ↦ ¬IsUnit x) (Multiset.map (⇑f) (factors m))
⊢ Prime x

Tactic:
Multiset.mem_filter,

Goal state after:
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
x : N
hx : x ∈ Multiset.map (⇑f) (factors m) ∧ ¬IsUnit x
⊢ Prime x
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
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))

Tactic:
set n := Nat.find (a.sameCycle hx'').exists_nat_pow_eq

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
⊢ a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))