mathlib-initiative/mathlib-tactics huggingface dataset:
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
hB : IntermediateField.map C.val B' = B
h₁ : A' ⊔ B' = ⊤
⊢ A ⊓ lift B' = ⊥

Tactic:
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
h₁ : A' ⊔ B' = ⊤
⊢ A ⊓ B = ⊥
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
i : E →ₐ[F] K
x : E
⊢ i x ∈ perfectClosure F K ↔ x ∈ perfectClosure F E

Tactic:
by
  simp_rw [mem_perfectClosure_iff]
  refine ⟨fun ⟨n, y, h⟩ ↦ ⟨n, y, ?_⟩, fun ⟨n, y, h⟩ ↦ ⟨n, y, ?_⟩⟩
  · apply_fun i using i.injective
    rwa [AlgHom.commutes, map_pow]
  simpa only [AlgHom.commutes, map_pow] using congr_arg i h

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 : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Algebra F A
inst✝¹ : Field B
inst✝ : Algebra F B
fa : A →ₐ[F] E
fb : B →ₐ[F] E
H : fa.fieldRange.LinearDisjoint ↥fb.fieldRange
⊢ IsDomain (A ⊗[F] B)

Tactic:
linearDisjoint_iff',

Goal state after:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Algebra F A
inst✝¹ : Field B
inst✝ : Algebra F B
fa : A →ₐ[F] E
fb : B →ₐ[F] E
H : fa.fieldRange.LinearDisjoint fb.fieldRange.toSubalgebra
⊢ IsDomain (A ⊗[F] B)
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
inst✝¹ : Algebra.IsSeparable F ↥(adjoin F S)
q : ℕ
inst✝ : ExpChar F q
n : ℕ
M : IntermediateField F E := adjoin F ((fun x ↦ x ^ q ^ n) '' S)
this✝¹ : ExpChar (↥M) q
x : E
hx : x ∈ S
this✝ : Algebra.IsSeparable ↥M ↥(↥M)⟮x⟯
this : IsPurelyInseparable ↥M ↥(↥M)⟮x⟯
hx' : x ∈ (↥M)⟮x⟯
⊢ x ∈ ↑M

Tactic:
M⟮x⟯.eq_bot_of_isPurelyInseparable_of_isSeparable,

Goal state after:
case refine_1
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
S : Set E
inst✝¹ : Algebra.IsSeparable F ↥(adjoin F S)
q : ℕ
inst✝ : ExpChar F q
n : ℕ
M : IntermediateField F E := adjoin F ((fun x ↦ x ^ q ^ n) '' S)
this✝¹ : ExpChar (↥M) q
x : E
hx : x ∈ S
this✝ : Algebra.IsSeparable ↥M ↥(↥M)⟮x⟯
this : IsPurelyInseparable ↥M ↥(↥M)⟮x⟯
hx' : x ∈ ⊥
⊢ x ∈ ↑M
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
this : Field K := Ideal.Quotient.field M
i : A ⊗[F] B →ₐ[F] K := IsScalarTower.toAlgHom F (A ⊗[F] B) K
fa : A →ₐ[F] K := i.comp Algebra.TensorProduct.includeLeft
fb : B →ₐ[F] K := i.comp Algebra.TensorProduct.includeRight
H : fa.fieldRange.LinearDisjoint ↥fb.fieldRange
⊢ M = ⊥

Tactic:
linearDisjoint_iff',

Goal state after:
F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
this : Field K := Ideal.Quotient.field M
i : A ⊗[F] B →ₐ[F] K := IsScalarTower.toAlgHom F (A ⊗[F] B) K
fa : A →ₐ[F] K := i.comp Algebra.TensorProduct.includeLeft
fb : B →ₐ[F] K := i.comp Algebra.TensorProduct.includeRight
H : fa.fieldRange.LinearDisjoint fb.fieldRange.toSubalgebra
⊢ M = ⊥
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
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
h : LinearIndependent F v
h' : LinearIndepOn F id (Set.range v)
ι' : Set E := h'.extend ⋯
b : Basis (↑ι') F E := Basis.extend h'
this : Fintype ↑ι' := FiniteDimensional.fintypeBasisIndex b
H : LinearIndependent F fun (x : ↑ι') ↦ b x ^ q ^ n
f : ι → ↑ι' := fun i ↦ ⟨v i, ⋯⟩
x✝ : ι
⊢ v x✝ ^ q ^ n = (Basis.extend h') (f x✝) ^ q ^ n

Tactic:
Basis.extend_apply_self

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
h : LinearIndependent F v
h' : LinearIndepOn F id (Set.range v)
ι' : Set E := h'.extend ⋯
b : Basis (↑ι') F E := Basis.extend h'
this : Fintype ↑ι' := FiniteDimensional.fintypeBasisIndex b
H : LinearIndependent F fun (x : ↑ι') ↦ b x ^ q ^ n
f : ι → ↑ι' := fun i ↦ ⟨v i, ⋯⟩
x✝ : ι
⊢ v x✝ ^ q ^ n = ↑(f x✝) ^ q ^ n
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
this✝ : UniqueFactorizationMonoid ↥K[f]
H : (f.minpolyX ↥K[f]).natDegree = 0
this : (Polynomial.map (algebraMap ↥K[f] ↥K⟮f⟯) (f.minpolyX ↥K[f])).natDegree ≤ (f.minpolyX ↥K[f]).natDegree
⊢ False

Tactic:
f.minpolyX_map K[f] K⟮f⟯,

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
this✝ : UniqueFactorizationMonoid ↥K[f]
H : (f.minpolyX ↥K[f]).natDegree = 0
this : (f.minpolyX ↥K⟮f⟯).natDegree ≤ (f.minpolyX ↥K[f]).natDegree
⊢ False
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_4
d₁ d₂ : DiffeologicalSpace X
h : @IsPlot X d₁ = @IsPlot X d₂
⊢ d₁ = d₂

Tactic:
obtain ⟨p₁, _, _, _, t₁, h₁⟩ := d₁
  obtain ⟨p₂, _, _, _, t₂, h₂⟩ := d₂
  congr 1; ext s
  exact ((show p₁ = p₂ from h) ▸ @h₁ s).trans (@h₂ s).symm

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 q : P
⊢ (orthogonalProjection s) p = (orthogonalProjection s) q ↔ p -ᵥ q ∈ s.directionᗮ

Tactic:
rw [orthogonalProjection_eq_iff_mem, ← s.directionᗮ.add_mem_iff_left (x := p -ᵥ q)
    (vsub_orthogonalProjection_mem_direction_orthogonal s q)]

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 q : P
⊢ p -ᵥ ↑((orthogonalProjection s) q) ∈ s.directionᗮ ↔ p -ᵥ q + (q -ᵥ ↑((orthogonalProjection s) q)) ∈ s.directionᗮ
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
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
r₁ r₂ : 𝕜
v : V
hv : v ∈ s.directionᗮ
⊢ ‖r₁ • v + (p₁ -ᵥ p₂) - r₂ • v‖ * ‖r₁ • v + (p₁ -ᵥ p₂) - r₂ • v‖ =
    ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖

Tactic:
sub_smul,

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
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
r₁ r₂ : 𝕜
v : V
hv : v ∈ s.directionᗮ
⊢ ‖r₁ • v + (p₁ -ᵥ p₂) - r₂ • v‖ * ‖r₁ • v + (p₁ -ᵥ p₂) - r₂ • v‖ =
    ‖p₁ -ᵥ p₂ + (r₁ • v - r₂ • v)‖ * ‖p₁ -ᵥ p₂ + (r₁ • v - r₂ • v)‖
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
x : V
⊢ (o.rotation θ₁) ((o.rotation θ₂) x) = (o.rotation (θ₁ + θ₂)) x

Tactic:
simp only [o.rotation_apply, Real.Angle.cos_add, Real.Angle.sin_add, map_add,
    map_smul, rightAngleRotation_rightAngleRotation]

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
x : V
⊢ θ₁.cos • (θ₂.cos • x + θ₂.sin • o.rightAngleRotation x) + θ₁.sin • (θ₂.cos • o.rightAngleRotation x + θ₂.sin • -x) =
    (θ₁.cos * θ₂.cos - θ₁.sin * θ₂.sin) • x + (θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin) • o.rightAngleRotation x
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case mpr
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)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
⊢ vectorSpan ℝ {p, s.points i} = (s.altitude i).direction

Tactic:
← direction_altitude

Goal state after:
case mpr
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)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ vectorSpan ℝ {p, s.points i} = (s.altitude i).direction
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 : V
r₁ r₂ : ℝ
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : 0 < r₁
⊢ o.oangle (r₁ • x) (r₂ • x) = 0

pp: case inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r₁ r₂ : ℝ
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : 0 = r₁
⊢ o.oangle (r₁ • x) (r₂ • x) = 0

Tactic:
· simp [h, hr₂]

Goal state after:
case inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r₁ r₂ : ℝ
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : 0 = r₁
⊢ o.oangle (r₁ • x) (r₂ • x) = 0
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)
x y : V
θ : Real.Angle
⊢ o.oangle x y = θ ↔ (x ≠ 0 ∧ y ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • (o.rotation θ) x) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
by_cases hx : x = 0
  · simp [hx, eq_comm]
  · by_cases hy : y = 0
    · simp [hy, eq_comm]
    · rw [o.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero hx hy]
      simp [hx, hy]

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

Tactic:
by
  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_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
h : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
⊢ p₃ -ᵥ p₂ = p₃ -ᵥ m + (midpoint ℝ p₁ p₂ -ᵥ p₂)

Tactic:
vsub_add_vsub_cancel

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 : dist p₃ p₁ = dist p₃ p₂
m : P := midpoint ℝ p₁ p₂
h1 : p₃ -ᵥ p₁ = p₃ -ᵥ m - (p₁ -ᵥ m)
⊢ p₃ -ᵥ p₂ = p₃ -ᵥ p₂
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 : ℕ
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.height i * s.height j)| < 1

Tactic:
abs_div,

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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| / |s.height i * s.height j| < 1
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
hx : x ≠ 0
hy : y ≠ 0
⊢ (o.oangle x y).cos = ‖x‖ * ‖y‖ * (o.oangle x y).cos / (‖x‖ * ‖y‖)

Tactic:
field

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: 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₂
⊢ π / 2 = π - π / 2

Tactic:
field

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

Goal state before:
pp: case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
⊢ (m 0 - m 1 * r) • x + m 1 • (r • x + y) = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0)

Tactic:
sub_smul,

Goal state after:
case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
⊢ m 0 • x - (m 1 * r) • x + m 1 • (r • x + y) = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case neg
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
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)

Tactic:
have hx : -x = r⁻¹ • o.rotation (π / 2 : ℝ) (r • o.rotation (π / 2 : ℝ) x) := by
    simp [hr, ← Real.Angle.coe_add]

Goal state after:
case neg
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
hx : -x = r⁻¹ • (o.rotation ↑(π / 2)) (r • (o.rotation ↑(π / 2)) x)
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x - x) = ↑(Real.arctan r⁻¹)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).cos * dist p₁ p₃ = dist p₃ p₂

Tactic:
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
  rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    cos_angle_mul_dist_of_angle_eq_pi_div_two (angle_eq_pi_div_two_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
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 : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ dist p₁ p₂ / (∡ p₃ p₁ p₂).cos = dist p₁ p₃

Tactic:
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
  rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe, dist_comm p₁ p₃,
    dist_div_cos_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inr (left_ne_of_oangle_eq_pi_div_two h))]

Goal state after:
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
r : ℝ
⊢ ⟪↑(SignType.sign r) • NormedSpace.normalize v, q -ᵥ p⟫ = ↑(SignType.sign r) * ⟪NormedSpace.normalize v, q -ᵥ p⟫

Tactic:
real_inner_smul_left

Goal state after:
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
r : ℝ
⊢ ↑(SignType.sign r) * ⟪NormedSpace.normalize v, q -ᵥ p⟫ = ↑(SignType.sign r) * ⟪NormedSpace.normalize 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 r : P
⊢ ⟪NormedSpace.normalize v, r -ᵥ q + (q -ᵥ p)⟫ = ⟪NormedSpace.normalize v, r -ᵥ p⟫

Tactic:
vsub_add_vsub_cancel

Goal state after:
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 r : P
⊢ ⟪NormedSpace.normalize v, r -ᵥ p⟫ = ⟪NormedSpace.normalize v, r -ᵥ 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
⊢ |⟪NormedSpace.normalize v, q -ᵥ p⟫| = dist p q ↔ ∃ a, a • v = q -ᵥ p

Tactic:
dist_eq_norm_vsub',

Goal state after:
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
⊢ |⟪NormedSpace.normalize v, q -ᵥ p⟫| = ‖q -ᵥ p‖ ↔ ∃ a, a • v = q -ᵥ p
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
c p₁ p₂ : P
⊢ ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪2⁻¹ • (c -ᵥ p₁ + (c -ᵥ p₂)), p₂ -ᵥ p₁⟫ = 0

Tactic:
real_inner_smul_left

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0 ↔ 2⁻¹ * ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0
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
p₁ p₂ : P
h : perpBisector p₁ p₂ = ⊤
⊢ p₁ ∈ ⊤

Tactic:
trivial

Goal state after:
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
⊢ ⟪NormedSpace.normalize v, q -ᵥ p⟫ = dist p q ↔ ∃ a, a • v = q -ᵥ p

Tactic:
dist_eq_norm_vsub',

Goal state after:
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
⊢ ⟪NormedSpace.normalize v, q -ᵥ p⟫ = ‖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
⊢ ⟪‖v‖⁻¹ • v, q -ᵥ p⟫ = ‖q -ᵥ p‖ ↔ ∃ a, a • v = q -ᵥ p

Tactic:
real_inner_smul_left

Goal state after:
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
⊢ ‖v‖⁻¹ * ⟪v, q -ᵥ p⟫ = ‖q -ᵥ p‖ ↔ ∃ a, a • v = q -ᵥ p
Module: Mathlib.Geometry.Euclidean.SignedDist

Goal state before:
pp: case h.right
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
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
⊢ (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p

Tactic:
· rw [← smul_smul, h, smul_smul, inv_mul_cancel₀ (by positivity), one_smul]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: P : Type u_2
inst✝ : MetricSpace P
s₁ s₂ : Sphere P
⊢ s₁ ≠ s₂ ↔ ¬(s₁.center = s₂.center ∧ s₁.radius = s₂.radius)

Tactic:
← Sphere.ext_iff

Goal state after:
P : Type u_2
inst✝ : MetricSpace P
s₁ s₂ : Sphere P
⊢ s₁ ≠ s₂ ↔ ¬s₁ = s₂
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

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 : Sphere P
p x : P
⊢ x ∈ s.orthRadius p ↔ ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0

Tactic:
by
  rw [orthRadius, mem_mk', Submodule.mem_orthogonal_singleton_iff_inner_left]

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

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 : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = s.direction
hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₁ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = dist p₁ c₁
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
hp' : p₂ -ᵥ p₁ ≠ 0
hp₂ : dist (1 • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = dist p₁ c₁
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂

Tactic:
dist_smul_vadd_eq_dist _ _ hp'

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = s.direction
hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₁ : t₂ = 0 ∨ t₂ = -2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ c₁⟫ / ⟪p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
hp' : p₂ -ᵥ p₁ ≠ 0
hp₂ : 1 = 0 ∨ 1 = -2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ c₁⟫ / ⟪p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