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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
m : ℤ
⊢ (inftyValuation F) (RatFunc.X ^ m) = exp m

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
⊢ (inftyValuation F) (1 / RatFunc.X) = exp (-1)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
p : F[X]
hp : p ≠ 0
⊢ ¬(algebraMap F[X] F⟮X⟯) p = 0

Tactic:
by

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 ≠ ⊥
⊢ (Φ E).natDegree = (φ E).natDegree

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
p : F[X]
hp : p ≠ 0
⊢ inftyValuationDef F ((algebraMap F[X] F⟮X⟯) p) = exp ↑p.natDegree

Tactic:
by

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : DecidableEq F⟮X⟯
⊢ (inftyValuation F) X ≠ 0 ∧ (inftyValuation F) X ≠ 1

Tactic:
by

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : DecidableEq F⟮X⟯
x✝ : F
hx : x✝ ≠ 0
⊢ (inftyValuation F) ((algebraMap F F⟮X⟯) x✝) = 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
⊢ A.relrank B * B.relrank C = A.relrank C

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
⊢ A.relfinrank B * B.relfinrank C = A.relfinrank C

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : PartialOrder R
inst✝³ : Semiring R
inst✝² : IsStrictOrderedRing R
X : Type u_2
Y : Type u_3
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
x✝¹ x✝ : ConvexSpace.AffineMap R X Y
f : X → Y
isAffineMap_toFun✝¹ : IsAffineMap R f
g : X → Y
isAffineMap_toFun✝ : IsAffineMap R g
h :
  { toFun := f, isAffineMap_toFun := isAffineMap_toFun✝¹ }.toFun =
    { toFun := g, isAffineMap_toFun := isAffineMap_toFun✝ }.toFun
⊢ { toFun := f, isAffineMap_toFun := isAffineMap_toFun✝¹ } = { toFun := g, isAffineMap_toFun := isAffineMap_toFun✝ }

Tactic:
by

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 ≠ ⊥
⊢ (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (φ E).natDegree) = c E

Tactic:
by

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 ≠ ⊥
⊢ (c E).denom = 1

Tactic:
by

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 ≠ ⊥
⊢ (Φ E).coeff (φ E).natDegree = (c E).num

Tactic:
by

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 ≠ ⊥
⊢ (Φ E).coeff (φ E).natDegree ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
x y : M
a b : R
hF : F.IsFaceOf C
hx : x ∈ C
hy : y ∈ C
ha : 0 < a
hb : 0 < b
h : a • x + b • y ∈ F
⊢ y ∈ F

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
h : F.IsFaceOf C
⊢ IsExtreme R ↑C ↑F

Tactic:
by

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 ≠ ⊥
⊢ (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) = (algebraMap K[X] K⟮X⟯) (c E).num * generator E

Tactic:
by

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 ≠ ⊥
⊢ (Φ E).coeff (generatorIndex h) ≠ 0

Tactic:
by

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

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 ≠ ⊥
⊢ Φ E ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Relrank

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

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Relrank

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

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.FieldTheory.Relrank

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C₁ C₂ F₁ F₂ : PointedCone R M
h₁ : F₁.IsFaceOf C₁
h₂ : F₂.IsFaceOf C₂
⊢ (F₁ ⊓ F₂).IsFaceOf (C₁ ⊓ C₂)

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (f E).natDegree ≤ ((Φ E).coeff (generatorIndex h)).natDegree

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Relrank

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

Tactic:
by

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).natDegree ≤ ((Φ E).coeff (φ E).natDegree).natDegree

Tactic:
by

Goal state after:
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 t : Set X
⊢ t ⊆ (convexHull R) s ↔ ∀ (C : Set X), s ⊆ C → IsConvexSet R C → t ⊆ C

Tactic:
by

Goal state after:
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
⊢ (convexHull R) s = ⋂ t, ⋂ (_ : s ⊆ t), ⋂ (_ : IsConvexSet R t), t

Tactic:
by

Goal state after:
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

Goal state after:
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
⊢ (A ⊓ B).relrank A = B.relrank A

Tactic:
by

Goal state after:
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
C : Set X
⊢ (convexHull R) C ⊆ C ↔ IsConvexSet R C

Tactic:
by

Goal state after:
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
⊢ (convexHull R) s = ∅ ↔ s = ∅

Tactic:
by

Goal state after:
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
⊢ ((convexHull R) s).Nonempty ↔ s.Nonempty

Tactic:
by

Goal state after:
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:
by

Goal state after:
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 : IntermediateField F E
f : L →ₐ[F] E
⊢ finrank (↥(comap f A)) L = A.relfinrank f.fieldRange

Tactic:
by

Goal state after:
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:
by

Goal state after:
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 : IntermediateField F E
f : L →ₐ[F] E
B : IntermediateField F L
⊢ (comap f A).relfinrank B = A.relfinrank (map f B)

Tactic:
by

Goal state after:
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
hs : (convexHull R) s = {x}
⊢ s.Nonempty

Tactic:
by_contra! hs
      simp_all [eq_comm (a := ∅)]

Goal state after:
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
hs : (convexHull R) s = {x}
⊢ s = {x}

Tactic:
by

Goal state after:
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
hs : s = {x}
⊢ (convexHull R) s = {x}

Tactic:
by

Goal state after:
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 : E →ₐ[F] L
⊢ Cardinal.lift.{v, w} ((map f A).relrank (map f B)) = Cardinal.lift.{w, v} (A.relrank B)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C : PointedCone R M
F : Set (PointedCone R M)
h : ∀ f ∈ F, f.IsFaceOf C
⊢ ∀ {x y : M} {a : R}, x ∈ C → y ∈ C → 0 < a → a • x + y ∈ C ⊓ sInf F → x ∈ C ⊓ sInf F

Tactic:
by

Goal state after:
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
hs : IsConvexSet R s
hsx : IsConvexSet R (s \ {x})
hx : x ∈ (convexHull R) (s \ {x})
⊢ False

Tactic:
by

Goal state after:
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:
by

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

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

Tactic:
by

Goal state after:
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 : E →ₐ[F] L
⊢ (map f A).relfinrank (map f B) = A.relfinrank B

Tactic:
by

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 ≠ ⊥
⊢ m E ≤ (Bivariate.swap (Φ E)).natDegree

Tactic:
by

Goal state after:
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
hs : IsConvexSet R s
hx : x ∉ (convexHull R) (s \ {x})
y : X
hy : y ∈ (convexHull R) (s \ {x})
⊢ y ∉ {x}

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ φ E ∣ Polynomial.map (algebraMap ↥K⟮generator E⟯ ↥E) ((generator E).minpolyX ↥K⟮generator E⟯)

Tactic:
by

Goal state after:
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
hs : IsConvexSet R s
hx : x ∉ (convexHull R) (s \ {x})
⊢ IsConvexSet R (s \ {x})

Tactic:
by

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

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

Tactic:
by

Goal state after:
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:
by

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

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

Tactic:
by

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 ≠ ⊥
⊢ Q₀ E ≠ 0

Tactic:
by

Goal state after:
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
⊢ (comap f A).relfinrank (comap f B) = A.relfinrank (B ⊓ f.fieldRange)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ Bivariate.swap (θ E) = -θ E

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
C F : PointedCone R M
ι : Type u_4
inst✝ : Fintype ι
f : ι → M
hF : F.IsFaceOf C
hsC : ∀ (i : ι), f i ∈ C
hs : ∑ i, f i ∈ F
i : ι
⊢ f i ∈ F

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Geometry.Convex.Hull

Goal state before:
pp: R : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
hf : IsAffineMap R f
s : Set X
⊢ f '' (convexHull R) s = (convexHull R) (f '' s)

Tactic:
by

Goal state after:
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:
by

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 ≠ ⊥
⊢ (θ E).natDegree ≤ m E

Tactic:
by

Goal state after:
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
⊢ (comap f A).relfinrank (comap f B) = A.relfinrank B

Tactic:
by

Goal state after:
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:
by

Goal state after:
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 : Function.Surjective ⇑f
⊢ (comap f A).relfinrank (comap f B) = A.relfinrank B

Tactic:
by

Goal state after:
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
h : A ≤ B
⊢ A.relfinrank B * finrank (↥B) E = finrank (↥A) E

Tactic:
by

Goal state after:
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
h : A ≤ B
⊢ Module.rank F ↥A * A.relrank B = Module.rank F ↥B

Tactic:
by

Goal state after:
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
h : A ≤ B
⊢ finrank F ↥A * A.relfinrank B = finrank F ↥B

Tactic:
by

Goal state after:
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
h1 : A ≤ B
h2 : B ≤ C
⊢ A.relfinrank B * B.relfinrank C = A.relfinrank C

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
C F : PointedCone R M
ι : Type u_4
inst✝ : Fintype ι
f : ι → M
c : ι → R
hF : F.IsFaceOf C
hsC : ∀ (i : ι), f i ∈ C
hc : ∀ (i : ι), 0 ≤ c i
hs : ∑ i, c i • f i ∈ F
i : ι
hci : 0 < c i
⊢ f i ∈ F

Tactic:
by

Goal state after:
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
⊢ A.relfinrank (B ⊓ C) * B.relfinrank C = (A ⊓ B).relfinrank C

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F₁ F₂ : PointedCone R M
h₁ : F₂.IsFaceOf F₁
h₂ : F₁.IsFaceOf C
⊢ F₂.IsFaceOf C

Tactic:
by

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 :
  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)
⊢ Q₀ E * Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E) = Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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.relfinrank B * B.relfinrank C = (A ⊓ B).relfinrank C

Tactic:
by

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

Goal state before:
pp: 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 : M →ₗ[R] N
hf : Function.Injective ⇑f
hF : F.IsFaceOf C
⊢ ∀ {x y : N} {a : R}, x ∈ map f C → y ∈ map f C → 0 < a → a • x + y ∈ map f F → x ∈ map f F

Tactic:
by

Goal state after:
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:
by

Goal state after:
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.relfinrank (B ⊓ C) * B.relfinrank C = A.relfinrank C

Tactic:
by

Goal state after:
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
⊢ A.relrank ⊤ = Module.rank (↥A) E

Tactic:
by

Goal state after:
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
⊢ A.relfinrank ⊤ = finrank (↥A) E

Tactic:
by

Goal state after:
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
⊢ ⊥.relrank A = Module.rank F ↥A

Tactic:
by

Goal state after:
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
⊢ ⊥.relfinrank A = finrank F ↥A

Tactic:
by

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

Goal state before:
pp: 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 : M →ₗ[R] N
hf : Function.Injective ⇑f
sub : map f F ≤ map f C
x✝ y✝ : M
a✝ : R
hx : x✝ ∈ C
hy : y✝ ∈ C
ha : 0 < a✝
h : a✝ • x✝ + y✝ ∈ F
hF :
  ∀ {x y : N} {a : R},
    ∀ x_1 ∈ C, f x_1 = x → ∀ x_2 ∈ C, f x_2 = y → 0 < a → ∀ x_3 ∈ F, f x_3 = a • x + y → ∃ x_4 ∈ F, f x_4 = x
⊢ f (a✝ • x✝ + y✝) = a✝ • f x✝ + f y✝

Tactic:
by

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

Goal state before:
pp: 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 : M →ₗ[R] N
hf : Function.Injective ⇑f
hc : (map f F).IsFaceOf (map f C)
⊢ F.IsFaceOf C

Tactic:
by

Goal state after: