mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x ↦ (↑x.1, p₅, x.2 +ᵥ ↑x.1)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p ↦ ∡ p.1 p.2.1 p.2.2) s
v : V
q : P
hq : q ∈ line[ℝ, p₁, p₂]
hv : SameRay ℝ (p₂ -ᵥ p₁) (⟨q, hq⟩, v).2 ∧ (⟨q, hq⟩, v).2 ≠ 0
⊢ ∡ (↑(⟨q, hq⟩, v).1) p₅ ((⟨q, hq⟩, v).2 +ᵥ ↑(⟨q, hq⟩, v).1) ≠ 0 ∧
    ∡ (↑(⟨q, hq⟩, v).1) p₅ ((⟨q, hq⟩, v).2 +ᵥ ↑(⟨q, hq⟩, v).1) ≠ ↑π

Tactic:
dsimp only [Subtype.coe_mk, Set.mem_ofPred] at hv ⊢

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x ↦ (↑x.1, p₅, x.2 +ᵥ ↑x.1)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p ↦ ∡ p.1 p.2.1 p.2.2) s
v : V
q : P
hq : q ∈ line[ℝ, p₁, p₂]
hv : SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0
⊢ ∡ q p₅ (v +ᵥ q) ≠ 0 ∧ ∡ q p₅ (v +ᵥ q) ≠ ↑π
Module: Mathlib.Geometry.Euclidean.Basic

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
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
| dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂

Tactic:
rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_smul_vadd_sq, mul_assoc,
      ← sub_eq_zero, add_sub_assoc, dist_eq_norm_vsub V p₁ p₂, ← real_inner_self_eq_norm_mul_norm,
      sub_self]

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
| ⟪v, v⟫ * (r * r) + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + 0 = 0
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ (Equiv.pointReflection s.center) p₂ = p₁

Tactic:
rw [← h.midpoint_eq_center, Equiv.pointReflection_midpoint_right]

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

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
hp : s.radius < dist p s.center
p' : P
⊢ 0 ≤ s.radius → p' -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ → ¬‖p' -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2

Tactic:
rintro hle - h

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hp : s.radius < dist p s.center
p' : P
hle : 0 ≤ s.radius
h : ‖p' -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
⊢ False
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

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₁ s₂ : Sphere P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
h : dist s₂.center s₁.center + s₁.radius = s₂.radius
⊢ dist s₁.center s₂.center = s₂.radius - s₁.radius

Tactic:
simp [← h, dist_comm]

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

Goal state before:
pp: case inl.inr.inr
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
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : ¬(ℝ ∙ (p -ᵥ s.center))ᗮ = ⊥
hn : ¬Subsingleton V
hnf : Module.finrank ℝ V ≠ 1
v : V
hvm : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
hv0 : v ≠ 0
⊢ (Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)).Nonempty

Tactic:
refine ⟨(√(s.radius ^ 2 - (dist p s.center) ^ 2) / ‖v‖) • v +ᵥ p, ?_⟩

Goal state after:
case inl.inr.inr
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
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : ¬(ℝ ∙ (p -ᵥ s.center))ᗮ = ⊥
hn : ¬Subsingleton V
hnf : Module.finrank ℝ V ≠ 1
v : V
hvm : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
hv0 : v ≠ 0
⊢ (√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • v +ᵥ p ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x z : V
hxzne : x ≠ z
hxz : ‖x‖ = ‖z‖
hxyne : x ≠ 0
hxy : ‖x‖ = 0
⊢ False

Tactic:
norm_eq_zero

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x z : V
hxzne : x ≠ z
hxz : ‖x‖ = ‖z‖
hxyne : x ≠ 0
hxy : x = 0
⊢ False
Module: Mathlib.Geometry.Euclidean.Triangle

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
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pb : ¬p = b
pc : p = c
⊢ ∠ b a p + ∠ p a c = ∠ b a c

pp: case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pb : ¬p = b
pc : ¬p = c
⊢ ∠ b a p + ∠ p a c = ∠ b a c

Tactic:
· simpa [pc] using angle_self_of_ne hc.symm

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
a b c p : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pb : ¬p = b
pc : ¬p = c
⊢ ∠ b a p + ∠ p a c = ∠ b a c
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
⊢ Cospherical {p₁, p₂, p₃, p₄}

Tactic:
have hn' : ¬Collinear ℝ ({p₁, p₃, p₄} : Set P) := by
    rwa [← collinear_iff_of_two_zsmul_oangle_eq h]
  let t₁ : Affine.Triangle ℝ P := ⟨![p₁, p₂, p₄], affineIndependent_iff_not_collinear_set.2 hn⟩
  let t₂ : Affine.Triangle ℝ P := ⟨![p₁, p₃, p₄], affineIndependent_iff_not_collinear_set.2 hn'⟩
  rw [cospherical_iff_exists_sphere]
  refine ⟨t₂.circumsphere, ?_⟩
  simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff]
  refine ⟨t₂.mem_circumsphere 0, ?_, t₂.mem_circumsphere 1, t₂.mem_circumsphere 2⟩
  rw [Affine.Triangle.circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq
    (by decide : (0 : Fin 3) ≠ 1) (by decide : (0 : Fin 3) ≠ 2) (by decide)
    (show t₂.points 0 = t₁.points 0 from rfl) rfl h.symm]
  exact t₁.mem_circumsphere 1

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ ∑ j, pointWeightsWithCircumcenter i j = 1

Tactic:
convert! sum_ite_eq' univ (pointIndex i) (Function.const _ (1 : ℝ)) with j

Goal state after:
case e'_2.a
n : ℕ
i : Fin (n + 1)
j : PointsWithCircumcenterIndex n
a✝ : j ∈ univ
⊢ pointWeightsWithCircumcenter i j = if j = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 j else 0

case e'_3
n : ℕ
i : Fin (n + 1)
⊢ 1 = if pointIndex i ∈ univ then Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex i) else 0
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
⊢ s.circumcenter = (affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter n)

Tactic:
← pointsWithCircumcenter_eq_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
n : ℕ
s : Simplex ℝ P n
⊢ s.pointsWithCircumcenter circumcenterIndex =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter n)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : angle x y = 0
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
· grind [Real.sin_zero, zero_smul, eq_of_angle_eq_zero]

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case refine_1
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
⊢ (s.signedInfDist j) ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) t) ≠ 0

Tactic:
intro h0
      rw [← abs_eq_zero, abs_signedInfDist_eq_dist_of_mem_affineSpan_range] at h0
      · rw [orthogonalProjectionSpan, dist_orthogonalProjection_eq_zero_iff] at h0
        by_cases ht1 : t = 1
        · subst ht1
          rw [AffineMap.lineMap_apply_one] at h0
          exact h.touchpoint_notMem_affineSpan_of_ne hne h0
        · refine (h.isTangentAt_touchpoint j).isTangent.notMem_of_dist_lt ?_ h0
          simp only [exsphere_center, dist_lineMap_left, Real.norm_eq_abs, h.dist_excenter,
            exsphere_radius, h.exradius_pos, mul_lt_iff_lt_one_left]
          rw [abs_lt]
          rcases ht with ⟨ht0, ht1'⟩
          exact ⟨by linarith, ht1'.lt_of_ne ht1⟩
      · exact AffineMap.lineMap_mem _ h.excenter_mem_affineSpan_range
          (s.touchpoint_mem_affineSpan_simplex _ _)

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
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
hc :
  ContinuousOn
    (fun t ↦ SignType.sign ((s.signedInfDist j) ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) t)))
    (Set.Icc 0 1)
⊢ SignType.sign ((s.signedInfDist j) ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) r)) =
    SignType.sign ((s.signedInfDist j) (s.excenter signs))

Tactic:
refine ((isConnected_Icc zero_le_one).image _ hc).isPreconnected.subsingleton
    (Set.mem_image_of_mem _ 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
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
hc :
  ContinuousOn
    (fun t ↦ SignType.sign ((s.signedInfDist j) ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) t)))
    (Set.Icc 0 1)
⊢ SignType.sign ((s.signedInfDist j) (s.excenter signs)) ∈
    (fun t ↦ SignType.sign ((s.signedInfDist j) ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) t))) ''
      Set.Icc 0 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
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 ∈ (⨆ i₂, ℝ ∙ (s.points i₁ -ᵥ s.points ↑i₂))ᗮ
⊢ p -ᵥ s.mongePoint = 0

Tactic:
← Submodule.span_iUnion

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 ∈ (Submodule.span ℝ (⋃ i, {s.points i₁ -ᵥ s.points ↑i}))ᗮ
⊢ p -ᵥ s.mongePoint = 0
Module: Mathlib.Geometry.Euclidean.Similarity

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
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 c * dist a c = dist a b * dist a b + dist c b * dist c b - 2 * dist a b * dist c b * Real.cos (∠ a b c)
⊢ ∠ a b c = ∠ a' b' c'

Tactic:
rw [h_ab, h_cb, h_ac] at h_cos

Goal state after:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
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 :
  r * dist a' c' * (r * dist a' c') =
    r * dist a' b' * (r * dist a' b') + r * dist c' b' * (r * dist c' b') -
      2 * (r * dist a' b') * (r * dist c' b') * Real.cos (∠ a b c)
⊢ ∠ a b c = ∠ a' b' c'
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist t.orthocenter ((reflection (affineSpan ℝ (t.points '' {i₁, i₂}))) (circumcenter t)) = circumradius t

Tactic:
by
  rw [← mul_self_inj_of_nonneg dist_nonneg t.circumradius_nonneg,
    t.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter h,
    t.orthocenter_eq_mongePoint, mongePoint_eq_affineCombination_of_pointsWithCircumcenter,
    dist_affineCombination t.pointsWithCircumcenter (sum_mongePointWeightsWithCircumcenter _)
      (sum_reflectionCircumcenterWeightsWithCircumcenter h)]
  simp_rw [sum_pointsWithCircumcenter, Pi.sub_apply, mongePointWeightsWithCircumcenter,
    reflectionCircumcenterWeightsWithCircumcenter]
  have hu : ({i₁, i₂} : Finset (Fin 3)) ⊆ univ := subset_univ _
  obtain ⟨i₃, hi₃, hi₃₁, hi₃₂⟩ :
      ∃ i₃, univ \ ({i₁, i₂} : Finset (Fin 3)) = {i₃} ∧ i₃ ≠ i₁ ∧ i₃ ≠ i₂ := by
    decide +revert
  simp_rw [← sum_sdiff hu, hi₃]
  norm_num [hi₃₁, hi₃₂]

Goal state after:
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 : ℕ∞ω
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : ContMDiffRing I' n R
a : C^n⟮I, N; I', R⟯
⊢ 0 * a = 0

Tactic:
by ext; exact zero_mul _

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

Goal state before:
pp: case inr
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝³ : I.Boundaryless
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
f : M → F
U : Set M
a b : M
hd : MDiff[U] f
hpc : IsPreconnected U
hc : IsCompact U
ho : IsOpen[inst✝²] U
ha : a ∈ U
hb : b ∈ U
this : ∀ {f : M → F}, MDiff[U] f → f b = 0 → f a = f b
hb₀ : ¬f b = 0
⊢ f a = f b

Tactic:
have hd' : MDiff[U] (f · - f b) := fun x hx ↦
      ⟨(hd x hx).1.sub continuousWithinAt_const, (hd x hx).2.sub_const _⟩
    simpa [sub_eq_zero] using this hd' (sub_self _)

Goal state after:
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 (↑hf.localInverse.toPartialEquiv (f x))

Tactic:
refine (hf.localInverse_mdifferentiableAt hn).isInteriorPoint_of_surjective_mfderiv ?_ h

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
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)
⊢ Surjective ⇑(mfderiv% ↑hf.localInverse.toPartialEquiv (f x))
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 : ↑(extChartAt (I.prod J) p) p ∈ interior (range ↑(I.prod J))
⊢ p ∈ ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N

Tactic:
← aux

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
M : Type u_5
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
EM : Type u_10
inst✝⁷ : NormedAddCommGroup EM
inst✝⁶ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝⁵ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace HM M
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
⊢ MDiffAt[s] f x₀ ↔
    (MDiffAt[s] fun x ↦ (f x).proj) x₀ ∧ (MDiffAt[s] fun x ↦ (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀

Tactic:
simp +singlePass only [mdifferentiableWithinAt_iff_target]

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
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
EM : Type u_10
inst✝⁷ : NormedAddCommGroup EM
inst✝⁶ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝⁵ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace HM M
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
⊢ ContinuousWithinAt f s x₀ ∧ MDiffAt[s] (↑(extChartAt (IB.prod 𝓘(𝕜, F)) (f x₀)) ∘ f) x₀ ↔
    (ContinuousWithinAt (fun x ↦ (f x).proj) s x₀ ∧ MDiffAt[s] (↑(extChartAt IB (f x₀).proj) ∘ fun x ↦ (f x).proj) x₀) ∧
      ContinuousWithinAt (fun x ↦ (↑(trivializationAt F E (f x₀).proj) (f x)).2) s x₀ ∧
        MDiffAt[s]
            (↑(extChartAt 𝓘(𝕜, F) (↑(trivializationAt F E (f x₀).proj) (f x₀)).2) ∘ fun x ↦
              (↑(trivializationAt F E (f x₀).proj) (f x)).2)
          x₀
Module: Mathlib.Geometry.Manifold.Instances.Real

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

Tactic:
Icc_chartedSpaceChartAt_of_le_top (by simp [hxy.out])

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