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

Goal state before:
pp: 𝕜 : Type u_1
inst✝²⁸ : NontriviallyNormedField 𝕜
E : Type u_2
E' : Type u_3
E''' : Type u_4
E'' : Type u
F : Type u_5
F' : Type u_6
inst✝²⁷ : NormedAddCommGroup E
inst✝²⁶ : NormedSpace 𝕜 E
inst✝²⁵ : NormedAddCommGroup E'
inst✝²⁴ : NormedSpace 𝕜 E'
inst✝²³ : NormedAddCommGroup E''
inst✝²² : NormedSpace 𝕜 E''
inst✝²¹ : NormedAddCommGroup E'''
inst✝²⁰ : NormedSpace 𝕜 E'''
inst✝¹⁹ : NormedAddCommGroup F
inst✝¹⁸ : NormedSpace 𝕜 F
inst✝¹⁷ : NormedAddCommGroup F'
inst✝¹⁶ : NormedSpace 𝕜 F'
H : Type u_7
inst✝¹⁵ : TopologicalSpace H
H' : Type u_8
inst✝¹⁴ : TopologicalSpace H'
G : Type u_9
inst✝¹³ : TopologicalSpace G
G' : Type u_10
inst✝¹² : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
M' : Type u_12
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 : ℕ∞ω
x✝¹ : M
f✝ : M → N
g✝ : M' → N'
x' : M'
inst✝³ : IsManifold I n M
inst✝² : IsManifold I' n M'
inst✝¹ : IsManifold J n N
inst✝ : IsManifold J' n N'
hf : IsImmersionAtOfComplement F I J n f✝ x✝¹
hg : IsImmersionAtOfComplement F' I' J' n g✝ x'
f : M → N
φ₁ : OpenPartialHomeomorph M H
ψ₁ : OpenPartialHomeomorph N G
g : M' → N'
φ₂ : OpenPartialHomeomorph M' H'
ψ₂ : OpenPartialHomeomorph N' G'
equiv₁ : (E × F) ≃L[𝕜] E''
hfprop : EqOn (↑(ψ₁.extend J) ∘ f ∘ ↑(φ₁.extend I).symm) (⇑equiv₁ ∘ fun x ↦ (x, 0)) (φ₁.extend I).target
equiv₂ : (E' × F') ≃L[𝕜] E'''
hgprop : EqOn (↑(ψ₂.extend J') ∘ g ∘ ↑(φ₂.extend I').symm) (⇑equiv₂ ∘ fun x ↦ (x, 0)) (φ₂.extend I').target
x : E × E'
x✝ : x ∈ (φ₁.extend I).target ×ˢ (φ₂.extend I').target
hx : x.1 ∈ (φ₁.extend I).target
hx' : x.2 ∈ (φ₂.extend I').target
⊢ (Prod.snd ∘ ↑((ψ₁.extend J).prod (ψ₂.extend J')) ∘ Prod.map f g ∘ ↑((φ₁.extend I).prod (φ₂.extend I')).symm) x =
    (Prod.snd ∘
        ⇑((ContinuousLinearEquiv.prodProdProdComm 𝕜 E E' F F').trans (equiv₁.prodCongr equiv₂)) ∘ fun x ↦ (x, 0))
      x

Tactic:
simpa using hgprop hx'

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

Goal state before:
pp: x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
⊢ (toLp 2 fun x_1 ↦ y - ↑⟨max (y - (↑⟨z, hz⟩).ofLp 0) x, ⋯⟩).ofLp i = z.ofLp i

Tactic:
have A : x ≤ y - z 0 := by linarith

Goal state after:
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
A : x ≤ y - z.ofLp 0
⊢ (toLp 2 fun x_1 ↦ y - ↑⟨max (y - (↑⟨z, hz⟩).ofLp 0) x, ⋯⟩).ofLp i = z.ofLp i
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case h'x
𝕜 : 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
⊢ ↑(extChartAt I x₀) x₀ ∈ ↑(extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target

Tactic:
simp [hsu hx₀]

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

Goal state before:
pp: H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
U V : Opens ↑(TopCat.of M)
i : U ⟶ V
f : ↥V → M'
h : ChartedSpace.LiftProp P f
⊢ ChartedSpace.LiftProp P fun x ↦ f (i x)

Tactic:
x

Goal state after:
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
U V : Opens ↑(TopCat.of M)
i : U ⟶ V
f : ↥V → M'
h : ChartedSpace.LiftProp P f
x : ↥U
⊢ ChartedSpace.LiftPropAt P (fun x ↦ f (i x)) x
Module: Mathlib.Geometry.Manifold.Sheaf.Basic

Goal state before:
pp: H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
V : Opens ↑(TopCat.of M)
f : ↥V → M'
h : ∀ (x : ↥V), ∃ V_1, ∃ (_ : ↑x ∈ V_1), ∃ i, ChartedSpace.LiftProp P fun x ↦ f (i x)
⊢ ChartedSpace.LiftProp P f

Tactic:
x

Goal state after:
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
V : Opens ↑(TopCat.of M)
f : ↥V → M'
h : ∀ (x : ↥V), ∃ V_1, ∃ (_ : ↑x ∈ V_1), ∃ i, ChartedSpace.LiftProp P fun x ↦ f (i x)
x : ↥V
⊢ ChartedSpace.LiftPropAt P f x
Module: Mathlib.Geometry.Manifold.Sheaf.Basic

Goal state before:
pp: H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
V : Opens ↑(TopCat.of M)
f : ↥V → M'
h : ∀ (x : ↥V), ∃ V_1, ∃ (_ : ↑x ∈ V_1), ∃ i, ChartedSpace.LiftProp P fun x ↦ f (i x)
x : ↥V
U : Opens ↑(TopCat.of M)
hxU : ↑x ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp P (f ∘ ⇑i)
x' : ↥U := ⟨↑x, hxU⟩
hUV : U ≤ V
this : ChartedSpace.LiftPropAt P f (Opens.inclusion hUV x')
⊢ ChartedSpace.LiftPropAt P f x

Tactic:
convert! this

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
x : M
⊢ ∃ C > 0, ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y)‖ < C

Tactic:
rcases eventually_norm_symmL_trivializationAt_lt E (fun (x : M) ↦ TangentSpace% x) x
    with ⟨C, C_pos, hC⟩
  refine ⟨C, C_pos, ?_⟩
  have hx : (chartAt H x).source ∈ 𝓝 x := chart_source_mem_nhds H x
  filter_upwards [hC, hx] with y hy h'y
  rw [TangentBundle.symmL_trivializationAt h'y] at hy
  have A : (extChartAt I x).symm (extChartAt I x y) = y :=
    (extChartAt I x).left_inv (by simpa using h'y)
  convert! hy using 3 <;> congr

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)
A :
  ContDiffWithinAt 𝕜 m' (lieBracketWithin 𝕜 U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s))
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
B :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m'
    (fun x₀ ↦ ⟨x₀, mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x₀⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
C :
  ContMDiffWithinAt I I.tangent m'
    (fun x_1 ↦
      ⟨x_1,
        mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
          (mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)) x_1⟩)
    s x
⊢ m' + 1 + 1 ≤ ?m.1064

Tactic:
by gcongr

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)
A :
  ContDiffWithinAt 𝕜 m' (lieBracketWithin 𝕜 U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s))
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
B :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m'
    (fun x₀ ↦ ⟨x₀, mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) x₀⟩)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
C :
  ContMDiffWithinAt I I.tangent m'
    (fun x_1 ↦
      ⟨x_1,
        mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
          (mlieBracketWithin 𝓘(𝕜, E) U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)) x_1⟩)
    s x
⊢ m' + 1 + 1 ≤ ?m.1119

Tactic:
by gcongr

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

Goal state before:
pp: 𝕜 : Type u_1
E' : Type u_2
E'' : Type u_3
E''' : Type u_4
F : Type u_5
F' : Type u_6
H : Type u_7
H' : Type u_8
G : Type u_9
G' : Type u_10
E : Type u
inst✝²⁸ : NontriviallyNormedField 𝕜
inst✝²⁷ : NormedAddCommGroup E
inst✝²⁶ : NormedSpace 𝕜 E
inst✝²⁵ : NormedAddCommGroup E'
inst✝²⁴ : NormedSpace 𝕜 E'
inst✝²³ : NormedAddCommGroup E''
inst✝²² : NormedSpace 𝕜 E''
inst✝²¹ : NormedAddCommGroup E'''
inst✝²⁰ : NormedSpace 𝕜 E'''
inst✝¹⁹ : NormedAddCommGroup F
inst✝¹⁸ : NormedSpace 𝕜 F
inst✝¹⁷ : NormedAddCommGroup F'
inst✝¹⁶ : NormedSpace 𝕜 F'
inst✝¹⁵ : TopologicalSpace H
inst✝¹⁴ : TopologicalSpace H'
inst✝¹³ : TopologicalSpace G
inst✝¹² : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
M' : Type u_12
N : Type u_13
N' : Type u_14
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
inst✝⁹ : TopologicalSpace M'
inst✝⁸ : ChartedSpace H' M'
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace G' N'
n : ℕ∞ω
x✝¹ : M
f✝ : M → N
g✝ : M' → N'
x' : M'
inst✝³ : IsManifold I n M
inst✝² : IsManifold I' n M'
inst✝¹ : IsManifold J n N
inst✝ : IsManifold J' n N'
hf : IsSubmersionAtOfComplement F I J n f✝ x✝¹
hg : IsSubmersionAtOfComplement F' I' J' n g✝ x'
f : M → N
φ₁ : OpenPartialHomeomorph M H
ψ₁ : OpenPartialHomeomorph N G
g : M' → N'
φ₂ : OpenPartialHomeomorph M' H'
ψ₂ : OpenPartialHomeomorph N' G'
equiv₁ : E ≃L[𝕜] E'' × F
hfprop : EqOn (↑(ψ₁.extend J) ∘ f ∘ ↑(φ₁.extend I).symm) (Prod.fst ∘ ⇑equiv₁) (φ₁.extend I).target
equiv₂ : E' ≃L[𝕜] E''' × F'
hgprop : EqOn (↑(ψ₂.extend J') ∘ g ∘ ↑(φ₂.extend I').symm) (Prod.fst ∘ ⇑equiv₂) (φ₂.extend I').target
x : E × E'
x✝ : x ∈ (φ₁.extend I).target ×ˢ (φ₂.extend I').target
hx : x.1 ∈ (φ₁.extend I).target
hx' : x.2 ∈ (φ₂.extend I').target
⊢ (Prod.snd ∘ ↑((ψ₁.extend J).prod (ψ₂.extend J')) ∘ Prod.map f g ∘ ↑((φ₁.extend I).prod (φ₂.extend I')).symm) x =
    (Prod.snd ∘ Prod.fst ∘ ⇑((equiv₁.prodCongr equiv₂).trans (ContinuousLinearEquiv.prodProdProdComm 𝕜 E'' F E''' F')))
      x

Tactic:
simpa using hgprop hx'

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₁)
this : ‖γ' t₁ - γ' 0‖ₑ < ↑r
⊢ ‖γ' t₁ - ↑(extChartAt I x) x‖ₑ < ↑r

Tactic:
convert! this

Goal state after:
case e'_3
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₁)
this : ‖γ' t₁ - γ' 0‖ₑ < ↑r
⊢ ↑(extChartAt I x) x = γ' 0
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

Goal state before:
pp: case mp
𝕜 : 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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
h : cov.torsion = 0
X Y : (x : M) → TangentSpace I x
⊢ ∀ {x : M}, MDiffAt (T% X) x → MDiffAt (T% Y) x → (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y x

Tactic:
x

Goal state after:
case mp
𝕜 : 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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
h : cov.torsion = 0
X Y : (x : M) → TangentSpace I x
x : M
⊢ MDiffAt (T% X) x → MDiffAt (T% Y) x → (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y x
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

Goal state before:
pp: case mp
𝕜 : 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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
X Y : (x : M) → TangentSpace I x
x : M
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
h : ((cov.torsion x) (X x)) (Y x) = ((0 x) (X x)) (Y x)
⊢ (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y x

Tactic:
rw [cov.torsion_apply hX hY] at h

Goal state after:
case mp
𝕜 : 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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
X Y : (x : M) → TangentSpace I x
x : M
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
h : (↑cov Y x) (X x) - (↑cov X x) (Y x) - mlieBracket I X Y x = ((0 x) (X x)) (Y x)
⊢ (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y x
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: case «1»
P : Type u_3
n : ℕ
inst✝ : NeZero 1
poly : Polygon P 1
h : poly.HasNondegenerateEdges
hlt : 1 < 2
⊢ False

Tactic:
exact h 0 (by simp)

Goal state after:
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Fintype (ConjClasses G)
inst✝¹ : Fintype G
inst✝ : (x : ConjClasses G) → Fintype ↑x.carrier
this : (x : ConjClasses G) × ↑x.carrier ≃ G
⊢ ∑ x, x.carrier.toFinset.card = Fintype.card G

Tactic:
simpa using! (Fintype.card_congr this)

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

Goal state before:
pp: case succ
n : ℕ
i : ZMod n
k : ℕ
IH : r i ^ k = r (i * ↑k)
⊢ r (i * ↑k) * r i = r (i * ↑(k + 1))

Tactic:
r_mul_r,

Goal state after:
case succ
n : ℕ
i : ZMod n
k : ℕ
IH : r i ^ k = r (i * ↑k)
⊢ r (i * ↑k + i) = r (i * ↑(k + 1))
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
k : ℤ
⊢ r 1 ^ k = r ↑k

Tactic:
simp only [r_zpow, one_mul]

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
ω : List B
hω : cs.IsReduced ω
h : cs.length (cs.wordProd ω) = 0
this : ω = []
⊢ cs.wordProd ω = 1

Tactic:
rw [this, wordProd_nil]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos.mp
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList = []
m₂ m₁ : M (w.toList.head hnil).fst
hw : ⟨(w.toList.head hnil).fst, m₁⟩ ∉ w.toList.tail
hm1 : ¬m₁ = 1
⊢ m₁ = m₂ * (w.toList.head ⋯).snd →
    (∃ m', w.toList.head hnil = ⟨(w.toList.head hnil).fst, m'⟩ ∧ m₁ = m₂ * m') ∨
      ¬w.fstIdx = some (w.toList.head hnil).fst ∧ m₁ = m₂

Tactic:
rintro rfl
          exact Or.inl ⟨_, rfl, rfl⟩

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)⁻¹ ≠ cs.length w

Tactic:
simpa using cs.length_mul_simple_ne w⁻¹ i

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
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
x : G
⊢ qi (q x) ∈ s

Tactic:
by simp [s]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
x : M i
hnotone : x * w.head ≠ 1
⊢ (w.mulHead x hnotone).head = x * w.head

Tactic:
induction w
  · rfl
  · simp [*, mulHead]

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:
by
  rw [mk_add_mk, mk_eq_mk]
  exact ⟨1, by simp [smul_smul]⟩

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
⊢ mk H K a = mk H K b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k

Tactic:
by
  rw [eq'']
  exact rel_iff

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : i = k
⊢ (lift f) w.prod ≠ 1

Tactic:
by_cases hl : j = k

Goal state after:
case pos
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : i = k
hl : j = k
⊢ (lift f) w.prod ≠ 1

case neg
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : i = k
hl : ¬j = k
⊢ (lift f) w.prod ≠ 1