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

Goal state before:
pp: case h
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
⊢ ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r

Tactic:
intro sx hsxps

Goal state after:
case h
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
⊢ sx.circumradius = r
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case h
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
⊢ ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c

Tactic:
intro sx hsxps

Goal state after:
case h
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
⊢ sx.circumcenter = c
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
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter
r₁ : ℝ
p₁o : P
hp₁o : p₁o ∈ affineSpan ℝ (Set.range s.points)
hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₁o
r₂ : ℝ
p₂o : P
hp₂o : p₂o ∈ affineSpan ℝ (Set.range s.points)
hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₂o
⊢ ↑(s.orthogonalProjectionSpan p₁) = p₁o

Tactic:
subst hp₁

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
p p₂ : P
r : ℝ
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter
r₁ : ℝ
p₁o : P
hp₁o : p₁o ∈ affineSpan ℝ (Set.range s.points)
r₂ : ℝ
p₂o : P
hp₂o : p₂o ∈ affineSpan ℝ (Set.range s.points)
hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₂o
h₁ :
  ∀ (i : Fin (n + 1)),
    dist (s.points i) (r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₁o) = r
h₁' :
  ↑(s.orthogonalProjectionSpan (r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₁o)) =
    s.circumcenter
⊢ ↑(s.orthogonalProjectionSpan (r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₁o)) =
    p₁o
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
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter
r₁ : ℝ
p₁o : P
hp₁o : p₁o ∈ affineSpan ℝ (Set.range s.points)
hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₁o
r₂ : ℝ
p₂o : P
hp₂o : p₂o ∈ affineSpan ℝ (Set.range s.points)
hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₂o
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) p₂

Tactic:
obtain rfl : ↑(s.orthogonalProjectionSpan p₁) = p₁o := by
    subst hp₁
    exact s.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection hp₁o

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
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter
r₁ r₂ : ℝ
p₂o : P
hp₂o : p₂o ∈ affineSpan ℝ (Set.range s.points)
hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₂o
hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)
hp₁ :
  p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ ↑(s.orthogonalProjectionSpan p₁)
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) p₂
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
⊢ angle x z ≤ angle x y + angle y z

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : x = 0
⊢ angle x z ≤ angle x y + angle y z

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ¬x = 0
⊢ angle x z ≤ angle x y + angle y z
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 = π
⊢ angle x z = π ∨ y ∈ Submodule.span ℝ≥0 {x, z}

Tactic:
right

Goal state after:
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 = π
⊢ y ∈ Submodule.span ℝ≥0 {x, z}
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
n : ℕ
inst✝¹ : NeZero n
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : Pi.single j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : SignType.sign (s.touchpointWeights signs i k) = 0
⊢ False

Tactic:
h.sign_touchpointWeights hki.symm,

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
n : ℕ
inst✝¹ : NeZero n
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : Pi.single j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : SignType.sign (s.excenterWeights signs k) = 0
⊢ 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
⊢ y ∈ Submodule.span ℝ≥0 {x, z}

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
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
⊢ y ∈ Submodule.span ℝ≥0 {x, z}

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
⊢ y ∈ Submodule.span ℝ≥0 {x, z}
Module: Mathlib.Geometry.Euclidean.Congruence

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₂
h : ¬Collinear ℝ {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
h' : ¬Collinear ℝ {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
h_bac : ¬Collinear ℝ {b, a, c}
h_bac' : ¬Collinear ℝ {b', a', c'}
⊢ dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')

Tactic:
dist_comm c' b',

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₂
h : ¬Collinear ℝ {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
h' : ¬Collinear ℝ {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
h_bac : ¬Collinear ℝ {b, a, c}
h_bac' : ¬Collinear ℝ {b', a', c'}
⊢ dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
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
signs : Finset (Fin 3)
⊢ Simplex.ExcenterExists t signs

Tactic:
have h : signs = ∅ ∨ signs = ∅ᶜ ∨ ∃ i, signs = {i} ∨ signs = {i}ᶜ := by decide +revert
  rcases h with rfl | rfl | ⟨i, rfl | rfl⟩
  · exact t.excenterExists_empty
  · rw [Simplex.excenterExists_compl]
    exact t.excenterExists_empty
  · exact t.excenterExists_singleton _
  · rw [Simplex.excenterExists_compl]
    exact t.excenterExists_singleton _

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

Goal state before:
pp: case neg.inr
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
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter
r₁ r₂ : ℝ
hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)
hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)
hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
h : s.points 0 ∈ span_s
hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius
hp : ¬p = ↑(s.orthogonalProjectionSpan p)
hz : ⟪p -ᵥ ↑((orthogonalProjection span_s) p), p -ᵥ ↑((orthogonalProjection span_s) p)⟫ ≠ 0
hd₁ : r₁ = -r₂
⊢ r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter =
      r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter ∨
    r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter =
      (reflection (affineSpan ℝ (Set.range s.points)))
        (r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter)

Tactic:
right

Goal state after:
case neg.inr
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
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := ⋯
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter
r₁ r₂ : ℝ
hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)
hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)
hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
h : s.points 0 ∈ span_s
hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius
hp : ¬p = ↑(s.orthogonalProjectionSpan p)
hz : ⟪p -ᵥ ↑((orthogonalProjection span_s) p), p -ᵥ ↑((orthogonalProjection span_s) p)⟫ ≠ 0
hd₁ : r₁ = -r₂
⊢ r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter =
    (reflection (affineSpan ℝ (Set.range s.points)))
      (r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter)
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h₁ : ∃ k, x = k • y
h₃ : ‖z - y‖ = ‖z + y‖
⊢ ‖x - y‖ * ‖x + y‖ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2|

Tactic:
by
  obtain ⟨r, hr⟩ := h₁
  have hzy : ⟪z, y⟫ = 0 := by
    rwa [inner_eq_zero_iff_angle_eq_pi_div_two, ← norm_add_eq_norm_sub_iff_angle_eq_pi_div_two,
      eq_comm]
  have hzx : ⟪z, x⟫ = 0 := by rw [hr, inner_smul_right, hzy, mul_zero]
  calc
    ‖x - y‖ * ‖x + y‖ = ‖(r - 1) • y‖ * ‖(r + 1) • y‖ := by simp [sub_smul, add_smul, hr]
    _ = ‖r - 1‖ * ‖y‖ * (‖r + 1‖ * ‖y‖) := by simp_rw [norm_smul]
    _ = ‖r - 1‖ * ‖r + 1‖ * ‖y‖ ^ 2 := by ring
    _ = |(r - 1) * (r + 1) * ‖y‖ ^ 2| := by simp [abs_mul]
    _ = |r ^ 2 * ‖y‖ ^ 2 - ‖y‖ ^ 2| := by ring_nf
    _ = |‖x‖ ^ 2 - ‖y‖ ^ 2| := by simp [hr, norm_smul, mul_pow, sq_abs]
    _ = |‖z + y‖ ^ 2 - ‖z - x‖ ^ 2| := by
      simp [norm_add_sq_real, norm_sub_sq_real, hzy, hzx, abs_sub_comm]

Goal state after:
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₂
h_not_col : ¬Collinear ℝ {a, b, c}
h_not_col' : ¬Collinear ℝ {a', b', c'}
h : ∠ a b c = ∠ a' b' c'
dist_a'b' : dist a' b' ≠ 0
dist_b'c' : dist b' c' ≠ 0
k : ℝ := dist a b / dist a' b'
hd : k = dist b c / dist b' c'
hk : k = dist a b / dist a' b'
k_pos : 0 < k
h_ab : dist a b = k * dist a' b'
h_bc : dist c b = k * dist c' b'
hcos : dist a c ^ 2 = k ^ 2 * (dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c'))
hcos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
⊢ ![a, b, c] ∼ ![a', b', c']

Tactic:
← hcos',

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₂
h_not_col : ¬Collinear ℝ {a, b, c}
h_not_col' : ¬Collinear ℝ {a', b', c'}
h : ∠ a b c = ∠ a' b' c'
dist_a'b' : dist a' b' ≠ 0
dist_b'c' : dist b' c' ≠ 0
k : ℝ := dist a b / dist a' b'
hd : k = dist b c / dist b' c'
hk : k = dist a b / dist a' b'
k_pos : 0 < k
h_ab : dist a b = k * dist a' b'
h_bc : dist c b = k * dist c' b'
hcos : dist a c ^ 2 = k ^ 2 * dist a' c' ^ 2
hcos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * 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₁ 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₃
⊢ line[ℝ, t₁.points i₁, t₁.points i₂] = altitude t₂ j₂

Tactic:
rw [← h₂, t₂.affineSpan_pair_eq_altitude_iff]

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₁ 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₁ ≠ t₂.points j₂ ∧
    t₁.points i₁ ∈ affineSpan ℝ (Set.range t₂.points) ∧
      t₁.points i₁ -ᵥ t₂.points j₂ ∈ (affineSpan ℝ (t₂.points '' {j₂}ᶜ)).directionᗮ
Module: Mathlib.Geometry.Euclidean.MongePoint

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
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
h : t.orthocenter ∉ Set.range p
⊢ (∃ i₁ i₂ i₃ j₂ j₃,
      i₁ ≠ i₂ ∧
        i₁ ≠ i₃ ∧
          i₂ ≠ i₃ ∧
            (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
              p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃) ∨
    Set.range p = Set.range t.points

Tactic:
right

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
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
h : t.orthocenter ∉ Set.range p
⊢ Set.range p = Set.range t.points
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
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 : Surjective ⇑(fderivWithin 𝕜 (↑φ) φ.source (↑(e.extend I) x)) → ↑(e'.extend I) x ∈ interior (range ↑I)
⊢ ↑(e'.symm.restr I.source).symm x ∈ e'.target

Tactic:
simp [hex']

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 (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))) - ↑Y (↑X (ContMDiffMap.comp f (𝑳 I g)))) 1 = ((Derivation.evalAt g) ⁅↑X, ↑Y⁆) f

Tactic:
ContMDiffMap.coe_sub,

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)))) - ⇑(↑Y (↑X (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
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:
by
  simp +singlePass only [mdifferentiableWithinAt_iff_target]
  rw [and_and_and_comm, ← FiberBundle.continuousWithinAt_totalSpace, and_congr_right_iff]
  intro hf
  simp_rw +instances [modelWithCornersSelf_prod, FiberBundle.extChartAt, Function.comp_def,
    PartialEquiv.trans_apply, PartialEquiv.prod_coe, PartialEquiv.refl_coe,
    extChartAt_self_apply, modelWithCornersSelf_coe, Function.id_def, ← chartedSpaceSelf_prod]
  refine (mdifferentiableWithinAt_prod_iff _).trans (and_congr ?_ Iff.rfl)
  have h1 : (fun x => (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet ∈ 𝓝[s] x₀ :=
    ((FiberBundle.continuous_proj F E).continuousWithinAt.comp hf (mapsTo_image f s))
      ((Trivialization.open_baseSet _).mem_nhds (mem_baseSet_trivializationAt F E _))
  refine EventuallyEq.mdifferentiableWithinAt_iff (eventually_of_mem h1 fun x hx => ?_) ?_
  · simp_rw [Function.comp, OpenPartialHomeomorph.coe_toPartialEquiv, Trivialization.coe_coe]
    rw [Trivialization.coe_fst']
    exact hx
  · simp only [mfld_simps]

Goal state after: