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

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 y : V
r : ℝ
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign

Tactic:
by_cases h : o.oangle x y = 0 ∨ o.oangle x y = π
  · rwa [Real.Angle.sign_eq_zero_iff.2 h, Real.Angle.sign_eq_zero_iff,
      oangle_smul_add_right_eq_zero_or_eq_pi_iff]
  have h' : ∀ r' : ℝ, o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ π := by
    intro r'
    rwa [← o.oangle_smul_add_right_eq_zero_or_eq_pi_iff r', not_or] at h
  let s : Set (V × V) := (fun r' : ℝ => (x, r' • x + y)) '' Set.univ
  have hc : IsConnected s := isConnected_univ.image _ (by fun_prop)
  have hf : ContinuousOn (fun z : V × V => o.oangle z.1 z.2) s := by
    refine continuousOn_of_forall_continuousAt fun z hz => o.continuousAt_oangle ?_ ?_
    all_goals
      simp_rw [s, Set.mem_image] at hz
      obtain ⟨r', -, rfl⟩ := hz
      simp only
      intro hz
    · simpa [hz] using (h' 0).1
    · simpa [hz] using (h' r').1
  have hs : ∀ z : V × V, z ∈ s → o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ π := by grind
  have hx : (x, y) ∈ s := by
    convert! Set.mem_image_of_mem (fun r' : ℝ => (x, r' • x + y)) (Set.mem_univ 0)
    simp
  have hy : (x, r • x + y) ∈ s := Set.mem_image_of_mem _ (Set.mem_univ _)
  convert! Real.Angle.sign_eq_of_continuousOn hc hf hs hx hy

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case neg.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hn : ¬x = y
hy : y ≠ 0
r : ℝ
h : |r + 1| * ‖y‖ = ‖y‖
hr0 : 0 ≤ r
hr : (r + 1) • y = x
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
abs_of_pos (Left.add_pos_of_nonneg_of_pos hr0 one_pos),

Goal state after:
case neg.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hn : ¬x = y
hy : y ≠ 0
r : ℝ
h : (r + 1) * ‖y‖ = ‖y‖
hr0 : 0 ≤ r
hr : (r + 1) • y = x
⊢ |(o.oangle (y - x) y).toReal| < π / 2
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

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
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
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign

Tactic:
have hf : ContinuousOn (fun p : P × P × P => ∡ p.1 p.2.1 p.2.2) s := by
      refine continuousOn_of_forall_continuousAt fun p hp => continuousAt_oangle ?_ ?_
      all_goals
        simp_rw [s, Set.mem_image, Set.mem_prod, Set.mem_univ, true_and, Prod.ext_iff] at hp
        obtain ⟨q₁, q₅, q₂⟩ := p
        dsimp only at hp ⊢
        obtain ⟨⟨⟨q, hq⟩, v⟩, hv, rfl, rfl, rfl⟩ := hp
        dsimp only [Subtype.coe_mk, Set.mem_ofPred] at hv ⊢
        obtain ⟨hvr, -⟩ := hv
        rintro rfl
        refine hc₅₁₂ ((collinear_insert_iff_of_mem_affineSpan ?_).2 (collinear_pair _ _ _))
      · exact hq
      · refine vadd_mem_of_mem_direction ?_ hq
        rw [← exists_nonneg_left_iff_sameRay (vsub_ne_zero.2 hp₁p₂.symm)] at hvr
        obtain ⟨r, -, rfl⟩ := hvr
        rw [direction_affineSpan]
        exact smul_vsub_rev_mem_vectorSpan_pair _ _ _

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
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
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: case inl.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
h : dist s.center s.center < s.radius
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius s.center) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬s.center = s.center ∨ Subsingleton V

pp: case inl.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
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔ Module.finrank ℝ V = 1 ∧ ¬p = s.center ∨ Subsingleton V

Tactic:
· rcases subsingleton_or_nontrivial V with hs | hs
      · have hs' := (AddTorsor.subsingleton_iff V P).1 hs
        simp [hs, Metric.sphere_eq_empty_of_subsingleton (dist_nonneg.trans_lt h).ne']
      · simp only [orthRadius_center, top_coe, Set.inter_univ, not_true_eq_false, and_false,
          not_subsingleton_iff_nontrivial.2 hs, or_self, iff_false, ← Set.nonempty_iff_ne_empty]
        obtain ⟨v, hv⟩ := exists_norm_eq V (dist_nonneg.trans_lt h).le
        exact ⟨v +ᵥ s.center, by simp [hv]⟩

Goal state after:
case inl.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
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔ Module.finrank ℝ V = 1 ∧ ¬p = s.center ∨ Subsingleton V
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf : ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ), ∃ c, c • ⟨v, hv⟩ = w
hvc : ∀ w ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ, ∃ c, c • v = w
hvp : 0 ≤ s.radius ^ 2 - dist p s.center ^ 2
p' : P
h' : p' -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
c : ℝ
h : ‖c • v‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
hc : c • v = p' -ᵥ p
⊢ c ^ 2 = √(s.radius ^ 2 - dist p s.center ^ 2) ^ 2

Tactic:
Real.sq_sqrt hvp

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf : ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ), ∃ c, c • ⟨v, hv⟩ = w
hvc : ∀ w ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ, ∃ c, c • v = w
hvp : 0 ≤ s.radius ^ 2 - dist p s.center ^ 2
p' : P
h' : p' -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
c : ℝ
h : ‖c • v‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
hc : c • v = p' -ᵥ p
⊢ c ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
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
p₁ p₂ p₃ : P
s : Sphere P
inst✝ : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this✝ : FiniteDimensional ℝ V
hne₁₃ : p₁ ≠ p₃
hd : (Sphere.ofDiameter p₁ p₃).IsDiameter p₁ p₃
hne : ¬s = Sphere.ofDiameter p₁ p₃
this : p₂ = p₁ ∨ p₂ = p₃
⊢ False

Tactic:
exact this.elim hne₁₂.symm hne₂₃

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

Goal state before:
pp: case refine_2
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
i : Fin (n + 1)
⊢ ∀ i_1 ∈ {k | k ≠ i},
    -(⟪s.points i -ᵥ s.altitudeFoot i, s.points i_1 -ᵥ s.altitudeFoot i_1⟫ / (s.height i * s.height i_1)) *
        (s.height i_1)⁻¹ <
      (s.height i_1)⁻¹

Tactic:
· rintro j hj
    refine mul_lt_of_lt_one_left ?_ ?_
    · simp [height_pos]
    · rw [neg_lt]
      exact neg_one_lt_inner_vsub_altitudeFoot_div _ _ _

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
inst✝ : n.AtLeastTwo
i : Fin (n + 1)
⊢ 0 < ∑ j, s.excenterWeightsUnnorm {i} j

Tactic:
by
  rw [← Finset.sum_add_sum_compl {i}, Finset.sum_singleton]
  nth_rw 1 [excenterWeightsUnnorm]
  simp only [Finset.mem_singleton, ↓reduceIte, neg_mul, one_mul, lt_neg_add_iff_add_lt, add_zero]
  convert! s.inv_height_lt_sum_inv_height i using 2 with j h
  · ext j
    simp
  · rw [Finset.mem_filter_univ] at h
    simp [excenterWeightsUnnorm, h]

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))
⊢ s.exsphere signsᶜ = s.exsphere signs

Tactic:
by
  simp [exsphere, excenterWeights_compl, excenterWeightsUnnorm_compl, Pi.neg_apply]

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

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
a b c p : P
h : ∠ b p c = π
⊢ (dist a p * dist a p + dist b p * dist b p - 2 * dist a p * dist b p * Real.cos (∠ a p b)) * dist c p +
      dist a c * dist a c * dist b p =
    dist b c * (dist a p ^ 2 + dist b p * dist c p)

Tactic:
law_cos a p c,

Goal state after:
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
h : ∠ b p c = π
⊢ (dist a p * dist a p + dist b p * dist b p - 2 * dist a p * dist b p * Real.cos (∠ a p b)) * dist c p +
      (dist a p * dist a p + dist c p * dist c p - 2 * dist a p * dist c p * Real.cos (∠ a p c)) * dist b p =
    dist b c * (dist a p ^ 2 + dist b p * dist c p)
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
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
r : ℝ
h : ∀ (i : Fin (n + 1)), |(s.signedInfDist i) p| = r
h' : ∀ (i : Fin (n + 1)), (s.signedInfDist i) p = r ∨ (s.signedInfDist i) p = -r
⊢ ∃ signs, s.ExcenterExists signs ∧ p = s.excenter signs

Tactic:
refine ⟨{i ∈ (Finset.univ : Finset (Fin (n + 1))) | s.signedInfDist i p = -r}, ?_⟩

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
r : ℝ
h : ∀ (i : Fin (n + 1)), |(s.signedInfDist i) p| = r
h' : ∀ (i : Fin (n + 1)), (s.signedInfDist i) p = r ∨ (s.signedInfDist i) p = -r
⊢ s.ExcenterExists {i | (s.signedInfDist i) p = -r} ∧ p = s.excenter {i | (s.signedInfDist i) p = -r}
Module: Mathlib.Geometry.Euclidean.Inversion.Calculus

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
a : E
hc : DifferentiableAt ℝ c a
hR : DifferentiableAt ℝ R a
hx : DifferentiableAt ℝ x a
hne : x a ≠ c a
⊢ DifferentiableAt ℝ (fun a ↦ inversion (c a) (R a) (x a)) a

Tactic:
← differentiableWithinAt_univ

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
a : E
hc : DifferentiableWithinAt ℝ c univ a
hR : DifferentiableWithinAt ℝ R univ a
hx : DifferentiableWithinAt ℝ x univ a
hne : x a ≠ c a
⊢ DifferentiableWithinAt ℝ (fun a ↦ inversion (c a) (R a) (x a)) univ a
Module: Mathlib.Geometry.Euclidean.Inversion.Calculus

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x ↦ c + x) x ≠ c
A : HasFDerivAt (fun x ↦ _root_.id x - c) (ContinuousLinearMap.id ℝ F) (c + x)
⊢ ‖_root_.id (c + x) - c‖ ^ 2 ≠ 0

Tactic:
by simpa using hx

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case «0»
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] ((fun i ↦ i) ⟨0, ⋯⟩) = (![a, b, c] ∘ ⇑(Equiv.swap 0 1)) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case «1»
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] ((fun i ↦ i) ⟨1, ⋯⟩) = (![a, b, c] ∘ ⇑(Equiv.swap 0 1)) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case «2»
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] ((fun i ↦ i) ⟨2, ⋯⟩) = (![a, b, c] ∘ ⇑(Equiv.swap 0 1)) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case «0»
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'] ((fun i ↦ i) ⟨0, ⋯⟩) = (![a', b', c'] ∘ ⇑(Equiv.swap 0 1)) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case «1»
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'] ((fun i ↦ i) ⟨1, ⋯⟩) = (![a', b', c'] ∘ ⇑(Equiv.swap 0 1)) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case «2»
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'] ((fun i ↦ i) ⟨2, ⋯⟩) = (![a', b', c'] ∘ ⇑(Equiv.swap 0 1)) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case «0»
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] ((fun i ↦ i) ⟨0, ⋯⟩) = (![a, b, c] ∘ ⇑(Equiv.swap 1 2)) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case «1»
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] ((fun i ↦ i) ⟨1, ⋯⟩) = (![a, b, c] ∘ ⇑(Equiv.swap 1 2)) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case «2»
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] ((fun i ↦ i) ⟨2, ⋯⟩) = (![a, b, c] ∘ ⇑(Equiv.swap 1 2)) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case «0»
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'] ((fun i ↦ i) ⟨0, ⋯⟩) = (![a', b', c'] ∘ ⇑(Equiv.swap 1 2)) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case «1»
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'] ((fun i ↦ i) ⟨1, ⋯⟩) = (![a', b', c'] ∘ ⇑(Equiv.swap 1 2)) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case «2»
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'] ((fun i ↦ i) ⟨2, ⋯⟩) = (![a', b', c'] ∘ ⇑(Equiv.swap 1 2)) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne]

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

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
he : s.Equilateral
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) = π / 3

Tactic:
rcases he with ⟨r, 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 : ℕ
s : Simplex ℝ P n
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) = π / 3
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 ∈ (Submodule.span ℝ (⋃ i, {s.points i₁ -ᵥ s.points ↑i}))ᗮ
x : V
⊢ x ∈ ⋃ i, {s.points i₁ -ᵥ s.points ↑i} ↔ x ∈ (fun x ↦ s.points i₁ -ᵥ s.points x) '' (Set.univ \ {i₁})

Tactic:
simp_rw [Set.mem_iUnion, Set.mem_image, Set.mem_singleton_iff, Set.mem_sdiff_singleton]

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}))ᗮ
x : V
⊢ (∃ i, x = s.points i₁ -ᵥ s.points ↑i) ↔ ∃ x_1, (x_1 ∈ Set.univ ∧ x_1 ≠ i₁) ∧ s.points i₁ -ᵥ s.points x_1 = x
Module: Mathlib.Geometry.Group.Growth.LinearLowerBound

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ ↑X ^ (n - m) * ↑X ^ (m - 1) = ↑(closure ↑X)

Tactic:
rw [hm, Set.pow_mul_subgroupClosure hX.nonempty.to_set]

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

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
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₂ : Fin 3
h₂ : t.points j₂ = p i₂
j₃ : Fin 3
h₃ : t.points j₃ = p i₃
⊢ ∃ 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₃

Tactic:
have hj₂₃ : j₂ ≠ j₃ := by
      intro he
      rw [he, h₃] at h₂
      exact h₂₃.symm (hpi h₂)

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
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₂ : Fin 3
h₂ : t.points j₂ = p i₂
j₃ : Fin 3
h₃ : t.points j₃ = p i₃
hj₂₃ : j₂ ≠ j₃
⊢ ∃ 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₃
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
inst✝ : BoundarylessManifold I M
⊢ ModelWithCorners.boundary M = ∅

Tactic:
← I.compl_interior,

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
inst✝ : BoundarylessManifold I M
⊢ (ModelWithCorners.interior M)ᶜ = ∅
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
s : Set P
t t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
i₁ i₂ i₃ j₂ j₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : t.points i₁ = t₀.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t₀.points j₂ = t.points i₂
h₃ : t₀.points j₃ = t.points i₃
j₁ : Fin 3
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₁₂₃ : ∀ (j : Fin 3), j = j₁ ∨ j = j₂ ∨ j = j₃
h : t₀.points j₁ = t.orthocenter
x : Fin 3
⊢ x ∈ Set.univ ↔ x ∈ {i₁, i₂, i₃}

Tactic:
simpa using h₁₂₃ x

Goal state after: