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

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω ↦ Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
x✝ : ↥FS
α : E
hα : α ∈ FS
β : K
hβ : (aeval β) (minpoly F α) = 0
ϕ : ↥F⟮α⟯ →ₐ[F] K' :=
  (IsScalarTower.toAlgHom F K K').comp
    ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F K) β hβ).comp ↑(adjoinRootEquivAdjoin F ⋯).symm)
ω : ↥(adjoin F ↑S) →ₐ[F] K'
hω : ω.comp (inclusion ⋯) = ϕ
⊢ (IsScalarTower.toAlgHom F K K')
      (((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F K) β hβ).comp ↑(adjoinRootEquivAdjoin F ⋯).symm)
        (AdjoinSimple.gen F α)) =
    (Algebra.ofId K K').toRingHom β

Tactic:
AlgHom.comp_apply,

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω ↦ Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
x✝ : ↥FS
α : E
hα : α ∈ FS
β : K
hβ : (aeval β) (minpoly F α) = 0
ϕ : ↥F⟮α⟯ →ₐ[F] K' :=
  (IsScalarTower.toAlgHom F K K').comp
    ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F K) β hβ).comp ↑(adjoinRootEquivAdjoin F ⋯).symm)
ω : ↥(adjoin F ↑S) →ₐ[F] K'
hω : ω.comp (inclusion ⋯) = ϕ
⊢ (IsScalarTower.toAlgHom F K K')
      ((AdjoinRoot.liftAlgHom (minpoly F α) (Algebra.ofId F K) β hβ)
        (↑(adjoinRootEquivAdjoin F ⋯).symm (AdjoinSimple.gen F α))) =
    (Algebra.ofId K K').toRingHom β
Module: Mathlib.FieldTheory.Isaacs

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, minpoly F x = minpoly F y
x : E
y : K
hy : minpoly F x = minpoly F y
⊢ (aeval y) (minpoly F y) = 0

Tactic:
minpoly.aeval

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, minpoly F x = minpoly F y
x : E
y : K
hy : minpoly F x = minpoly F y
⊢ 0 = 0
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 : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
hz : z ∈ y • ↑(H j)
⊢ ∃ i ∈ s, x * (y⁻¹ * z) ∈ g i • ↑(H i)

Tactic:
by
        simpa using Set.eq_univ_iff_forall.mp hcovers (x * (y⁻¹ * z))

Goal state after:
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
hm : ∑ i ∈ s, m i • (x - (algebraMap F E) i)⁻¹ = 0
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
⊢ m i = 0

Tactic:
have h1 : ∀ i ∈ s, m i • (b * (x - algebraMap F E i)⁻¹) =
      m i • (s.erase i).prod fun j ↦ x - algebraMap F E j := fun i hi ↦ by
    simp_rw [b, ← s.prod_erase_mul _ hi, mul_inv_cancel_right₀ (hnz i)]

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
hm : ∑ i ∈ s, m i • (x - (algebraMap F E) i)⁻¹ = 0
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)
⊢ m i = 0
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 ι
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
hcovers : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
hempty : IsEmpty κ
⊢ False

Tactic:
rw [Set.iUnion_of_empty] at hcovers

Goal state after:
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 ι
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
hcovers : ∅ = Set.univ
hempty : IsEmpty κ
⊢ False
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case prime_mul
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝ : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
⊢ ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ p - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))

Tactic:
intro E _ _ x hx

Goal state after:
case prime_mul
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝² : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst✝¹ : Field E
inst✝ : Algebra K E
x : E
hx : minpoly K x = X ^ p - C a
⊢ Irreducible (X ^ n - C (AdjoinSimple.gen K x))
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case pos
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
η : ↥(rootsOfUnity n K)
this✝¹ : Fact (Irreducible (X ^ n - C a))
this✝ : IsDomain K[n√a]
this : Algebra K K[n√a] := inferInstance
h : a = 0
⊢ 1 = (of (X ^ n - C a)) ↑↑η

pp: case neg
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
η : ↥(rootsOfUnity n K)
this✝¹ : Fact (Irreducible (X ^ n - C a))
this✝ : IsDomain K[n√a]
this : Algebra K K[n√a] := inferInstance
h : ¬a = 0
⊢ (of (X ^ n - C a)) ↑↑η * root (X ^ n - C a) / root (X ^ n - C a) = (of (X ^ n - C a)) ↑↑η

Tactic:
· obtain rfl := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) h
      have : (η : Kˣ) = 1 := (pow_one _).symm.trans η.prop
      simp only [this, Units.val_one, map_one]

Goal state after:
case neg
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
η : ↥(rootsOfUnity n K)
this✝¹ : Fact (Irreducible (X ^ n - C a))
this✝ : IsDomain K[n√a]
this : Algebra K K[n√a] := inferInstance
h : ¬a = 0
⊢ (of (X ^ n - C a)) ↑↑η * root (X ^ n - C a) / root (X ^ n - C a) = (of (X ^ n - C a)) ↑↑η
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: case mpr.h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
y : L
⊢ ∃ a, mk K a = -mk K y ∧ ∃ b, mk K b = mk K y ∧ a + b = 0

Tactic:
exact ⟨-y, mk_neg y, y, rfl, neg_add_cancel _⟩

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

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : HasExponent K L
p : ℕ
inst✝ : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
⊢ iterateFrobeniusAux K L p n 1 = 1

Tactic:
apply (algebraMap K L).injective
    rw [(algebraMap K L).map_one,
      algebraMap_iterateFrobeniusAux K p hn 1,
      one_pow]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
⊢ 1 - ↑0 = 1

Tactic:
Int.ofNat_zero,

Goal state after:
K : Type u
inst✝ : Field K
⊢ 1 - 0 = 1
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
p : K[X]
⊢ ↑p.natDegree - ↑0 = ↑p.natDegree

Tactic:
Int.ofNat_zero,

Goal state after:
K : Type u
inst✝ : Field K
p : K[X]
⊢ ↑p.natDegree - 0 = ↑p.natDegree
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
⊢ Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree F K)

Tactic:
have h := (separableClosure F K).linearDisjoint_of_isPurelyInseparable_of_isSeparable E
    |>.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left

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
inst✝ : IsPurelyInseparable F E
h :
  Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (Module.rank (↥(adjoin E ↑(separableClosure F K))) K) =
    Cardinal.lift.{v, w} (Module.rank (↥(separableClosure F K)) K)
⊢ Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree F K)
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (φ E).natDegree = Module.finrank (↥E) K⟮X⟯

Tactic:
← (IntermediateField.adjoinXEquiv E).toLinearEquiv.finrank_eq,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (φ E).natDegree = Module.finrank ↥E ↥(↥E)⟮ X⟯
Module: Mathlib.FieldTheory.RatFunc.Valuation

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x : F⟮X⟯
hx : x ≠ 0
⊢ inftyValuationDef F x = exp x.intDegree

Tactic:
rw [inftyValuationDef, if_neg hx]

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 ≠ ⊥
⊢ g E ∣ (c E).num

Tactic:
denom_dvd (num_ne_zero (c_ne_zero h))

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ ∃ p, generator E = (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) (c E).num
Module: Mathlib.Geometry.Convex.Hull

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
x : X
⊢ x ∈ (convexHull R) s ↔ ∀ (t : Set X), s ⊆ t → IsConvexSet R t → x ∈ t

Tactic:
by
  simp_rw [convexHull_eq_iInter, mem_iInter]

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
C F : PointedCone R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
hf : Function.Surjective ⇑f
hc : (comap f F).IsFaceOf (comap f C)
x y : M
x✝ : R
xC : f ⋯.choose ∈ C
yC : y ∈ C
a0 : 0 < x✝
h : x✝ • f ⋯.choose + y ∈ F
⊢ f ⋯.choose ∈ F

Tactic:
rw [← (hf y).choose_spec] at h yC

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
C F : PointedCone R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
hf : Function.Surjective ⇑f
hc : (comap f F).IsFaceOf (comap f C)
x y : M
x✝ : R
xC : f ⋯.choose ∈ C
yC : f ⋯.choose ∈ C
a0 : 0 < x✝
h : x✝ • f ⋯.choose + f ⋯.choose ∈ F
⊢ f ⋯.choose ∈ F
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : DiffeologicalSpace X
inst✝ : DiffeologicalSpace Y
f : X → Y
hf : DSmooth f
⊢ Continuous[dTopology, dTopology] f

Tactic:
simp_rw [continuous_def, isOpen_iff_preimages_plots (X := X), isOpen_iff_preimages_plots (X := Y)]
  exact fun u hu n p hp ↦ hu n (f ∘ p) (hf n p hp)

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 : P
⊢ dist p ↑((orthogonalProjection s) p) = Metric.infDist p ↑s

Tactic:
by
  refine le_antisymm ?_ (Metric.infDist_le_dist_of_mem (orthogonalProjection_mem _))
  rw [Metric.infDist_eq_iInf]
  refine le_ciInf fun x ↦ le_of_sq_le_sq ?_ dist_nonneg
  rw [dist_comm _ (x : P)]
  simp_rw [pow_two,
    dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p x.property]
  simp [mul_self_nonneg]

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
ps : Set P
hps : ps ⊆ ↑s
p : P
h :
  (ps.Pairwise fun p₁ p₂ ↦ dist p₁ p = dist p₂ p) ↔
    ps.Pairwise fun p₁ p₂ ↦ dist p₁ ↑((orthogonalProjection s) p) = dist p₂ ↑((orthogonalProjection s) p)
⊢ (∃ r, ∀ p₁ ∈ ps, dist p₁ p = r) ↔ ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑((orthogonalProjection s) p) = r

Tactic:
Set.pairwise_eq_iff_exists_eq

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
ps : Set P
hps : ps ⊆ ↑s
p : P
h : (∃ z, ∀ x ∈ ps, dist x p = z) ↔ ∃ z, ∀ x ∈ ps, dist x ↑((orthogonalProjection s) p) = z
⊢ (∃ r, ∀ p₁ ∈ ps, dist p₁ p = r) ↔ ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑((orthogonalProjection s) p) = 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
⊢ (↑⟪x, y⟫ + (o.areaForm x) y • I).arg = Real.Angle.toReal 0 ↔ SameRay ℝ x y

Tactic:
Real.Angle.toReal_zero,

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 : V
⊢ (↑⟪x, y⟫ + (o.areaForm x) y • I).arg = 0 ↔ SameRay ℝ 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
h : π / 2 = π
heq : p₁ = p₂
⊢ π = 0

Tactic:
by linarith

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

Goal state before:
pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : y ≠ 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
· exact
        Left.add_pos_of_nonneg_of_pos (mul_self_nonneg _) (mul_self_pos.2 (norm_ne_zero_iff.2 h0))

Goal state after:
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 = Real.cos (InnerProductGeometry.angle x y)

Tactic:
rw [o.cos_oangle_eq_inner_div_norm_mul_norm hx hy, InnerProductGeometry.cos_angle]

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₅ p₆ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆
⊢ AffineIndependent ℝ ![p₁, p₂, p₃] ↔ AffineIndependent ℝ ![p₄, p₅, p₆]

Tactic:
by
  simp_rw [← oangle_ne_zero_and_ne_pi_iff_affineIndependent, ← Real.Angle.two_zsmul_ne_zero_iff, h]

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

Goal state before:
pp: case refine_2.inr.inr.inl.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 : Wbtw ℝ p₂ p₃ p₁
⊢ Collinear ℝ {p₁, p₂, p₃}

Tactic:
· rw [Set.insert_comm, Set.pair_comm]
        exact h.collinear

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
⊢ Real.sin (angle x (x - y)) * ‖x - y‖ = ‖y‖

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h
  rw [sub_eq_add_neg, sin_angle_add_mul_norm_of_inner_eq_zero h, norm_neg]

Goal state after:
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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = -(o.oangle y z).sign
⊢ o.oangle w x = -o.oangle y z

Tactic:
by
  rw [← oangle_rev]
  rw [← Real.Angle.sign_neg, ← oangle_rev] at hs
  nth_rw 2 [InnerProductGeometry.angle_comm] at h
  exact o.oangle_eq_of_angle_eq_of_sign_eq h hs

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : p₁ = p₂
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hp₁'p₂ : p₁' = p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃

Tactic:
exact False.elim (hp₁p₂ h)

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

Goal state before:
pp: case neg.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
he : InnerProductGeometry.angle x y = 0
r : ℝ
hr0 : 0 < r
hz : r • y ≠ 0
hr : ¬SameRay ℝ x (r • y)
hs : ¬(o.oangle x y).sign = (o.oangle y (r • y)).sign
hn : o.oangle x y ≠ o.oangle y (r • y)
hs' : ¬(o.oangle x y).sign = -(o.oangle y (r • y)).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y (r • y)).sign = 0
h0' : InnerProductGeometry.angle y (r • y) = 0
⊢ SameRay ℝ x (r • y)

Tactic:
obtain ⟨-, r', hr'0, rfl⟩ := InnerProductGeometry.angle_eq_zero_iff.1 he

Goal state after:
case neg.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
r : ℝ
hr0 : 0 < r
r' : ℝ
hr'0 : 0 < r'
hy : ¬r' • x = 0
he : InnerProductGeometry.angle x (r' • x) = 0
hz : r • r' • x ≠ 0
hr : ¬SameRay ℝ x (r • r' • x)
hs : ¬(o.oangle x (r' • x)).sign = (o.oangle (r' • x) (r • r' • x)).sign
hn : o.oangle x (r' • x) ≠ o.oangle (r' • x) (r • r' • x)
hs' : ¬(o.oangle x (r' • x)).sign = -(o.oangle (r' • x) (r • r' • x)).sign
h0 : (o.oangle x (r' • x)).sign = 0 ∨ (o.oangle (r' • x) (r • r' • x)).sign = 0
h0' : InnerProductGeometry.angle (r' • x) (r • r' • x) = 0
⊢ SameRay ℝ x (r • r' • x)
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 ∈ perpBisector p₁ p₂ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫

Tactic:
mem_perpBisector_iff_inner_eq_inner

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₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : dist p ↑((orthogonalProjection s₁) p) = dist p p'
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp : ↑((orthogonalProjection s₂) p) = p'
⊢ False

Tactic:
dist_orthogonalProjection_eq_dist_iff_eq_of_mem 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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : ↑((orthogonalProjection s₁) p) = p'
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp : ↑((orthogonalProjection s₂) p) = p'
⊢ False