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

Goal state before:
pp: case hb
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✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := ⋯
t : ℝ
ht : t < a'
⊢ t - a' ≤ 0

Tactic:
linarith

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

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✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := fun t ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
t : ℝ
ht : b' < t
⊢ b' - a' ≤ t - a'

Tactic:
linarith

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

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✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := fun t ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
t : ℝ
ht : b' < t
⊢ 0 < b' - a'

Tactic:
linarith

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
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 : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this : mpullback I I' f (mlieBracketWithin I' V W t) x₀ = mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀
⊢ mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ =
    mlieBracketWithin I (mpullback I I' f V) (mpullback I I' f W) s x₀

Tactic:
mpullbackWithin_mlieBracketWithin' hV hW hu uniqueMDiffOn_univ hf.contMDiffWithinAt
    hx₀ hn hst (by simp) (subset_univ _)

Goal state after:
𝕜 : 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 : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this : mpullback I I' f (mlieBracketWithin I' V W t) x₀ = mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀
⊢ mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀ =
    mlieBracketWithin I (mpullback I I' f V) (mpullback I I' f W) s x₀
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: 𝕜 : 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
EN : Type u_3
inst✝⁴ : NormedAddCommGroup EN
inst✝³ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝² : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace HN N
f : M → N
hf : ContMDiff IM IN ∞ f
x : M
⊢ PresheafedSpace.Hom.stalkMap (locallyRingedSpaceMapAux f hf) x ≫ smoothSheafCommRing.evalHom IM 𝓘(𝕜, 𝕜) M 𝕜 x =
    smoothSheafCommRing.evalHom IN 𝓘(𝕜, 𝕜) N 𝕜 (f x)

Tactic:
apply TopCat.Presheaf.stalk_hom_ext
  intro U hxU
  rw [PresheafedSpace.stalkMap_germ_assoc]
  ext a
  refine Eq.trans ?_ (smoothSheafCommRing.evalHom_germ _ _ _ _ _ _ _ a).symm
  apply smoothSheafCommRing.evalHom_germ

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
⊢ mlieBracketWithin I U (mlieBracketWithin I V W s) s x =
    mlieBracketWithin I (mlieBracketWithin I U V s) W s x + mlieBracketWithin I V (mlieBracketWithin I U W s) s x

Tactic:
have pre_mem : (extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s)
      ∈ 𝓝[s] x := by
    filter_upwards [s_inter_mem] with y hy
    exact ⟨(extChartAt I x).map_source hy.2,
      by simpa only [mem_preimage, (extChartAt I x).left_inv hy.2] using hy.1⟩

Goal state after:
𝕜 : 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
⊢ mlieBracketWithin I U (mlieBracketWithin I V W s) s x =
    mlieBracketWithin I (mlieBracketWithin I U V s) W s x + mlieBracketWithin I V (mlieBracketWithin I U W s) s x
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δ : (r' ^ 2)⁻¹ < 1 - δ * C
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' x - g' y‖ ≤ δ
⊢ 0 ≤ r'

Tactic:
linarith

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

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✝³ : RiemannianBundle fun x ↦ TangentSpace I x
inst✝² : IsManifold I 1 M
inst✝¹ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
inst✝ : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC✝ : ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst✝⁵] u
us : u ⊆ s
hu : u ⊆ {y | ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (chartAt H x).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst✝⁵] v
r : ℝ≥0
hr : ball (↑(extChartAt I x) x) ↑r ⊆ ↑(extChartAt I x).symm ⁻¹' v
r_pos : 0 < r
y : M
hy : y ∈ {y | riemannianEDist I x y < ↑(r / C)}
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < ↑(r / C)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := ↑(extChartAt I x) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
⊢ ∫⁻ (t' : ℝ) in Icc 0 t₁, ‖derivWithin γ' (Icc 0 t₁) t'‖ₑ = ∫⁻ (t' : ℝ) in Icc 0 t₁, ‖(mfderiv[Icc 0 t₁] γ' t') 1‖ₑ

Tactic:
simp_rw [← fderivWithin_derivWithin, mfderivWithin_eq_fderivWithin]

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✝³ : RiemannianBundle fun x ↦ TangentSpace I x
inst✝² : IsManifold I 1 M
inst✝¹ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
inst✝ : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC✝ : ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst✝⁵] u
us : u ⊆ s
hu : u ⊆ {y | ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (chartAt H x).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst✝⁵] v
r : ℝ≥0
hr : ball (↑(extChartAt I x) x) ↑r ⊆ ↑(extChartAt I x).symm ⁻¹' v
r_pos : 0 < r
y : M
hy : y ∈ {y | riemannianEDist I x y < ↑(r / C)}
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < ↑(r / C)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := ↑(extChartAt I x) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
⊢ ∫⁻ (t' : ℝ) in Icc 0 t₁, ‖(fderivWithin ℝ γ' (Icc 0 t₁) t') 1‖ₑ =
    ∫⁻ (t' : ℝ) in Icc 0 t₁, ‖(fderivWithin ℝ γ' (Icc 0 t₁) t') 1‖ₑ
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
y : M
a✝ : y ∈ s
h :
  ∀ (x_1 : ι),
    (↑(f.toFun x_1) x • ↑(extChartAt I (f.c x_1)) x, ↑(f.toFun x_1) x) =
      (↑(f.toFun x_1) y • ↑(extChartAt I (f.c x_1)) y, ↑(f.toFun x_1) y)
h₁ : ↑(extChartAt I (f.c (f.ind x hx))) x = 1 • ↑(extChartAt I (f.c (f.ind x hx))) y
h₂ : 1 = ↑(f.toFun (f.ind x hx)) y
⊢ x = y

Tactic:
one_smul

Goal state after:
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (x_1 : ι),
    (↑(f.toFun x_1) x • ↑(extChartAt I (f.c x_1)) x, ↑(f.toFun x_1) x) =
      (↑(f.toFun x_1) y • ↑(extChartAt I (f.c x_1)) y, ↑(f.toFun x_1) y)
h₁ : ↑(extChartAt I (f.c (f.ind x hx))) x = ↑(extChartAt I (f.c (f.ind x hx))) y
h₂ : 1 = ↑(f.toFun (f.ind x hx)) y
⊢ x = y
Module: Mathlib.Geometry.Manifold.WhitneyEmbedding

Goal state before:
pp: case convert_2
ι : 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
L : (ι → E × ℝ) →L[ℝ] E := ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (f.ind x hx)
this : HasMFDerivAt% (⇑L ∘ ⇑f.embeddingPiTangent) x (L ∘SL mfderiv% ⇑f.embeddingPiTangent x)
y : M
hy : ↑(f.toFun (f.ind x hx)) y = 1 y
⊢ 1 • ↑(extChartAt I (f.c (f.ind x hx))) y = ↑(extChartAt I (f.c (f.ind x hx))) y

Tactic:
one_smul

Goal state after:
case convert_2
ι : 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
L : (ι → E × ℝ) →L[ℝ] E := ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (f.ind x hx)
this : HasMFDerivAt% (⇑L ∘ ⇑f.embeddingPiTangent) x (L ∘SL mfderiv% ⇑f.embeddingPiTangent x)
y : M
hy : ↑(f.toFun (f.ind x hx)) y = 1 y
⊢ ↑(extChartAt I (f.c (f.ind x hx))) y = ↑(extChartAt I (f.c (f.ind x hx))) y
Module: Mathlib.GroupTheory.Commensurable

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

Tactic:
one_smul

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Commensurable H
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
⊢ ⁅pi Set.univ H, pi Set.univ K⁆ = pi Set.univ fun i ↦ ⁅H i, K i⁆

Tactic:
classical
    apply le_antisymm (commutator_pi_pi_le H K)
    rw [pi_le_iff]
    intro i hi
    rw [map_commutator]
    apply commutator_mono <;>
      · rw [le_pi_iff]
        intro j _hj
        rintro _ ⟨x, hx, rfl⟩
        by_cases h : j = i
        · subst h
          simpa using hx
        · simp [h, one_mem]

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δ : (r' ^ 2)⁻¹ < 1 - δ * C
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' x - g' y‖ ≤ δ
v : E y
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y) v
hgy : ((g y) v) v = ((g' y) w) w
hgx : ((g x) ((trivializationAt F E x).symm x w)) ((trivializationAt F E x).symm x w) = ((g' x) w) w
this : ((g' x) w) w ≤ δ * C * ((g' x) w) w + ((g' y) w) w
⊢ (1 - δ * C) * ((g' x) w) w ≤ ((g' y) w) w

Tactic:
linarith

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

Goal state before:
pp: case inl
⊢ orderOf (r 1) = 0

Tactic:
rw [orderOf_eq_zero_iff']

Goal state after:
case inl
⊢ ∀ (n : ℕ), 0 < n → r 1 ^ n ≠ 1
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
hn : Odd n
⊢ Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2

Tactic:
by
  rw [← Nat.mul_div_mul_left _ 2 hn.pos, ← card_commute_odd hn, mul_comm,
    card_comm_eq_card_conjClasses_mul_card, nat_card, Nat.mul_div_left _ (mul_pos two_pos hn.pos)]

Goal state after:
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: α : Type u_1
rels : Set (FreeGroup α)
⊢ Subgroup.closure (Set.range of) = ⊤

Tactic:
have : (PresentedGroup.of : α → PresentedGroup rels) = QuotientGroup.mk' _ ∘ FreeGroup.of := rfl
  rw [this, Set.range_comp, ← MonoidHom.map_closure (QuotientGroup.mk' _),
    FreeGroup.closure_range_of, ← MonoidHom.range_eq_map]
  exact MonoidHom.range_eq_top.2 (QuotientGroup.mk'_surjective _)

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case mul
ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
x y : CoprodI G
hx : (lift f) x ∈ s
hy : (lift f) y ∈ s
⊢ (lift f) (x * y) ∈ s

Tactic:
simp only [map_mul]

Goal state after:
case mul
ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
x y : CoprodI G
hx : (lift f) x ∈ s
hy : (lift f) y ∈ s
⊢ (lift f) x * (lift f) y ∈ s
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) x ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
    2
A :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
      Trivialization.symmL ℝ (trivializationAt F E x) x =
    ContinuousLinearMap.id ℝ F
this :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y =
    ContinuousLinearMap.id ℝ F ∘SL Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y
⊢ ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ <
    1 + ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖

Tactic:
linarith

Goal state after:
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
i : ι
⊢ empty.fstIdx ≠ some i

Tactic:
tauto

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

Goal state before:
pp: B : Type u_1
i i' : B
m : ℕ
⊢ alternatingWord i i' (m + 1) = (if Even m then i' else i) :: alternatingWord i i' m

Tactic:
induction m generalizing i i' with
  | zero => simp [alternatingWord]
  | succ m ih =>
    rw [alternatingWord]
    nth_rw 1 [ih i' i]
    rw [alternatingWord]
    simp [Nat.even_add_one, -Nat.not_even_iff_odd]

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

Goal state before:
pp: case pos
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 i j k
⊢ (if Even (2 * p + k) then i else j) = i

Tactic:
simp [(by apply Nat.even_add.mpr; simp [h_even] : Even (2 * p + k))]

Goal state after:
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 : ℕ
k : ℤ
⊢ Even (↑(M.M i i') * 2 - 2 * k)

Tactic:
use -k + (M i i'); ring

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

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

Tactic:
exact (cs.length_mul_simple w i).resolve_left (by lia)

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
i : B
⊢ cs.length (cs.simple i * w) + 1 = cs.length w ↔ cs.length w = cs.length (cs.simple i * w) + 1

Tactic:
tauto

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
i : B
⊢ cs.length (w * cs.simple i) + 1 = cs.length w ↔ cs.length w = cs.length (w * cs.simple i) + 1

Tactic:
tauto

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case empty
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
⊢ 1 • empty = empty

Tactic:
one_smul

Goal state after:
case empty
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
⊢ empty = empty
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ∀ l ∈ _w₁✝.toList, l.snd ≠ 1
_w₂_ih✝ : ∀ l ∈ _w₂✝.toList, l.snd ≠ 1
l : (i : ι) × M i
h : l ∈ _w₁✝.toList ∨ l ∈ _w₂✝.toList
⊢ l.snd ≠ 1

Tactic:
cases h

Goal state after:
case append.inl
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ∀ l ∈ _w₁✝.toList, l.snd ≠ 1
_w₂_ih✝ : ∀ l ∈ _w₂✝.toList, l.snd ≠ 1
l : (i : ι) × M i
h✝ : l ∈ _w₁✝.toList
⊢ l.snd ≠ 1

case append.inr
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ∀ l ∈ _w₁✝.toList, l.snd ≠ 1
_w₂_ih✝ : ∀ l ∈ _w₂✝.toList, l.snd ≠ 1
l : (i : ι) × M i
h✝ : l ∈ _w₂✝.toList
⊢ l.snd ≠ 1
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.prod = (singleton x✝ a✝).prod⁻¹

Tactic:
simp [inv, *]

Goal state after: