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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_7
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
n : ℕ∞ω
M' : Type u_15
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M'
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I n M'
⊢ IsImmersionOfComplement Unit I I n Sum.inl

Tactic:
by
  intro x
  apply IsImmersionAtOfComplement.mk_of_continuousAt (equiv := (.prodUnique 𝕜 E _))
    (by fun_prop) _ _ (mem_chart_source H x) (mem_chart_source H (Sum.inl x))
    (IsManifold.chart_mem_maximalAtlas x) (IsManifold.chart_mem_maximalAtlas (Sum.inl x))
  intro y hy
  have : I ((chartAt H x) ((chartAt H x).symm (I.symm y))) = y := by
    rw [(chartAt H x).right_inv (by simp_all), I.right_inv (by simp_all)]
  simpa

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
inst✝¹² : NormedAddCommGroup E'''
inst✝¹¹ : NormedSpace 𝕜 E'''
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁸ : TopologicalSpace H
G : Type u_9
inst✝⁷ : TopologicalSpace G
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
φ : N → N'
hφ : IsImmersionOfComplement F J J' n φ
x✝ : Continuous[inst✝⁵, inst✝³] f ∧ ContMDiff I J' n (φ ∘ f)
x : M
h : Continuous[inst✝⁵, inst✝³] f
h' : ContMDiff I J' n (φ ∘ f)
⊢ ContMDiffAt I J n f x

Tactic:
ContMDiffAt.iff_comp_isImmersionAtOfComplement (hφ (f x))

Goal state after:
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
inst✝¹² : NormedAddCommGroup E'''
inst✝¹¹ : NormedSpace 𝕜 E'''
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁸ : TopologicalSpace H
G : Type u_9
inst✝⁷ : TopologicalSpace G
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
f : M → N
φ : N → N'
hφ : IsImmersionOfComplement F J J' n φ
x✝ : Continuous[inst✝⁵, inst✝³] f ∧ ContMDiff I J' n (φ ∘ f)
x : M
h : Continuous[inst✝⁵, inst✝³] f
h' : ContMDiff I J' n (φ ∘ f)
⊢ ContinuousAt f x ∧ ContMDiffAt I J' n (φ ∘ f) x
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
n : ℕ∞ω
x : E
h : x ∈ {x | ((innerSL ℝ) v) x ≠ 1}
⊢ 1 - ((innerSL ℝ) v) x ≠ 0

Tactic:
h'

Goal state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
n : ℕ∞ω
x : E
h : x ∈ {x | ((innerSL ℝ) v) x ≠ 1}
h' : 1 - ((innerSL ℝ) v) x = 0
⊢ False
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
h₁ : (ℝ ∙ v)ᗮ.orthogonalProjectionOnto v = 0
h₂ : ⟪v, ↑w⟫ = 0
⊢ (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • ⟪v, ↑w⟫ + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • ⟪v, v⟫))) • (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • ⟪v, ↑w⟫ + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • ⟪v, v⟫))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto v =
    w

Tactic:
have h₃ : ⟪v, v⟫ = 1 := by simp [hv]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
h₁ : (ℝ ∙ v)ᗮ.orthogonalProjectionOnto v = 0
h₂ : ⟪v, ↑w⟫ = 0
h₃ : ⟪v, v⟫ = 1
⊢ (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • ⟪v, ↑w⟫ + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • ⟪v, v⟫))) • (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • ⟪v, ↑w⟫ + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • ⟪v, v⟫))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto v =
    w
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ Injective
    ⇑(fderivWithin ℝ (writtenInExtChartAt (𝓡 n) 𝓘(ℝ, E) v Subtype.val) (Set.range ↑(𝓡 n)) (↑(extChartAt (𝓡 n) v) v))

Tactic:
simp only [chartAt, fderivWithin_univ, mfld_simps]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ Injective
    ⇑(fderiv ℝ (↑(ChartedSpace.chartAt ↑v) ∘ Subtype.val ∘ ↑(ChartedSpace.chartAt v).symm)
        (↑(ChartedSpace.chartAt v) v))
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ ContMDiff (𝓡 1) (𝓡 1) ω fun a ↦ a⁻¹

Tactic:
apply ContMDiff.codRestrict_sphere
    simp only [← Circle.coe_inv, Circle.coe_inv_eq_conj]
    exact Complex.conjCLE.contDiff.contMDiff.comp contMDiff_coe_sphere

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
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : (MDiffAt fun x ↦ ⟨x, 0⟩) x
⊢ (fderivWithin 𝕜 (fun x' ↦ (x', 0)) (range ↑I) (↑I (↑(chartAt H x) x))) v = (v, 0)

Tactic:
rw [fderivWithin_eq_fderiv, DifferentiableAt.fderiv_prodMk]

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))
A : (MDiffAt fun x ↦ ⟨x, 0⟩) x
⊢ ((fderiv 𝕜 (fun x' ↦ x') (↑I (↑(chartAt H x) x))).prod (fderiv 𝕜 (fun x' ↦ 0) (↑I (↑(chartAt H x) x)))) v = (v, 0)

case hf₁
𝕜 : 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
⊢ DifferentiableAt 𝕜 (fun x' ↦ x') (↑I (↑(chartAt H x) x))

case hf₂
𝕜 : 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
⊢ DifferentiableAt 𝕜 (fun x' ↦ 0) (↑I (↑(chartAt H x) x))

case hs
𝕜 : 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
⊢ UniqueDiffWithinAt 𝕜 (range ↑I) (↑I (↑(chartAt H x) x))

case h
𝕜 : 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
⊢ DifferentiableAt 𝕜 (fun x' ↦ (x', 0)) (↑I (↑(chartAt H x) x))
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 2 M
inst✝² : IsManifold I' 2 M'
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace E'
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 : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
A' : x₀ = ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)
h'f : MDiffAt[s] f x₀
this : (mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)).inverse = mfderiv% ↑(extChartAt I x₀) x₀
V' : (x : E') → TangentSpace 𝓘(𝕜, E') x := ⋯
hV' : V' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) V (range ↑I')
W' : (x : E') → TangentSpace 𝓘(𝕜, E') x := ⋯
hW' : W' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) W (range ↑I')
F : E → E' := ⋯
hF : F = (↑(extChartAt I' (f x₀)) ∘ f) ∘ ↑(extChartAt I x₀).symm
hFx₀ : ↑(extChartAt I' (f x₀)) (f x₀) = F (↑(extChartAt I x₀) x₀)
P :
  ∀ (Y : (x : M') → TangentSpace I' x),
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm) (mpullbackWithin I I' f Y s)
        (range ↑I) =ᶠ[𝓝[↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x₀) x₀]
      mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') F (mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) Y (range ↑I'))
        (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I)
⊢ MapsTo (↑(extChartAt I x₀).symm) (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) s

Tactic:
exact (mapsTo_preimage _ _).mono_left inter_subset_left

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

Goal state before:
pp: case hV
𝕜 : 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 2 M
inst✝² : IsManifold I' 2 M'
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace E'
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 : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
A' : x₀ = ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)
h'f : MDiffAt[s] f x₀
this : (mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)).inverse = mfderiv% ↑(extChartAt I x₀) x₀
V' : (x : E') → TangentSpace 𝓘(𝕜, E') x := mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) V (range ↑I')
hV' : V' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) V (range ↑I')
W' : (x : E') → TangentSpace 𝓘(𝕜, E') x := mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) W (range ↑I')
hW' : W' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) W (range ↑I')
F : E → E' := (↑(extChartAt I' (f x₀)) ∘ f) ∘ ↑(extChartAt I x₀).symm
hF : F = (↑(extChartAt I' (f x₀)) ∘ f) ∘ ↑(extChartAt I x₀).symm
hFx₀ : ↑(extChartAt I' (f x₀)) (f x₀) = F (↑(extChartAt I x₀) x₀)
P :
  ∀ (Y : (x : M') → TangentSpace I' x),
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm) (mpullbackWithin I I' f Y s)
        (range ↑I) =ᶠ[𝓝[↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x₀) x₀]
      mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') F (mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) Y (range ↑I'))
        (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I)
⊢ DifferentiableWithinAt 𝕜 V' (↑(extChartAt I' (f x₀)).symm ⁻¹' t ∩ range ↑I') (F (↑(extChartAt I x₀) x₀))

Tactic:
rw [← hFx₀]
    exact hV.differentiableWithinAt_mpullbackWithin_vectorField

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 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
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 : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
hfi : (mfderiv[s] f x₀).IsInvertible
this : CompleteSpace E'
u : Set M
u_open : IsOpen[inst✝⁹] u
x₀u : x₀ ∈ u
hu : ContMDiffOn I I' 2 f (insert x₀ s ∩ u)
⊢ ∃ u,
    IsOpen[inst✝⁹] u ∧
      x₀ ∈ u ∧ s ∩ u ⊆ f ⁻¹' t ∧ s ∩ u ⊆ f ⁻¹' (extChartAt I' (f x₀)).source ∧ ContMDiffOn I I' 2 f (s ∩ u)

Tactic:
have : f ⁻¹' (extChartAt I' (f x₀)).source ∈ 𝓝[s] x₀ :=
      hf.continuousWithinAt.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds (f x₀))

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 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
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 : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
hfi : (mfderiv[s] f x₀).IsInvertible
this✝ : CompleteSpace E'
u : Set M
u_open : IsOpen[inst✝⁹] u
x₀u : x₀ ∈ u
hu : ContMDiffOn I I' 2 f (insert x₀ s ∩ u)
this : f ⁻¹' (extChartAt I' (f x₀)).source ∈ 𝓝[s] x₀
⊢ ∃ u,
    IsOpen[inst✝⁹] u ∧
      x₀ ∈ u ∧ s ∩ u ⊆ f ⁻¹' t ∧ s ∩ u ⊆ f ⁻¹' (extChartAt I' (f x₀)).source ∧ ContMDiffOn I I' 2 f (s ∩ u)
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ ↑(carrier (Quot.mk (⇑(IsConj.setoid G)) g)).toFinset = ↑{g}

Tactic:
simpa using hg.eq_singleton_of_mem mem_carrier_mk

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

Goal state before:
pp: 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✝ : CompactSpace M
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ IsClosedEmbedding e ∧ ∀ (x : M), Injective ⇑(mfderiv% e x)

Tactic:
by
  rcases SmoothBumpCovering.exists_isSubordinate I isClosed_univ fun (x : M) _ => univ_mem with
    ⟨ι, f, -⟩
  have := f.fintype
  rcases f.exists_immersion_euclidean with ⟨n, e, hsmooth, hinj, hinj_mfderiv⟩
  exact ⟨n, e, hsmooth, hsmooth.continuous.isClosedEmbedding hinj, hinj_mfderiv⟩

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

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

Tactic:
· exact congr_arg sr (add_zero a)

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

Goal state before:
pp: case inr.a.r
n : ℕ
hn : NeZero n
m : ZMod n
⊢ n = n / n.gcd m.val * gcd n m.val

Tactic:
exact (Nat.div_mul_cancel (Nat.gcd_dvd_left n m.val)).symm

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

Goal state before:
pp: case inr.a
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (DihedralGroup n) ∣ lcm n 2

Tactic:
apply Monoid.exponent_dvd_of_forall_pow_eq_one
    rintro (m | m)
    · rw [← orderOf_dvd_iff_pow_eq_one, orderOf_r]
      refine Nat.dvd_trans ⟨gcd n m.val, ?_⟩ (dvd_lcm_left n 2)
      exact (Nat.div_mul_cancel (Nat.gcd_dvd_left n m.val)).symm
    · rw [← orderOf_dvd_iff_pow_eq_one, orderOf_sr]
      exact dvd_lcm_right n 2

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
hn : Odd n
⊢ 2 ∣ n + 3

Tactic:
rw [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, Nat.odd_iff.mp hn]

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
this : (1 - δ * C) * ((g' x) w) w ≤ ((g' y) w) w
⊢ ((g' x) w) w ≤ r' ^ 2 * ((g' y) w) w

Tactic:
rw [← (le_div_iff₀' (lt_of_le_of_lt (by positivity) hδ)), div_eq_inv_mul] at this

Goal state after:
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
this : ((g' x) w) w ≤ (1 - δ * C)⁻¹ * ((g' y) w) w
⊢ ((g' x) w) w ≤ r' ^ 2 * ((g' y) w) w
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
fi : (i : ι) → M i →* N
x✝¹ x✝ : FreeMonoid ((i : ι) × M i)
⊢ Rel M x✝¹ x✝ ≤ (Con.ker (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd)) x✝¹ x✝

Tactic:
simp_rw [Con.ker_rel]
        rintro (i | ⟨x, y⟩) <;> simp

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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
w : Word M
⊢ rcons { head := 1, tail := empty, fstIdx_ne := ⋯ } = empty

Tactic:
simp [rcons]

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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
w✝ : Word M
j : ι
m : M j
w : Word M
h1 : w.fstIdx ≠ some j
h2 : m ≠ 1
x✝ : { p // rcons p = w }
ij : ¬i = j
⊢ rcons { head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ } = cons m w h1 h2

Tactic:
simp [rcons]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m : M i
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx ≠ some k
h2 : g ≠ 1
ih :
  ⟨i, m⟩ ∈
      (↑(consRecOn tail ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x ↦
              if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
              else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ tail.toList.tail ∨ ¬i = j ∧ ∃ (h : ¬tail.toList = []), tail.toList.head h = ⟨i, m⟩
h : j = k
⊢ ⟨i, m⟩ ∈ (↑⟨{ head := ⋯ ▸ g, tail := tail, fstIdx_ne := ⋯ }, ⋯⟩).tail.toList ↔
    ⟨i, m⟩ ∈ (cons g tail h1 h2).toList.tail ∨
      ¬i = j ∧ ∃ (h : ¬(cons g tail h1 h2).toList = []), (cons g tail h1 h2).toList.head h = ⟨i, m⟩

Tactic:
subst k
      by_cases hij : j = i <;> simp_all

Goal state after:
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 <;> aesop

Goal state after: