mathlib-initiative/mathlib-tactics huggingface dataset:
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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
h : n = m
⊢ (s.reindex e).eulerPoint = s.eulerPoint ∘ ⇑e.symm

Tactic:
ext i

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
h : n = m
i : Fin (m + 1)
⊢ (s.reindex e).eulerPoint i = (s.eulerPoint ∘ ⇑e.symm) i
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
⊢ ![b, a, c] = ![a, b, c] ∘ ⇑(Equiv.swap 0 1)

Tactic:
ext i

Goal state after:
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
i : Fin (Nat.succ 0).succ.succ
⊢ ![b, a, c] i = (![a, b, c] ∘ ⇑(Equiv.swap 0 1)) i
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
hl : ![b, a, c] = ![a, b, c] ∘ ⇑(Equiv.swap 0 1)
⊢ ![b', a', c'] = ![a', b', c'] ∘ ⇑(Equiv.swap 0 1)

Tactic:
ext i

Goal state after:
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
hl : ![b, a, c] = ![a, b, c] ∘ ⇑(Equiv.swap 0 1)
i : Fin (Nat.succ 0).succ.succ
⊢ ![b', a', c'] i = (![a', b', c'] ∘ ⇑(Equiv.swap 0 1)) i
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
⊢ ![a, c, b] = ![a, b, c] ∘ ⇑(Equiv.swap 1 2)

Tactic:
ext i

Goal state after:
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
i : Fin (Nat.succ 0).succ.succ
⊢ ![a, c, b] i = (![a, b, c] ∘ ⇑(Equiv.swap 1 2)) i
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
hl : ![a, c, b] = ![a, b, c] ∘ ⇑(Equiv.swap 1 2)
⊢ ![a', c', b'] = ![a', b', c'] ∘ ⇑(Equiv.swap 1 2)

Tactic:
ext i

Goal state after:
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
hl : ![a, c, b] = ![a, b, c] ∘ ⇑(Equiv.swap 1 2)
i : Fin (Nat.succ 0).succ.succ
⊢ ![a', c', b'] i = (![a', b', c'] ∘ ⇑(Equiv.swap 1 2)) i
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ Similar v₁ v₂ ↔ ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂)

Tactic:
similar_iff_exists_pairwise_edist_eq,

Goal state after:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ (∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)) ↔
    ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂)
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ =
    mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ

Tactic:
ext i

Goal state after:
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
i : PointsWithCircumcenterIndex (n + 2)
⊢ mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ i =
    (mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ) i
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case e'_2.e'_5.e'_9
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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ {i₁, i₂}ᶜ = Finset.map e.toEmbedding {e.symm i₁, e.symm i₂}ᶜ

Tactic:
ext i

Goal state after:
case e'_2.e'_5.e'_9
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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ i : Fin (n + 3)
⊢ i ∈ {i₁, i₂}ᶜ ↔ i ∈ Finset.map e.toEmbedding {e.symm i₁, e.symm i₂}ᶜ
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}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ : dist d a = dist a p / dist b p * dist b c
h₃ : dist d p = dist a p * dist c p / dist b p
x y : ℝ
⊢ x * (y * x) = x * x * y

Tactic:
mul_left_comm,

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
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ : dist d a = dist a p / dist b p * dist b c
h₃ : dist d p = dist a p * dist c p / dist b p
x y : ℝ
⊢ y * (x * x) = x * x * y
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: case e'_9
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ {p₁, p, p₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := S.subtypeₐᵢ
p₁' : ↥S := ⟨p₁, ⋯⟩
p' : ↥S := ⟨p, ⋯⟩
p₃' : ↥S := ⟨p₃, ⋯⟩
p₂' : ↥S := ⟨p₂, hp₂⟩
p₄' : ↥S := ⟨p₄, hp₄⟩
h_dist' : dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
hf2 : Fact (finrank ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := (finBasisOfFinrankEq ℝ ↥S.direction ⋯).orientation }
⊢ ⇑s_isom.toAffineMap ∘ ![p₁', p', p₃'] = ![p₁, p, p₃]

Tactic:
ext i

Goal state after:
case e'_9
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ {p₁, p, p₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := S.subtypeₐᵢ
p₁' : ↥S := ⟨p₁, ⋯⟩
p' : ↥S := ⟨p, ⋯⟩
p₃' : ↥S := ⟨p₃, ⋯⟩
p₂' : ↥S := ⟨p₂, hp₂⟩
p₄' : ↥S := ⟨p₄, hp₄⟩
h_dist' : dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
hf2 : Fact (finrank ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2) :=
  { positiveOrientation := (finBasisOfFinrankEq ℝ ↥S.direction ⋯).orientation }
i : Fin (Nat.succ 0).succ.succ
⊢ (⇑s_isom.toAffineMap ∘ ![p₁', p', p₃']) i = ![p₁, p, p₃] i
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 t p : P
s : Sphere P
ha : a ∈ s
hb : b ∈ s
hp : p ∈ line[ℝ, a, b]
h_tangent : s.IsTangentAt t line[ℝ, p, t]
hr : 0 ≤ s.radius
radius_le_dist : s.radius ≤ dist p s.center
⊢ dist p t ^ 2 = dist p a * dist p b

Tactic:
mul_dist_eq_power_of_radius_le_dist_center hr hp ha hb radius_le_dist,

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 t p : P
s : Sphere P
ha : a ∈ s
hb : b ∈ s
hp : p ∈ line[ℝ, a, b]
h_tangent : s.IsTangentAt t line[ℝ, p, t]
hr : 0 ≤ s.radius
radius_le_dist : s.radius ≤ dist p s.center
⊢ dist p t ^ 2 = s.power p
Module: Mathlib.Geometry.Group.Growth.LinearLowerBound

Goal state before:
pp: G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n✝ : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
hn₁ : n = 1
⊢ ↑X ^ n = ↑(closure (↑X ^ n))

Tactic:
subst hn₁

Goal state after:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : 1 ≠ 0
hXn : X ^ 1 = X ^ (1 + 1)
⊢ ↑X ^ 1 = ↑(closure (↑X ^ 1))
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₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h : ∀ (i : Fin 3), i₁ ≠ i → ∃ j, t.points j = p i
j₂ j₃ : Fin 3
h₂ : p i₃ = p i₂
h₃ : t.points j₃ = p i₃
he : j₂ = j₃
⊢ False

Tactic:
exact h₂₃.symm (hpi h₂)

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 ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
x' : M
hx' : x' ∈ hf.localInverse.target
⊢ ↑hf.localInverse.toPartialEquiv (f x') = x'

Tactic:
rw [hf.choose_spec.2 (hf.choose.symm_target ▸ hx')]
  exact hf.choose.left_inv 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
n : WithTop ℕ∞
inst✝ : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : e ∈ atlas H M
he' : e' ∈ atlas H M
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : ↑(e.extend I) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange e e'
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφx' : Surjective ⇑(fderivWithin 𝕜 (↑φ) φ.source (↑(e.extend I) 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] {n : WithTop ℕ∞} [IsManifold I n M]
    {e e' : OpenPartialHomeomorph M H} {x : M},
    n ≠ 0 →
      e ∈ atlas H M →
        e' ∈ atlas H M →
          x ∈ e.source →
            x ∈ e'.source →
              ↑(e.extend I) x ∈ interior (e.extend I).target →
                let φ := extendCoordChange e e';
                ContDiffOn 𝕜 n (↑φ) φ.source →
                  Surjective ⇑(fderivWithin 𝕜 (↑φ) φ.source (↑(e.extend I) x)) →
                    IsRCLikeNormedField 𝕜 → ↑(e'.extend I) x ∈ interior (range ↑I)
h✝ : ¬IsRCLikeNormedField 𝕜
⊢ ↑(e'.extend I) x ∈ interior (range ↑I)

Tactic:
simp [I.range_eq_univ_of_not_isRCLikeNormedField ‹_›]

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

Goal state before:
pp: case refine_1
𝕜✝ : 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 ⇑(fderiv ℝ (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x))
hf'' : DifferentiableAt ℝ (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x)
⊢ (extChartAt I x).target ∈ 𝓝 (↑(extChartAt I x) x)

Tactic:
rw [← nhdsWithin_eq_nhds.2 (mem_interior_iff_mem_nhds.1 hx)]
    exact extChartAt_target_mem_nhdsWithin x

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

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
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
h : G
⊢ ((X f).comp (𝑳 I g)) h = (X (f.comp (𝑳 I g))) h

Tactic:
rw [ContMDiffMap.comp_apply, L_apply, ← evalAt_apply, evalAt_mul, hfdifferential_apply,
    fdifferential_apply, evalAt_apply]

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g✝ h : G
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^∞⟮I, G; 𝕜⟯⟨g⟩
hX : (↑X ((Y f).comp (𝑳 I g))) 1 = ((Derivation.evalAt g) ↑X) (Y f)
hY : (↑Y ((X f).comp (𝑳 I g))) 1 = ((Derivation.evalAt g) ↑Y) (X f)
⊢ (⁅↑X, ↑Y⁆ (ContMDiffMap.comp f (𝑳 I g))) 1 = ((Derivation.evalAt g) ⁅↑X, ↑Y⁆) f

Tactic:
rw [comp_L] at hX hY

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g✝ h : G
r : 𝕜
X✝ Y✝ : LeftInvariantDerivation I G
f✝ f' : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
X Y : LeftInvariantDerivation I G
g : G
f : C^∞⟮I, G; 𝕜⟯⟨g⟩
hX : (↑X (Y (ContMDiffMap.comp f (𝑳 I g)))) 1 = ((Derivation.evalAt g) ↑X) (Y f)
hY : (↑Y (X (ContMDiffMap.comp f (𝑳 I g)))) 1 = ((Derivation.evalAt g) ↑Y) (X f)
⊢ (⁅↑X, ↑Y⁆ (ContMDiffMap.comp f (𝑳 I g))) 1 = ((Derivation.evalAt g) ⁅↑X, ↑Y⁆) f
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
u : Set B
x₀ : B
hs : MDiffAt[u] (T% s) x₀
ht : MDiffAt[u] (T% t) x₀
⊢ (MDiffAt[u] fun x ↦ ⟨x, (s - t) x⟩) x₀

Tactic:
by
  rw [sub_eq_add_neg]
  apply mdifferentiableWithinAt_add_section hs <| mdifferentiableWithinAt_neg_section ht

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Hom

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
n : WithTop ℕ∞
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ϕ : ContMDiffAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂) n (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀
hv : ContMDiffAt IM (IB₁.prod 𝓘(𝕜, F₁)) n (fun m ↦ ⟨b₁ m, v m⟩) m₀
hb₂ : ContMDiffAt IM IB₂ n b₂ m₀
⊢ ContMDiffAt IM (IB₂.prod 𝓘(𝕜, F₂)) n (fun m ↦ ⟨b₂ m, (ϕ m) (v m)⟩) m₀

Tactic:
rw [← contMDiffWithinAt_univ] at hϕ hv hb₂ ⊢
  exact ContMDiffWithinAt.clm_apply_of_inCoordinates hϕ hv hb₂

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

Goal state before:
pp: n : ℕ
x✝⁶ : EuclideanSpace ℝ (Fin n)
hx : ∀ (i : Fin n), 0 ≤ x✝⁶.ofLp i
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
⊢ 0 ≤ x✝⁴ * x✝⁶.ofLp i + x✝³ * x✝⁵.ofLp i

Tactic:
specialize hx i

Goal state after:
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
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
x : EuclideanQuadrant n
x✝ : x ∈ univ
⊢ ⟨toLp 2 fun i ↦ max ((↑x).ofLp i) 0, ⋯⟩ = x

Tactic:
ext i

Goal state after:
n : ℕ
x : EuclideanQuadrant n
x✝ : x ∈ univ
i : Fin n
⊢ (↑⟨toLp 2 fun i ↦ max ((↑x).ofLp i) 0, ⋯⟩).ofLp i = (↑x).ofLp i
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : ⟨z, hz⟩ ∈ {z | (↑z).ofLp 0 < y - x}
⊢ (toLp 2 fun x_1 ↦ ↑⟨min ((↑⟨z, hz⟩).ofLp 0 + x) y, ⋯⟩ - x) = z

Tactic:
ext i

Goal state after:
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : ⟨z, hz⟩ ∈ {z | (↑z).ofLp 0 < y - x}
i : Fin 1
⊢ (toLp 2 fun x_1 ↦ ↑⟨min ((↑⟨z, hz⟩).ofLp 0 + x) y, ⋯⟩ - x).ofLp i = z.ofLp i
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : ⟨z, hz⟩ ∈ {z | (↑z).ofLp 0 < y - x}
⊢ (toLp 2 fun x_1 ↦ y - ↑⟨max (y - (↑⟨z, hz⟩).ofLp 0) x, ⋯⟩) = z

Tactic:
ext i

Goal state after:
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : ⟨z, hz⟩ ∈ {z | (↑z).ofLp 0 < y - x}
i : Fin 1
⊢ (toLp 2 fun x_1 ↦ y - ↑⟨max (y - (↑⟨z, hz⟩).ofLp 0) x, ⋯⟩).ofLp i = z.ofLp i
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
⊢ ↑⊥ < y

Tactic:
simp [hxy.out]

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

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : x < ↑p ∧ ↑p < y
⊢ (𝓡∂ 1).IsInteriorPoint p

Tactic:
by
  rw [ModelWithCorners.IsInteriorPoint, extChartAt, Icc_chartedSpaceChartAt_of_le_top hp.2,
    interior_range_modelWithCornersEuclideanHalfSpace]
  exact IccLeftChart_extend_interior_pos hp

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

Goal state before:
pp: case inl.inr
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
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✝
x y : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : z.ofLp 0 + x < y
hz₂ : 0 < z.ofLp 0
⊢ (↑(𝓡∂ 1) ∘ ↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) ∘ ↑(𝓡∂ 1).symm) (↑(𝓡∂ 1) ⟨z, hz₀⟩) =
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
      this)
      (↑(𝓡∂ 1) ⟨z, hz₀⟩)

Tactic:
ext i

Goal state after:
case inl.inr
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
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✝
x y : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : z.ofLp 0 + x < y
hz₂ : 0 < z.ofLp 0
i : Fin 1
⊢ ((↑(𝓡∂ 1) ∘ ↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) ∘ ↑(𝓡∂ 1).symm) (↑(𝓡∂ 1) ⟨z, hz₀⟩)).ofLp i =
    ((have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
          this)
          (↑(𝓡∂ 1) ⟨z, hz₀⟩)).ofLp
      i