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

Goal state before:
pp: case rs
𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hP : IsLocalSourceTargetProperty P
hf : LiftSourceTargetPropertyAt I J n f x P
h' : f =ᶠ[𝓝 x] g
s' : Set M
hxs' : s' ∈ 𝓝 x
hfg : EqOn f g s'
s : Set M
hss' : s ⊆ s'
hs : IsOpen[inst✝³] s
hxs : x ∈ s
⊢ (hf.domChart.restr s).source ⊆ s'

Tactic:
exact Subset.trans (by simp [interior_eq_iff_isOpen.mpr hs]) hss'

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: case left
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : ℕ∞ω
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ Continuous Subtype.val

Tactic:
exact continuous_subtype_val

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I m M
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), f x ∈ sphere 0 1
⊢ ContMDiff I (𝓡 n) m (Set.codRestrict f (sphere 0 1) hf')

Tactic:
rw [contMDiff_iff_target]
  refine ⟨continuous_induced_rng.2 hf.continuous, ?_⟩
  intro v
  let U : _ ≃ₗᵢ[ℝ] _ :=
    (-- Again, partially removing type ascription... Weird that this helps!
        OrthonormalBasis.fromOrthogonalSpanSingleton
        n (ne_zero_of_mem_unit_sphere (-v))).repr
  have h : ContDiffOn ℝ ω _ Set.univ := U.contDiff.contDiffOn
  have H₁ := (h.comp_inter contDiffOn_stereoToFun).contMDiffOn
  have H₂ : CMDiff[Set.univ] m f := hf.contMDiffOn
  convert! (H₁.of_le le_top).comp' H₂ using 1
  ext x
  have hfxv : f x = -↑v ↔ ⟪f x, -↑v⟫_ℝ = 1 := by
    have hfx : ‖f x‖ = 1 := by simpa using hf' x
    rw [inner_eq_one_iff_of_norm_eq_one hfx]
    exact norm_eq_of_mem_sphere (-v)
  simp [chartAt, ChartedSpace.chartAt, Subtype.ext_iff, hfxv, real_inner_comm]

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

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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
⊢ tangentMap I I.tangent (zeroSection E (TangentSpace I)) ⟨x, v⟩ = ⟨⟨⟨x, v⟩.proj, 0⟩, (⟨x, v⟩.snd, 0)⟩

Tactic:
have N : I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (I ((chartAt H x) x)) := by
    apply IsOpen.mem_nhds
    · apply (OpenPartialHomeomorph.open_target _).preimage I.continuous_invFun
    · simp only [mfld_simps]

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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
⊢ tangentMap I I.tangent (zeroSection E (TangentSpace I)) ⟨x, v⟩ = ⟨⟨⟨x, v⟩.proj, 0⟩, (⟨x, v⟩.snd, 0)⟩
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')
smooth_pM : ContMDiffAt (I.tangent.prod I'.tangent) I.tangent n Prod.fst (a, b)
p : TangentBundle I M × TangentBundle I' M'
⊢ p ∈ (chartAt (ModelProd (ModelProd H E) (ModelProd H' E')) (a, b)).source →
    (Prod.fst ∘ 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))
        p =
      (↑(trivializationAt E (TangentSpace I) a.proj) p.1).2

Tactic:
hp

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')
smooth_pM : ContMDiffAt (I.tangent.prod I'.tangent) I.tangent n Prod.fst (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p ∈ (chartAt (ModelProd (ModelProd H E) (ModelProd H' E')) (a, b)).source
⊢ (Prod.fst ∘ 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))
      p =
    (↑(trivializationAt E (TangentSpace I) a.proj) p.1).2
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')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
⊢ p ∈ (chartAt (ModelProd (ModelProd H E) (ModelProd H' E')) (a, b)).source →
    (Prod.snd ∘ 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))
        p =
      (↑(trivializationAt E' (TangentSpace I') b.proj) p.2).2

Tactic:
hp

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')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p ∈ (chartAt (ModelProd (ModelProd H E) (ModelProd H' E')) (a, b)).source
⊢ (Prod.snd ∘ 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))
      p =
    (↑(trivializationAt E' (TangentSpace I') b.proj) p.2).2
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⟩
⊢ Xor (∃ T > 0, Periodic γ T) (Injective γ)

Tactic:
by
  rw [xor_iff_iff_not]
  refine ⟨fun ⟨T, hT, hf⟩ ↦ hf.not_injective (ne_of_gt hT), ?_⟩
  intro h
  rw [Injective] at h
  push Not at h
  obtain ⟨a, b, heq, hne⟩ := h
  refine ⟨|a - b|, ?_, ?_⟩
  · rw [gt_iff_lt, abs_pos, sub_ne_zero]
    exact hne
  · by_cases! hab : a - b < 0
    · rw [abs_of_neg hab, neg_sub]
      exact hγ.periodic_of_eq hv heq.symm
    · rw [abs_of_nonneg hab]
      exact hγ.periodic_of_eq hv heq

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian

