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

Goal state before:
pp: case inj
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⋯
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ Function.Injective (HMul.hMul ((aeval x) (derivative (minpoly F x))))

Tactic:
apply mul_right_injective₀

Goal state after:
case inj
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⋯
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ (aeval x) (derivative (minpoly F x)) ≠ 0
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: case neg.inl
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 0
⊢ x = 0

pp: case neg.inr
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 1
⊢ x = 0

Tactic:
· by_cases hn : n = 0
    · rwa [hn, pow_zero, pow_one] at h
    rw [hp, zero_pow hn, pow_zero] at h
    subsingleton [subsingleton_of_zero_eq_one h.symm]

Goal state after:
case neg.inr
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
x : R
hp✝ : ¬1 < p
x✝ : ∃ n, x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 1
⊢ x = 0
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
a : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
⊢ mk K p ((m, x).1 + (0, 0).1, (⇑(frobenius K p))^[(0, 0).1] (m, x).2 * (⇑(frobenius K p))^[(m, x).1] (0, 0).2) =
    mk K p (0, 0)

Tactic:
simp only [iterate_zero, id_eq, iterate_map_zero, mul_zero, mk_zero_right]

Goal state after:
Module: Mathlib.FieldTheory.Laurent

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
r : R
inst✝ : IsDomain R
x✝¹ x✝ : R⟮X⟯
h : (laurent r) x✝¹ = (laurent r) x✝
⊢ x✝¹ = x✝

Tactic:
by
  simpa [laurent_laurent] using congr_arg (laurent (-r)) h

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x_1 ↦
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
y : G
⊢ ∃ i, ∃ (_ : i ∈ Finset.univ), y ∈ f i • ↑(K i)

Tactic:
by
      rw [← s.filter_union_filter_not_eq (H · = H j), Finset.set_biUnion_union] at hcovers
      cases (Set.mem_union _ _ _).mp (hcovers.superset (Set.mem_univ y)) with
      | inl hy =>
        have ⟨k, hk, hy⟩ := Set.mem_iUnion₂.mp hy
        have hk' : H k = H j := And.right <| by simpa using hk
        have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp (hx (g k) (hk' ▸ hy))
        exact ⟨⟨⟨i, hi⟩, some ⟨k, hk⟩⟩, Finset.mem_univ _, hy⟩
      | inr hy =>
        have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp hy
        exact ⟨⟨⟨i, hi⟩, none⟩, Finset.mem_univ _, hy⟩

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial

Goal state before:
pp: σ : Type u
K : Type v
inst✝¹ : CommRing K
inst✝ : Nontrivial K
⊢ lift.{max u v, u} #(σ →₀ ℕ) = lift.{max v u, u} #(σ →₀ ℕ)

Tactic:
lift_umax.{u, v}

Goal state after:
σ : Type u
K : Type v
inst✝¹ : CommRing K
inst✝ : Nontrivial K
⊢ lift.{v, u} #(σ →₀ ℕ) = lift.{v, u} #(σ →₀ ℕ)
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case refine_2
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
q : K [X]
hq : q.Monic
hq' : (aeval α) q = 0
⊢ finrank K L ≤ finrank K ↥⊤

Tactic:
exact (finrank_top K L).ge

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
hindex : (H i).index ≠ 0
⊢ 0 < ↑s.card

Tactic:
exact_mod_cast hs'

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : FiniteDimensional F K
a : K
⊢ normalizedTraceAux F K a = (↑(Module.finrank F K))⁻¹ • (trace F K) a

Tactic:
by
  have h := (Nat.cast_ne_zero (R := F)).mpr <|
    Nat.pos_iff_ne_zero.mp <| Module.finrank_pos (R := F⟮a⟯) (M := K)
  rw [smul_eq_mul, mul_comm, ← div_eq_mul_inv, trace_eq_trace_adjoin F a,
    ← Module.finrank_mul_finrank F F⟮a⟯ K, nsmul_eq_mul, Nat.cast_mul, mul_comm,
    mul_div_mul_right _ _ h, div_eq_mul_inv, mul_comm, ← smul_eq_mul, normalizedTraceAux_def]

Goal state after:
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 : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Cardinal.lift.{w, v} (Module.rank ↥A ↥(extendScalars ⋯)) = Cardinal.lift.{v, w} (Module.rank F L)

Tactic:
(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv.lift_rank_eq,

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
⊢ Cardinal.lift.{w, v} (Module.rank ↥A ↥(extendScalars ⋯)) =
    Cardinal.lift.{w, v} (Module.rank F ↥(IsScalarTower.toAlgHom F L E).range)
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

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
p : ℕ
inst✝¹ : ExpChar E p
inst✝ : PerfectRing E p
x : ↥(perfectClosure F E)
this : ExpChar F p
x' : E
hx : x' ^ p = ↑x
n : ℕ
y : F
hy : (algebraMap F E) y = x' ^ p ^ (n + 1)
⊢ (frobenius (↥(perfectClosure F E)) p) ⟨x', ⋯⟩ = x

Tactic:
simp_rw [frobenius_def, SubmonoidClass.mk_pow, hx]

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

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
⊢ generator E ∈ E

Tactic:
rw [generator_eq_coeff h]

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
⊢ ↑((φ E).coeff (generatorIndex h)) ∈ E
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ generator E ∉ (algebraMap K K⟮X⟯).range

Tactic:
rw [generator_eq_coeff h]

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ ↑((φ E).coeff (generatorIndex h)) ∉ (algebraMap K K⟮X⟯).range
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  (algebraMap K[X] K⟮X⟯) (c E).num * ↑((φ E).coeff (generatorIndex h)) =
    (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h))
⊢ (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) = (algebraMap K[X] K⟮X⟯) (c E).num * generator E

Tactic:
rw [generator_eq_coeff h]

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  (algebraMap K[X] K⟮X⟯) (c E).num * ↑((φ E).coeff (generatorIndex h)) =
    (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h))
⊢ (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) =
    (algebraMap K[X] K⟮X⟯) (c E).num * ↑((φ E).coeff (generatorIndex h))
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: case inr
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
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))
H : (aeval α) (generator E).denom ≠ 0
⊢ (aeval α) (f E) ≠ 0 ∧ (aeval α) (g E) ≠ 0

Tactic:
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

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 = ⊥
this : (φ E).natDegree = m E
⊢ K⟮generator E⟯.relfinrank E = 1

Tactic:
refine (mul_eq_right₀ ?_).mp <| this ▸ (generator E).finrank_eq_max_natDegree ▸
      φ_natDegree h ▸ relfinrank_mul_finrank_top (adjoin_generator_le (E := E))

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
this : (φ E).natDegree = m E
⊢ m E ≠ 0
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
⊢ IsCompl s.direction s.directionᗮ

Tactic:
exact s.direction.isCompl_orthogonal

Goal state after:
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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
h :
  finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : #{i}ᶜ = n - 1 + 1
⊢ finrank ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) = 1

Tactic:
refine add_left_cancel (_root_.trans h ?_)

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
i : Fin (n + 1)
h :
  finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : #{i}ᶜ = n - 1 + 1
⊢ finrank ℝ ↥(vectorSpan ℝ (Set.range s.points)) = finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) + 1
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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
h :
  finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : #{i}ᶜ = n - 1 + 1
⊢ n = finrank ℝ ↥(vectorSpan ℝ (s.points '' (↑{i})ᶜ)) + 1

Tactic:
← Finset.coe_compl,

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
i : Fin (n + 1)
h :
  finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
hc : #{i}ᶜ = n - 1 + 1
⊢ n = finrank ℝ ↥(vectorSpan ℝ (s.points '' ↑{i}ᶜ)) + 1
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case a
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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| ≠
    ‖s.points i -ᵥ s.altitudeFoot i‖ * ‖s.points j -ᵥ s.altitudeFoot j‖

Tactic:
← Real.norm_eq_abs,

Goal state after:
case a
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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ ‖⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫‖ ≠
    ‖s.points i -ᵥ s.altitudeFoot i‖ * ‖s.points j -ᵥ s.altitudeFoot j‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case 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₃ : P
r : ℝ
h : r ≠ 0
hlt : r < 0
⊢ InnerProductGeometry.angle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

Tactic:
simp [hlt, -neg_vsub_eq_vsub_rev]

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

Goal state before:
pp: case 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₃ : P
r : ℝ
h : r ≠ 0
hlt : 0 < r
⊢ InnerProductGeometry.angle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

Tactic:
simp [hlt, -neg_vsub_eq_vsub_rev]

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
h : p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ ∠ p₂ p₁ p₃ = 0

Tactic:
rcases h with ⟨hp₁p₂, ⟨r, ⟨hr, hpr⟩⟩⟩

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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ ∠ p₂ p₁ p₃ = 0
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₃) = π
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) + InnerProductGeometry.angle (p₄ -ᵥ p₃) (p₁ -ᵥ p₃) = π

Tactic:
exact angle_add_angle_eq_pi_of_angle_eq_pi _ h

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₂ : p₃ ≠ p₂
⊢ dist p₁ p₃ = dist p₁ p₂ + dist p₃ p₂ ↔ ∠ p₁ p₂ p₃ = π

Tactic:
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]
  exact
    norm_sub_eq_add_norm_iff_angle_eq_pi (fun he => hp₁p₂ (vsub_eq_zero_iff_eq.1 he)) fun he =>
      hp₃p₂ (vsub_eq_zero_iff_eq.1 he)

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ angle x (x + y) = Real.arccos (‖x‖ / ‖x + y‖)

Tactic:
by
  rw [angle, inner_add_right, h, add_zero, real_inner_self_eq_norm_mul_norm]
  by_cases hx : ‖x‖ = 0; · simp [hx]
  rw [div_mul_eq_div_div, mul_self_div_self]

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

Goal state before:
pp: case inl
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
r : ℝ
h : r ≠ 0
hlt : r < 0
⊢ o.oangle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

Tactic:
simp [hlt, -neg_vsub_eq_vsub_rev]

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

Goal state before:
pp: case 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
r : ℝ
h : r ≠ 0
hlt : 0 < r
⊢ o.oangle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

Tactic:
simp [hlt, -neg_vsub_eq_vsub_rev]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖

Tactic:
rw [sub_eq_add_neg, ← norm_neg, norm_div_tan_angle_add_of_inner_eq_zero h h0]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

Goal state before:
pp: case neg.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
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
h : dist p ↑((orthogonalProjection s₁) p) / dist p p' = dist p ↑((orthogonalProjection s₂) p) / dist p p'
hp : p ≠ p'
hpd : 0 < dist p p'
⊢ dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)

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
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
h :
  Real.arcsin (dist p ↑((orthogonalProjection s₁) p) / dist p p') =
    Real.arcsin (dist p ↑((orthogonalProjection s₂) p) / dist p p')
hp : p ≠ p'
hpd : 0 < dist p p'
⊢ dist p ↑((orthogonalProjection s₁) p) ≤ dist p p'

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
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
h :
  Real.arcsin (dist p ↑((orthogonalProjection s₁) p) / dist p p') =
    Real.arcsin (dist p ↑((orthogonalProjection s₂) p) / dist p p')
hp : p ≠ p'
hpd : 0 < dist p p'
⊢ dist p ↑((orthogonalProjection s₂) p) ≤ dist p p'

Tactic:
· rwa [div_left_inj' hpd.ne'] at h

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
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
h :
  Real.arcsin (dist p ↑((orthogonalProjection s₁) p) / dist p p') =
    Real.arcsin (dist p ↑((orthogonalProjection s₂) p) / dist p p')
hp : p ≠ p'
hpd : 0 < dist p p'
⊢ dist p ↑((orthogonalProjection s₁) p) ≤ dist p p'

V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
h :
  Real.arcsin (dist p ↑((orthogonalProjection s₁) p) / dist p p') =
    Real.arcsin (dist p ↑((orthogonalProjection s₂) p) / dist p p')
hp : p ≠ p'
hpd : 0 < dist p p'
⊢ dist p ↑((orthogonalProjection s₂) p) ≤ dist p p'
Module: Mathlib.Geometry.Euclidean.SignedDist

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
v : V
p q : P
h : ¬v = 0
⊢ |⟪v, q -ᵥ p⟫| = ‖v‖ * ‖q -ᵥ p‖ ↔ ∃ a, a • v = q -ᵥ p

Tactic:
← Real.norm_eq_abs,

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
v : V
p q : P
h : ¬v = 0
⊢ ‖⟪v, q -ᵥ p⟫‖ = ‖v‖ * ‖q -ᵥ p‖ ↔ ∃ a, a • v = q -ᵥ p
Module: Mathlib.Geometry.Euclidean.SignedDist

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
v : V
p q : P
⊢ ((signedDist v) p) q = dist p q ↔ q -ᵥ p ∈ ℝ≥0 ∙ v

Tactic:
rw [Submodule.mem_span_singleton]
  rw [signedDist_apply_apply, dist_eq_norm_vsub', NormedSpace.normalize, real_inner_smul_left]
  by_cases h : v = 0
  · simp [h, eq_comm (a := (0 : ℝ)), eq_comm (a := (0 : V))]
  rw [inv_mul_eq_iff_eq_mul₀ (by positivity)]
  rw [inner_eq_norm_mul_iff_real]
  simp only [smul_def]
  refine ⟨fun h => ?_, fun ⟨c, h⟩ => ?_⟩
  · simp only [NNReal.exists, coe_mk, exists_prop]
    use ‖v‖⁻¹ * ‖q -ᵥ p‖
    constructor
    · positivity
    · rw [← smul_smul, h, smul_smul, inv_mul_cancel₀ (by positivity), one_smul]
  · rw [← h, norm_smul, smul_smul, mul_comm]
    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₂].SOppSide p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' : ∡ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) = ∡ ((AffineEquiv.pointReflection ℝ p₂) p₃) p₂ p₄
hs' : line[ℝ, p₁, p₂].SOppSide p₃ ((AffineEquiv.pointReflection ℝ p₂) p₃)
h : ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) = ∠ p₁ p₂ p₄ / 2
⊢ ∠ p₁ p₂ p₃ = π - ∠ p₁ p₂ p₄ / 2

Tactic:
angle_pointReflection_right

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