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

Goal state before:
pp: F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
S : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange
j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
⊢ sepDegree E ↥L = sepDegree F ↥M

Tactic:
have hi : M ≤ L.restrictScalars F := by
    rw [restrictScalars_adjoin_of_algEquiv (E := K) j rfl, restrictScalars_adjoin]
    exact adjoin.mono _ _ _ Set.subset_union_right

Goal state after:
F : Type u
E : Type v
inst✝⁸ : Field F
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
S : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange
j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
⊢ sepDegree E ↥L = sepDegree F ↥M
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⟯
⊢ Module.finrank F ↥F⟮x⟯ = (minpoly E x).natDegree

Tactic:
← adjoin.finrank hi',

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⟯
⊢ Module.finrank F ↥F⟮x⟯ = Module.finrank E ↥E⟮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
⊢ Associated f (minpoly F x)

Tactic:
have := isUnit_C.2 (leadingCoeff_ne_zero.2 hirr.ne_zero).isUnit.inv

Goal state after:
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
this : IsUnit (C f.leadingCoeff⁻¹)
⊢ Associated f (minpoly F x)
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A : Subfield E
⊢ Module.rank ↥A ↥⊤ = Module.rank (↥A) E

Tactic:
IntermediateField.topEquiv.toLinearEquiv.rank_eq

Goal state after:
E : Type v
inst✝ : Field E
A : Subfield E
⊢ Module.rank (↥A) E = Module.rank (↥A) E
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝¹ : Field E
A B : Subfield E
L : Type v
inst✝ : Field L
f : E →+* L
⊢ (map f A).relrank (map f B) = A.relrank B

Tactic:
simpa using

Goal state after:
E : Type v
inst✝¹ : Field E
A B : Subfield E
L : Type v
inst✝ : Field L
f : E →+* L
⊢ (map f A).relrank (map f B) = A.relrank B
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝¹ : Field E
A : Subfield E
L : Type v
inst✝ : Field L
f : L →+* E
B : Subfield L
⊢ (comap f A).relrank B = A.relrank (map f B)

Tactic:
simpa using

Goal state after:
E : Type v
inst✝¹ : Field E
A : Subfield E
L : Type v
inst✝ : Field L
f : L →+* E
B : Subfield L
⊢ (comap f A).relrank B = A.relrank (map f B)
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A : Subfield E
f : L →+* E
⊢ lift.{v, w} (Module.rank (↥(comap f A)) L) = lift.{w, v} (A.relrank f.fieldRange)

Tactic:
simpa using

Goal state after:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A : Subfield E
f : L →+* E
⊢ lift.{v, w} (Module.rank (↥(comap f A)) L) = lift.{w, v} (A.relrank f.fieldRange)
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝¹ : Field E
A : Subfield E
L : Type v
inst✝ : Field L
f : L →+* E
⊢ Module.rank (↥(comap f A)) L = A.relrank f.fieldRange

Tactic:
simpa using

Goal state after:
E : Type v
inst✝¹ : Field E
A : Subfield E
L : Type v
inst✝ : Field L
f : L →+* E
⊢ Module.rank (↥(comap f A)) L = A.relrank f.fieldRange
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
f : K[X]
hf : Polynomial.map (algebraMap K ↥E) f = φ E
⊢ (aeval X) f = 0

Tactic:
simpa using

Goal state after:
case refine_2
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
f : K[X]
hf : Polynomial.map (algebraMap K ↥E) f = φ E
⊢ f = 0
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
x✝ : ∃ c, generator E = C c
c : K
hc : generator E = C c
⊢ (algebraMap K K⟮X⟯) c = generator E

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
x✝ : ∃ c, generator E = C c
c : K
hc : generator E = C c
⊢ C c = generator E
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝¹ : Field E
A B : Subfield E
L : Type v
inst✝ : Field L
f : L →+* E
⊢ (comap f A).relrank (comap f B) = A.relrank (B ⊓ f.fieldRange)

Tactic:
simpa using

Goal state after:
E : Type v
inst✝¹ : Field E
A B : Subfield E
L : Type v
inst✝ : Field L
f : L →+* E
⊢ (comap f A).relrank (comap f B) = A.relrank (B ⊓ f.fieldRange)
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
h : B ≤ f.fieldRange
⊢ lift.{v, w} ((comap f A).relrank (comap f B)) = lift.{w, v} (A.relrank B)

Tactic:
simpa using

Goal state after:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
h : B ≤ f.fieldRange
⊢ lift.{v, w} ((comap f A).relrank (comap f B)) = lift.{w, v} (A.relrank B)
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝¹ : Field E
A B : Subfield E
L : Type v
inst✝ : Field L
f : L →+* E
h : B ≤ f.fieldRange
⊢ (comap f A).relrank (comap f B) = A.relrank B

Tactic:
simpa using

Goal state after:
E : Type v
inst✝¹ : Field E
A B : Subfield E
L : Type v
inst✝ : Field L
f : L →+* E
h : B ≤ f.fieldRange
⊢ (comap f A).relrank (comap f B) = A.relrank B
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝¹ : Field E
A B : Subfield E
L : Type v
inst✝ : Field L
f : L →+* E
h : Function.Surjective ⇑f
⊢ (comap f A).relrank (comap f B) = A.relrank B

Tactic:
simpa using

Goal state after:
E : Type v
inst✝¹ : Field E
A B : Subfield E
L : Type v
inst✝ : Field L
f : L →+* E
h : Function.Surjective ⇑f
⊢ (comap f A).relrank (comap f B) = A.relrank B
Module: Mathlib.FieldTheory.Relrank

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

Tactic:
simpa using

Goal state after:
E : Type v
inst✝ : Field E
A B C : Subfield E
h : B ≤ C
⊢ A.relrank B * B.relrank C = (A ⊓ B).relrank C
Module: Mathlib.FieldTheory.Relrank

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

Tactic:
simpa using

Goal state after:
E : Type v
inst✝ : Field E
A B C : Subfield E
h : A ≤ B
⊢ A.relrank (B ⊓ C) * B.relrank C = A.relrank C
Module: Mathlib.FieldTheory.Relrank

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 v
inst✝¹ : Field L
inst✝ : Algebra F L
f : L →ₐ[F] E
⊢ Module.rank (↥(comap f A)) L = A.relrank f.fieldRange

Tactic:
simpa using

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 v
inst✝¹ : Field L
inst✝ : Algebra F L
f : L →ₐ[F] E
⊢ Module.rank (↥(comap f A)) L = A.relrank f.fieldRange
Module: Mathlib.FieldTheory.Relrank

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 v
inst✝¹ : Field L
inst✝ : Algebra F L
f : L →ₐ[F] E
B : IntermediateField F L
⊢ (comap f A).relrank B = A.relrank (map f B)

Tactic:
simpa using

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 v
inst✝¹ : Field L
inst✝ : Algebra F L
f : L →ₐ[F] E
B : IntermediateField F L
⊢ (comap f A).relrank B = A.relrank (map f B)
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 : PointedCone R M
F : Set (PointedCone R M)
h : ∀ f ∈ F, f.IsFaceOf C
x✝ y✝ : M
a : R
xc : x✝ ∈ C
yc : y✝ ∈ C
a0 : 0 < a
a✝ : a • x✝ + y✝ ∈ C
h' : ∀ p ∈ F, a • x✝ + y✝ ∈ p
⊢ x✝ ∈ C ∧ ∀ p ∈ F, x✝ ∈ p

Tactic:
simpa using

Goal state after:
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 : PointedCone R M
F : Set (PointedCone R M)
h : ∀ f ∈ F, f.IsFaceOf C
x✝ y✝ : M
a : R
xc : x✝ ∈ C
yc : y✝ ∈ C
a0 : 0 < a
a✝ : a • x✝ + y✝ ∈ C
h' : ∀ p ∈ F, a • x✝ + y✝ ∈ p
⊢ ∀ p ∈ F, x✝ ∈ p
Module: Mathlib.FieldTheory.Relrank

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
L : Type v
inst✝¹ : Field L
inst✝ : Algebra F L
f : E →ₐ[F] L
⊢ (map f A).relrank (map f B) = A.relrank B

Tactic:
simpa using

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
L : Type v
inst✝¹ : Field L
inst✝ : Algebra F L
f : E →ₐ[F] L
⊢ (map f A).relrank (map f B) = A.relrank B
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 using

Goal state after:
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
Module: Mathlib.FieldTheory.Relrank

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
L : Type v
inst✝¹ : Field L
inst✝ : Algebra F L
f : L →ₐ[F] E
⊢ (comap f A).relrank (comap f B) = A.relrank (B ⊓ f.fieldRange)

Tactic:
simpa using

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
L : Type v
inst✝¹ : Field L
inst✝ : Algebra F L
f : L →ₐ[F] E
⊢ (comap f A).relrank (comap f B) = A.relrank (B ⊓ f.fieldRange)
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
L : Type w
inst✝¹ : Field L
inst✝ : Algebra F L
A B : IntermediateField F E
f : L →ₐ[F] E
h : B ≤ f.fieldRange
⊢ Cardinal.lift.{v, w} ((comap f A).relrank (comap f B)) = Cardinal.lift.{w, v} (A.relrank B)

Tactic:
simpa using

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
L : Type w
inst✝¹ : Field L
inst✝ : Algebra F L
A B : IntermediateField F E
f : L →ₐ[F] E
h : B ≤ f.fieldRange
⊢ Cardinal.lift.{v, w} ((comap f A).relrank (comap f B)) = Cardinal.lift.{w, v} (A.relrank B)
Module: Mathlib.FieldTheory.Relrank

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
L : Type v
inst✝¹ : Field L
inst✝ : Algebra F L
f : L →ₐ[F] E
h : B ≤ f.fieldRange
⊢ (comap f A).relrank (comap f B) = A.relrank B

Tactic:
simpa using

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
L : Type v
inst✝¹ : Field L
inst✝ : Algebra F L
f : L →ₐ[F] E
h : B ≤ f.fieldRange
⊢ (comap f A).relrank (comap f B) = A.relrank B
Module: Mathlib.FieldTheory.Relrank

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
L : Type v
inst✝¹ : Field L
inst✝ : Algebra F L
f : L →ₐ[F] E
h : Function.Surjective ⇑f
⊢ (comap f A).relrank (comap f B) = A.relrank B

Tactic:
simpa using

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
L : Type v
inst✝¹ : Field L
inst✝ : Algebra F L
f : L →ₐ[F] E
h : Function.Surjective ⇑f
⊢ (comap f A).relrank (comap f B) = A.relrank B
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) *
      Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E) / c E) *
      (Polynomial.C (c E) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) *
      Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) *
      Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B C : IntermediateField F E
h : B ≤ C
⊢ A.relrank B * B.relrank C = (A ⊓ B).relrank C

Tactic:
simpa using

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B C : IntermediateField F E
h : B ≤ C
⊢ A.relrank B * B.relrank C = (A ⊓ B).relrank C
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B C : IntermediateField F E
h : A ≤ B
⊢ A.relrank (B ⊓ C) * B.relrank C = A.relrank C

Tactic:
simpa using

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B C : IntermediateField F E
h : A ≤ B
⊢ A.relrank (B ⊓ C) * B.relrank C = A.relrank C
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : DivisionRing R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
h₁ : F ≤ C
h₂ : ∀ {x y : M}, x ∈ C → y ∈ C → x + y ∈ F → x ∈ F
x✝ y✝ : M
a✝ : R
hx : x✝ ∈ C
hy : y✝ ∈ C
ha : 0 < a✝
haxy : a✝ • x✝ + y✝ ∈ F
⊢ x✝ ∈ F

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : DivisionRing R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
h₁ : F ≤ C
h₂ : ∀ {x y : M}, x ∈ C → y ∈ C → x + y ∈ F → x ∈ F
x✝ y✝ : M
a✝ : R
hx : x✝ ∈ C
hy : y✝ ∈ C
ha : 0 < a✝
haxy : a✝ • x✝ + y✝ ∈ F
⊢ x✝ ∈ F
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : DivisionRing R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C : PointedCone R M
x✝ y✝ : M
xc : x✝ ∈ C
yc : y✝ ∈ C
xyf : x✝ + y✝ ∈ C ∧ -y✝ + -x✝ ∈ C
⊢ -x✝ ∈ C

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : DivisionRing R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C : PointedCone R M
x✝ y✝ : M
xc : x✝ ∈ C
yc : y✝ ∈ C
xyf : x✝ + y✝ ∈ C ∧ -y✝ + -x✝ ∈ C
⊢ -x✝ ∈ C
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ F₁ : PointedCone R M
C₂ F₂ : PointedCone R N
hF₁ : F₁.IsFaceOf C₁
hF₂ : F₂.IsFaceOf C₂
x : M × N
hx : x ∈ prod F₁ F₂
⊢ x ∈ prod C₁ C₂

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ F₁ : PointedCone R M
C₂ F₂ : PointedCone R N
hF₁ : F₁.IsFaceOf C₁
hF₂ : F₂.IsFaceOf C₂
x : M × N
hx : x ∈ prod F₁ F₂
⊢ x.1 ∈ C₁ ∧ x.2 ∈ C₂
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ u,
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
x : EuclideanSpace ℝ (Fin n)
x✝ : x ∈ Set.univ
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
⊢ ∃ v, ∃ (hv : IsOpen v), x ∈ v ∧ d.isPlotOn hv p

Tactic:
let ⟨ε, hε, hε'⟩ := Metric.isOpen_iff.mp hu x hxu

Goal state after:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ u,
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
x : EuclideanSpace ℝ (Fin n)
x✝ : x ∈ Set.univ
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
⊢ ∃ v, ∃ (hv : IsOpen v), x ∈ v ∧ d.isPlotOn hv p
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
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))
isUnit₁ : IsUnit (Polynomial.C ((aeval α) (f E)))
isUnit₂ : IsUnit (Polynomial.C ((aeval α) (g E)))
isCoprime :
  IsCoprime ((Polynomial.mapRingHom (algebraMap K F)) (generator E).num)
    ((Polynomial.mapRingHom (algebraMap K F)) (generator E).denom)
this✝ : Associated ((Polynomial.mapRingHom (algebraMap K F)) (f E)) ((Polynomial.mapRingHom (algebraMap K F)) (g E))
this :
  IsUnit ((Polynomial.mapRingHom (algebraMap K F)) (generator E).num) ∧
    IsUnit ((Polynomial.mapRingHom (algebraMap K F)) (generator E).denom)
⊢ (generator E).num.natDegree = 0

Tactic:
simpa using

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
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))
isUnit₁ : IsUnit (Polynomial.C ((aeval α) (f E)))
isUnit₂ : IsUnit (Polynomial.C ((aeval α) (g E)))
isCoprime :
  IsCoprime ((Polynomial.mapRingHom (algebraMap K F)) (generator E).num)
    ((Polynomial.mapRingHom (algebraMap K F)) (generator E).denom)
this✝ : Associated ((Polynomial.mapRingHom (algebraMap K F)) (f E)) ((Polynomial.mapRingHom (algebraMap K F)) (g E))
this :
  IsUnit ((Polynomial.mapRingHom (algebraMap K F)) (generator E).num) ∧
    IsUnit ((Polynomial.mapRingHom (algebraMap K F)) (generator E).denom)
⊢ (generator E).num.natDegree = 0
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
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))
isUnit₁ : IsUnit (Polynomial.C ((aeval α) (f E)))
isUnit₂ : IsUnit (Polynomial.C ((aeval α) (g E)))
isCoprime :
  IsCoprime ((Polynomial.mapRingHom (algebraMap K F)) (generator E).num)
    ((Polynomial.mapRingHom (algebraMap K F)) (generator E).denom)
this✝ : Associated ((Polynomial.mapRingHom (algebraMap K F)) (f E)) ((Polynomial.mapRingHom (algebraMap K F)) (g E))
this :
  IsUnit ((Polynomial.mapRingHom (algebraMap K F)) (generator E).num) ∧
    IsUnit ((Polynomial.mapRingHom (algebraMap K F)) (generator E).denom)
⊢ (generator E).denom.natDegree = 0

Tactic:
simpa using

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
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))
isUnit₁ : IsUnit (Polynomial.C ((aeval α) (f E)))
isUnit₂ : IsUnit (Polynomial.C ((aeval α) (g E)))
isCoprime :
  IsCoprime ((Polynomial.mapRingHom (algebraMap K F)) (generator E).num)
    ((Polynomial.mapRingHom (algebraMap K F)) (generator E).denom)
this✝ : Associated ((Polynomial.mapRingHom (algebraMap K F)) (f E)) ((Polynomial.mapRingHom (algebraMap K F)) (g E))
this :
  IsUnit ((Polynomial.mapRingHom (algebraMap K F)) (generator E).num) ∧
    IsUnit ((Polynomial.mapRingHom (algebraMap K F)) (generator E).denom)
⊢ (generator E).denom.natDegree = 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
⊢ s.direction.orthogonalProjectionOnto (p -ᵥ ↑((orthogonalProjection s) p)) = 0

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ p -ᵥ ↑((orthogonalProjection s) p) ∈ 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
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ s.direction.orthogonalProjectionOnto (p -ᵥ ↑((orthogonalProjection s) p)) = 0

Tactic:
by
  simpa using vsub_orthogonalProjection_mem_direction_orthogonal _ _

Goal state after: