cancellation with oangles

Stream: new members

[Riley Riles]

Hi! I have an MWE of

import Mathlib.Geometry.Euclidean.Angle.Sphere
import Mathlib.Geometry.Euclidean.Sphere.SecondInter
import Mathlib.Geometry.Euclidean.Circumcenter

open Affine Affine.Simplex EuclideanGeometry FiniteDimensional Module

open scoped Affine EuclideanGeometry Real

variable (V : Type*) (Pt : Type*)

variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt]

variable [NormedAddTorsor V Pt]

variable [hd2 : Fact (finrank ℝ V = 2)]
variable [Module.Oriented ℝ V (Fin 2)]

variable (C S B K : Pt)

theorem test : ↑π + 2 • ∡ C S K = 2 • ∡ C S B + ↑π → ∡ C S K =  ∡ C S B := by {
  intros calceq
  have calc1 : 2 • ∡ C S B + ↑π = ↑ π + 2 • ∡ C S B := by exact Eq.symm (AddCommMagma.add_comm (↑π) (2 • ∡ C S B))
  rewrite [calc1] at calceq
}

and I am trying to arrive at ∡ C S K = ∡ C S B. I cannot, however, figure out how to cancel the pi angles at the sides, and I'm not sure if I even can cancel the multiplication by two. Is there a place I can look to see what I can do to manipulate oangles? The site https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.html#Real.Angle.toReal does not appear to have any lemmas related to addition or multiplication.

[Aaron Liu]

docs#add_right_inj

[Aaron Liu]

The multiplication by two is not cancellable, because 2 • π = 2 • 0.

[Riley Riles]

I'm not entirely sure how to apply add_right_inj; how do I tell the function what the values of b and c are if the values of b and c are implicit?

Also, if I have that both angles are between 0 and pi, would that allow me to cancel them?

[Aaron Liu]

You can do rw [add_right_inj] at calceq.

[Aaron Liu]

Riley Riles said:

Also, if I have that both angles are between 0 and pi, would that allow me to cancel them?

What do you mean by this?

[Riley Riles]

In the wider context of the problem, I know that both the angles in question are between 0 and pi (they're angles in a triangle). Is there a way to add in an assumption to represent that (which would allow me to cancel the multiplication by two)?

[Aaron Liu]

Which angles do you know are between 0 and pi?

[Riley Riles]

∡ C S K and ∡ C S B.

[Matt Diamond]

I'm a bit confused by the original question... you're one line away from solving the theorem with exact calceq

[Riley Riles]

Matt Diamond said:

I'm a bit confused by the original question... you're one line away from solving the theorem with exact calceq

My bad, the correct desired end result was ∡ C S K = ∡ C S B. (I was a little hasty when making the MWE.)

[Matt Diamond]

oh okay, gotcha

[Aaron Liu]

I found docs#Real.Angle.two_nsmul_eq_iff

[Aaron Liu]

You should be able to combine this with a bound on the angles to get that they're equal.

[Riley Riles]

Thanks, that works great! Quick question, how do you find theorems like this which do not have a natural language description? Moogle does not seem to bring this up, and directly searching the documentation does not help either.

[Aaron Liu]

I used @loogle Real.Angle, 2 • _

[loogle]

:search: Real.Angle.two_zsmul_coe_pi, Real.Angle.two_zsmul_coe_div_two, and 65 more

[Aaron Liu]

It was very far down in the results

[Matt Diamond]

yeah, Loogle can be pretty useful

[Riley Riles]

Oh, thanks! This looks a lot like Search from Coq; I can't believe I didn't know about this!

[Joseph Myers]

Depending on the orientation of the triangle, all the angles could be negative. What you do know is that they have the same sign (oangle_rotate_sign). You should be able to combine that with two_nsmul_eq_iff or two_zsmul_eq_iff, and sign_add_pi (together with the signs not being 0) to get what you want. (Probably we should have lemmas saying that angles with nonzero sign are equal if twice those angles are equal and their signs are equal.)

[Joseph Myers]

(If you want equality where the angles aren't all in the same triangle, you may need to find another lemma to show signs are equal.)