Goal state before:
pp: EB : Type u_1
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace ℝ EB
HB : Type u_2
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n : ℕ∞ω
B : Type u_3
inst✝¹³ : TopologicalSpace B
inst✝¹² : ChartedSpace HB B
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
E : B → Type u_5
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
EM : Type u_6
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace ℝ EM
HM : Type u_7
inst✝² : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB n F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ ⟨b m, v m⟩) s x
hw : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ ⟨b m, w m⟩) s x
⊢ ContMDiffWithinAt IM 𝓘(ℝ, ℝ) n (fun m ↦ ⟪v m, w m⟫) s x

Tactic:
by
  rcases h.exists_contMDiff with ⟨g, g_smooth, hg⟩
  have hb : CMDiffAt[s] n b x := by
    simp only [contMDiffWithinAt_totalSpace] at hv
    exact hv.1
  simp only [hg]
  have : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ)) n
      (fun m ↦ TotalSpace.mk' ℝ (E := Bundle.Trivial B ℝ) (b m) (g (b m) (v m) (w m))) s x := by
    apply ContMDiffWithinAt.clm_bundle_apply₂ (F₁ := F) (F₂ := F)
    · exact ContMDiffAt.comp_contMDiffWithinAt x g_smooth.contMDiffAt hb
    · exact hv
    · exact hw
  simp only [contMDiffWithinAt_totalSpace] at this
  exact this.2

Goal state after:
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
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : M → 𝕜 := fun x' ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
this✝ : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
this : (MDiffAt fun _x ↦ 1) x
x' : M
hx' : σ x' = σ' x'
⊢ ψ x' = (fun _x ↦ 1) x'

Tactic:
simp [ψ, hx']

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

Goal state before:
pp: E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → NormedAddCommGroup (V x)
inst✝³ : (x : M) → InnerProductSpace ℝ (V x)
inst✝² : FiberBundle F V
cov : CovariantDerivative I F V
inst✝¹ : VectorBundle ℝ F V
inst✝ : IsContMDiffRiemannianBundle I 1 F V
x : M
τ : (x : M) → V x
hτ : MDiffAt (T% τ) x
σ✝ σ'✝ : (x : M) → V x
hσ : MDiffAt (T% σ✝) x
hσ' : MDiffAt (T% σ'✝) x
⊢ derivMetricTensorAux I cov (σ✝ + σ'✝) τ x = derivMetricTensorAux I cov σ✝ τ x + derivMetricTensorAux I cov σ'✝ τ x

Tactic:
by
    ext X₀
    simp [mvfderiv_fun_add (hσ.inner_bundle hτ) (hσ'.inner_bundle hτ),
      cov.isCovariantDerivativeOn.add hσ hσ', inner_add_left]
    abel

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
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
⊢ g x • ∑ i ∈ s, f i x • cov i σ x + (∑ i ∈ s, f i) x • (d% g x).smulRight (σ x) =
    g x • ∑ i ∈ s, f i x • cov i σ x + (d% g x).smulRight (σ x)

Tactic:
by rw [hf]; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Group α
inst✝⁴ : MulAction α β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ Fintype.card α / Fintype.card ↥(stabilizer α (φ ω)) = Fintype.card (α ⧸ stabilizer α (φ ω))

Tactic:
Fintype.card_congr (@Subgroup.groupEquivQuotientProdSubgroup α _ (stabilizer α <| φ ω)),

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Group α
inst✝⁴ : MulAction α β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
ω : Quotient (orbitRel α β)
⊢ Fintype.card ((α ⧸ stabilizer α (φ ω)) × ↥(stabilizer α (φ ω))) / Fintype.card ↥(stabilizer α (φ ω)) =
    Fintype.card (α ⧸ stabilizer α (φ ω))
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
p q : { p // Commute p.1 p.2 }
h : (fun p ↦ ⟨(↑(↑p).1, ↑(↑p).2), ⋯⟩) p = (fun p ↦ ⟨(↑(↑p).1, ↑(↑p).2), ⋯⟩) q
⊢ p = q

Tactic:
by simpa only [Subtype.ext_iff, Prod.ext_iff] using h

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

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
P' : Type u_4
inst✝ : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
⊢ (f.comp (lift g₁ g₂)).comp inl = (lift (f.comp g₁) (f.comp g₂)).comp inl

Tactic:
rw [MonoidHom.comp_assoc, lift_comp_inl, lift_comp_inl]

Goal state after:
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: α : Type u_1
rels : Set (FreeGroup α)
this : of = ⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) ∘ FreeGroup.of
⊢ Subgroup.closure (Set.range (⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) ∘ FreeGroup.of)) = ⊤

Tactic:
Set.range_comp,

Goal state after:
α : Type u_1
rels : Set (FreeGroup α)
this : of = ⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) ∘ FreeGroup.of
⊢ Subgroup.closure (⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) '' Set.range FreeGroup.of) = ⊤
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: α : Type u_1
rels : Set (FreeGroup α)
this : of = ⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) ∘ FreeGroup.of
⊢ Subgroup.map (QuotientGroup.mk' (Subgroup.normalClosure rels)) (Subgroup.closure (Set.range FreeGroup.of)) = ⊤

Tactic:
FreeGroup.closure_range_of,

Goal state after:
α : Type u_1
rels : Set (FreeGroup α)
this : of = ⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) ∘ FreeGroup.of
⊢ Subgroup.map (QuotientGroup.mk' (Subgroup.normalClosure rels)) ⊤ = ⊤
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
this : cs.simple = ⇑cs.mulEquiv.symm ∘ PresentedGroup.of
⊢ Subgroup.closure (Set.range (⇑cs.mulEquiv.symm ∘ PresentedGroup.of)) = ⊤

Tactic:
Set.range_comp,

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
this : cs.simple = ⇑cs.mulEquiv.symm ∘ PresentedGroup.of
⊢ Subgroup.closure (⇑cs.mulEquiv.symm '' Set.range PresentedGroup.of) = ⊤
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case cons
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
x : B
ω' : List B
ih : cs.wordProd ω'.reverse = (cs.wordProd ω')⁻¹
⊢ cs.wordProd (x :: ω').reverse = (cs.wordProd (x :: ω'))⁻¹

Tactic:
simpa [wordProd_cons, wordProd_append] using ih

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

Goal state before:
pp: B : Type u_1
i j : B
p : ℕ
⊢ ∀ (k : ℕ) (hk : k < p), (alternatingWord i j p)[k] = if Even (p + k) then i else j

Tactic:
induction p with

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
m1 m2 : M
s : ℕ+
⊢ mk m1 s + mk m2 s = mk (m1 + m2) s

Tactic:
rw [mk_add_mk, mk_eq_mk]

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
m1 m2 : M
s : ℕ+
⊢ ∃ u, ↑u • ↑s • (↑s • m1 + ↑s • m2) = ↑u • ↑(s * s) • (m1 + m2)
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
h : a ≤ 0
x : DivisibleHull M
⊢ a • x =
    -((have this := ⟨-a, ⋯⟩;
        this) •
        x)

Tactic:
have := h.eq_or_lt
  aesop (add simp [qsmul_def, abs_of_neg])

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
⊢ (↑⟨a.den, ⋯⟩ * a.num * ↑sc) • mb < (↑⟨a.den, ⋯⟩ * a.num * ↑sb) • mc

Tactic:
mul_smul _ _ mc,

Goal state after:
case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
⊢ (↑⟨a.den, ⋯⟩ * a.num * ↑sc) • mb < (↑⟨a.den, ⋯⟩ * a.num) • ↑sb • mc
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: case refine_1
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
x✝¹ x✝ : G
h : ∀ (x : G →* Mˣ), x x✝¹ = x x✝
⊢ x✝¹ = x✝

Tactic:
forall_apply_eq_apply_iff

Goal state after:
case refine_1
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
x✝¹ x✝ : G
h : x✝¹ = x✝
⊢ x✝¹ = x✝
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
h1n : n ≤ -1
⊢ a i ^ n • (X i)ᶜ ⊆ Y i

Tactic:
clear hnne0 hgt

Goal state after:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
h1n : n ≤ -1
⊢ a i ^ n • (X i)ᶜ ⊆ Y i
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
⊢ orderOf ↑g ∣ Monoid.exponent G

Tactic:
exact Monoid.order_dvd_exponent (g : G)

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := hR.toRightFun
U : Set G := (fun g ↦ g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u : G
hu : u ∈ ↑(closure U)
r : G
hr : r ∈ R
⊢ u * (↑(f (r * s⁻¹)) * s * r⁻¹)⁻¹ * ↑(f (r * s⁻¹)) ∈ ↑(closure U) * R

Tactic:
refine Set.mul_mem_mul ((closure U).mul_mem hu ((closure U).inv_mem ?_)) (f (r * s⁻¹)).2

Goal state after:
case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := hR.toRightFun
U : Set G := (fun g ↦ g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u : G
hu : u ∈ ↑(closure U)
r : G
hr : r ∈ R
⊢ ↑(f (r * s⁻¹)) * s * r⁻¹ ∈ closure U
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g ↦ g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ ↑(closure ((fun g ↦ g * (↑(hR.toRightFun g))⁻¹) '' (R * S)))
r : G
hr : r ∈ R
hh : (fun x1 x2 ↦ x1 * x2) g r ∈ H
⊢ r * (↑⟨r, hr⟩)⁻¹ ∈ ↑H

Tactic:
rw [Subtype.coe_mk, mul_inv_cancel]
    exact H.one_mem

Goal state after: