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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).ninePointCircle = { center := f s.ninePointCircle.center, radius := s.ninePointCircle.radius }

Tactic:
ext
  · simp [ninePointCircle_center, centroid_map]
  · simp [ninePointCircle_radius]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ Similar v₁ v₂ ↔ ∃ r, 0 < r ∧ Pairwise fun i₁ i₂ ↦ dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)

Tactic:
by
  simp_rw [similar_iff_exists_pairwise_dist_eq]
  simp_rw [← pos_iff_ne_zero, NNReal.exists, ← NNReal.coe_pos, NNReal.coe_mk]
  grind

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
⊢ Similar ![a, b, c] ![a', b', c']

Tactic:
apply Similar.of_exists_pos_pairwise_dist_eq

Goal state after:
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := ⋯
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
⊢ ∃ r,
    0 < r ∧ Pairwise fun i₁ i₂ ↦ dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
⊢ ‖x - y‖ * ‖x + y‖ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2|

Tactic:
have hzy : ⟪z, y⟫ = 0 := by
    rwa [inner_eq_zero_iff_angle_eq_pi_div_two, ← norm_add_eq_norm_sub_iff_angle_eq_pi_div_two,
      eq_comm]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₃ : ‖z - y‖ = ‖z + y‖
r : ℝ
hr : x = r • y
hzy : ⟪z, y⟫ = 0
⊢ ‖x - y‖ * ‖x + y‖ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2|
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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ -(∑ x ∈ fs,
            (∑ x_1,
                (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
                    ((if x_1 = i₁ then 1 else 0) - if x_1 = i₂ then 1 else 0) *
                  (dist (s.points x) (s.points x_1) * dist (s.points x) (s.points x_1)) +
              (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) * (0 - 0) *
                (dist (s.points x) s.circumcenter * dist (s.points x) s.circumcenter)) +
          (∑ x ∈ fs,
              -2 / ↑(n + 1) * ((if x = i₁ then 1 else 0) - if x = i₂ then 1 else 0) *
                (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) +
            -2 / ↑(n + 1) * (0 - 0) * (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
      2 =
    0

pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ ∀ x ∈ univ,
    x ∉ fs →
      -2 / ↑(n + 1) * ((if x = i₁ then 1 else 0) - if x = i₂ then 1 else 0) *
          (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) =
        0

Tactic:
· simp_rw [fs, sum_insert (notMem_singleton.2 h), sum_singleton]
      repeat rw [← sum_subset fs.subset_univ _]
      · simp_rw [fs, sum_insert (notMem_singleton.2 h), sum_singleton]
        simp [h, Ne.symm h, dist_comm (s.points i₁)]
      all_goals intro i _ hi; simp [hfs i hi]

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ ∀ x ∈ univ,
    x ∉ fs →
      -2 / ↑(n + 1) * ((if x = i₁ then 1 else 0) - if x = i₂ then 1 else 0) *
          (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) =
        0
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : Sphere P
n : ℕ
inst✝ : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Ioo 0 1
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P := (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points) w)) r
hp' : p' -ᵥ sx.points i = r • ((Finset.affineCombination ℝ Finset.univ sx.points) w -ᵥ sx.points i)
⊢ (Finset.affineCombination ℝ Finset.univ sx.points) (r • (w - Pi.single i 1) + Pi.single i 1) ∈
    (sx.faceOpposite i).interior

Tactic:
Affine.Simplex.faceOpposite

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : Sphere P
n : ℕ
inst✝ : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Ioo 0 1
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P := (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points) w)) r
hp' : p' -ᵥ sx.points i = r • ((Finset.affineCombination ℝ Finset.univ sx.points) w -ᵥ sx.points i)
⊢ (Finset.affineCombination ℝ Finset.univ sx.points) (r • (w - Pi.single i 1) + Pi.single i 1) ∈ (sx.face ⋯).interior
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b t p : P
s : Sphere P
ha : a ∈ s
hb : b ∈ s
hp : p ∈ line[ℝ, a, b]
h_tangent : s.IsTangentAt t line[ℝ, p, t]
⊢ dist p t ^ 2 = dist p a * dist p b

Tactic:
by
  have hr := radius_nonneg_of_mem ha
  have radius_le_dist := h_tangent.isTangent.radius_le_dist_center (left_mem_affineSpan_pair ℝ p t)
  rw [mul_dist_eq_power_of_radius_le_dist_center hr hp ha hb radius_le_dist,
    Sphere.power, h_tangent.dist_sq_eq_of_mem (left_mem_affineSpan_pair ℝ p t)]
  ring

Goal state after:
Module: Mathlib.Geometry.Group.Growth.QuotientInter

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x ↦ x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' ↑A ^ m)
hφA : ∀ {a : G ⧸ H}, a ∈ ⇑π '' ↑A ^ m → φ a ∈ A ^ m
hπφ : ∀ {a : G ⧸ H}, a ∈ ⇑π '' ↑A ^ m → π (φ a) = a
a₁ b₁ : G
hb₁ : b₁ ∈ ↑A ^ m
ha₁ : a₁ ∈ H
a₂ b₂ : G
hb₂ : b₂ ∈ ↑A ^ m
ha₂ : a₂ ∈ H
hab : φ (π b₁) * a₁ = φ (π b₂) * a₂
hπa₁ : π a₁ = 1
hπa₂ : π a₂ = 1
hπb : π b₁ = π b₂
⊢ φ (π b₁) = φ (π b₂) ∧ a₁ = a₂

Tactic:
simp_all

Goal state after:
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
hu : Set.univ = {j₁, j₂, j₃}
⊢ {t₁.orthocenter, t₂.points j₂, t₂.points j₃} ⊆ ↑(affineSpan ℝ (Set.range t₁.points))

Tactic:
h₂,

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
hu : Set.univ = {j₁, j₂, j₃}
⊢ {t₁.orthocenter, t₁.points i₂, t₂.points j₃} ⊆ ↑(affineSpan ℝ (Set.range t₁.points))
Module: Mathlib.Geometry.Group.Growth.QuotientInter

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x ↦ x ∈ H
inst✝ : H.Normal
A : Finset G
hAsymm : A⁻¹ = A
π : G →* G ⧸ H := QuotientGroup.mk' H
a : G
ha : a ∈ A
⊢ #({x ∈ A⁻¹ * A | x ∈ H}) = #({x ∈ A ^ 2 | x ∈ H})

Tactic:
by simp [hAsymm, sq]

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent

Goal state before:
pp: case e_f.e_f.hc
𝕜 : 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✝⁶ : IsManifold I 1 M
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)
x₀ x : N
hx : f x ∈ (chartAt H (f x₀)).source
hy : g x ∈ (chartAt H' (g x₀)).source
⊢ MDiffAt[range ↑I] ↑(extChartAt I (f x₀)).symm (↑(extChartAt I (f x₀)) (f x))

Tactic:
apply mdifferentiableWithinAt_extChartAt_symm
      apply (extChartAt I (f x₀)).map_source
      simpa using hx

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

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
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g h : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝕜⟯⟨g * h⟩
⊢ ((𝒅 ((𝑳 I g).comp (𝑳 I h)) 1) ((evalAt 1) X)) f = ((𝒅 (𝑳 I g) h) ((evalAt h) X)) f

Tactic:
fdifferential_comp,

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
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g h : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝕜⟯⟨g * h⟩
⊢ ((𝒅 (𝑳 I g) ((𝑳 I h) 1) ∘ₗ 𝒅 (𝑳 I h) 1) ((evalAt 1) X)) f = ((𝒅 (𝑳 I g) h) ((evalAt h) X)) f
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
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
EM : Type u_10
inst✝¹³ : NormedAddCommGroup EM
inst✝¹² : NormedSpace 𝕜 EM
HM : Type u_11
inst✝¹¹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace HM M
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
e' : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e'
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : MDiffAt[s] (TotalSpace.proj ∘ f) x₀
he'f : (MDiffAt[s] fun x ↦ (↑e (f x)).2) x₀
he : (f x₀).proj ∈ e.baseSet
he' : (f x₀).proj ∈ e'.baseSet
y : M
hy : y ∈ TotalSpace.proj ∘ f ⁻¹' e.baseSet
⊢ (↑e' (f y)).2 = e.coordChange e' ((TotalSpace.proj ∘ f) y) (↑e (f y)).2

Tactic:
simp_all

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
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
ht : LocallyFinite fun i ↦ {x | t i x ≠ 0}
ht' : ∀ (i : ι), MDiffAt[u] (T% t) x₀
⊢ (MDiffAt[u] fun x ↦ ⟨x, ∑ᶠ (i : ι), t i x⟩) x₀

Tactic:
by
  apply (MDifferentiableWithinAt.sum_section_of_locallyFinite ht ht').congr' (t := Set.univ)
      (fun y hy ↦ ?_) (by grind) trivial
  choose U hu hfin using ht y
  have : {x | t x y ≠ 0} ⊆ {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ U).Nonempty} := by
    intro x hx
    rw [Set.mem_ofPred] at hx ⊢
    use y
    simpa using ⟨hx, mem_of_mem_nhds hu⟩
  rw [tsum_eq_finsum (hfin.subset this)]

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace

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_8
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set M
g g' : M → F
x : M
hg : MDiffAt[s] g x
hg' : MDiffAt[s] g' x
hs : UniqueMDiffAt[s] x
⊢ d[s] (g - g') x = d[s] g x - d[s] g' x

Tactic:
simp [mvfderivWithin, mfderivWithin_sub hg hg' hs]
  rfl

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
V : (x : M) → TangentSpace I x
x : M
⊢ 0 univ x = 0 x

Tactic:
Pi.zero_apply

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
V : (x : M) → TangentSpace I x
⊢ mlieBracket I V V = 0

Tactic:
ext x; simp_rw [mlieBracket, mlieBracketWithin_self, Pi.zero_apply]

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
s t : Set M
x : M
V W : (x : M) → TangentSpace I x
ht : t ∈ 𝓝 x
y : M
hy : y ∈ t
⊢ (y ∈ s ∩ t) = (y ∈ s)

Tactic:
simp_all

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

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
s : Set M
x : M
m n : ℕ∞ω
inst✝¹ : CompleteSpace E
inst✝ : IsManifold I 1 M
V : (x : M) → TangentSpace I x
hV : ContMDiffWithinAt I I.tangent m (fun x ↦ ⟨x, V x⟩) s x
hs : UniqueMDiff[s]
hx : x ∈ s
hmn : m + 1 ≤ n
hm : m ≠ ∞
⊢ ∀ᶠ (y : M) in 𝓝[s] x,
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m
      (fun x_1 ↦ ⟨x_1, mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) x_1⟩)
      ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)

Tactic:
have T := nhdsWithin_mono _ (subset_insert _ _)
    ((contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin hm).1
      (contMDiffWithinAt_mpullbackWithin_extChartAt_symm hV hs hx hmn))
  have A := (continuousAt_extChartAt (I := I) x).continuousWithinAt.preimage_mem_nhdsWithin'' T rfl
  apply (nhdsWithin_le_iff.2 _) A
  filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds (extChartAt_source_mem_nhds (I := I) x)]
    with y hy h'y
  simp only [mfld_simps] at hy h'y
  simp [hy, h'y]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
F : Type u_5
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
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝¹ : TopologicalSpace M
N : Type u_13
inst✝ : TopologicalSpace N
f g : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hfg : EqOn f g φ.source
equiv : (E × F) ≃L[𝕜] E''
hf : EqOn (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (⇑equiv ∘ fun x ↦ (x, 0)) (φ.extend I).target
x : E
hx : x ∈ (φ.extend I).target
⊢ ↑(φ.extend I).symm x ∈ φ.source

Tactic:
simp_all

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ if h : IsRCLikeNormedField ℝ then Convex ℝ (range Subtype.val) else range Subtype.val = univ

Tactic:
simp only [instIsRCLikeNormedField, ↓reduceDIte]

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ Convex ℝ (range Subtype.val)
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
⊢ if h : IsRCLikeNormedField ℝ then Convex ℝ (range Subtype.val) else range Subtype.val = univ

Tactic:
simp only [instIsRCLikeNormedField, ↓reduceDIte]

Goal state after:
n : ℕ
⊢ Convex ℝ (range Subtype.val)
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 : ℕ∞ω
inst✝ : IsManifold I n M
s : TopologicalSpace.Opens M
y : ↥s
x : E
hx : x ∈ ((chartAt H y).extend I).target
⊢ ↑I (↑(chartAt H y) (↑(chartAt H y).symm (↑I.symm x))) = x

Tactic:
simp_all

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

Goal state before:
pp: case hφ
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
this : ContDiff ℝ n fun y ↦ -x + y
⊢ ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) n (↑(Homeomorph.addLeft (-x)).toOpenPartialHomeomorph)
    (Homeomorph.addLeft (-x)).toOpenPartialHomeomorph.source

Tactic:
simpa [contMDiffOn_iff_contDiffOn, contDiffOn_univ]

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

Goal state before:
pp: case hφ
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
this : ContDiff ℝ n ((fun v ↦ v + y / 2) ∘ fun x ↦ y / 2 - x)
⊢ ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) n (↑(Homeomorph.pointReflection (y / 2)).toOpenPartialHomeomorph)
    (Homeomorph.pointReflection (y / 2)).toOpenPartialHomeomorph.source

Tactic:
simpa [contMDiffOn_iff_contDiffOn, contDiffOn_univ]

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

Goal state before:
pp: case hφ'
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
this : ContDiff ℝ n ((fun v ↦ -v + y / 2) ∘ fun p' ↦ p' - y / 2)
⊢ ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) n (↑(Homeomorph.pointReflection (y / 2)).toOpenPartialHomeomorph.symm)
    (Homeomorph.pointReflection (y / 2)).toOpenPartialHomeomorph.target

Tactic:
simpa [contMDiffOn_iff_contDiffOn, contDiffOn_univ]

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)
n : WithTop ℕ∞
f : M → ↑(Icc x y)
⊢ ContMDiff I (𝓡∂ 1) n f ↔ Continuous[inst✝¹, _] f ∧ ContMDiff I 𝓘(ℝ, ℝ) n ((fun z ↦ ↑z) ∘ f)

Tactic:
by
  rw [← ContMDiff.iff_comp_isImmersionOfComplement isImmersionOfComplement_subtypeVal_Icc]

Goal state after:
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 : ℕ∞ω
inst✝ : IsManifold I n M
x : M
y : E
hy : y ∈ ((chartAt H x).extend I).target
⊢ ↑I.symm y ∈ (chartAt H x).target

Tactic:
simp_all

Goal state after:
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 : ℕ∞ω
inst✝ : IsManifold I n M
x : M
y : E
hy : y ∈ ((chartAt H x).extend I).target
⊢ y ∈ range ↑I

Tactic:
simp_all

Goal state after:
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'
x : M
y : E
hy : y ∈ ((chartAt H x).extend I).target
⊢ ↑I.symm y ∈ (chartAt H x).target

Tactic:
simp_all

Goal state after:
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'
x : M
y : E
hy : y ∈ ((chartAt H x).extend I).target
⊢ y ∈ range ↑I

Tactic:
simp_all

Goal state after: