mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Algebraic.LinearIndependent

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j) = 0
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
⊢ ∑ x_1 ∈ s, (aeval x) (C (m x_1)) * ∏ x_2 ∈ s.erase x_1, (x - (aeval x) (C x_2)) =
    ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j)

Tactic:
aeval_C,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j) = 0
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
⊢ ∑ x_1 ∈ s, (algebraMap F E) (m x_1) * ∏ x_2 ∈ s.erase x_1, (x - (algebraMap F E) x_2) =
    ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j)
Module: Mathlib.RingTheory.Algebraic.LinearIndependent

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
hm : ∑ x ∈ s, (aeval i) (C (m x)) * ∏ x ∈ s.erase x, (i - (aeval i) (C x)) = 0
⊢ m i = 0

Tactic:
aeval_C,

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
hm : ∑ x ∈ s, (algebraMap F F) (m x) * ∏ x ∈ s.erase x, (i - (algebraMap F F) x) = 0
⊢ m i = 0
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
η : ↥(rootsOfUnity n K)
this : ↑↑η ^ n = 1
⊢ (aeval (↑↑η • root (X ^ n - C a))) X ^ n - (aeval (↑↑η • root (X ^ n - C a))) (C a) = 0

Tactic:
aeval_C,

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
η : ↥(rootsOfUnity n K)
this : ↑↑η ^ n = 1
⊢ (aeval (↑↑η • root (X ^ n - C a))) X ^ n - (algebraMap K K[n√a]) a = 0
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
inst✝¹ : Free R ↥B
inst✝ : Module.Finite R ↥B
x : ↥B
⊢ ((Algebra.leftMulMatrix (H.basisOfBasisRight H' (Free.chooseBasis R ↥B))) ((algebraMap (↥B) S) x)).trace =
    (algebraMap R ↥A) ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B)) x).trace

Tactic:
Matrix.trace,

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
inst✝¹ : Free R ↥B
inst✝ : Module.Finite R ↥B
x : ↥B
⊢ ∑ i, ((Algebra.leftMulMatrix (H.basisOfBasisRight H' (Free.chooseBasis R ↥B))) ((algebraMap (↥B) S) x)).diag i =
    (algebraMap R ↥A) (∑ i, ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B)) x).diag i)
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✝² : IsGalois F ↥A
inst✝¹ : FiniteDimensional F ↥A
inst✝ : FiniteDimensional F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
hA : IntermediateField.map C.val A' = A
⊢ A.LinearDisjoint ↥B

Tactic:
have hB : IntermediateField.map C.val B' = B := lift_restrict le_sup_right

Goal state after:
F : Type u
E : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E
inst✝³ : Algebra F E
A B : IntermediateField F E
inst✝² : IsGalois F ↥A
inst✝¹ : FiniteDimensional F ↥A
inst✝ : FiniteDimensional F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
hA : IntermediateField.map C.val A' = A
hB : IntermediateField.map C.val B' = B
⊢ A.LinearDisjoint ↥B
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
this : (aeval a) (X ^ ringExpChar K ^ elemExponent K a) - (aeval a) (C (elemReduct K a)) = 0
⊢ (algebraMap K L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a

Tactic:
aeval_C,

Goal state after:
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
this : (aeval a) (X ^ ringExpChar K ^ elemExponent K a) - (algebraMap K L) (elemReduct K a) = 0
⊢ (algebraMap K L) (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
n : ℕ
h : a ^ ringExpChar K ^ n ∈ (algebraMap K L).range
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
y : K
hy : (algebraMap K L) y = a ^ ringExpChar K ^ n
f : K[X] := X ^ ringExpChar K ^ n - C y
⊢ (aeval a) (X ^ ringExpChar K ^ n) - (aeval a) (C y) = 0

Tactic:
aeval_C,

Goal state after:
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
n : ℕ
h : a ^ ringExpChar K ^ n ∈ (algebraMap K L).range
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
y : K
hy : (algebraMap K L) y = a ^ ringExpChar K ^ n
f : K[X] := X ^ ringExpChar K ^ n - C y
⊢ (aeval a) (X ^ ringExpChar K ^ n) - (algebraMap K L) y = 0
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: case neg
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (finrank R ↥A).Coprime (finrank R ↥B)
a✝ : Nontrivial R
h1 : ¬finrank R ↥A = 0
h2 : ¬finrank R ↥B = 0
this✝¹ : Module.Finite R ↥A
this✝ : Module.Finite R ↥B
this : Module.Finite R ↥(A ⊔ B)
⊢ A.LinearDisjoint B

Tactic:
have : Module.finrank R A ≤ Module.finrank R ↥(A ⊔ B) :=
    LinearMap.finrank_le_finrank_of_injective <|
      Submodule.inclusion_injective (show toSubmodule A ≤ toSubmodule (A ⊔ B) by simp)

Goal state after:
case neg
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (finrank R ↥A).Coprime (finrank R ↥B)
a✝ : Nontrivial R
h1 : ¬finrank R ↥A = 0
h2 : ¬finrank R ↥B = 0
this✝² : Module.Finite R ↥A
this✝¹ : Module.Finite R ↥B
this✝ : Module.Finite R ↥(A ⊔ B)
this : finrank R ↥A ≤ finrank R ↥(A ⊔ B)
⊢ A.LinearDisjoint B
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
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i✝ : ι
f : ι → ℕ
hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∉ l.support
⊢ (algebraMap F E) 0 = l i ^ q ^ n

Tactic:
rw [map_zero, Finsupp.notMem_support_iff.1 hs, zero_pow this]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ (x / y).intDegree = x.intDegree - y.intDegree

Tactic:
rw [div_eq_mul_inv, intDegree_mul, intDegree_inv, ← sub_eq_add_neg]

Goal state after:
case hx
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ x ≠ 0

case hy
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ y⁻¹ ≠ 0
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
x : K
hsep : IsSeparable F x
inst✝ : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this✝¹ : Algebra.IsSeparable F ↥F⟮x⟯
this✝ : Algebra.IsSeparable E ↥E⟮x⟯
this : Algebra.IsAlgebraic F ↥F⟮x⟯
⊢ Cardinal.toNat (sepDegree F ↥F⟮x⟯) = Cardinal.toNat (sepDegree E ↥E⟮x⟯)

Tactic:
sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E

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
x : K
hsep : IsSeparable F x
inst✝ : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this✝¹ : Algebra.IsSeparable F ↥F⟮x⟯
this✝ : Algebra.IsSeparable E ↥E⟮x⟯
this : Algebra.IsAlgebraic F ↥F⟮x⟯
⊢ Cardinal.toNat (sepDegree F ↥F⟮x⟯) = Cardinal.toNat (sepDegree F ↥F⟮x⟯)
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
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
ha : Associated f (minpoly F x)
ha' : Associated (Polynomial.map (algebraMap F E) f) (Polynomial.map (algebraMap F E) (minpoly F x))
heq : Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x
⊢ Irreducible (minpoly E x)

Tactic:
exact minpoly.irreducible (Algebra.IsIntegral.isIntegral x)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
hF : F.IsFaceOf C
x y : M
hx : x ∈ C
hy : y ∈ C
hxy : x + y ∈ F
a✝ : Nontrivial R
⊢ x ∈ F

Tactic:
simpa [hxy] using hF.mem_of_smul_add_mem hx hy zero_lt_one

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
this :
  (aeval (Polynomial.C α)) (Polynomial.C (g E)) * (aeval (Polynomial.C α)) (Polynomial.map Polynomial.C (f E)) -
      (aeval (Polynomial.C α)) (Polynomial.C (f E)) * (aeval (Polynomial.C α)) (Polynomial.map Polynomial.C (g E)) =
    0
⊢ (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))

Tactic:
aeval_C,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
this :
  (algebraMap K[X] F[X]) (g E) * (aeval (Polynomial.C α)) (Polynomial.map Polynomial.C (f E)) -
      (aeval (Polynomial.C α)) (Polynomial.C (f E)) * (aeval (Polynomial.C α)) (Polynomial.map Polynomial.C (g E)) =
    0
⊢ (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
this :
  (algebraMap K[X] F[X]) (g E) * (aeval (Polynomial.C α)) (Polynomial.map Polynomial.C (f E)) -
      (aeval (Polynomial.C α)) (Polynomial.C (f E)) * (aeval (Polynomial.C α)) (Polynomial.map Polynomial.C (g E)) =
    0
⊢ (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))

Tactic:
aeval_C,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
this :
  (algebraMap K[X] F[X]) (g E) * (aeval (Polynomial.C α)) (Polynomial.map Polynomial.C (f E)) -
      (algebraMap K[X] F[X]) (f E) * (aeval (Polynomial.C α)) (Polynomial.map Polynomial.C (g E)) =
    0
⊢ (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))
Module: Mathlib.Geometry.Euclidean.Altitude

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 : Simplex ℝ P 1
i : Fin 2
⊢ s.height i = dist (s.points 0) (s.points 1)

Tactic:
fin_cases i
  · simp [height]
  · rw [dist_comm]
    simp [height]

Goal state after:
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
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : (AffineMap.lineMap p₁ p₃) 1 ≠ p₃
hp₂ : (AffineMap.lineMap p₁ p₃) 1 = p₂
hr0 : 0 ≤ 1
hr1 : 1 ≤ 1
hr0' : 1 ≠ 0
⊢ False

Tactic:
simp at hp₂p₃

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

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

Tactic:
refine Or.inr ⟨?_, r, ⟨hr0.le, hr1.le⟩, ?_⟩
      · rw [← @vsub_ne_zero V, hp₃p₂, smul_ne_zero_iff]
        exact ⟨hr0.ne.symm, hp₁p₂⟩
      · rw [AffineMap.lineMap_apply, ← hp₃p₂, vsub_vadd]

Goal state after:
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₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) = π - ∠ p₁ p₂ p₃

Tactic:
by_cases! h₃₂ : 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
h₃₂ : p₃ = p₂
⊢ ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) = π - ∠ 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
h₃₂ : p₃ ≠ p₂
⊢ ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) = π - ∠ p₁ p₂ p₃
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ o.oangle (x + y) y = ↑(Real.arcsin (‖x‖ / ‖x + y‖))

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
  rw [add_comm]
  exact (-o).oangle_add_right_eq_arcsin_of_oangle_eq_pi_div_two h

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ o.oangle x (x + y) = ↑(Real.arctan (‖y‖ / ‖x‖))

Tactic:
by
  have hs : (o.oangle x (x + y)).sign = 1 := by
    rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
  rw [o.oangle_eq_angle_of_sign_eq_one hs,
    InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h) (o.left_ne_zero_of_oangle_eq_pi_div_two h)]

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

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
ha : (-o).oangle x (r • (o.rotation ↑(π / 2)) x) = ↑(π / 2)
⊢ -↑(Real.arctan (‖r‖ * (‖x‖ / ‖x‖))) = ↑(Real.arctan r)

Tactic:
div_self (norm_ne_zero_iff.2 h),

Goal state after:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
ha : (-o).oangle x (r • (o.rotation ↑(π / 2)) x) = ↑(π / 2)
⊢ -↑(Real.arctan (‖r‖ * 1)) = ↑(Real.arctan r)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : 0 < r
ha : o.oangle x (r • (o.rotation ↑(π / 2)) x) = ↑(π / 2)
⊢ ↑(Real.arctan (‖r‖ * (‖x‖ / ‖x‖))) = ↑(Real.arctan r)

Tactic:
div_self (norm_ne_zero_iff.2 h),

Goal state after:
case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : 0 < r
ha : o.oangle x (r • (o.rotation ↑(π / 2)) x) = ↑(π / 2)
⊢ ↑(Real.arctan (‖r‖ * 1)) = ↑(Real.arctan r)
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
h : ‖x‖ = ‖y‖
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
by_cases hn : x = y

Goal state after:
case pos
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‖
hn : x = y
⊢ |(o.oangle (y - x) y).toReal| < π / 2

case neg
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‖
hn : ¬x = y
⊢ |(o.oangle (y - x) y).toReal| < π / 2
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
h : ‖x‖ = ‖y‖
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
by
  by_cases hn : x = y; · simp [hn, Real.pi_pos]
  have hs : ((2 : ℤ) • o.oangle (y - x) y).sign = (o.oangle (y - x) y).sign := by
    conv_rhs => rw [oangle_sign_sub_left_swap]
    rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hn h, Real.Angle.sign_pi_sub]
  rw [Real.Angle.sign_two_zsmul_eq_sign_iff] at hs
  rcases hs with (hs | hs)
  · rw [oangle_eq_pi_iff_oangle_rev_eq_pi, oangle_eq_pi_iff_sameRay_neg, neg_sub] at hs
    rcases hs with ⟨hy, -, hr⟩
    rw [← exists_nonneg_left_iff_sameRay hy] at hr
    rcases hr with ⟨r, hr0, hr⟩
    rw [eq_sub_iff_add_eq] at hr
    nth_rw 2 [← one_smul ℝ y] at hr
    rw [← add_smul] at hr
    rw [← hr, norm_smul, Real.norm_eq_abs, abs_of_pos (Left.add_pos_of_nonneg_of_pos hr0 one_pos),
      mul_left_eq_self₀, or_iff_left (norm_ne_zero_iff.2 hy), add_eq_right] at h
    rw [h, zero_add, one_smul] at hr
    exact False.elim (hn hr.symm)
  · exact hs

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

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_sbtw : Sbtw ℝ a b c
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c) t = b
ht0 : 0 < t
ht1 : t < 1
hb : b -ᵥ a = t • (c -ᵥ a)
⊢ ⟪p -ᵥ a, c -ᵥ a⟫ = 0

Tactic:
simpa [ht0.ne', hb, inner_smul_right] using h_inner

Goal state after:
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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
this : ((∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal) / 2 = (∡ p₁ p₂ p₄).toReal / 2
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₄ / 2

Tactic:
by
    rw [← ha, add_self_div_two] at this
    rw [angle_eq_abs_oangle_toReal h₁₂ h₃₂, angle_eq_abs_oangle_toReal h₁₂ h₄₂, this, abs_div]
    simp

Goal state after:
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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₄ / 2

Tactic:
by
  have h₃₂ : p₃ ≠ p₂ := by
    rintro rfl
    exact hs.left_notMem (right_mem_affineSpan_pair _ _ _)
  have h₄₂ : p₄ ≠ p₂ := by
    rintro rfl
    exact hs.right_notMem (right_mem_affineSpan_pair _ _ _)
  suffices ((∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal) / 2 = (∡ p₁ p₂ p₄).toReal / 2 by
    rw [← ha, add_self_div_two] at this
    rw [angle_eq_abs_oangle_toReal h₁₂ h₃₂, angle_eq_abs_oangle_toReal h₁₂ h₄₂, this, abs_div]
    simp
  have hadd := oangle_add h₁₂ h₃₂ h₄₂
  rw [div_left_inj' (by norm_num), ← hadd]
  have h : ∡ p₁ p₂ p₃ ≠ π := fun h ↦ hs.left_notMem ((oangle_eq_zero_or_eq_pi_iff_collinear.1
    (.inr h)).mem_affineSpan_of_mem_of_ne (by grind) (by grind) (by grind) h₁₂)
  refine (Real.Angle.toReal_add_eq_toReal_add_toReal h (ha ▸ h) (.inr ?_)).symm
  rw [hadd, ← oangle_swap₂₃_sign p₁ p₃ p₂, ← oangle_swap₂₃_sign p₁ p₄ p₂, neg_inj, eq_comm]
  exact hs.oangle_sign_eq (left_mem_affineSpan_pair _ _ _) (right_mem_affineSpan_pair _ _ _)

Goal state after: