mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
e f g : PerfectClosure K p
x✝² : ℕ × K
m : ℕ
x : K
x✝¹ : ℕ × K
n : ℕ
y : K
x✝ : ℕ × K
s : ℕ
z : K
⊢ (((m, x).1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] (m, x).2 + (⇑(frobenius K p))^[(m, x).1] (n, y).2).1 + (s, z).1,
      (⇑(frobenius K p))^[(s, z).1]
          ((m, x).1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] (m, x).2 + (⇑(frobenius K p))^[(m, x).1] (n, y).2).2 +
        (⇑(frobenius K
                p))^[((m, x).1 + (n, y).1,
                (⇑(frobenius K p))^[(n, y).1] (m, x).2 + (⇑(frobenius K p))^[(m, x).1] (n, y).2).1]
          (s, z).2) =
    ((m, x).1 +
        ((n, y).1 + (s, z).1, (⇑(frobenius K p))^[(s, z).1] (n, y).2 + (⇑(frobenius K p))^[(n, y).1] (s, z).2).1,
      (⇑(frobenius K
                p))^[((n, y).1 + (s, z).1,
                (⇑(frobenius K p))^[(s, z).1] (n, y).2 + (⇑(frobenius K p))^[(n, y).1] (s, z).2).1]
          (m, x).2 +
        (⇑(frobenius K p))^[(m, x).1]
          ((n, y).1 + (s, z).1, (⇑(frobenius K p))^[(s, z).1] (n, y).2 + (⇑(frobenius K p))^[(n, y).1] (s, z).2).2)

Tactic:
simp only [iterate_map_add, ← iterate_add_apply, add_assoc, add_comm s _]

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ ∃ z_1, (⇑(frobenius K p))^[z.1 + z_1] x.2 = (⇑(frobenius K p))^[x.1 + z_1] z.2

Tactic:
exists z2 + (y.1 + z1)

Goal state after:
case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ (⇑(frobenius K p))^[z.1 + (z2 + (y.1 + z1))] x.2 = (⇑(frobenius K p))^[x.1 + (z2 + (y.1 + z1))] z.2
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
D H : Subgroup G
inst✝ : D.FiniteIndex
hD_le_H : D ≤ H
t : Set ↥H
ht : IsComplement t ↑(D.subgroupOf H) ∧ 1 ∈ t
hf : t.Finite
x : G
⊢ x ∈ H → ∃ y ∈ t, ∃ d ∈ D, ↑y * d = x

Tactic:
intro hx
    exact ⟨_, (ht.1.toLeftFun ⟨x, hx⟩).2, _,
      ht.1.inv_toLeftFun_mul_mem ⟨x, hx⟩, mul_inv_cancel_left _ _⟩

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝ : Flat R ↥A
ι : Type u_1
b : ι → ↥B
hb : LinearIndependent R b
h : ((toSubmodule A).mulRightMap b).ker = ⊥
⊢ LinearIndependent (↥A) (⇑B.val ∘ b)

Tactic:
mulRightMap_ker_eq_bot_iff_linearIndependent

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝ : Flat R ↥A
ι : Type u_1
b : ι → ↥B
hb : LinearIndependent R b
h : LinearIndependent (↥A) (⇑B.val ∘ b)
⊢ LinearIndependent (↥A) (⇑B.val ∘ b)
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : Basis ι R ↥B
H : LinearIndependent (↥A) (⇑B.val ∘ ⇑b)
⊢ A.LinearDisjoint B

Tactic:
rw [← mulRightMap_ker_eq_bot_iff_linearIndependent] at H
  exact Submodule.LinearDisjoint.of_basis_right _ _ b H

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
c : ConjRootClass K L
⊢ c.minpoly.Separable

Tactic:
induction c
  exact Algebra.IsSeparable.isSeparable K _

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this✝³ : Field (A ⊗[R] B) := H.toField
a : A
hta : Transcendental R a
b : B
htb : Transcendental R b
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
this✝² : IsDomain A
this✝¹ : IsDomain B
this✝ : IsDomain R
this : Flat R ↥(toSubmodule fa.range)
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
⊢ False

Tactic:
replace hta : Function.Injective ga := transcendental_iff_injective.1 hta

Goal state after:
R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this✝³ : Field (A ⊗[R] B) := H.toField
a : A
b : B
htb : Transcendental R b
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
this✝² : IsDomain A
this✝¹ : IsDomain B
this✝ : IsDomain R
this : Flat R ↥(toSubmodule fa.range)
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective ⇑ga
⊢ False
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
inst✝¹ : FiniteDimensional F ↥A
inst✝ : FiniteDimensional F ↥B
H : finrank F ↥(A ⊔ B) = finrank F ↥A * finrank F ↥B
⊢ finrank F ↥(A.toSubalgebra ⊔ B.toSubalgebra) = finrank F ↥A.toSubalgebra * finrank F ↥B.toSubalgebra

Tactic:
by rwa [← sup_toSubalgebra_of_left]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ ⊤ ≤ IntermediateField.adjoin K (↑E ∪ {X})

Tactic:
exact le_trans (le_of_eq RatFunc.adjoin_X.symm) (adjoin.mono _ _ _ (by simp))

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

Goal state before:
pp: F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
S : IntermediateField F K
inst✝¹ : Algebra.IsAlgebraic F ↥S
inst✝ : IsPurelyInseparable F E
⊢ sepDegree E ↥(adjoin E ↑S) = sepDegree F ↥S

Tactic:
have : Algebra.IsAlgebraic F (adjoin F (S : Set K)) := by rwa [adjoin_self]

Goal state after:
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
S : IntermediateField F K
inst✝¹ : Algebra.IsAlgebraic F ↥S
inst✝ : IsPurelyInseparable F E
this : Algebra.IsAlgebraic F ↥(adjoin F ↑S)
⊢ sepDegree E ↥(adjoin E ↑S) = sepDegree F ↥S
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B : Subfield E
⊢ A.relrank B = 1 ↔ B ≤ A

Tactic:
relrank_eq_one_iff

Goal state after:
E : Type v
inst✝ : Field E
A B : Subfield E
⊢ B ≤ A ↔ B ≤ A
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B : Subfield E
⊢ A.relfinrank B = 1 ↔ B ≤ A

Tactic:
rw [relfinrank_eq_toNat_relrank, toNat_eq_one, relrank_eq_one_iff]

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
⊢ Module.rank ↥A ↥(extendScalars h1) * B.relrank C = A.relrank C

Tactic:
relrank_eq_rank_of_le h2,

Goal state after:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = A.relrank C
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B C : Subfield E
⊢ A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C

Tactic:
by
  rw [← inf_relrank_right A (B ⊓ C), ← inf_relrank_right B C, ← inf_relrank_right (A ⊓ B) C,
    inf_assoc, relrank_mul_relrank inf_le_right inf_le_right]

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ F₁ : PointedCone R M
C₂ F₂ : PointedCone R N
hF₁ : F₁.IsFaceOf C₁
hF₂ : F₂.IsFaceOf C₂
a✝² : M
b✝¹ : N
a✝¹ : M
b✝ : N
a✝ : R
xc₁ : a✝² ∈ C₁
xc₂ : b✝¹ ∈ C₂
yc₁ : a✝¹ ∈ C₁
yc₂ : b✝ ∈ C₂
a0 : 0 < a✝
⊢ a✝ • a✝² + a✝¹ ∈ F₁ → a✝ • b✝¹ + b✝ ∈ F₂ → a✝² ∈ F₁ ∧ b✝¹ ∈ F₂

Tactic:
hab₁

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ F₁ : PointedCone R M
C₂ F₂ : PointedCone R N
hF₁ : F₁.IsFaceOf C₁
hF₂ : F₂.IsFaceOf C₂
a✝² : M
b✝¹ : N
a✝¹ : M
b✝ : N
a✝ : R
xc₁ : a✝² ∈ C₁
xc₂ : b✝¹ ∈ C₂
yc₁ : a✝¹ ∈ C₁
yc₂ : b✝ ∈ C₂
a0 : 0 < a✝
hab₁ : a✝ • a✝² + a✝¹ ∈ F₁
⊢ a✝ • b✝¹ + b✝ ∈ F₂ → a✝² ∈ F₁ ∧ b✝¹ ∈ F₂
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (Q₂ h).natDegree = 0

Tactic:
by
  -- We have f(X)*g(Y) - g(X)*f(Y) = Q₂(X) * Φ
  -- Assume Q₂ has positive degree, take a root in an algebraic extension
  by_contra H
  apply (generator E).eq_C_iff.not.mp (generator_ne_C h)
  let F := AlgebraicClosure K
  rw [natDegree_eq_zero_iff_degree_le_zero.not, ← degree_map _ (algebraMap K F)] at H
  obtain ⟨α, hα⟩ := IsAlgClosed.exists_root ((Q₂ h).map (algebraMap K F)) (ne_of_not_ge H).symm
  -- Evaluate at the root, get that f(α)*g(Y) = g(α)*f(Y)
  rw [IsRoot.def, eval_map_algebraMap] at hα
  have eq :
      (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
      (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E)) := by
    have := congr(aeval (Polynomial.C α) $(Q₂_mul_Φ h)).symm
    rwa [aeval_mul, ← map_aeval_eq_aeval_map (by ext; simp), hα, map_zero, zero_mul, aeval_sub,
      aeval_mul, aeval_mul, aeval_C, aeval_C, ← map_aeval_eq_aeval_map (by ext; simp),
      ← map_aeval_eq_aeval_map (by ext; simp), algebraMap_def, coe_mapRingHom, sub_eq_zero,
      ← Polynomial.coe_mapRingHom] at this
  obtain ⟨isUnit₁, isUnit₂⟩ :
      IsUnit (Polynomial.C <| aeval α (f E)) ∧ IsUnit (Polynomial.C <| aeval α (g E)) := by
    rw [Polynomial.isUnit_C, isUnit_iff_ne_zero, Polynomial.isUnit_C, isUnit_iff_ne_zero]
    obtain (H | H) := aeval_ne_zero_of_isCoprime (generator E).isCoprime_num_denom α
    · refine ⟨H, Polynomial.C_injective.ne_iff.mp ?_⟩
      rw [map_zero, ← mul_ne_zero_iff_left <| Polynomial.map_ne_zero <|
        num_ne_zero (generator_ne_zero h)]
      exact eq ▸ mul_ne_zero (Polynomial.map_ne_zero (generator E).denom_ne_zero) <|
        Polynomial.C_ne_zero.mpr H
    · refine ⟨Polynomial.C_injective.ne_iff.mp ?_, H⟩
      rw [map_zero, ← mul_ne_zero_iff_left <| Polynomial.map_ne_zero (generator E).denom_ne_zero]
      exact eq ▸ mul_ne_zero (Polynomial.map_ne_zero (num_ne_zero (generator_ne_zero h))) <|
        Polynomial.C_ne_zero.mpr H
  -- obtain contradiction because f and g are coprime
  have isCoprime := IsCoprime.map (generator E).isCoprime_num_denom <|
    Polynomial.mapRingHom (algebraMap K F)
  have : Associated ((f E).mapRingHom (algebraMap K F)) ((g E).mapRingHom (algebraMap K F)) := by
    rw [← associated_mul_isUnit_left_iff isUnit₂, Associated.comm]
    exact ⟨isUnit₁.unit, by simpa⟩
  have := isCoprime.isUnit_of_associated this
  exact ⟨by simpa using (natDegree_eq_zero_of_isUnit this.1),
    by simpa using (natDegree_eq_zero_of_isUnit this.2)⟩

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p x : P
hx : x ∈ s
⊢ ↑(s.direction.orthogonalProjectionOnto (p -ᵥ ↑(Classical.arbitrary ↥s)) +ᵥ Classical.arbitrary ↥s) =
    ↑(s.direction.orthogonalProjectionOnto (p -ᵥ x)) +ᵥ x

Tactic:
coe_vadd,

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p x : P
hx : x ∈ s
⊢ ↑(s.direction.orthogonalProjectionOnto (p -ᵥ ↑(Classical.arbitrary ↥s))) +ᵥ ↑(Classical.arbitrary ↥s) =
    ↑(s.direction.orthogonalProjectionOnto (p -ᵥ x)) +ᵥ x
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ ↑(s.direction.orthogonalProjectionOnto (p -ᵥ ↑(Classical.arbitrary ↥s)) +ᵥ Classical.arbitrary ↥s) -ᵥ p ∈ s.directionᗮ

Tactic:
coe_vadd,

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ (↑(s.direction.orthogonalProjectionOnto (p -ᵥ ↑(Classical.arbitrary ↥s))) +ᵥ ↑(Classical.arbitrary ↥s)) -ᵥ p ∈
    s.directionᗮ
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
⊢ (o.rotation (o.oangle x y)) x = y

Tactic:
o.eq_iff_oangle_eq_zero_of_norm_eq

Goal state after:
case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
⊢ o.oangle ((o.rotation (o.oangle x y)) x) y = 0

case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
⊢ ‖(o.rotation (o.oangle x y)) x‖ = ‖y‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
⊢ ∠ p₁ p₃ p₂ + ∠ p₁ p₃ p₄ = π

Tactic:
angle_comm p₁ p₃ p₂,

Goal state after:
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₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
⊢ ∠ p₂ p₃ p₁ + ∠ p₁ p₃ p₄ = π
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x : V
⊢ f ((o.rotation θ) x) = ↑θ.toCircle * f x

Tactic:
← Complex.rotation,

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
f : V ≃ₗᵢ[ℝ] ℂ
hf : (map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x : V
⊢ f ((o.rotation θ) x) = (Complex.orientation.rotation θ) (f x)
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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle x y + o.oangle y z = o.oangle x z

Tactic:
o.oangle_add hx hy hz

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle x z = o.oangle x z
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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle x z = o.oangle x y + o.oangle y z

Tactic:
o.oangle_add hx hy hz

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle x z = o.oangle x z
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h0 : 0 ≤ InnerProductGeometry.angle x y
hpi : InnerProductGeometry.angle x y ≤ π
h : o.oangle x y = ↑(InnerProductGeometry.angle x y)
⊢ InnerProductGeometry.angle x y = |(o.oangle x y).toReal|

Tactic:
rw [h, eq_comm, Real.Angle.abs_toReal_coe_eq_self_iff]

Goal state after:
case inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h0 : 0 ≤ InnerProductGeometry.angle x y
hpi : InnerProductGeometry.angle x y ≤ π
h : o.oangle x y = ↑(InnerProductGeometry.angle x y)
⊢ 0 ≤ InnerProductGeometry.angle x y ∧ InnerProductGeometry.angle x y ≤ π
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case mp.inr.refine_1
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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
⊢ p₃ ≠ p₂

Tactic:
rw [← @vsub_ne_zero V, hp₃p₂, smul_ne_zero_iff]
        exact ⟨hr0.ne.symm, hp₁p₂⟩

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
hp₁p₂ : ¬p₁ = p₂
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁

Tactic:
by_cases hp₁p₃ : p₁ = p₃

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
p₁ p₂ p₃ : P
hp₁p₂ : ¬p₁ = p₂
hp₁p₃ : p₁ = p₃
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁

case neg
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
hp₁p₂ : ¬p₁ = p₂
hp₁p₃ : ¬p₁ = p₃
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

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
p₁ p₂ p₃ : P
h : p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
⊢ Collinear ℝ {p₁, p₂, p₃}

Tactic:
rcases h with (rfl | rfl | h | h)

Goal state after:
case refine_2.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₃ : P
⊢ Collinear ℝ {p₁, p₁, p₃}

case refine_2.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₃ : P
⊢ Collinear ℝ {p₁, p₃, p₃}

case refine_2.inr.inr.inl
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
h : ∠ p₁ p₂ p₃ = 0
⊢ Collinear ℝ {p₁, p₂, p₃}

case refine_2.inr.inr.inr
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
h : ∠ p₁ p₂ p₃ = π
⊢ Collinear ℝ {p₁, p₂, p₃}
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
h : dist p₁ p₂ = dist p₁ p₃
⊢ ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁

Tactic:
simp_rw [dist_eq_norm_vsub V] at h
  rw [oangle, oangle, ← vsub_sub_vsub_cancel_left p₃ p₂ p₁, ← vsub_sub_vsub_cancel_left p₂ p₃ p₁,
    o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

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
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)

Tactic:
by
  rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
    inner_neg_left, neg_vsub_eq_vsub_rev] at h
  rw [← @vsub_ne_zero V, @ne_comm _ p₃, ← @vsub_ne_zero V _ _ _ p₂, or_comm] at h0
  rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
    add_comm, angle_add_eq_arcsin_of_inner_eq_zero h h0]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

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
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) = Real.arctan (‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃‖)

Tactic:
angle_add_eq_arctan_of_inner_eq_zero h h0

Goal state after:
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
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ Real.arctan (‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃‖) = Real.arctan (‖p₁ -ᵥ p₂‖ / ‖p₂ -ᵥ p₃‖)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆
h1 : p₂ ≠ p₁
h2 : p₂ ≠ p₃
h3 : p₅ ≠ p₄
h4 : p₅ ≠ p₆
h₁ : ∡ p₁ p₂ p₃ = ↑(∠ p₁ p₂ p₃)
h₂ : ∡ p₄ p₅ p₆ = -↑(∠ p₄ p₅ p₆)
⊢ ∡ p₁ p₂ p₃ = ∡ p₄ p₅ p₆ ∨ ∡ p₁ p₂ p₃ = -∡ p₄ p₅ p₆

Tactic:
right
    rw [h₁, h₂, h, neg_neg]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

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
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ < π / 2

Tactic:
by
  rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
    inner_neg_left, neg_vsub_eq_vsub_rev] at h
  rw [ne_comm, ← @vsub_ne_zero V] at h0
  rw [angle, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm]
  exact angle_add_lt_pi_div_two_of_inner_eq_zero h h0

Goal state after: