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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h✝ : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
h : n ≤ -1
⊢ angle x y + -(2 * π) < angle x (x + y) + angle y (x + y)

Tactic:
angle_le_pi,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h✝ : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
h : n ≤ -1
⊢ π + -(2 * π) < angle x (x + y) + angle y (x + y)
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
fs : Finset (Fin (n + 1))
⊢ Finset.centroid ℝ fs s.points =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (centroidWeightsWithCircumcenter fs)

Tactic:
centroid_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
n : ℕ
s : Simplex ℝ P n
fs : Finset (Fin (n + 1))
⊢ (affineCombination ℝ fs s.points) (centroidWeights ℝ fs) =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (centroidWeightsWithCircumcenter fs)
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ (univ.weightedVSub s.pointsWithCircumcenter)
      (centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n +
          centroidWeightsWithCircumcenter {i₁, i₂} -
        reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) =
    0

Tactic:
weightedVSub_apply,

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₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ i,
      (centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n +
              centroidWeightsWithCircumcenter {i₁, i₂} -
            reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
          i •
        (s.pointsWithCircumcenter i -ᵥ Classical.choice ⋯) =
    0
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

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

Tactic:
sub_ne_zero,

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

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : r ∈ Set.Icc 0 1
t : ℝ
ht : t ∈ Set.Icc 0 1
h0 :
  (AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) t ∈ affineSpan ℝ (Set.range (s.faceOpposite j).points)
ht1 : t = 1
⊢ False

Tactic:
subst ht1

Goal state after:
case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : r ∈ Set.Icc 0 1
ht : 1 ∈ Set.Icc 0 1
h0 :
  (AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) 1 ∈ affineSpan ℝ (Set.range (s.faceOpposite j).points)
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
h_sin_xz : Real.sin (angle x z) ≠ 0
hx : ¬x = 0
hz : ¬z = 0
hnneg₁ : 0 ≤ Real.sin (angle y z) / ‖x‖
hnneg₂ : 0 ≤ Real.sin (angle x y) / ‖z‖
hnneg₃ : 0 ≤ Real.sin (angle x z) / ‖y‖
hnonzero : ⟨Real.sin (angle x z) / ‖y‖, hnneg₃⟩ ≠ 0
h₁ :
  angle x z ≠ π →
    angle x z = angle x y + angle y z →
      Real.sin (angle x z) • NormedSpace.normalize y =
        Real.sin (angle y z) • NormedSpace.normalize x + Real.sin (angle x y) • NormedSpace.normalize z
h₂ :
  Real.sin (angle x z) • NormedSpace.normalize y =
    Real.sin (angle y z) • NormedSpace.normalize x + Real.sin (angle x y) • NormedSpace.normalize z
h₃ :
  ⟨Real.sin (angle x z) / ‖y‖, hnneg₃⟩ • y =
    ⟨Real.sin (angle y z) / ‖x‖, hnneg₁⟩ • x + ⟨Real.sin (angle x y) / ‖z‖, hnneg₂⟩ • z
⊢ y ∈ Submodule.span ℝ≥0 {x, z}

Tactic:
exact mem_span_of_linear_combination hnonzero h₃

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 : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ s.faceOppositeCentroid i ∈ s.ninePointCircle

Tactic:
by
  rw [mem_sphere, ninePointCircle_center, ninePointCircle_radius,
    ← dist_circumcenter_eq_circumradius' s i]
  simp_rw [dist_eq_norm_vsub]
  rw [eq_div_iff_mul_eq (by simpa using NeZero.ne n), mul_comm]
  nth_rw 1 [show (n : ℝ) = ‖(n : ℝ)‖ by simp]
  rw [← norm_smul, vsub_vadd_eq_vsub_sub, smul_sub, smul_smul,
    mul_div_cancel₀ _ (by simpa using NeZero.ne n), add_smul, one_smul, ← sub_sub, ← smul_sub,
    vsub_sub_vsub_cancel_right, ← centroid_vsub_point_eq_smul_vsub, vsub_sub_vsub_cancel_left]

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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (↑(m + 1) / ↑(m - 1)) • (Finset.centroid ℝ univ (s.reindex e).points -ᵥ s.circumcenter) +ᵥ s.circumcenter =
    (↑(n + 1) / ↑(n - 1)) • (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) +ᵥ s.circumcenter

Tactic:
centroid_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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (↑(m + 1) / ↑(m - 1)) •
        ((affineCombination ℝ univ (s.reindex e).points) (centroidWeights ℝ univ) -ᵥ s.circumcenter) +ᵥ
      s.circumcenter =
    (↑(n + 1) / ↑(n - 1)) • ((affineCombination ℝ univ s.points) (centroidWeights ℝ univ) -ᵥ s.circumcenter) +ᵥ
      s.circumcenter
Module: Mathlib.Geometry.Euclidean.NinePointCircle

Goal state before:
pp: case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : ↑(n - 1) = ↑n - 1
this :
  (↑n)⁻¹ • (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)
⊢ ⅟2 • (((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter) + ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)

Tactic:
← two_smul ℝ,

Goal state after:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : ↑(n - 1) = ↑n - 1
this :
  (↑n)⁻¹ • (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)
⊢ ⅟2 • 2 • ((↑n + 1) / ↑n) • (s.centroid -ᵥ 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)
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points =
    (univ.weightedVSub s.pointsWithCircumcenter) (mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂)

Tactic:
simp_rw [mongePoint_eq_affineCombination_of_pointsWithCircumcenter,
    centroid_eq_affineCombination_of_pointsWithCircumcenter, affineCombination_vsub,
    mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub h]

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
n : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ mk' (Finset.centroid ℝ {i₁, i₂}ᶜ (s.reindex e).points) (ℝ ∙ (s.points (e.symm i₁) -ᵥ s.points (e.symm i₂)))ᗮ ⊓
      affineSpan ℝ (Set.range s.points) =
    mk' (Finset.centroid ℝ {e.symm i₁, e.symm i₂}ᶜ s.points) (ℝ ∙ (s.points (e.symm i₁) -ᵥ s.points (e.symm i₂)))ᗮ ⊓
      affineSpan ℝ (Set.range s.points)

Tactic:
centroid_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
n : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ mk' ((affineCombination ℝ {i₁, i₂}ᶜ (s.reindex e).points) (centroidWeights ℝ {i₁, i₂}ᶜ))
        (ℝ ∙ (s.points (e.symm i₁) -ᵥ s.points (e.symm i₂)))ᗮ ⊓
      affineSpan ℝ (Set.range s.points) =
    mk' ((affineCombination ℝ {e.symm i₁, e.symm i₂}ᶜ s.points) (centroidWeights ℝ {e.symm i₁, e.symm i₂}ᶜ))
        (ℝ ∙ (s.points (e.symm i₁) -ᵥ s.points (e.symm i₂)))ᗮ ⊓
      affineSpan ℝ (Set.range s.points)
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₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (vectorSpan ℝ (s.points '' Set.univ))ᗮ
hu : ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x ↦ s.points i₁ -ᵥ x) '' s.points '' (Set.univ \ {i₁})
⊢ p -ᵥ s.mongePoint = 0

Tactic:
Set.image_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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (vectorSpan ℝ (Set.range s.points))ᗮ
hu : ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x ↦ s.points i₁ -ᵥ x) '' s.points '' (Set.univ \ {i₁})
⊢ p -ᵥ s.mongePoint = 0
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

Goal state before:
pp: case neg
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' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
h : ¬p' = p
he : ⟪- -(p' -ᵥ p), p -ᵥ s.center⟫ = 0
⊢ False

Tactic:
inner_neg_left,

Goal state after:
case neg
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' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
h : ¬p' = p
he : -⟪-(p' -ᵥ p), p -ᵥ s.center⟫ = 0
⊢ False
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
⊢ t.orthocenter = 3 • (Finset.centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t

Tactic:
rw [orthocenter_eq_mongePoint, mongePoint_eq_smul_vsub_vadd_circumcenter]

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
⊢ (↑(2 + 1) / ↑(2 - 1)) • (Finset.centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t =
    3 • (Finset.centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t
Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
E'' : Type u_7
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝¹⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace H'' N'
n : ℕ∞ω
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : ContMDiffMul I' n G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : ContMDiffMul I'' n G''
φ : G' →* G''
hφ : ContMDiff I' I'' n ⇑φ
x✝ : N
⊢ ⟨⇑φ ∘ ⇑1, ⋯⟩ x✝ = 1 x✝

Tactic:
change φ 1 = 1

Goal state after:
𝕜 : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
E'' : Type u_7
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝¹⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace H'' N'
n : ℕ∞ω
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : ContMDiffMul I' n G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : ContMDiffMul I'' n G''
φ : G' →* G''
hφ : ContMDiff I' I'' n ⇑φ
x✝ : N
⊢ φ 1 = 1
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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
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
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
h : I'.IsInteriorPoint (f x)
⊢ I.IsInteriorPoint x

Tactic:
· rw [← hf.localInverse_left_inv hf.localInverse_mem_target]
    refine (hf.localInverse_mdifferentiableAt hn).isInteriorPoint_of_surjective_mfderiv ?_ h
    exact (hf.mfderivToContinuousLinearEquiv hn).symm.surjective

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

Goal state before:
pp: case mp
𝕜 : 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'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux : interior (range ↑I) ×ˢ interior (range ↑J) = interior (range ↑(I.prod J))
hp : (I.prod J).IsInteriorPoint p
⊢ p ∈ ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N

Tactic:
rw [IsInteriorPoint, ← aux] at hp

Goal state after:
case mp
𝕜 : 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'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux : interior (range ↑I) ×ˢ interior (range ↑J) = interior (range ↑(I.prod J))
hp : ↑(extChartAt (I.prod J) p) p ∈ interior (range ↑I) ×ˢ interior (range ↑J)
⊢ p ∈ ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁰ : NormedAddCommGroup EB
inst✝⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁷ : TopologicalSpace B
inst✝⁶ : ChartedSpace HB B
inst✝⁵ : FiberBundle F E
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle 1 F E IB
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
s : (b : B) → E b
u : Set B
b₀ : B
hex₀ : b₀ ∈ e.baseSet
⊢ MDiffAt[u] (T% s) b₀ ↔ (MDiffAt[u] fun x ↦ (↑e ⟨x, s x⟩).2) b₀

Tactic:
by
  rw [e.mdifferentiableWithinAt_totalSpace_iff IB]
  · change MDiffAt[u] (@id B) b₀ ∧ _ ↔ _
    simp [mdifferentiableWithinAt_id]
  exact (coe_mem_source e).mpr hex₀

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 ℕ∞
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₀
this : ContMDiffOn I 𝓘(𝕜, F) k (fun x ↦ (↑t ⟨x, extend F σ₀ x⟩).2) t.baseSet
x : M
hx : x ∈ t.baseSet
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) k (fun x' ↦ ⟨x', extend F σ₀ x'⟩) t.baseSet x

Tactic:
t.contMDiffWithinAt_section _ 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
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₀
this : ContMDiffOn I 𝓘(𝕜, F) k (fun x ↦ (↑t ⟨x, extend F σ₀ x⟩).2) t.baseSet
x : M
hx : x ∈ t.baseSet
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) k (fun x ↦ (↑t ⟨x, extend F σ₀ x⟩).2) t.baseSet x
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case hV
𝕜 : 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
hV : V x = 0
hW : W x = 0
this : ↑(extChartAt I x).symm (↑(extChartAt I x) x) = x
⊢ (mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x)).inverse
      (V (↑(extChartAt I x).symm (↑(extChartAt I x) x))) =
    0

Tactic:
rw [this, hV]

Goal state after:
case hV
𝕜 : 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
hV : V x = 0
hW : W x = 0
this : ↑(extChartAt I x).symm (↑(extChartAt I x) x) = x
⊢ (mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x)).inverse 0 = 0
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
v w : GroupLieAlgebra I G
g : G
⊢ mulInvariantVectorField (v + w) g = (mulInvariantVectorField v + mulInvariantVectorField w) g

Tactic:
simp [mulInvariantVectorField]

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
c : 𝕜
v : GroupLieAlgebra I G
g : G
⊢ mulInvariantVectorField (c • v) g = (c • mulInvariantVectorField v) g

Tactic:
simp [mulInvariantVectorField]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
E'' : Type u
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
H : Type u_7
inst✝⁵ : TopologicalSpace H
G : Type u_9
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_13
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
hf : IsImmersionAt I J n f x
hfg : f =ᶠ[𝓝 x] g
⊢ IsImmersionAt I J n g x

Tactic:
use hf.complement, by infer_instance, by infer_instance
  exact hf.isImmersionAtOfComplement_complement.congr_of_eventuallyEq hfg

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

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
⊢ (mfderiv[Icc x y] (projIcc x y ⋯) z) 1 = 1

Tactic:
change _ = oneTangentSpaceIcc (Set.projIcc x y h.out.le z)

Goal state after:
x y : ℝ
h : Fact (x < y)
z : ℝ
hz : z ∈ Icc x y
⊢ (mfderiv[Icc x y] (projIcc x y ⋯) z) 1 = oneTangentSpaceIcc (projIcc x y ⋯ z)