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

Goal state before:
pp: case refine_2
𝕜 : 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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : (MDiffAt fun x ↦ ⟨x, 0⟩) x
B : (fderivWithin 𝕜 (fun x' ↦ (x', 0)) (range ↑I ∩ ↑I.symm ⁻¹' (chartAt H x).target) (↑I (↑(chartAt H x) x))) v = (v, 0)
⊢ (↑I (↑(ChartedSpace.chartAt x) (↑(ChartedSpace.chartAt x).symm (↑I.symm (↑I (↑(chartAt H x) x))))), 0) =
    (↑I (↑(chartAt H x) x), 0)

Tactic:
simp only [mfld_simps]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
⊢ ContMDiffAt (I.tangent.prod I'.tangent) (I.prod I') n (fun x ↦ ((equivTangentBundleProd I M I' M').symm x).proj)
      (a, b) ∧
    ContMDiffAt (I.tangent.prod I'.tangent) 𝓘(𝕜, E × E') n
      (fun x ↦
        (↑(trivializationAt (E × E') (TangentSpace (I.prod I')) ((equivTangentBundleProd I M I' M').symm (a, b)).proj)
            ((equivTangentBundleProd I M I' M').symm x)).2)
      (a, b)

Tactic:
simp only [equivTangentBundleProd, TangentBundle.trivializationAt_apply, mfld_simps,
    Equiv.coe_fn_symm_mk]

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
⊢ ContMDiffAt (I.tangent.prod I'.tangent) (I.prod I') n (fun x ↦ (x.1.proj, x.2.proj)) (a, b) ∧
    ContMDiffAt (I.tangent.prod I'.tangent) 𝓘(𝕜, E × E') n
      (fun x ↦
        (fderivWithin 𝕜
            (((fun p ↦ (↑I p.1, ↑I' p.2)) ∘ fun p ↦ (↑(chartAt H a.proj) p.1, ↑(chartAt H' b.proj) p.2)) ∘
              ↑((chartAt H x.1.proj).prod (chartAt H' x.2.proj).toPartialEquiv).symm ∘ ↑(I.prod I'.toPartialEquiv).symm)
            (range (Prod.map ↑I ↑I')) (↑I (↑(chartAt H x.1.proj) x.1.proj), ↑I' (↑(chartAt H' x.2.proj) x.2.proj)))
          (x.1.snd, x.2.snd))
      (a, b)
Module: Mathlib.Geometry.Manifold.Sheaf.Smooth

Goal state before:
pp: 𝕜 : Type u_1
inst✝²⁶ : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝²⁵ : NormedAddCommGroup EM
inst✝²⁴ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝²³ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace 𝕜 E
H : Type u_5
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst✝¹⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace HM M
N G A A' R : Type u
inst✝¹⁶ : TopologicalSpace N
inst✝¹⁵ : ChartedSpace H N
inst✝¹⁴ : TopologicalSpace G
inst✝¹³ : ChartedSpace H G
inst✝¹² : TopologicalSpace A
inst✝¹¹ : ChartedSpace H A
inst✝¹⁰ : TopologicalSpace A'
inst✝⁹ : ChartedSpace H' A'
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ChartedSpace H R
EP : Type u_7
inst✝⁶ : NormedAddCommGroup EP
inst✝⁵ : NormedSpace 𝕜 EP
HP : Type u_8
inst✝⁴ : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝³ : TopologicalSpace P
inst✝² : ChartedSpace HP P
inst✝¹ : Group G
inst✝ : LieGroup I ∞ G
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(TopCat.of M)) (smoothPresheafGroup IM I M G)

Tactic:
rw [CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget _ _ (CategoryTheory.forget GrpCat)]

Goal state after:
𝕜 : Type u_1
inst✝²⁶ : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝²⁵ : NormedAddCommGroup EM
inst✝²⁴ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝²³ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace 𝕜 E
H : Type u_5
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst✝¹⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace HM M
N G A A' R : Type u
inst✝¹⁶ : TopologicalSpace N
inst✝¹⁵ : ChartedSpace H N
inst✝¹⁴ : TopologicalSpace G
inst✝¹³ : ChartedSpace H G
inst✝¹² : TopologicalSpace A
inst✝¹¹ : ChartedSpace H A
inst✝¹⁰ : TopologicalSpace A'
inst✝⁹ : ChartedSpace H' A'
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ChartedSpace H R
EP : Type u_7
inst✝⁶ : NormedAddCommGroup EP
inst✝⁵ : NormedSpace 𝕜 EP
HP : Type u_8
inst✝⁴ : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝³ : TopologicalSpace P
inst✝² : ChartedSpace HP P
inst✝¹ : Group G
inst✝ : LieGroup I ∞ G
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(TopCat.of M))
    (CategoryTheory.Functor.comp (smoothPresheafGroup IM I M G) (CategoryTheory.forget GrpCat))
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: case mpr
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
H : ∃ t, (∀ y ∈ t, f y ≠ 0) ∧ IsOpen[instTopologicalSpaceSubtype] t ∧ ⟨x, hxU⟩ ∈ t
⊢ IsUnit ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f)

Tactic:
obtain ⟨V₀, hV₀f, hV₀, hxV₀⟩ := H

Goal state after:
case mpr
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
V₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, f y ≠ 0
hV₀ : IsOpen[instTopologicalSpaceSubtype] V₀
hxV₀ : ⟨x, hxU⟩ ∈ V₀
⊢ IsUnit ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f)
Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality

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
A : Type u_9
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst✝³ : VectorBundle 𝕜 F V
inst✝² : CompleteSpace 𝕜
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : ContMDiffVectorBundle 1 F V I
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : σ x = σ' x
t : Trivialization F TotalSpace.proj := trivializationAt F V x
x_mem : x ∈ t.baseSet
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 F)) 𝕜 F := Basis.ofVectorSpace 𝕜 F
s : ↑(Basis.ofVectorSpaceIndex 𝕜 F) → (x : M) → V x := t.localFrame b
c : ↑(Basis.ofVectorSpaceIndex 𝕜 F) → (x : M) → V x →ₗ[𝕜] 𝕜 := Trivialization.localFrameCoeff I t b
hs : ∀ (i : ↑(Basis.ofVectorSpaceIndex 𝕜 F)), MDiffAt (T% s) x
hc :
  ∀ {σ : (x : M) → V x},
    MDiffAt (T% σ) x → ∀ (i : ↑(Basis.ofVectorSpaceIndex 𝕜 F)), MDiffAt ((LinearMap.piApply (c i)) σ) x
hΦ_eq : ∀ {σ : (x : M) → V x}, MDiffAt (T% σ) x → Φ σ = Φ fun x' ↦ ∑ i, (c i x') (σ x') • s i x'
i : ↑(Basis.ofVectorSpaceIndex 𝕜 F)
a✝ : i ∈ Finset.univ
⊢ (c i x) (σ x) • Φ (s i) = (c i x) (σ' x) • Φ (s i)

Tactic:
by rw [hσσ']

Goal state after:
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
ι : Type u_7
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : ι → Set M
hcov : ∀ (i : ι), IsCovariantDerivativeOn F cov (s i)
σ✝ : (x : M) → V x
g✝ : M → 𝕜
x✝ : M
hσ : MDiffAt (T% σ✝) x✝
hf' : MDiffAt g✝ x✝
hx : x✝ ∈ ⋃ i, s i
⊢ cov (g✝ • σ✝) x✝ = g✝ x✝ • cov σ✝ x✝ + (d% g✝ x✝).smulRight (σ✝ x✝)

Tactic:
obtain ⟨si, ⟨i, rfl⟩, hxsi⟩ := hx
    exact (hcov i).leibniz hσ hf'

Goal state after:
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑x.carrier =
    ∑ x ∈ (noncenter G).toFinset, Fintype.card ↑x.carrier

Tactic:
convert! finsum_cond_eq_sum_of_cond_iff _ _
    simp [Set.mem_toFinset]

Goal state after:
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case e'_2.e'_6
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card = ∑ᶠ (j : ↑(noncenter G)), Nat.card ↑(↑j).carrier

Tactic:
finsum_eq_sum_of_fintype,

Goal state after:
case e'_2.e'_6
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card = ∑ i, Nat.card ↑(↑i).carrier
Module: Mathlib.GroupTheory.Commensurable

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ 1 ∈ {g | (g • H).Commensurable H}

Tactic:
rw [Set.mem_ofPred_eq, one_smul]

Goal state after:
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
hx : x ∈ s
⊢ (ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (f.ind x hx)) ∘SL mfderiv% ⇑f.embeddingPiTangent x =
    mfderiv% ↑(chartAt H (f.c (f.ind x hx))) x

Tactic:
by
  set L :=
    (ContinuousLinearMap.fst ℝ E ℝ).comp
      (@ContinuousLinearMap.proj ℝ _ ι (fun _ => E × ℝ) _ _ (fun _ => inferInstance) (f.ind x hx))
  have := L.hasMFDerivAt.comp x
    (f.embeddingPiTangent.contMDiff.mdifferentiableAt (by simp)).hasMFDerivAt
  convert! hasMFDerivAt_unique this _
  refine (hasMFDerivAt_extChartAt (f.mem_chartAt_ind_source x hx)).congr_of_eventuallyEq ?_
  refine (f.eventuallyEq_one x hx).mono fun y hy => ?_
  simp only [L, embeddingPiTangent_coe, ContinuousLinearMap.coe_comp, (· ∘ ·),
    ContinuousLinearMap.coe_fst', ContinuousLinearMap.proj_apply]
  rw [hy, Pi.one_apply, one_smul]

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

Goal state before:
pp: case hg
n : ℕ
i : ZMod n
⊢ sr i * sr i = 1

Tactic:
sr_mul_self

Goal state after:
case hg
n : ℕ
i : ZMod n
⊢ 1 = 1
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ Submonoid.closure (Set.range ⇑inl ∪ Set.range ⇑inr) = MonoidHom.mrange mk

Tactic:
MonoidHom.mrange_eq_map,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ Submonoid.closure (Set.range ⇑inl ∪ Set.range ⇑inr) = Submonoid.map mk ⊤
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : M ∗ N →* P
⊢ MonoidHom.mrange f = MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr)

Tactic:
MonoidHom.mrange_eq_map,

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : M ∗ N →* P
⊢ Submonoid.map f ⊤ = MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr)
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : M ∗ N →* P
⊢ Submonoid.map f (MonoidHom.mrange inl) ⊔ Submonoid.map f (MonoidHom.mrange inr) =
    MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr)

Tactic:
MonoidHom.map_mrange,

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : M ∗ N →* P
⊢ MonoidHom.mrange (f.comp inl) ⊔ Submonoid.map f (MonoidHom.mrange inr) =
    MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
⊢ ∀ (i : ι), (f i).range ≤ (lift f).range

Tactic:
rintro i _ ⟨x, rfl⟩

Goal state after:
ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
i : ι
x : G i
⊢ (f i) x ∈ (lift f).range
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
⊢ cs.IsReflection t⁻¹

Tactic:
rwa [ht.inv]

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

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ ↑(cs.length (w₁ * w₂)) = ↑(cs.length w₁ + cs.length w₂)

Tactic:
Nat.cast_add

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ ↑(cs.length (w₁ * w₂)) = ↑(cs.length w₁) + ↑(cs.length w₂)
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
⊢ cs.length (cs.simple i * w) < cs.length w → cs.length (cs.simple i * w) + 1 = cs.length w

Tactic:
intro _

Goal state after:
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) + 1 = cs.length w
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
⊢ ¬cs.length (cs.simple i * w) < cs.length w → cs.length (cs.simple i * w) = cs.length w + 1

Tactic:
intro _

Goal state after:
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
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
⊢ cs.length (w * cs.simple i) < cs.length w → cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
intro _

Goal state after:
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 (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) + 1 = cs.length w
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
⊢ ¬cs.length (w * cs.simple i) < cs.length w → cs.length (w * cs.simple i) = cs.length w + 1

Tactic:
intro _

Goal state after:
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 (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ Finite (Quotient ↑H ↑K) → ∃ I, ⋃ i ∈ I, quotToDoubleCoset H K i = Set.univ

Tactic:
intro _

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a✝ : Finite (Quotient ↑H ↑K)
⊢ ∃ I, ⋃ i ∈ I, quotToDoubleCoset H K i = Set.univ
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg
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))
hk : ¬k = 0
⊢ (g ^ if k = 0 then ↑(minimalPeriod (fun x ↦ g • x) (Quotient.out ⟨q, k - 1⟩.fst)) else k.cast) *
      Quotient.out (Quotient.out ⟨q, k - 1⟩.fst) =
    if k = 0 then g ^ minimalPeriod (fun x ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else g ^ k.cast * Quotient.out (Quotient.out q)

Tactic:
· rw [if_neg hk, if_neg hk]

Goal state after:
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
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
hR : IsComplement ↑H ↑R
⊢ 1 ∈ R

Tactic:
Set.mem_toFinset

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
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
hR : IsComplement ↑H ↑R
⊢ 1 ∈ R₀
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: case mul
G : Type u_1
inst✝ : Group G
H : Subgroup G
n g : G
hg : g ∈ H
x✝ y✝ : G
hx✝ : x✝ ∈ closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}
hy✝ : y✝ ∈ closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}
IHa : g * x✝ * g⁻¹ ∈ H.focalSubgroup
IHb : g * y✝ * g⁻¹ ∈ H.focalSubgroup
⊢ g * (x✝ * y✝) * g⁻¹ ∈ H.focalSubgroup

Tactic:
simpa using mul_mem IHa IHb

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
a b : G
ha : a ∈ {x | ∀ (y : G), ⁅x, y⁆ ∈ N}
hb : b ∈ {x | ∀ (y : G), ⁅x, y⁆ ∈ N}
y : G
⊢ ⁅a * b, y⁆ ∈ N

Tactic:
by
    convert! Subgroup.mul_mem _ (ha (b * y * b⁻¹)) (hb y) using 1
    group

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case right
G : Type u_1
inst✝ : Group G
⊢ ∀ (x : G) (n : ℕ), x ∈ ⊤.lowerCentralSeries n → ∀ (g : G), ⁅x, g⁆ ∈ ⊤.lowerCentralSeries (n + 1)

Tactic:
intro x n hxn g

Goal state after:
case right
G : Type u_1
inst✝ : Group G
x : G
n : ℕ
hxn : x ∈ ⊤.lowerCentralSeries n
g : G
⊢ ⁅x, g⁆ ∈ ⊤.lowerCentralSeries (n + 1)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ upperCentralSeries G (nilpotencyClass G) = ⊤

Tactic:
by
  classical
  rw [nilpotencyClass_def, Nat.find_spec (IsNilpotent.nilpotent G)]

Goal state after:
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
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
⊢ ((QuotientGroup.mk' (P.prod Q).range.goursatFst).prodMap (QuotientGroup.mk' (P.prod Q).range.goursatSnd)).ker ≤
    (P.prod Q).range

Tactic:
· convert! goursatFst_prod_goursatSnd_le (P.prod Q).range
    ext ⟨g, h⟩
    simp_rw [G', H', MonoidHom.mem_ker, MonoidHom.coe_prodMap, Prod.map_apply, Subgroup.mem_prod,
      Prod.one_eq_mk, Prod.ext_iff, ← MonoidHom.mem_ker, QuotientGroup.ker_mk']

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨g, hx⟩ := hG x

Goal state after:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
⊢ ∃ g, g • x = y
Module: Mathlib.GroupTheory.Perm.ConjAct

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
⊢ (k • g).cycleFactorsFinset = k • g.cycleFactorsFinset

Tactic:
ext c
  rw [← mem_cycleFactorsFinset_conj' k⁻¹ (k • g) c]
  simp only [inv_smul_smul]
  exact Finset.inv_smul_mem_iff

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

Goal state before:
pp: case mp
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 M α → IsPreprimitive N β

Tactic:
intro _

Goal state after:
case mp
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
a✝ : IsPreprimitive M α
⊢ IsPreprimitive N β
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 _

Goal state after:
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
a✝ : IsPreprimitive N β
⊢ IsPreprimitive M α
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : g ∈ {σ | σ.IsThreeCycle}
a : α
ha : a ∈ g.support
h_support : g.support = {a, g a, g (g a)}
h_nodup : [a, g a, g (g a)].Nodup
this : 1 < g.supportᶜ.card
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
⊢ g = swap a (g a) * swap b c * (swap b c * swap (g a) (g (g a)))

Tactic:
simp [mul_assoc, ← hg3.eq_swap_mul_swap_iff_mem_support.mpr ha]

Goal state after: