mathlib-initiative/mathlib-tactics huggingface dataset:
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 ↑I ×ˢ range ↑I') (↑I w, ↑I' w')
smooth_pM : ContMDiffAt (I.tangent.prod I'.tangent) I.tangent n Prod.fst (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E → E := fun x ↦ ↑I (↑(chartAt H a.proj) (↑(chartAt H p.1.proj).symm (↑I.symm x)))
D0 : DifferentiableWithinAt 𝕜 φ (range ↑I) (↑I (↑(chartAt H p.1.proj) p.1.proj))
D :
  ∀ (w : TangentBundle I' M'),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.fst) (range (Prod.map ↑I ↑I'))
      (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' w.proj) w.proj))
⊢ (fderivWithin 𝕜 φ (range ↑I) (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj)).1 ∘SL
        fderivWithin 𝕜 Prod.fst (range ↑I ×ˢ range ↑I')
          (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj)))
      (p.1.snd, p.2.snd) =
    (fderivWithin 𝕜 φ (range ↑I) (↑I (↑(chartAt H p.1.proj) p.1.proj))) p.1.snd

Tactic:
simp [fderivWithin_fst, U]

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

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
inst✝² : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
h : ¬Injective γ
⊢ ∃ T > 0, Periodic γ T

Tactic:
Injective

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
inst✝² : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
h : ¬∀ ⦃a₁ a₂ : ℝ⦄, γ a₁ = γ a₂ → a₁ = a₂
⊢ ∃ T > 0, Periodic γ T
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
pp: F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
v : TangentSpace 𝓘(ℝ, F) x
⊢ ‖v‖ = ‖v‖

Tactic:
norm_eq_sqrt_real_inner,

Goal state after:
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
v : TangentSpace 𝓘(ℝ, F) x
⊢ √⟪v, v⟫ = ‖v‖
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
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
U : (OpenNhds x)ᵒᵖ
⊢ colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U ≫ (forgetStalk IM I M R x).inv =
    ↾⇑(CommRingCat.Hom.hom (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U))

Tactic:
rw [Iso.comp_inv_eq, ← smoothSheafCommRing.ι_forgetStalk_hom]

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
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
U : (OpenNhds x)ᵒᵖ
⊢ ↾⇑(CommRingCat.Hom.hom (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U)) ≫
      (forgetStalk IM I M R x).hom =
    ↾⇑(CommRingCat.Hom.hom (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U)) ≫
      (forgetStalk IM I M R x).hom
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case hf
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
H' : Type u_5
inst✝⁷ : TopologicalSpace H'
E' : Type u_6
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H' M'
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : IsManifold I' (minSmoothness 𝕜 2) M'
inst✝ : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s u : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hs : UniqueMDiff[s]
hu : UniqueMDiff[u]
hf : ContMDiffWithinAt I I' n f u x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
h'x₀ : x₀ ∈ closure[inst✝⁹] (interior u)
hsu : s ⊆ u
B :
  ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (↑(extChartAt I x₀) x₀)
this✝ :
  ↑(extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target =ᶠ[𝓝 (↑(extChartAt I x₀) x₀)]
    ↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I
this :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (↑(extChartAt I x₀) x₀)
⊢ ContDiffWithinAt 𝕜 2 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (↑(extChartAt I x₀) x₀)

Tactic:
exact (B.of_le hn).of_le le_minSmoothness

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : CompleteSpace E
n : ℕ∞ω
inst✝ : IsManifold I (n + 1) M
m : ℕ∞ω
U V : (x : M) → TangentSpace I x
s : Set M
x : M
hU : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, V x⟩) s x
hs : UniqueMDiff[s]
hx : x ∈ s
hmn : minSmoothness 𝕜 (m + 1) ≤ n
min2 : minSmoothness 𝕜 2 ≤ n + 1
m' : ℕ∞ω
hm' : m' ≤ m
h'm' : m' ≠ ∞
hn : 1 ≤ m' + 1
hm'n : m' + 1 ≤ n
pre_mem : ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) ∈ 𝓝[s] x
U' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) U (range ↑I)
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)
⊢ ↑(extChartAt I x) x ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : CompleteSpace E
m n : ℕ∞
inst✝ : IsManifold I (↑n + 1) M
U V : (x : M) → TangentSpace I x
x : M
hmn : minSmoothness 𝕜 (↑m + 1) ≤ ↑n
hU : ContMDiffWithinAt I I.tangent (↑n) (fun x ↦ ⟨x, U x⟩) univ x
hV : ContMDiffWithinAt I I.tangent (↑n) (fun x ↦ ⟨x, V x⟩) univ x
⊢ ContMDiffWithinAt I I.tangent (↑m) (fun x₀ ↦ ⟨x₀, mlieBracketWithin I U V univ x₀⟩) univ x

