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

Goal state before:
pp: case refine_1.inr
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₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : s.excenterWeights signs₁ = s.excenterWeights signs₂
hi :
  ∀ (i : Fin (n + 1)),
    SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₁ i) =
      SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₂ i)
hn₁ : ∑ i, s.excenterWeightsUnnorm signs₁ i ≠ 0
hn₂ : ∑ i, s.excenterWeightsUnnorm signs₂ i ≠ 0
hs : SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ = -SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹
⊢ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ

Tactic:
hs,

Goal state after:
case refine_1.inr
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₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : s.excenterWeights signs₁ = s.excenterWeights signs₂
hn₁ : ∑ i, s.excenterWeightsUnnorm signs₁ i ≠ 0
hn₂ : ∑ i, s.excenterWeightsUnnorm signs₂ i ≠ 0
hs : SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ = -SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹
hi :
  ∀ (i : Fin (n + 1)),
    -SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₁ i) =
      SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₂ i)
⊢ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case h
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
p : P
r : ℝ
hr : ∀ (i : Fin (n + 1)), (fun x ↦ dist x p = r) (s.points i)
⊢ ∀ (i : Fin (n + 1)), dist (s.points i) p = r

Tactic:
exact hr

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

Goal state before:
pp: case inl
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 : P
hb : b ≠ p
hx : Sbtw ℝ a p c
hxb : SameRay ℝ (p -ᵥ p) (b -ᵥ p)
⊢ ∠ a p b + ∠ b p c = ∠ a p c

Tactic:
have hpi : ∠ a p c = π := hx.angle₁₂₃_eq_pi
    rw [hpi, angle_comm a p b]
    exact angle_add_angle_eq_pi_of_angle_eq_pi b hpi

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
n : ℕ
s : Simplex ℝ P n
fs : Finset (Fin (n + 1))
⊢ Finset.centroid ℝ fs s.points =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (centroidWeightsWithCircumcenter fs)

Tactic:
by
  simp_rw [centroid_def, affineCombination_apply, weightedVSubOfPoint_apply,
    sum_pointsWithCircumcenter, centroidWeightsWithCircumcenter,
    pointsWithCircumcenter_point, zero_smul, add_zero, centroidWeights,
    ← sum_indicator_subset_of_eq_zero (Function.const (Fin (n + 1)) (#fs : ℝ)⁻¹)
      (fun i wi => wi • (s.points i -ᵥ Classical.choice AddTorsor.nonempty)) fs.subset_univ fun _ =>
      zero_smul ℝ _,
    Set.indicator_apply]
  congr

Goal state after:
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))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : ∑ i, w i = 1
hp : (Finset.affineCombination ℝ Finset.univ s.points) w ∈ affineSpan ℝ (Set.range s.points)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) = (if i ∈ signs then -1 else 1) * r
h' : ∀ (i : Fin (n + 1)), w i * dist (s.points i) (s.altitudeFoot i) = (if i ∈ signs then -1 else 1) * r
⊢ ∀ (i : Fin (n + 1)), w i = r * s.excenterWeightsUnnorm signs i

Tactic:
simp_rw [excenterWeightsUnnorm]

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))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : ∑ i, w i = 1
hp : (Finset.affineCombination ℝ Finset.univ s.points) w ∈ affineSpan ℝ (Set.range s.points)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) = (if i ∈ signs then -1 else 1) * r
h' : ∀ (i : Fin (n + 1)), w i * dist (s.points i) (s.altitudeFoot i) = (if i ∈ signs then -1 else 1) * r
⊢ ∀ (i : Fin (n + 1)), w i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ 1 - ⟪x, y⟫ ^ 2 ≠ 0

Tactic:
rw [sub_ne_zero, ne_comm, sq_ne_one_iff]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ ⟪x, y⟫ ≠ 1 ∧ ⟪x, y⟫ ≠ -1
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case right
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ⟪x, y⟫ = -1
⊢ x - ⟪x, y⟫ • y = 0

Tactic:
· rw [inner_eq_neg_one_iff_of_norm_eq_one hx hy] at hxy
      simp [hy, hxy]

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

Goal state before:
pp: case mp
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}
⊢ ∠ a c b < ∠ a b c → dist a b < dist a c

pp: case mpr
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}
⊢ dist a b < dist a c → ∠ a c b < ∠ a b c

Tactic:
case mp =>
    exact dist_lt_of_angle_lt h

Goal state after:
case mpr
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}
⊢ dist a b < dist a c → ∠ a c b < ∠ a b c
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy1 : angle x y ≠ 0
hxy2 : angle x y ≠ π
h : y = ⟪x, y⟫ • x
⊢ False

Tactic:
grind [abs, norm_smul, Real.norm_eq_abs, norm_zero, inner_eq_mul_norm_iff_angle_eq_zero,
    inner_eq_neg_mul_norm_iff_angle_eq_pi]

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

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
h_not_col : ¬Collinear ℝ {a, b, c}
h₁ : ∠ a b c = ∠ a' b' c'
h₂ : ∠ b c a = ∠ b' c' a'
hne_pi_div_two : ∠ a b c ≠ Real.pi / 2 ∨ ∠ b c a ≠ Real.pi / 2
not_all_eq : a' ≠ b' ∨ b' ≠ c' ∨ a' ≠ c'
h_not_col' : ¬Collinear ℝ {a', b', c'}
h_pos1 : 0 < dist a b
h_pos1' : 0 < dist a' b'
h_pos2 : 0 < dist b c
⊢ 0 < dist b' c'

Tactic:
simp [dist_pos, ne₂₃_of_not_collinear h_not_col']

Goal state after:
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
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : ↑(n - 1) = ↑n - 1
⊢ ↑n ≠ 0

Tactic:
by simpa using hn.out

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

Goal state before:
pp: case e_6.pointIndex
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)
a✝ : Fin (n + 2 + 1)
⊢ ↑(n + 2 + 1) / ↑(n + 1) * ((if a✝ ∈ univ then (↑(#univ))⁻¹ else 0) - 0) + 0 = (↑(n + 1))⁻¹

Tactic:
rw [if_pos (mem_univ _), card_fin]
    field

Goal state after:
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 c d p : P
h : Cospherical {a, b, c, d}
hapb : p ∈ line[ℝ, a, b]
hcpd : p ∈ line[ℝ, c, d]
q : P
r : ℝ
h' : ∀ p ∈ {a, b, c, d}, dist p q = r
ha : dist a q = dist b q
hb : dist b q = r
hc : dist c q = dist d q
hd : dist d q = r
⊢ |r ^ 2 - dist p q ^ 2| = dist c p * dist d p

Tactic:
mul_dist_eq_abs_sub_sq_dist hcpd hc,

Goal state after:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapb : p ∈ line[ℝ, a, b]
hcpd : p ∈ line[ℝ, c, d]
q : P
r : ℝ
h' : ∀ p ∈ {a, b, c, d}, dist p q = r
ha : dist a q = dist b q
hb : dist b q = r
hc : dist c q = dist d q
hd : dist d q = r
⊢ |r ^ 2 - dist p q ^ 2| = |dist d q ^ 2 - dist p q ^ 2|
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
p : P
v : V
⊢ s.secondInter p v ∈ s ↔ p ∈ s

Tactic:
simp_rw [mem_sphere, Sphere.secondInter_dist]

Goal state after:
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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : {i₂, i₃}ᶜ = {i₁}
he : {i₁}ᶜ = {i₂, i₃}
⊢ mk' (t.points i₁) (vectorSpan ℝ (t.points '' {i₁}ᶜ))ᗮ ⊓ affineSpan ℝ (Set.range t.points) =
    mk' (Finset.centroid ℝ {i₂, i₃}ᶜ t.points) (ℝ ∙ (t.points i₂ -ᵥ t.points i₃))ᗮ ⊓ affineSpan ℝ (Set.range t.points)

Tactic:
hs,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : {i₂, i₃}ᶜ = {i₁}
he : {i₁}ᶜ = {i₂, i₃}
⊢ mk' (t.points i₁) (vectorSpan ℝ (t.points '' {i₁}ᶜ))ᗮ ⊓ affineSpan ℝ (Set.range t.points) =
    mk' (Finset.centroid ℝ {i₁} t.points) (ℝ ∙ (t.points i₂ -ᵥ t.points i₃))ᗮ ⊓ affineSpan ℝ (Set.range t.points)
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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
x : M
h : I.IsInteriorPoint x
⊢ range ↑I ∈ 𝓝 (↑(extChartAt I x) x)

Tactic:
mem_nhds_iff

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
x : M
h : I.IsInteriorPoint x
⊢ ∃ t ⊆ range ↑I, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑(extChartAt I x) x ∈ t
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
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left✝ : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
hs : affineSpan ℝ s = affineSpan ℝ (Set.range t.points)
hfd : FiniteDimensional ℝ ↥(affineSpan ℝ s).direction
⊢ finrank ℝ ↥(affineSpan ℝ (Set.range p)).direction = finrank ℝ ↥(affineSpan ℝ s).direction

Tactic:
hs,

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 : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
ha : AffineIndependent ℝ p
t : Triangle ℝ P
left✝ : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
hs : affineSpan ℝ s = affineSpan ℝ (Set.range t.points)
hfd : FiniteDimensional ℝ ↥(affineSpan ℝ s).direction
⊢ finrank ℝ ↥(affineSpan ℝ (Set.range p)).direction = finrank ℝ ↥(affineSpan ℝ (Set.range t.points)).direction
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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 : WithTop ℕ∞
inst✝ : IsManifold I n M
e : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : e ∈ atlas H M
hx : x ∈ e.source
⊢ ↑(e.extend I) x ∈ (e.extend I).target

Tactic:
exact (e.extend I).mapsTo <| e.extend_source (I := I) ▸ hx

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: case inr
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hf' : Surjective ⇑(mfderiv% f x)
hx : I.IsInteriorPoint x
this :
  ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
    [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
    [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
    [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
    {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {f : M → N} {x : M},
    MDiffAt f x → Surjective ⇑(mfderiv% f x) → I.IsInteriorPoint x → IsRCLikeNormedField 𝕜 → I'.IsInteriorPoint (f x)
h✝ : ¬IsRCLikeNormedField 𝕜
⊢ I'.IsInteriorPoint (f x)

Tactic:
simp [IsInteriorPoint, I'.range_eq_univ_of_not_isRCLikeNormedField ‹_›]

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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✝
E'✝ : Type u_5
inst✝¹⁵ : NormedAddCommGroup E'✝
inst✝¹⁴ : NormedSpace 𝕜✝ E'✝
H'✝ : Type u_6
inst✝¹³ : TopologicalSpace H'✝
I'✝ : ModelWithCorners 𝕜✝ E'✝ H'✝
N✝ : Type u_7
inst✝¹² : TopologicalSpace N✝
inst✝¹¹ : ChartedSpace H'✝ N✝
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h✝ : IsRCLikeNormedField 𝕜
x✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝ : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' : Surjective ⇑(if True then fderiv 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x) else 0)
hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x)
⊢ Surjective ⇑(ContinuousLinearMap.restrictScalars ℝ (fderiv 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x)))

Tactic:
ContinuousLinearMap.coe_restrictScalars'

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✝
E'✝ : Type u_5
inst✝¹⁵ : NormedAddCommGroup E'✝
inst✝¹⁴ : NormedSpace 𝕜✝ E'✝
H'✝ : Type u_6
inst✝¹³ : TopologicalSpace H'✝
I'✝ : ModelWithCorners 𝕜✝ E'✝ H'✝
N✝ : Type u_7
inst✝¹² : TopologicalSpace N✝
inst✝¹¹ : ChartedSpace H'✝ N✝
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h✝ : IsRCLikeNormedField 𝕜
x✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝ : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' : Surjective ⇑(if True then fderiv 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x) else 0)
hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x)
⊢ Surjective ⇑(fderiv 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x))
Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent

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
inst✝ : IsManifold I 1 M
p q : TangentBundle I M
h : q.proj ∈ (chartAt H p.proj).source
⊢ MDiffAt ↑(chartAt H p.proj) q.proj

Tactic:
exact mdifferentiableAt_atlas (chart_mem_atlas _ _) h

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

Goal state before:
pp: case e_a
𝕜 : 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
p : TangentBundle I M
q : TangentBundle I H
h : q.proj ∈ (chartAt H p.proj).target
⊢ ↑(chartAt H q.proj) q.proj =
    ↑↑(achart H p.proj)
      (↑(((chartAt H p.proj).prod (OpenPartialHomeomorph.refl E)).restrOpen
                ({ baseSet := fun i ↦ (↑i).source, isOpen_baseSet := ⋯, indexAt := achart H, mem_baseSet_at := ⋯,
                          coordChange := fun i j x ↦
                            fderivWithin 𝕜 ((↑I ∘ ↑↑j) ∘ ↑(↑i).symm ∘ ↑I.symm) (range ↑I) (↑I (↑↑i x)),
                          coordChange_self := ⋯, continuousOn_coordChange := ⋯,
                          coordChange_comp := ⋯ }.toFiberBundleCore.localTriv
                    (achart H p.proj)).target
                ⋯).symm
          ((TotalSpace.toProd H E) q)).1

Tactic:
exact ((chartAt H (TotalSpace.proj p)).right_inv h).symm

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✝¹³ : 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

Tactic:
apply (mdifferentiableAt_const (c := 0)).congr_of_eventuallyEq

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
⊢ (fun b ↦ (↑(trivializationAt F E x) ⟨b, 0⟩).2) =ᶠ[𝓝 x] fun x ↦ 0
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

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
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → TopologicalSpace (V x)
inst✝¹ : FiberBundle F V
inst✝ : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) k (fun x' ↦ ⟨x', extend F σ₀ x'⟩) x

Tactic:
contMDiffAt_section

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
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → TopologicalSpace (V x)
inst✝¹ : FiberBundle F V
inst✝ : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
⊢ ContMDiffAt I 𝓘(𝕜, F) k (fun x_1 ↦ (↑(trivializationAt F V x) ⟨x_1, extend F σ₀ x_1⟩).2) x