mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
h : t.orthocenter ∉ Set.range p
hs : Set.range p ⊆ Set.range t.points
⊢ Fintype.card ↑(Set.range t.points) ≤ Fintype.card ↑(Set.range p)

Tactic:
rw [Set.card_range_of_injective hpi, Set.card_range_of_injective t.independent.injective]

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

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
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ : C^∞⟮I, 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'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : f x = y
v : PointDerivation I x
k : 𝕜
g : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ k • v (ContMDiffMap.comp g f) = k * v (ContMDiffMap.comp g f)

Tactic:
smul_eq_mul

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
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ : C^∞⟮I, 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'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : f x = y
v : PointDerivation I x
k : 𝕜
g : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ k * v (ContMDiffMap.comp g f) = k * v (ContMDiffMap.comp g f)
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: E : Type u_5
H : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, F a < F (f x)
hF' : MapsTo (⇑F) s (Iic (F (f x)))
hFφ : IsLocalMax (⇑F ∘ f) x
h : fderiv ℝ (⇑F) (f x) ∘SL fderiv ℝ f x = 0
⊢ ∀ (y : E), F ((fderiv ℝ f x) y) = 0

Tactic:
ContinuousLinearMap.fderiv

Goal state after:
E : Type u_5
H : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, F a < F (f x)
hF' : MapsTo (⇑F) s (Iic (F (f x)))
hFφ : IsLocalMax (⇑F ∘ f) x
h : F ∘SL fderiv ℝ f x = 0
⊢ ∀ (y : E), F ((fderiv ℝ f x) y) = 0
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁰ : NormedAddCommGroup EB
inst✝⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁷ : TopologicalSpace B
inst✝⁶ : ChartedSpace HB B
inst✝⁵ : FiberBundle F E
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle 1 F E IB
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
s : (b : B) → E b
u : Set B
b₀ : B
hex₀ : b₀ ∈ e.baseSet
⊢ MDiffAt[u] (T% s) b₀ ↔ (MDiffAt[u] fun x ↦ (↑e ⟨x, s x⟩).2) b₀

Tactic:
rw [e.mdifferentiableWithinAt_totalSpace_iff IB]
  · change MDiffAt[u] (@id B) b₀ ∧ _ ↔ _
    simp [mdifferentiableWithinAt_id]
  exact (coe_mem_source e).mpr hex₀

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
x₀ : B
hs : MDiffAt (T% s) x₀
⊢ (MDiffAt fun x ↦ ⟨x, (-s) x⟩) x₀

Tactic:
by
  rw [← mdifferentiableWithinAt_univ] at hs ⊢
  exact mdifferentiableWithinAt_neg_section hs

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ interior (range ↑(𝓡∂ n)) = {y | 0 < y.ofLp 0}

Tactic:
by
  calc interior (range (𝓡∂ n))
    _ = interior ({ y | 0 ≤ y 0}) := by
      congr!
      apply range_euclideanHalfSpace
    _ = { y | 0 < y 0 } := interior_halfSpace _ _ _

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

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) :=
  ContinuousLinearEquiv.prodUnique ℝ (EuclideanSpace ℝ (Fin 1)) Unit
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := φ₀.trans (PiLp.equivOfUnique 2 ℝ fun x ↦ ℝ)
hz : ¬↑z < y
⊢ ↑z ∈ (Homeomorph.pointReflection (y / 2)).toOpenPartialHomeomorph.source

Tactic:
simp [Homeomorph.pointReflection]

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

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
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
⊢ (mfderiv[Icc x y] (f ∘ projIcc x y ⋯) ↑w) 1 = (mfderiv% f w) 1

Tactic:
by
  by_cases hw : MDiffAt f w; swap
  · rw [mfderiv_zero_of_not_mdifferentiableAt hw, mfderivWithin_zero_of_not_mdifferentiableWithinAt]
    · rfl
    · rwa [mdifferentiableWithinAt_comp_projIcc_iff]
  rw [mfderiv_comp_mfderivWithin (I' := 𝓡∂ 1)]; rotate_left
  · simp [hw]
  · exact (contMDiffOn_projIcc _ w.2).mdifferentiableWithinAt one_ne_zero
  · exact (uniqueDiffOn_Icc h.out _ w.2).uniqueMDiffWithinAt
  simp only [Function.comp_apply, ContinuousLinearMap.comp_apply]
  have : w = projIcc x y h.out.le (w : ℝ) := by rw [projIcc_of_mem]
  rw [projIcc_of_mem _ w.2]
  congr 1
  convert! mfderivWithin_projIcc_one w.2

Goal state after:
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
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(ℝ ∙ v)ᗮ := (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
pythag : 1 = a ^ 2 + ‖y‖ ^ 2
ha : 0 < 1 - a
⊢ (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • 4 • (2 / (1 - a)) • ↑y +
      (‖(2 / (1 - a)) • y‖ ^ 2 + 4)⁻¹ • (‖(2 / (1 - a)) • y‖ ^ 2 - 4) • v =
    a • v + ↑y

Tactic:
simp only [norm_smul, norm_div, Real.norm_eq_abs, abs_of_nonneg ha.le]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(ℝ ∙ v)ᗮ := (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
pythag : 1 = a ^ 2 + ‖y‖ ^ 2
ha : 0 < 1 - a
⊢ ((|2| / (1 - a) * ‖y‖) ^ 2 + 4)⁻¹ • 4 • (2 / (1 - a)) • ↑y +
      ((|2| / (1 - a) * ‖y‖) ^ 2 + 4)⁻¹ • ((|2| / (1 - a) * ‖y‖) ^ 2 - 4) • v =
    a • v + ↑y
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
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

Tactic:
rw [h₁, h₂, h₃]

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 • 0 + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • 1))) • (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • 0 + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • 1))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • 0 =
    w
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

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
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
⊢ -(ε / 2) < 0

Tactic:
by rw [neg_lt, neg_zero]; exact half_pos hε

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
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
hf : ContMDiff (𝓡∂ 1) I 1 f
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A : riemannianEDist I x y ≤ ∫⁻ (x_1 : ↑unitInterval), ‖(mfderiv% ⇑g x_1) 1‖ₑ
t : ℝ
ht : t ∈ Icc 0 1
⊢ (⇑g ∘ projIcc 0 1 ⋯) t = (γ ∘ ⇑η) t

Tactic:
simp only [Function.comp_apply, ht, projIcc_of_mem]

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✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
hf : ContMDiff (𝓡∂ 1) I 1 f
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A : riemannianEDist I x y ≤ ∫⁻ (x_1 : ↑unitInterval), ‖(mfderiv% ⇑g x_1) 1‖ₑ
t : ℝ
ht : t ∈ Icc 0 1
⊢ g ⟨t, ht⟩ = γ (η t)
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
⊢ ∫⁻ (t : ℝ) in Icc 0 1, ‖(fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y)) (Icc 0 1) t) 1‖ₑ =
    ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ

Tactic:
apply setLIntegral_congr_fun measurableSet_Icc (fun z hz ↦ ?_)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
z : ℝ
hz : z ∈ Icc 0 1
⊢ ‖(fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y)) (Icc 0 1) z) 1‖ₑ = ‖y - x‖ₑ
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 : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ < C

Tactic:
rcases eventually_norm_mfderivWithin_symm_extChartAt_comp_lt I x with ⟨C, C_pos, hC⟩
  refine ⟨C, C_pos, ?_⟩
  have : 𝓝 x = 𝓝 ((extChartAt I x).symm (extChartAt I x x)) := by simp
  rw [this] at hC
  have : ContinuousAt (extChartAt I x).symm (extChartAt I x x) := continuousAt_extChartAt_symm _
  filter_upwards [nhdsWithin_le_nhds (this.preimage_mem_nhds hC),
    extChartAt_target_mem_nhdsWithin x] with y hy h'y
  have : y = (extChartAt I x) ((extChartAt I x).symm y) := by simp [-extChartAt, h'y]
  simp only [preimage_ofPred_eq, mem_ofPred_eq] at hy
  convert! hy

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

Goal state before:
pp: case refine_2.refine_2
𝕜 : 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
EP : Type u_5
inst✝⁴ : NormedAddCommGroup EP
inst✝³ : NormedSpace 𝕜 EP
HP : Type u_6
inst✝² : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace HP P
U : Opens M
V : Opens ↑↑(ChartedSpace.locallyRingedSpace IM ↥U).toPresheafedSpace
x✝¹ :
  ↑(((TopCat.Presheaf.pushforward CommRingCat
              (LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.base).obj
          (ChartedSpace.locallyRingedSpace IM ↥U).presheaf).obj
      (Opposite.op (⋯.functor.obj V)))
g :
  (x :
      ↥(Opposite.unop
          ((Opens.map
                  (LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.base).op.obj
            (Opposite.op (⋯.functor.obj V))))) →
    (fun x ↦ 𝕜) ↑x
hg : (StructureGroupoid.LocalInvariantProp.localPredicate (↥U) 𝕜 ⋯).pred g
a : TopCat.of ↥U ⟶ TopCat.of M := TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ }
ha : IsOpenEmbedding ⇑(TopCat.Hom.hom a)
V' : Opens ↥U := (Opens.map a).obj (⋯.functor.obj V)
b : ↥V' ≃ₜ ↥(⋯.functor.obj V) := ⋯.homeomorphOfSubsetRange ⋯
x✝ :
  ↥(Opposite.unop
      ((Opens.map (LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.base).op.obj
        (Opposite.op (⋯.functor.obj V))))
⊢ b.symm ((Opposite.unop (Opposite.op (⋯.functor.obj V))).1.restrictPreimage Subtype.val x✝) = x✝

Tactic:
apply b.symm_apply_apply

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 : ℝ
r_pos : r > 0
hr : ball (↑(extChartAt I x) x) r ⊆ ↑(extChartAt I x).symm ⁻¹' v
⊢ ∃ c > 0, {y | riemannianEDist I x y < ↑c} ⊆ s

Tactic:
lift r to ℝ≥0 using r_pos.le

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
r_pos : ↑r > 0
hr : ball (↑(extChartAt I x) x) ↑r ⊆ ↑(extChartAt I x).symm ⁻¹' v
⊢ ∃ c > 0, {y | riemannianEDist I x y < ↑c} ⊆ s
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
hf : ContinuousAt f x
equiv : E ≃L[𝕜] E'' × F
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : domChart ∈ IsManifold.maximalAtlas I n M
hcodChart : codChart ∈ IsManifold.maximalAtlas J n N
hwrittenInExtend :
  EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (Prod.fst ∘ ⇑equiv) (domChart.extend I).target
⊢ IsSubmersionAt I J n f x

Tactic:
by
  have aux : IsSubmersionAtOfComplement F I J n f x := by
    apply IsSubmersionAtOfComplement.mk_of_continuousAt <;> assumption
  use aux.smallComplement, by infer_instance, by infer_instance
  rwa [← IsSubmersionAtOfComplement.congr_F aux.smallEquiv]

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

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
inst✝² : VectorBundle 𝕜 F V
ι : Type u_7
e : Trivialization F TotalSpace.proj
inst✝¹ : MemTrivializationAtlas e
b : Basis ι 𝕜 F
inst✝ : ContMDiffVectorBundle 1 F V I
x : M
s s' : (x : M) → V x
i : ι
hss' : s x = s' x
⊢ (localFrameCoeff I e b i x) (s x) = (localFrameCoeff I e b i x) (s' x)

Tactic:
by
  simpa using! (isLocalFrameOn_localFrame_baseSet I 1 e b).coeff_congr hss' i

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
σ τ : (x : M) → V x
x : M
X₀ : TangentSpace I x
⊢ (derivMetricTensorAux I cov σ τ x) X₀ =
    ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) X₀ - inner ℝ ((↑cov σ x) X₀) (τ x) - inner ℝ (σ x) ((↑cov τ x) X₀)

Tactic:
rw [real_inner_comm]

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
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
σ τ : (x : M) → V x
x : M
X₀ : TangentSpace I x
⊢ (derivMetricTensorAux I cov σ τ x) X₀ =
    ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) X₀ - inner ℝ (τ x) ((↑cov σ x) X₀) - inner ℝ (σ x) ((↑cov τ x) X₀)
Module: Mathlib.Geometry.Polygon.Basic

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

Tactic:
interval_cases n

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

case «1»
P : Type u_3
n : ℕ
inst✝ : NeZero 1
poly : Polygon P 1
h : poly.HasNondegenerateEdges
hlt : 1 < 2
⊢ False
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
n : ℕ
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : NeZero n
inst✝ : Nontrivial R
poly : Polygon P n
h : HasNondegenerateVertices R poly
this : 2 ≤ n
hlt : n < 3
⊢ False

Tactic:
interval_cases n

Goal state after:
case «2»
R : Type u_1
V : Type u_2
P : Type u_3
n : ℕ
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : AddTorsor V P
inst✝¹ : Nontrivial R
inst✝ : NeZero 2
poly : Polygon P 2
h : HasNondegenerateVertices R poly
this : 2 ≤ 2
hlt : 2 < 3
⊢ False
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G

Tactic:
cases nonempty_fintype G
  simp [← sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype]

Goal state after:
Module: Mathlib.GroupTheory.Commensurable

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : ConjAct G
a b : ↥K
⊢ a⁻¹ * b ∈ H.subgroupOf K ↔ ((equivSMul g K) a)⁻¹ * (equivSMul g K) b ∈ (g • H).subgroupOf (g • K)

Tactic:
mem_subgroupOf,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : ConjAct G
a b : ↥K
⊢ ↑(a⁻¹ * b) ∈ H ↔ ((equivSMul g K) a)⁻¹ * (equivSMul g K) b ∈ (g • H).subgroupOf (g • K)
Module: Mathlib.GroupTheory.Commensurable

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : ConjAct G
a b : ↥K
⊢ ↑(a⁻¹ * b) ∈ H ↔ ((equivSMul g K) a)⁻¹ * (equivSMul g K) b ∈ (g • H).subgroupOf (g • K)

Tactic:
mem_subgroupOf,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : ConjAct G
a b : ↥K
⊢ ↑(a⁻¹ * b) ∈ H ↔ ↑(((equivSMul g K) a)⁻¹ * (equivSMul g K) b) ∈ g • H