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

Goal state before:
pp: ι : Type u_1
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₂
v₁ : ι → P₁
v₂ : ι → P₂
h : v₁ ≅ v₂
i j k : ι
⊢ InnerProductGeometry.angle (v₁ i -ᵥ v₁ j) (v₁ k -ᵥ v₁ j) = InnerProductGeometry.angle (v₂ i -ᵥ v₂ j) (v₂ k -ᵥ v₂ j)

Tactic:
unfold InnerProductGeometry.angle

Goal state after:
ι : Type u_1
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₂
v₁ : ι → P₁
v₂ : ι → P₂
h : v₁ ≅ v₂
i j k : ι
⊢ Real.arccos (inner ℝ (v₁ i -ᵥ v₁ j) (v₁ k -ᵥ v₁ j) / (‖v₁ i -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖)) =
    Real.arccos (inner ℝ (v₂ i -ᵥ v₂ j) (v₂ k -ᵥ v₂ j) / (‖v₂ i -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖))
Module: Mathlib.Geometry.Euclidean.Inversion.Calculus

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
a : E
hc : DifferentiableWithinAt ℝ c univ a
hR : DifferentiableWithinAt ℝ R univ a
hx : DifferentiableWithinAt ℝ x univ a
hne : x a ≠ c a
⊢ DifferentiableWithinAt ℝ (fun a ↦ inversion (c a) (R a) (x a)) univ a

Tactic:
exact hc.inversion hR hx hne

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 : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ s.points i -ᵥ s.eulerPoint i = ((↑n - 1) / ↑n) • (s.points i -ᵥ s.mongePoint)

Tactic:
eulerPoint,

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 : Fin (n + 1)
⊢ s.points i -ᵥ ((↑n)⁻¹ • (s.points i -ᵥ s.mongePoint) +ᵥ s.mongePoint) = ((↑n - 1) / ↑n) • (s.points i -ᵥ s.mongePoint)
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)
⊢ ⅟2 • (s.faceOppositeCentroid i -ᵥ s.circumcenter) + ⅟2 • (s.eulerPoint i -ᵥ s.circumcenter) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)

Tactic:
eulerPoint,

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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ ⅟2 • (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      ⅟2 • (((↑n)⁻¹ • (s.points i -ᵥ s.mongePoint) +ᵥ s.mongePoint) -ᵥ s.circumcenter) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)
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
n : ℕ
s : Simplex ℝ P (n + 2)
h : Invertible (↑n + 2 + 1)
⊢ Finset.centroid ℝ univ s.points -ᵥ s.circumcenter = ∑ x, ⅟(↑n + 2 + 1) • (s.points x -ᵥ s.circumcenter)

Tactic:
rw [univ_centroid_eq, centroid_eq_affineCombination]

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)
h : Invertible (↑n + 2 + 1)
⊢ (affineCombination ℝ univ s.points) (centroidWeights ℝ univ) -ᵥ s.circumcenter =
    ∑ x, ⅟(↑n + 2 + 1) • (s.points x -ᵥ s.circumcenter)
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'
⊢ Similar ![a, b, c] ![a', b', c']

Tactic:
set r : ℝ := (dist a b / dist a' b') with hr
  have hr_pos : 0 < r := by positivity
  apply Similar.of_exists_pos_pairwise_dist_eq
  use r
  refine ⟨hr_pos, ?_⟩
  intro i j hij
  fin_cases i <;> fin_cases j <;> try {rw [dist_self, dist_self, mul_zero]}
  all_goals simp; grind [dist_comm]

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_not_col' : ¬Collinear ℝ {a', b', c'}
h : ∠ a b c = ∠ a' b' c'
dist_a'b' : dist a' b' ≠ 0
dist_b'c' : dist b' c' ≠ 0
k : ℝ := dist a b / dist a' b'
hd : k = dist b c / dist b' c'
hk : k = dist a b / dist a' b'
k_pos : 0 < k
h_ab : dist a b = k * dist a' b'
h_bc : dist c b = k * dist c' b'
hcos : dist c a = k * dist a' c'
hcos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
dist_ac_pos : 0 < dist a c
k_dist_a'c' : 0 ≤ k * dist a' c'
⊢ ![a, b, c] ∼ ![a', b', c']

Tactic:
dist_comm a' _

Goal state after:
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_not_col' : ¬Collinear ℝ {a', b', c'}
h : ∠ a b c = ∠ a' b' c'
dist_a'b' : dist a' b' ≠ 0
dist_b'c' : dist b' c' ≠ 0
k : ℝ := dist a b / dist a' b'
hd : k = dist b c / dist b' c'
hk : k = dist a b / dist a' b'
k_pos : 0 < k
h_ab : dist a b = k * dist a' b'
h_bc : dist c b = k * dist c' b'
hcos : dist c a = k * dist c' a'
hcos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
dist_ac_pos : 0 < dist a c
k_dist_a'c' : 0 ≤ k * dist a' c'
⊢ ![a, b, c] ∼ ![a', b', c']
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₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
h₁ : p ∈ altitude t i₁
h₂ : p ∈ altitude t i₂
i₃ : Fin 3
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
⊢ p = t.orthocenter

Tactic:
rw [t.altitude_eq_mongePlane h₁₃ h₁₂ h₂₃.symm] at h₁

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₂ : Fin 3
p : P
h₁₂ : i₁ ≠ i₂
h₂ : p ∈ altitude t i₂
i₃ : Fin 3
h₁ : p ∈ mongePlane t i₃ i₂
h₂₃ : i₂ ≠ i₃
h₁₃ : i₁ ≠ i₃
⊢ p = t.orthocenter
Module: Mathlib.Geometry.Group.Growth.LinearLowerBound

Goal state before:
pp: case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hXclosure : ↑X ^ 0 ≠ ↑(closure ↑X)
⊢ X ^ 0 ⊂ X ^ (0 + 1)

Tactic:
simpa [ssubset_iff_subset_not_subset, hX₁, -Finset.subset_singleton_iff]
      using! hX.not_subset_singleton

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
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : 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
n : WithTop ℕ∞
Φ : M ≃ₘ^n⟮I, J⟯ N
_x : M
⊢ _x ∈ Φ.toPartialDiffeomorph.source

Tactic:
by trivial

Goal state after:
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)
h : ∀ (y : E), F ((fderiv ℝ f x) y) = 0
y : H
hy : y ∈ interior s
z : E
⊢ 0 ≠ F (f x) - F y

Tactic:
exact (sub_pos.2 <| hF _ hy).ne

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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
⊢ ↑(extChartAt I (Sum.inl x)) (Sum.inl x) ∈ interior (extChartAt I (Sum.inl x)).target

Tactic:
extChartAt,

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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
⊢ ↑((chartAt H (Sum.inl x)).extend I) (Sum.inl x) ∈ interior ((chartAt H (Sum.inl x)).extend I).target
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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsBoundaryPoint x
⊢ ↑(extChartAt I (Sum.inl x)) (Sum.inl x) ∈ frontier (range ↑I)

Tactic:
extChartAt,

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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsBoundaryPoint x
⊢ ↑((chartAt H (Sum.inl x)).extend I) (Sum.inl x) ∈ frontier (range ↑I)
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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
hx : I.IsInteriorPoint x
⊢ ↑(extChartAt I (Sum.inr x)) (Sum.inr x) ∈ interior (extChartAt I (Sum.inr x)).target

Tactic:
extChartAt,

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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
hx : I.IsInteriorPoint x
⊢ ↑((chartAt H (Sum.inr x)).extend I) (Sum.inr x) ∈ interior ((chartAt H (Sum.inr x)).extend I).target
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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
hx : I.IsBoundaryPoint x
⊢ ↑(extChartAt I (Sum.inr x)) (Sum.inr x) ∈ frontier (range ↑I)

Tactic:
extChartAt,

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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
hx : I.IsBoundaryPoint x
⊢ ↑((chartAt H (Sum.inr x)).extend I) (Sum.inr x) ∈ frontier (range ↑I)
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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
n : WithTop ℕ∞
hM : BoundarylessManifold I M
hM' : BoundarylessManifold I M'
⊢ BoundarylessManifold I (M ⊕ M')

Tactic:
by
  rw [← Boundaryless.iff_boundary_eq_empty] at hM hM' ⊢
  simp [boundary_disjointUnion, hM, hM']

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 t : (x : B) → E x
x₀ : B
hs : MDiffAt (T% s) x₀
ht : MDiffAt (T% t) x₀
⊢ (MDiffAt fun x ↦ ⟨x, (s + t) x⟩) x₀

Tactic:
rw [← mdifferentiableWithinAt_univ] at hs ht ⊢

Goal state after:
𝕜 : 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
x₀ : B
hs : MDiffAt[univ] (T% s) x₀
ht : MDiffAt[univ] (T% t) x₀
⊢ (MDiffAt[univ] fun x ↦ ⟨x, (s + t) x⟩) x₀
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_2
𝕜 : 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 ℕ∞
inst✝² : (x : M) → Module 𝕜 (V x)
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization F TotalSpace.proj := trivializationAt F V x₀
w : F := (↑t ⟨x₀, σ₀⟩).2
⊢ ContMDiffOn I 𝓘(𝕜, F) k (fun x ↦ (↑t ⟨x, extend F σ₀ x⟩).2) t.baseSet

Tactic:
have : CMDiff[t.baseSet] k (fun (_x : M) ↦ w) := contMDiffOn_const

Goal state after:
case refine_2
𝕜 : 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 ℕ∞
inst✝² : (x : M) → Module 𝕜 (V x)
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization F TotalSpace.proj := trivializationAt F V x₀
w : F := (↑t ⟨x₀, σ₀⟩).2
this : ContMDiffOn I 𝓘(𝕜, F) k (fun _x ↦ w) t.baseSet
⊢ ContMDiffOn I 𝓘(𝕜, F) k (fun x ↦ (↑t ⟨x, extend F σ₀ x⟩).2) t.baseSet
Module: Mathlib.Geometry.Manifold.VectorBundle.Hom

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_6
inst✝²⁸ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E₁ : B → Type u_7
inst✝²⁷ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁵ : NormedAddCommGroup F₁
inst✝²⁴ : NormedSpace 𝕜 F₁
inst✝²³ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²² : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_8
inst✝²¹ : (x : B) → AddCommGroup (E₂ x)
inst✝²⁰ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁹ : NormedAddCommGroup F₂
inst✝¹⁸ : NormedSpace 𝕜 F₂
inst✝¹⁷ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁶ : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_10
inst✝¹⁵ : NormedAddCommGroup EB
inst✝¹⁴ : NormedSpace 𝕜 EB
HB : Type u_11
inst✝¹³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹² : TopologicalSpace B
inst✝¹¹ : ChartedSpace HB B
EM : Type u_12
inst✝¹⁰ : NormedAddCommGroup EM
inst✝⁹ : NormedSpace 𝕜 EM
HM : Type u_13
inst✝⁸ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace HM M
inst✝⁵ : FiberBundle F₁ E₁
inst✝⁴ : VectorBundle 𝕜 F₁ E₁
inst✝³ : FiberBundle F₂ E₂
inst✝² : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
x : M
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)
hϕ : ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F₁ →L[𝕜] F₂)) n (fun m ↦ ⟨b m, ϕ m⟩) s x
hv : ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F₁)) n (fun m ↦ ⟨b m, v m⟩) s x
⊢ ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F₂)) n (fun m ↦ ⟨b m, (ϕ m) (v m)⟩) s x

Tactic:
by
  simp only [contMDiffWithinAt_hom_bundle] at hϕ
  exact hϕ.2.clm_apply_of_inCoordinates hv hϕ.1

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiff[u]
t' : Set N := ⋯
ht't : t' ⊆ t
this :
  ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv[u] (f x) (g x)) x₀) t' x₀
⊢ g ⁻¹' (extChartAt I (g x₀)).source ∈ 𝓝[t] x₀

Tactic:
exact hg.continuousWithinAt.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds (g x₀))

Goal state after:
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
n : WithTop ℕ∞
inst✝³ : (x : M) → Module 𝕜 (V x)
W : Type u_7
inst✝² : AddCommGroup W
inst✝¹ : Module 𝕜 W
inst✝ : TopologicalSpace W
x : M
⊢ Function.Injective fun A Z x_1 ↦ A (Z x)

Tactic:
by
  intro X X' h
  ext σ₀
  simpa using congr($h (extend F σ₀) (contMDiffAt_extend ..))

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
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
V : (x : M') → TangentSpace I' x
⊢ mpullbackWithin I I' f V univ = mpullback I I' f V

Tactic:
by
  ext x
  simp [mpullback_apply, mpullbackWithin_apply]

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
g g' : M → F
x : M
hg : MDiffAt g x
hg' : MDiffAt g' x
⊢ d% (g - g') x = d% g x - d% g' x

Tactic:
by
  simp [mvfderiv, mfderiv_sub hg hg']
  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
s : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
⊢ mlieBracketWithin I V₁ W₁ s x = mlieBracketWithin I V W s x

Tactic:
by
  simp only [mlieBracketWithin_apply]
  congr 1
  let I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) (extChartAt I x x)) :=
    inferInstanceAs (NormedAddCommGroup E)
  let _I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (extChartAt I x x)) :=
    ‹NormedSpace 𝕜 E›
  apply Filter.EventuallyEq.lieBracketWithin_vectorField_eq
  · apply nhdsWithin_mono _ inter_subset_left
    filter_upwards [(continuousAt_extChartAt_symm x).continuousWithinAt.preimage_mem_nhdsWithin''
      hV (by simp)] with y hy
    simp only [mpullbackWithin_apply]
    congr 1
  · simp only [mpullbackWithin_apply]
    congr 1
    convert! hxV <;> exact extChartAt_to_inv x
  · apply nhdsWithin_mono _ inter_subset_left
    filter_upwards [(continuousAt_extChartAt_symm x).continuousWithinAt.preimage_mem_nhdsWithin''
      hW (by simp)] with y hy
    simp only [mpullbackWithin_apply]
    congr 1
  · simp only [mpullbackWithin_apply]
    congr 1
    convert! hxW <;> exact extChartAt_to_inv x

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

Goal state before:
pp: n : ℕ
⊢ (interior (range Subtype.val)).Nonempty

Tactic:
rw [range_euclideanQuadrant, interior_euclideanQuadrant]
    exact ⟨toLp 2 fun i ↦ 1, by simp⟩

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

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
⊢ ↑(extChartAt (𝓡∂ 1) ⊥) ⊥ ∈ frontier (range ↑(𝓡∂ 1))

Tactic:
extChartAt,

Goal state after:
x y : ℝ
hxy : Fact (x < y)
⊢ ↑((chartAt (EuclideanHalfSpace 1) ⊥).extend (𝓡∂ 1)) ⊥ ∈ frontier (range ↑(𝓡∂ 1))