mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H2 : x = ⟪y, x⟫ • y
hx : ⟪y, x⟫ = 1 ∨ ⟪y, x⟫ = -1
⊢ False

Tactic:
rcases hx with hx | hx <;> simp [*] at H2

Goal state after:
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 = 0
⊢ False

Tactic:
sub_eq_zero

Goal state after:
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
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
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ (s.reindex e).touchpointWeights signs i =
    s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm i) ∘ ⇑e.symm

Tactic:
by
  rw [eq_comm, ← affineCombination_eq_touchpoint_iff]
  · rw [touchpoint_reindex, ← affineCombination_touchpointWeights, reindex]
    dsimp only
    rw [← Equiv.coe_toEmbedding, ← Finset.affineCombination_map]
    simp
  · rw [Finset.sum_comp_equiv]
    simp

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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
h :
  Simplex.touchpointWeights t {i₁} i₂ =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃)
⊢ Sbtw ℝ
    ((Finset.affineCombination ℝ Finset.univ t.points)
      (Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃)))
    (t.points i₃) (t.points i₁)

Tactic:
Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _)
    (Finset.mem_univ _),

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₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
h :
  Simplex.touchpointWeights t {i₁} i₂ =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃)
⊢ Sbtw ℝ ((AffineMap.lineMap (t.points i₁) (t.points i₃)) (Simplex.touchpointWeights t {i₁} i₂ i₃)) (t.points i₃)
    (t.points i₁)
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)
hn : ¬n = 0
⊢ ↑n ≠ 0

Tactic:
simpa using hn

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy

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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical {a, c, b, d}
⊢ dist a b * dist c d + dist b c * dist d a = dist a c * dist b d

Tactic:
have hmul := mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi h' hapc hbpd

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}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
⊢ dist a b * dist c d + dist b c * dist d a = dist a c * dist b d
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)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
⊢ p = s.mongePoint

Tactic:
rw [← @vsub_eq_zero_iff_eq V]

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₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
⊢ p -ᵥ s.mongePoint = 0
Module: Mathlib.Geometry.Euclidean.Similarity

Goal state before:
pp: case pos
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')
heq : dist a' b' * dist c' b' * 2 = 0
⊢ ∠ a b c = ∠ a' b' c'

Tactic:
rw [mul_eq_zero_iff_right (by norm_num), mul_eq_zero] at heq

Goal state after:
case pos
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')
heq : dist a' b' = 0 ∨ 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
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : {i₂, i₃}ᶜ = {i₁}
he : {i₁}ᶜ = {i₂, i₃}
⊢ altitude t i₁ =
    mk' (Finset.centroid ℝ {i₂, i₃}ᶜ t.points) (ℝ ∙ (t.points i₂ -ᵥ t.points i₃))ᗮ ⊓ affineSpan ℝ (Set.range t.points)

Tactic:
altitude_def,

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₁) (affineSpan ℝ (t.points '' {i₁}ᶜ)).directionᗮ ⊓ affineSpan ℝ (Set.range t.points) =
    mk' (Finset.centroid ℝ {i₂, i₃}ᶜ t.points) (ℝ ∙ (t.points i₂ -ᵥ t.points i₃))ᗮ ⊓ affineSpan ℝ (Set.range t.points)
Module: Mathlib.Geometry.Group.Growth.LinearLowerBound

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {X : Finset G} {n : ℕ},
    1 ∈ X → X.Nontrivial → n ≠ 0 → X ^ n = X ^ (n + 1) → n = 1 → ↑X = ↑(closure ↑X)
hXn : ∀ (d : ℕ), X ^ (n + d) = X ^ n
⊢ (X ^ n) ^ 1 = (X ^ n) ^ (1 + 1)

Tactic:
by simp [hXn, ← pow_mul, mul_two]

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₁ 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₃
⊢ t₂.orthocenter = t₁.points i₁

Tactic:
refine (Triangle.eq_orthocenter_of_forall_mem_altitude hj₂₃ ?_ ?_).symm

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₃
⊢ t₁.points i₁ ∈ altitude t₂ j₂

case refine_2
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₃
⊢ t₁.points i₁ ∈ altitude t₂ j₃
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)
hF' : MapsTo (⇑F) s (Iic (F (f x)))
⊢ ∀ (y : E), F ((fderiv ℝ f x) y) = 0

Tactic:
have hFφ : IsLocalMax (F ∘ f) x := Filter.eventually_of_mem hu fun y hy ↦ hF' <| hfus hy

Goal state after:
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)
hF' : MapsTo (⇑F) s (Iic (F (f x)))
hFφ : IsLocalMax (⇑F ∘ f) x
⊢ ∀ (y : E), F ((fderiv ℝ f x) y) = 0
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
⊢ I.IsBoundaryPoint (Sum.inl x)

Tactic:
by
  rw [I.isBoundaryPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inl]
  dsimp
  rw [Sum.inl_injective.extend_apply (chartAt H x)]
  simpa [I.isBoundaryPoint_iff, extChartAt] using hx

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'
⊢ ModelWithCorners.boundary (M ⊕ M') = Sum.inl '' ModelWithCorners.boundary M ∪ Sum.inr '' ModelWithCorners.boundary M'

Tactic:
by
  simp only [← ModelWithCorners.compl_interior, interior_disjointUnion, inl_compl_union_inr_compl]

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
x : TotalSpace F E
⊢ MDiffAt TotalSpace.proj x

Tactic:
have : MDiffAt (@id <| TotalSpace F E) x := mdifferentiableAt_id
  rw [mdifferentiableAt_totalSpace] at this
  exact this.1

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 : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hW : (MDiffAt[s] fun x ↦ ⟨x, W x⟩) x
hs : UniqueMDiffAt[s] x
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := ⋯
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x := ⋯
f' : E → 𝕜 := ⋯
s' : Set E := ⋯
A : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := ⋯
B : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := ⋯
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (fun y ↦ A y + B y) x =
    (d[s] f x) (V x) • W x + f x • mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (lieBracketWithin 𝕜 V' W' s') x

Tactic:
← Pi.add_def,

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
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hW : (MDiffAt[s] fun x ↦ ⟨x, W x⟩) x
hs : UniqueMDiffAt[s] x
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)
f' : E → 𝕜 := f ∘ ↑(extChartAt I x).symm
s' : Set E := ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I
A : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := fun x₀ ↦ (fderivWithin 𝕜 f' s' x₀) (V' x₀) • W' x₀
B : (x₀ : E) → TangentSpace 𝓘(𝕜, E) x₀ := fun x₀ ↦ f' x₀ • lieBracketWithin 𝕜 V' W' s' x₀
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (A + B) x =
    (d[s] f x) (V x) • W x + f x • mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (lieBracketWithin 𝕜 V' W' s') x
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
x✝⁶ x✝⁵ : EuclideanSpace ℝ (Fin n)
hy : ∀ (i : Fin n), 0 ≤ x✝⁵.ofLp i
x✝⁴ x✝³ : ℝ
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
i : Fin n
hx : 0 ≤ x✝⁶.ofLp i
⊢ 0 ≤ x✝⁴ * x✝⁶.ofLp i + x✝³ * x✝⁵.ofLp i

Tactic:
specialize hy i

Goal state after:
n : ℕ
x✝⁶ x✝⁵ : EuclideanSpace ℝ (Fin n)
x✝⁴ x✝³ : ℝ
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
i : Fin n
hy : 0 ≤ x✝⁵.ofLp i
hx : 0 ≤ x✝⁶.ofLp i
⊢ 0 ≤ x✝⁴ * x✝⁶.ofLp i + x✝³ * x✝⁵.ofLp i
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: case inr.inr
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p ∈ Ioo x y
⊢ p ∈ ModelWithCorners.boundary ↑(Icc x y) ↔ p ∈ {⊥, ⊤}

Tactic:
apply iff_of_false
    · simpa [← mem_compl_iff, ModelWithCorners.compl_boundary] using!
        Icc_isInteriorPoint_interior hp
    · rintro (rfl | rfl) <;> simp at hp

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

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ↑(projIcc x y ⋯ z) < y
this :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x_1 ↦ w - x;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
⊢ (((Subtype.val ∘ ↑(IccLeftChart x y)) ∘ projIcc x y ⋯ ∘ ↑(chartAt ℝ z).symm) w).ofLp i =
    (have this := toLp 2 fun x_1 ↦ w - x;
        this).ofLp
      i

Tactic:
suffices max x (min y w) - x = w - x by
      simpa [modelWithCornersEuclideanHalfSpace, IccLeftChart]

Goal state after:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ↑(projIcc x y ⋯ z) < y
this :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x_1 ↦ w - x;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
⊢ max x (min y w) - x = w - x
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ↑(projIcc x y ⋯ z) < y
this :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x_1 ↦ w - x;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
⊢ min y w - x = w - x

pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ↑(projIcc x y ⋯ z) < y
this :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x_1 ↦ w - x;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
⊢ x ≤ min y w

Tactic:
min_eq_right hw.2

Goal state after:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ↑(projIcc x y ⋯ z) < y
this :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x_1 ↦ w - x;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
⊢ w - x = w - x

x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ↑(projIcc x y ⋯ z) < y
this :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x_1 ↦ w - x;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
⊢ x ≤ min y w
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ¬↑(projIcc x y ⋯ z) < y
this :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x ↦ y - w;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
⊢ y - min y w = y - w

pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ¬↑(projIcc x y ⋯ z) < y
this :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x ↦ y - w;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
⊢ x ≤ min y w

Tactic:
min_eq_right hw.2

Goal state after:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ¬↑(projIcc x y ⋯ z) < y
this :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x ↦ y - w;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
⊢ y - w = y - w

x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ℝ
hz : z ∈ Icc x y
h'z : ¬↑(projIcc x y ⋯ z) < y
this :
  ContDiff ℝ n fun w ↦
    have this := toLp 2 fun x ↦ y - w;
    this
w : ℝ
hw : w ∈ Icc x y
i : Fin 1
⊢ x ≤ min y w
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

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
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
a a' : ℝ
hpos : 0 < a'
hle : a' ≤ a
⊢ γ a' 0 = x

Tactic:
hγx a'

Goal state after:
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
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
a a' : ℝ
hpos : 0 < a'
hle : a' ≤ a
⊢ x = x
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: case hs
𝕜 : 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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : (MDiffAt fun x ↦ ⟨x, 0⟩) x
⊢ UniqueDiffWithinAt 𝕜 (range ↑I) (↑I (↑(chartAt H x) x))

pp: case h
𝕜 : 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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : (MDiffAt fun x ↦ ⟨x, 0⟩) x
⊢ DifferentiableAt 𝕜 (fun x' ↦ (x', 0)) (↑I (↑(chartAt H x) x))

Tactic:
· exact ModelWithCorners.uniqueDiffWithinAt_image I

Goal state after:
case h
𝕜 : 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
Is : IsManifold I 1 M
x : M
v : TangentSpace I x
N : ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (↑I (↑(chartAt H x) x))
A : (MDiffAt fun x ↦ ⟨x, 0⟩) x
⊢ DifferentiableAt 𝕜 (fun x' ↦ (x', 0)) (↑I (↑(chartAt H x) x))
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: case hs
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
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'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
w : H
w' : H'
⊢ UniqueDiffWithinAt 𝕜 (range ↑I) (↑I w)

pp: case ht
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
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'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
w : H
w' : H'
⊢ UniqueDiffWithinAt 𝕜 (range ↑I') (↑I' w')

Tactic:
· exact ModelWithCorners.uniqueDiffWithinAt_image I

Goal state after:
case ht
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
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'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
w : H
w' : H'
⊢ UniqueDiffWithinAt 𝕜 (range ↑I') (↑I' w')