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
signs : Finset (Fin (n + 1))
h : ∑ i, s.excenterWeightsUnnorm signs i ≠ 0
i j : Fin (n + 1)
he : Pi.single j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : s.excenterWeightsUnnorm signs k = 0
⊢ False

Tactic:
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
inst✝ : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : ∑ i, s.excenterWeightsUnnorm signs i ≠ 0
i j : Fin (n + 1)
he : Pi.single j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : (if k ∈ signs then -1 else 1) * (s.height k)⁻¹ = 0
⊢ False
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:
rw [eulerPoint, vsub_vadd_eq_vsub_sub]
  by_cases hn : n = 0
  · obtain rfl := hn
    have hrange : Set.range s.points = {s.points i} := by simp [Subsingleton.eq_zero (α := Fin 1) i]
    obtain hmonge := s.mongePoint_mem_affineSpan
    rw [hrange, mem_affineSpan_singleton] at hmonge
    simp [hmonge]
  rw [sub_div, div_self (by simpa using hn), one_div, sub_smul, one_smul]

Goal state after:
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
r : ℝ
hr : r ≠ 0
⊢ (r * (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r) / r / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p

Tactic:
mul_div_cancel_left₀ _ hr,

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
p : P
v : V
r : ℝ
hr : r ≠ 0
⊢ (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
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
r : ℝ
hr : r ≠ 0
⊢ (r * (⟪v, p -ᵥ s.center⟫ * -2) / r / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p

Tactic:
mul_div_cancel_left₀ _ hr,

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
p : P
v : V
r : ℝ
hr : r ≠ 0
⊢ (⟪v, p -ᵥ s.center⟫ * -2 / ⟪v, v⟫) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
Module: Mathlib.Geometry.Euclidean.Similarity

Goal state before:
pp: case pos.inr
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₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
h2 : dist c' b' = 0
⊢ ∠ a b c = ∠ a' b' c'

Tactic:
have h_dist_cb : dist c b = 0 := by grind

Goal state after:
case pos.inr
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₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
h2 : dist c' b' = 0
h_dist_cb : dist c b = 0
⊢ ∠ 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
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ : Fin 3
h₁ : p i₁ = t.orthocenter
⊢ ∃ i₂ i₃, i₁ ≠ i₂ ∧ i₁ ≠ i₃ ∧ i₂ ≠ i₃ ∧ ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃

Tactic:
by
      clear h₁
      decide +revert

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : f x = y
v : PointDerivation I x
g g' : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ v (ContMDiffMap.comp (g + g') f) = v (ContMDiffMap.comp g f) + v (ContMDiffMap.comp g' f)

Tactic:
rw [ContMDiffMap.add_comp, Derivation.map_add]

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

Goal state before:
pp: case right
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
hs : Set.range p = Set.range t.points
p₁ : P
hp₁ : p₁ ∈ Set.range p
⊢ dist p₁ (Simplex.circumcenter t) = Simplex.circumradius t

Tactic:
rw [hs] at hp₁

Goal state after:
case right
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
hs : Set.range p = Set.range t.points
p₁ : P
hp₁ : p₁ ∈ Set.range t.points
⊢ dist p₁ (Simplex.circumcenter t) = Simplex.circumradius t
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 fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (range ↑I) (↑(extChartAt I x) x) else 0)
⊢ I'.IsInteriorPoint (f x)

Tactic:
have hf'' := hf.differentiableWithinAt_writtenInExtChartAt.differentiableAt <| by
    simpa [← mem_interior_iff_mem_nhds] using! hx

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 fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (range ↑I) (↑(extChartAt I x) x) else 0)
hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x)
⊢ I'.IsInteriorPoint (f 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✝¹³ : 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:
obtain ⟨u', hu', hfin⟩ := ht x₀

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
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₀
u' : Set B
hu' : u' ∈ 𝓝 x₀
hfin : {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ u').Nonempty}.Finite
⊢ (MDiffAt[u] fun x ↦ ⟨x, ∑' (i : ι), t i x⟩) x₀
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst✝³¹ : NontriviallyNormedField 𝕜
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)
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_9
inst✝¹⁸ : NormedAddCommGroup EB₁
inst✝¹⁷ : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst✝¹⁶ : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst✝¹⁵ : TopologicalSpace B₁
inst✝¹⁴ : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst✝¹³ : NormedAddCommGroup EB₂
inst✝¹² : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst✝¹¹ : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst✝¹⁰ : TopologicalSpace B₂
inst✝⁹ : ChartedSpace HB₂ B₂
EM : Type u_13
inst✝⁸ : NormedAddCommGroup EM
inst✝⁷ : NormedSpace 𝕜 EM
HM : Type u_14
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₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)
v : (m : M) → E₁ (b₁ m)
hϕ : (MDiffAt[univ] fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀
hv : (MDiffAt[univ] fun m ↦ ⟨b₁ m, v m⟩) m₀
hb₂ : MDiffAt[univ] b₂ m₀
⊢ (MDiffAt[univ] fun m ↦ ⟨b₂ m, (ϕ m) (v m)⟩) m₀

Tactic:
exact MDifferentiableWithinAt.clm_apply_of_inCoordinates hϕ hv hb₂

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
k : WithTop ℕ∞
x : M
σ₀ : V x
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) k (fun x' ↦ ⟨x', extend F σ₀ x'⟩) x

Tactic:
rw [contMDiffAt_section]
  set t := trivializationAt F V x
  let w : F := (t ⟨x, σ₀⟩).2
  have : CMDiffAt k (fun (_x : M) ↦ w) x := contMDiffAt_const
  refine this.congr_of_eventuallyEq ?_
  apply eventually_nhds_iff.mpr
  refine ⟨t.baseSet, ?_, t.open_baseSet, ?_⟩
  · intro x hx
    simp [extend, t, hx, w]
  · exact FiberBundle.mem_baseSet_trivializationAt' x

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
V : (x : M) → TangentSpace I x
h : UniqueMDiffAt[s] x
⊢ mpullbackWithin I I id V s x = V x

Tactic:
by
  simp [mpullbackWithin_apply, mfderivWithin_id h]

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'
⊢ mpullback I I' f 0 = 0

Tactic:
by simp [← mpullbackWithin_univ]

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_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : MDiffAt[s] g x
hf : MDiffAt[s] f x
⊢ DifferentiableWithinAt 𝕜 (fun x ↦ x.1 x.2) univ (g x, f x)

Tactic:
apply (Differentiable.differentiableAt _).differentiableWithinAt
        exact differentiable_fst.clm_apply differentiable_snd

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_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
x : M
hg : MDiffAt g x
hf : MDiffAt f x
⊢ DifferentiableWithinAt 𝕜 (fun x ↦ x.1 x.2) univ (g x, f x)

Tactic:
apply (Differentiable.differentiableAt _).differentiableWithinAt
        exact differentiable_fst.clm_apply differentiable_snd

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

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
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : LieGroup I (minSmoothness 𝕜 3) G
g h : G
M : minSmoothness 𝕜 3 ≠ 0
this : ((fun x ↦ g⁻¹ * x) ∘ fun x ↦ g * x) = id
⊢ mfderiv% id h = ContinuousLinearMap.id 𝕜 (TangentSpace I h)

Tactic:
id_eq,

Goal state after:
𝕜 : 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
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : LieGroup I (minSmoothness 𝕜 3) G
g h : G
M : minSmoothness 𝕜 3 ≠ 0
this : ((fun x ↦ g⁻¹ * x) ∘ fun x ↦ g * x) = id
⊢ mfderiv% id h = ContinuousLinearMap.id 𝕜 (TangentSpace I h)
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

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
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : LieGroup I (minSmoothness 𝕜 3) G
g h : G
M : minSmoothness 𝕜 3 ≠ 0
A : (mfderiv% fun x ↦ g⁻¹ * x) (g * h) ∘SL (mfderiv% fun x ↦ g * x) h = ContinuousLinearMap.id 𝕜 (TangentSpace I h)
this : ((fun x ↦ g * x) ∘ fun x ↦ g⁻¹ * x) = id
⊢ mfderiv% id (g * h) = ContinuousLinearMap.id 𝕜 (TangentSpace I (g * h))

Tactic:
id_eq,

Goal state after:
𝕜 : 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
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : LieGroup I (minSmoothness 𝕜 3) G
g h : G
M : minSmoothness 𝕜 3 ≠ 0
A : (mfderiv% fun x ↦ g⁻¹ * x) (g * h) ∘SL (mfderiv% fun x ↦ g * x) h = ContinuousLinearMap.id 𝕜 (TangentSpace I h)
this : ((fun x ↦ g * x) ∘ fun x ↦ g⁻¹ * x) = id
⊢ mfderiv% id (g * h) = ContinuousLinearMap.id 𝕜 (TangentSpace I (g * h))
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case e_6
𝕜 : 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
⊢ lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V₁ (range ↑I))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W₁ (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
      (↑(extChartAt I x) x) =
    lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
      (↑(extChartAt I x) x)

Tactic:
let I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) (extChartAt I x x)) :=
    inferInstanceAs (NormedAddCommGroup E)

Goal state after:
case e_6
𝕜 : 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
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) :=
  { toNorm := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1_1,
    toAddCommGroup := instAddCommGroupTangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x),
    toPseudoMetricSpace := EventuallyEq.mlieBracketWithin_vectorField_eq._aux_1_13, eq_of_dist_eq_zero := ⋯,
    dist_eq := ⋯ }
⊢ lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V₁ (range ↑I))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W₁ (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
      (↑(extChartAt I x) x) =
    lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
      (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
      (↑(extChartAt I x) x)