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

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
n : ℕ
inst✝¹ : NeZero n
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i : Fin (n + 1)
⊢ (s.height i)⁻¹ < ∑ j with j ≠ i, (s.height j)⁻¹

Tactic:
by
  rw [inv_height_eq_sum_mul_inv_dist]
  refine Finset.sum_lt_sum_of_nonempty ?_ ?_
  · rw [Finset.filter_ne', ← Finset.card_ne_zero]
    simp only [Finset.mem_univ, Finset.card_erase_of_mem, Finset.card_univ, Fintype.card_fin,
      add_tsub_cancel_right]
    exact NeZero.ne _
  · rintro j hj
    refine mul_lt_of_lt_one_left ?_ ?_
    · simp [height_pos]
    · rw [neg_lt]
      exact neg_one_lt_inner_vsub_altitudeFoot_div _ _ _

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

Goal state before:
pp: case h.left
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ι : Type u_3
hne : Nonempty ι
inst✝ : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val✝ : Fintype ι
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P},
    AffineIndependent ℝ p →
      ∀ (val : Fintype ι),
        Fintype.card ι = 0 →
          ∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius
i : ι
hi : ∀ (y : ι), y = i
this : Unique ι
⊢ p i = p default ∧ {p default} ⊆ Metric.sphere (p i) 0

Tactic:
simp_rw [hi default, Set.singleton_subset_iff]

Goal state after:
case h.left
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ι : Type u_3
hne : Nonempty ι
inst✝ : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val✝ : Fintype ι
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P},
    AffineIndependent ℝ p →
      ∀ (val : Fintype ι),
        Fintype.card ι = 0 →
          ∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius
i : ι
hi : ∀ (y : ι), y = i
this : Unique ι
⊢ True ∧ p i ∈ Metric.sphere (p i) 0
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
⊢ Real.sin (angle x y) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖) * (⟪y, y + x⟫ / (‖y‖ * ‖y + x‖)) +
      ⟪x, x + y⟫ / (‖x‖ * ‖x + y‖) * (√(⟪y, y⟫ * ⟪x, x⟫ - ⟪y, x⟫ * ⟪y, x⟫) / (‖y‖ * ‖y + x‖))

Tactic:
sin_angle hx hy,

Goal state after:
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
⊢ √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖x + y‖) * (⟪y, y + x⟫ / (‖y‖ * ‖y + x‖)) +
      ⟪x, x + y⟫ / (‖x‖ * ‖x + y‖) * (√(⟪y, y⟫ * ⟪x, x⟫ - ⟪y, x⟫ * ⟪y, x⟫) / (‖y‖ * ‖y + x‖))
Module: Mathlib.Geometry.Euclidean.Incenter

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ |(if i ∈ signs then -1 else 1) * ↑(SignType.sign (∑ j, s.excenterWeightsUnnorm signs j)) * s.exradius signs| =
    s.exradius signs

Tactic:
abs_mul,

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 : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ |(if i ∈ signs then -1 else 1) * ↑(SignType.sign (∑ j, s.excenterWeightsUnnorm signs j))| * |s.exradius signs| =
    s.exradius signs
Module: Mathlib.Geometry.Euclidean.Incenter

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ |(if i ∈ signs then -1 else 1) * ↑(SignType.sign (∑ j, s.excenterWeightsUnnorm signs j))| * |s.exradius signs| =
    s.exradius signs

Tactic:
abs_mul,

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 : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ |if i ∈ signs then -1 else 1| * |↑(SignType.sign (∑ j, s.excenterWeightsUnnorm signs j))| * |s.exradius signs| =
    s.exradius signs
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₂, p₁, p₄}
he : ¬p₁ = p₄
hc' : Collinear ℝ {p₁, p₃, p₄}
⊢ Collinear ℝ {p₁, p₂, p₃, p₄}

Tactic:
Set.insert_comm p₁ p₂,

Goal state after:
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₂, p₁, p₄}
he : ¬p₁ = p₄
hc' : Collinear ℝ {p₁, p₃, p₄}
⊢ Collinear ℝ {p₂, p₁, p₃, p₄}
Module: Mathlib.Geometry.Euclidean.Circumcenter

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
n : ℕ
s : Simplex ℝ P n
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ((s.face hc).circumcenter -ᵥ s.circumcenter) +ᵥ (s.face hc).circumcenter =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)

Tactic:
circumcenter_eq_centroid,

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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ (Finset.centroid ℝ univ (s.face hc).points -ᵥ s.circumcenter) +ᵥ Finset.centroid ℝ univ (s.face hc).points =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
Module: Mathlib.Geometry.Euclidean.Triangle

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
a b c : P
h : ¬Collinear ℝ {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : ∠ a b c ≤ π / 2
⊢ -(π / 2) ≤ ∠ a c b

Tactic:
linarith [angle_nonneg a c b]

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

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
a b c : P
h : ¬Collinear ℝ {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
h3 : Real.sin (π - ∠ a b c) ≤ Real.sin (∠ a c b)
h5 : π - ∠ a b c < π / 2
w1 : ∠ a c b < π - ∠ a b c
⊢ -(π / 2) ≤ ∠ a c b

Tactic:
linarith [angle_nonneg a c b]

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

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
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c

Tactic:
rw [← finrank_top, ← direction_top ℝ V P] at hd
  refine exists_circumcenter_eq_of_cospherical_subset ?_ hd hc
  exact Set.subset_univ _

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

Goal state before:
pp: P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ ∀ (i j : Fin 3), dist (![a, b, c] i) (![a, b, c] j) = dist (![a', b', c'] i) (![a', b', c'] j)

Tactic:
intro i j

Goal state after:
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
i j : Fin 3
⊢ dist (![a, b, c] i) (![a, b, c] j) = dist (![a', b', c'] i) (![a', b', c'] j)
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
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ {p₁, p, p₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := S.subtypeₐᵢ
p₁' : ↥S := ⟨p₁, ⋯⟩
p' : ↥S := ⟨p, ⋯⟩
p₃' : ↥S := ⟨p₃, ⋯⟩
p₂' : ↥S := ⟨p₂, hp₂⟩
p₄' : ↥S := ⟨p₄, hp₄⟩
h_dist' : dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'
hp₁'p₂' : ∠ p₁' p' p₂' = π
⊢ Cospherical {p₁, p₂, p₃, p₄}

Tactic:
have hp₃'p₄' : ∠ p₃' p' p₄' = π := by simpa [AffineIsometry.angle_map s_isom]

Goal state after:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ {p₁, p, p₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := S.subtypeₐᵢ
p₁' : ↥S := ⟨p₁, ⋯⟩
p' : ↥S := ⟨p, ⋯⟩
p₃' : ↥S := ⟨p₃, ⋯⟩
p₂' : ↥S := ⟨p₂, hp₂⟩
p₄' : ↥S := ⟨p₄, hp₄⟩
h_dist' : dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
⊢ Cospherical {p₁, p₂, p₃, p₄}
Module: Mathlib.Geometry.Manifold.LocalDiffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
F : Type u_3
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace 𝕜 F
F' : Type u_4
inst✝¹⁰ : NormedAddCommGroup F'
inst✝⁹ : NormedSpace 𝕜 F'
H₁ : Type u_5
inst✝⁸ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁷ : TopologicalSpace H₂
H₃ : Type u_7
inst✝⁶ : TopologicalSpace H₃
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
K : ModelWithCorners 𝕜 F' H₃
M : Type u_8
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H₁ M
N : Type u_9
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace H₂ N
P : Type u_10
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace H₃ P
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
g : N → P
hg : IsLocalDiffeomorphAt J K n g (f x)
⊢ IsLocalDiffeomorphAt I K n (g ∘ f) x

Tactic:
by
  obtain ⟨Φ, hx, heq⟩ := hf
  obtain ⟨Ψ, hy, heq'⟩ := hg
  refine ⟨Φ.trans Ψ, by simp [hx, ← heq.eq_of_mem hx, hy], ?_⟩
  intro y ⟨hyl, hyr⟩
  have hfy : f y ∈ Ψ.source := by rwa [heq.eq_of_mem hyl]
  simp [← heq.eq_of_mem hyl, ← heq'.eq_of_mem hfy]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
F : Type u_3
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace 𝕜 F
F' : Type u_4
inst✝¹⁰ : NormedAddCommGroup F'
inst✝⁹ : NormedSpace 𝕜 F'
H₁ : Type u_5
inst✝⁸ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁷ : TopologicalSpace H₂
H₃ : Type u_7
inst✝⁶ : TopologicalSpace H₃
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
K : ModelWithCorners 𝕜 F' H₃
M : Type u_8
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H₁ M
N : Type u_9
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace H₂ N
P : Type u_10
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace H₃ P
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
I' : ?m.25
hf : IsLocalDiffeomorphAt I J n f x
hn : n ≠ 0
⊢ ∀ (m : 𝕜) (x_1 : TangentSpace I x), (mfderiv% f x) (m • x_1) = (RingHom.id 𝕜) m • (mfderiv% f x) x_1

Tactic:
intros; simp

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

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝³ : I.Boundaryless
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑e.symm) (𝓝 (↑e c)) = 𝓝 c
⊢ ∀ᶠ (y : E) in 𝓝 (↑e c), DifferentiableAt ℂ (f ∘ ↑e.symm) y

Tactic:
have : e.target ∈ 𝓝 (e c) := H₁ ▸ extChartAt_target_mem_nhdsWithin c

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝³ : I.Boundaryless
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑e.symm) (𝓝 (↑e c)) = 𝓝 c
this : e.target ∈ 𝓝 (↑e c)
⊢ ∀ᶠ (y : E) in 𝓝 (↑e c), DifferentiableAt ℂ (f ∘ ↑e.symm) y
Module: Mathlib.Geometry.Euclidean.MongePoint

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 : Set P
t t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
i₁ i₂ i₃ j₂ j₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : t.points i₁ = t₀.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t₀.points j₂ = t.points i₂
h₃ : t₀.points j₃ = t.points i₃
j₁ : Fin 3
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₁₂₃ : ∀ (j : Fin 3), j = j₁ ∨ j = j₂ ∨ j = j₃
h : t₀.points j₁ = t.orthocenter
⊢ s = insert t.orthocenter (Set.range t.points)

Tactic:
have hui : (Set.univ : Set (Fin 3)) = {i₁, i₂, i₃} := by ext x; simpa using h₁₂₃ x
      have huj : (Set.univ : Set (Fin 3)) = {j₁, j₂, j₃} := by ext x; simpa using hj₁₂₃ x
      rw [← h, ht₀s, ← Set.image_univ, huj, ← Set.image_univ, hui]
      simp_rw [Set.image_insert_eq, Set.image_singleton, h₁, ← h₂, ← h₃]
      rw [Set.insert_comm]

Goal state after:
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
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
⊢ MDiffAt[s]
        (↑((trivializationAt F E (f x₀).proj).toPartialEquiv ≫ (extChartAt IB (f x₀).proj).prod (PartialEquiv.refl F)) ∘
          f)
      x₀ ↔
    MDiffAt[s] (↑(extChartAt IB (f x₀).proj) ∘ fun x ↦ (f x).proj) x₀ ∧
      MDiffAt[s]
          (↑(extChartAt 𝓘(𝕜, F) (↑(trivializationAt F E (f x₀).proj) (f x₀)).2) ∘ fun x ↦
            (↑(trivializationAt F E (f x₀).proj) (f x)).2)
        x₀

Tactic:
Function.comp_def,

Goal state after:
𝕜 : 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
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
⊢ (MDiffAt[s] fun x ↦
        ↑((trivializationAt F E (f x₀).proj).toPartialEquiv ≫ (extChartAt IB (f x₀).proj).prod (PartialEquiv.refl F))
          (f x))
      x₀ ↔
    (MDiffAt[s] fun x ↦ ↑(extChartAt IB (f x₀).proj) (f x).proj) x₀ ∧
      (MDiffAt[s] fun x ↦
          ↑(extChartAt 𝓘(𝕜, F) (↑(trivializationAt F E (f x₀).proj) (f x₀)).2)
            (↑(trivializationAt F E (f x₀).proj) (f x)).2)
        x₀
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
x : B
⊢ (MDiffAt fun x ↦ ⟨x, 0⟩) x

Tactic:
rw [mdifferentiableAt_section]

Goal state after:
𝕜 : 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
x : B
⊢ (MDiffAt fun b ↦ (↑(trivializationAt F E x) ⟨b, 0⟩).2) x
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_1
𝕜 : 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 t : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization F TotalSpace.proj := trivializationAt F E x₀
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
ht : (MDiffAt[u] fun b ↦ (↑e ⟨b, t b⟩).2) x₀
⊢ (fun b ↦ (↑e ⟨b, (s + t) b⟩).2) =ᶠ[𝓝[u] x₀] (fun b ↦ (↑e ⟨b, s b⟩).2) + fun b ↦ (↑e ⟨b, t b⟩).2

Tactic:
apply eventually_of_mem (U := e.baseSet)

Goal state after:
case refine_1.hU
𝕜 : 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 t : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization F TotalSpace.proj := ⋯
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
ht : (MDiffAt[u] fun b ↦ (↑e ⟨b, t b⟩).2) x₀
⊢ e.baseSet ∈ 𝓝[u] x₀

case refine_1.h
𝕜 : 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 t : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization F TotalSpace.proj := ⋯
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
ht : (MDiffAt[u] fun b ↦ (↑e ⟨b, t b⟩).2) x₀
⊢ ∀ x ∈ e.baseSet, (fun b ↦ (↑e ⟨b, (s + t) b⟩).2) x = ((fun b ↦ (↑e ⟨b, s b⟩).2) + fun b ↦ (↑e ⟨b, t b⟩).2) x