Tactic:
exact hU.mlieBracketWithin_vectorField hV uniqueMDiffOn_univ (mem_univ _) hmn

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I (minSmoothness 𝕜 3) M
inst✝ : CompleteSpace E
U V W : (x : M) → TangentSpace I x
s : Set M
x : M
hs : UniqueMDiff[s]
h's : x ∈ closure[inst✝³] (interior s)
hx : x ∈ s
hU : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, V x⟩) s x
hW : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, W x⟩) s x
A : minSmoothness 𝕜 2 + 1 ≤ minSmoothness 𝕜 3
s_inter_mem : s ∩ (extChartAt I x).source ∈ 𝓝[s] x
pre_mem : ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) ∈ 𝓝[s] x
U' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) U (range ↑I)
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)
J0U :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U' x⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
J0V :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, V' x⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
J0W :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, W' x⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
J1U :
  ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U' x⟩)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
J1V :
  ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, V' x⟩)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
J1W :
  ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, W' x⟩)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
JU : U =ᶠ[𝓝[s] x] mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) U'
JV : V =ᶠ[𝓝[s] x] mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) V'
JW : W =ᶠ[𝓝[s] x] mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) W'
this :
  ∀ᶠ (y : M) in 𝓝[s] x,
    mlieBracketWithin I (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) V') (mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) W') s y =
      mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
        (mlieBracketWithin 𝓘(𝕜, E) V' W' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)) y
⊢ ↑(extChartAt I x) x ∈ ↑(extChartAt I x).symm ⁻¹' s

Tactic:
simp [hx]

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
⊢ (Finset.univ \ (noncenter G).toFinset).card = ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier

Tactic:
rw [Finset.card_eq_sum_ones]

Goal state after:
case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ x ∈ Finset.univ \ (noncenter G).toFinset, 1 = ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier
Module: Mathlib.GroupTheory.Commensurable

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : ConjAct G
a b : ↥K
⊢ (QuotientGroup.leftRel (H.subgroupOf K)) a b ↔
    (QuotientGroup.leftRel ((g • H).subgroupOf (g • K))) ((equivSMul g K).toEquiv a) ((equivSMul g K).toEquiv b)

Tactic:
dsimp
    rw [← Quotient.eq'', ← Quotient.eq'', QuotientGroup.eq, QuotientGroup.eq,
      mem_subgroupOf, mem_subgroupOf, ← map_inv, ← map_mul, equivSMul_apply_coe]
    exact smul_mem_pointwise_smul_iff.symm

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

Goal state before:
pp: case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h2 : (↑(orderOf (r 1))).val = 0
⊢ False

Tactic:
ZMod.val_natCast,

Goal state after:
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h2 : orderOf (r 1) % n = 0
⊢ False
Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G : Type u_3
H✝ : Type u_4
inst✝¹ : Group G
inst✝ : Group H✝
b b' : G ≃* FreeGroup ι
hbb' : (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b } = (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b' }
H : ↑b.symm = ↑b'.symm
this : b.symm = b'.symm
⊢ b = b'

Tactic:
← MulEquiv.symm_symm b,

Goal state after:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H✝ : Type u_4
inst✝¹ : Group G
inst✝ : Group H✝
b b' : G ≃* FreeGroup ι
hbb' : (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b } = (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b' }
H : ↑b.symm = ↑b'.symm
this : b.symm = b'.symm
⊢ b.symm.symm = b'
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
⊢ Function.RightInverse (fun f x ↦ f.comp of) fun fi ↦
    (conGen (Rel M)).lift (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) ⋯

Tactic:
by
    intro f
    ext i x
    rfl

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

Goal state before:
pp: case neg
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ take (k + 1) (alternatingWord i j (2 * p)) = alternatingWord i j (k + 1)

Tactic:
rw [← List.take_concat_get (by simp; lia), alternatingWord_succ, hk]

Goal state after:
case neg
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ (alternatingWord j i k).concat (alternatingWord i j (2 * p))[k] = (alternatingWord j i k).concat j
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
⊢ cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)

Tactic:
induction m with
  | zero => simp [alternatingWord]
  | succ m ih =>
    rw [alternatingWord_succ', wordProd_cons, ih]
    by_cases hm : Even m
    · have h₁ : ¬ Even (m + 1) := by simp [hm, parity_simps]
      have h₂ : (m + 1) / 2 = m / 2 := Nat.succ_div_of_not_dvd <| by rwa [← even_iff_two_dvd]
      simp [hm, h₁, h₂]
    · have h₁ : Even (m + 1) := by simp [hm, parity_simps]
      have h₂ : (m + 1) / 2 = m / 2 + 1 := Nat.succ_div_of_dvd h₁.two_dvd
      simp [hm, h₁, h₂, ← pow_succ', ← mul_assoc]

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

Goal state before:
pp: case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
⊢ cs.leftInvSeq (i :: ω) = (cs.rightInvSeq (i :: ω).reverse).reverse

Tactic:
| cons i ω ih =>

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

Goal state before:
pp: case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : (cs.rightInvSeq ω).length = ω.length
⊢ (cs.rightInvSeq (i :: ω)).length = (i :: ω).length

Tactic:
| cons i ω ih =>

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

Goal state before:
pp: case cons
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.rightInvSeq ω).getD j 1 =
      (cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)
j : ℕ
⊢ (cs.rightInvSeq (i :: ω)).getD j 1 =
    (cs.wordProd (drop (j + 1) (i :: ω)))⁻¹ * (Option.map cs.simple (i :: ω)[j]?).getD 1 *
      cs.wordProd (drop (j + 1) (i :: ω))

Tactic:
| cons i ω ih =>

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

Goal state before:
pp: case cons
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 : ℕ
⊢ (cs.leftInvSeq (i :: ω)).getD j 1 =
    cs.wordProd (take j (i :: ω)) * (Option.map cs.simple (i :: ω)[j]?).getD 1 * (cs.wordProd (take j (i :: ω)))⁻¹

Tactic:
| cons i ω ih =>

Goal state after:
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * ↑f.range = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h (f x)
inst✝ : Northcott h
⊢ FG G

Tactic:
set q := QuotientGroup.mk (s := map f ⊤)
  -- Main proof idea: `s` together with elements of sufficiently small "height" `h` generates `G`.
  let S : Set G := s ∪ {x : G | h x ≤ 2 * c / (b - a)}
  let U := closure S
  suffices U = ⊤ from Group.fg_iff.mpr ⟨S, this, hs.union <| Northcott.finite_le _⟩
  by_contra! H -- Assume for contradiction that these elements generate a proper subgroup `U`.
  rw [← SetLike.coe_ne_coe, coe_top, ← Set.nonempty_compl] at H
  -- Then we can find an element `x : G` not in `U` and of minimal height.
  obtain ⟨x, hx₁, hx₂⟩ := Northcott.exists_min_image h Uᶜ H
  -- Now we construct an element `y` of smaller height and not in `U`.
  obtain ⟨g, hg, z, ⟨y, rfl⟩, rfl⟩ := Set.mem_mul.mp <| H₁ ▸ Set.mem_univ x
  have H' : h y < h (g * f y) := by
    suffices a * h (g * f y) + 2 * c < b * h (g * f y) by nlinarith [H₂ g hg (f y), H₃ y]
    suffices 2 * c / (b - a) < h (g * f y) by field_simp [sub_pos.mpr H₀] at this; grind
    suffices g * f y ∉ S by grind
    exact notMem_of_notMem_closure hx₁
  -- To obtain a contradiction, we do cases on whether `y ∈ U`.
  by_cases hy : y ∈ U
  · exact hx₁ <| U.mul_mem (mem_closure_of_mem <| .inl hg) <| hf U <| mem_map_of_mem f hy
  · exact H'.not_ge <| hx₂ y hy

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

Goal state before:
pp: case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
i : B
ω : List B
ih : t ∈ cs.rightInvSeq ω → cs.IsReflection t
ht : t ∈ cs.rightInvSeq (i :: ω)
⊢ cs.IsReflection t

Tactic:
| cons i ω ih =>

Goal state after:
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : (powMonoidHom n).range.FiniteIndex
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
f : G →* G := powMonoidHom n
q : G → G ⧸ f.range := QuotientGroup.mk
⊢ Group.FG G

Tactic:
let qi : G ⧸ f.range → G := Function.surjInv mk_surjective

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : (powMonoidHom n).range.FiniteIndex
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
f : G →* G := powMonoidHom n
q : G → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
⊢ Group.FG G
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih : (cs.rightInvSeq ω).prod = (cs.wordProd ω)⁻¹
⊢ (cs.rightInvSeq (i :: ω)).prod = (cs.wordProd (i :: ω))⁻¹

Tactic:
| cons i ω ih =>

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a : ℕ
m : M
s : ℕ+
⊢ a • mk m s = mk (a • m) s

Tactic:
induction a with
  | zero => simp
  | succ n h => simp [add_nsmul, mk_add_mk_left, h]

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ ∃ x ∈ ↑H, ∃ y ∈ ↑K, b = x * a * y

Tactic:
refine ⟨y⁻¹ * l, H.mul_mem (H.inv_mem hy) hl, r * r'⁻¹, K.mul_mem hr (K.inv_mem hr'), ?_⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ b = y⁻¹ * l * a * (r * r'⁻¹)
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)
ι : Type
w✝ : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h₂.some
e' : (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) ≃* ((i : ι) → Multiplicative (ZMod (n i)) →* Mˣ) :=
  Pi.monoidHomMulEquiv (fun i ↦ Multiplicative (ZMod (n i))) Mˣ
this : ∀ (i : ι), NeZero (n i)
i : ι
hdvd : Nat.card (Multiplicative (ZMod (n i))) ∣ Monoid.exponent G
⊢ HasEnoughRootsOfUnity M (Nat.card (Multiplicative (ZMod (n i))))

Tactic:
exact HasEnoughRootsOfUnity.of_dvd M hdvd

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:
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✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : ↥S) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ ∏ a, Nat.card ↥(zpowers ↑a)
g : ↥S
x✝ : g ∈ Finset.univ
⊢ Nat.card ↥(zpowers ↑g) ∣ Monoid.exponent G

Tactic:
rw [Nat.card_zpowers]

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