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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ∃ c, f = C c
⊢ Module.finrank (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree

pp: case neg
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
⊢ Module.finrank (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ∃ c, f = C c
⊢ Module.finrank (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: case refine_1
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

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

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

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
⊢ (aeval X) f = 0
Module: Mathlib.FieldTheory.RatFunc.Luroth

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

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

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E = ⊥
⊢ generator E ∈ E
Module: Mathlib.FieldTheory.RatFunc.Luroth

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

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
⊢ generator E ∈ E
Module: Mathlib.FieldTheory.RatFunc.Valuation

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : x = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree

pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree

Tactic:
·

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : x = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree
Module: Mathlib.FieldTheory.RatFunc.Valuation

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree

Tactic:
·

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree
Module: Mathlib.FieldTheory.RatFunc.Valuation

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree

pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree

Tactic:
·

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree
Module: Mathlib.FieldTheory.RatFunc.Valuation

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree

Tactic:
·

Goal state after:
case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree
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).content ≠ 0

Tactic:
·

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (algebraMap K[X] K⟮X⟯) (Φ' E).content ≠ 0
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
h3 : A ≤ C
⊢ A.relrank B * B.relrank C = A.relrank C

Tactic:
relrank_eq_rank_of_le h1,

Goal state after:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
⊢ Module.rank ↥A ↥(extendScalars h1) * B.relrank C = A.relrank C
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
h3 : A ≤ C
⊢ A.relrank B * B.relrank C = A.relrank C

Tactic:
rw [relrank_eq_rank_of_le h1, relrank_eq_rank_of_le h2, relrank_eq_rank_of_le h3]

Goal state after:
E : Type v
inst✝ : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case mem_of_smul_add_mem.refine_1
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₂
x✝ y✝ : M
a✝ : R
xc₁ : x✝ ∈ C₁
xc₂ : x✝ ∈ C₂
yc₁ : y✝ ∈ C₁
yc₂ : y✝ ∈ C₂
a0 : 0 < a✝
hz₁ : a✝ • x✝ + y✝ ∈ F₁
hz₂ : a✝ • x✝ + y✝ ∈ F₂
⊢ x✝ ∈ F₁

pp: case mem_of_smul_add_mem.refine_2
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₂
x✝ y✝ : M
a✝ : R
xc₁ : x✝ ∈ C₁
xc₂ : x✝ ∈ C₂
yc₁ : y✝ ∈ C₁
yc₂ : y✝ ∈ C₂
a0 : 0 < a✝
hz₁ : a✝ • x✝ + y✝ ∈ F₁
hz₂ : a✝ • x✝ + y✝ ∈ F₂
⊢ x✝ ∈ F₂

Tactic:
·

Goal state after:
case mem_of_smul_add_mem.refine_1
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₂
x✝ y✝ : M
a✝ : R
xc₁ : x✝ ∈ C₁
xc₂ : x✝ ∈ C₂
yc₁ : y✝ ∈ C₁
yc₂ : y✝ ∈ C₂
a0 : 0 < a✝
hz₁ : a✝ • x✝ + y✝ ∈ F₁
hz₂ : a✝ • x✝ + y✝ ∈ F₂
⊢ x✝ ∈ F₁
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case mem_of_smul_add_mem.refine_2
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₂
x✝ y✝ : M
a✝ : R
xc₁ : x✝ ∈ C₁
xc₂ : x✝ ∈ C₂
yc₁ : y✝ ∈ C₁
yc₂ : y✝ ∈ C₂
a0 : 0 < a✝
hz₁ : a✝ • x✝ + y✝ ∈ F₁
hz₂ : a✝ • x✝ + y✝ ∈ F₂
⊢ x✝ ∈ F₂

Tactic:
·

Goal state after:
case mem_of_smul_add_mem.refine_2
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₂
x✝ y✝ : M
a✝ : R
xc₁ : x✝ ∈ C₁
xc₂ : x✝ ∈ C₂
yc₁ : y✝ ∈ C₁
yc₂ : y✝ ∈ C₂
a0 : 0 < a✝
hz₁ : a✝ • x✝ + y✝ ∈ F₁
hz₂ : a✝ • x✝ + y✝ ∈ F₂
⊢ x✝ ∈ F₂
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 ⊆ (convexHull R) s

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

Goal state after:
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 ⊆ (convexHull R) s
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:
·

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

Goal state before:
pp: case h₁
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (f E).natDegree ≤ (Φ E).support.sup fun i ↦ ((Φ E).coeff i).natDegree

pp: case h₂
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (g E).natDegree ≤ (Φ E).support.sup fun i ↦ ((Φ E).coeff i).natDegree

Tactic:
·

Goal state after:
case h₁
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (f E).natDegree ≤ (Φ E).support.sup fun i ↦ ((Φ E).coeff i).natDegree
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: case h₂
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (g E).natDegree ≤ (Φ E).support.sup fun i ↦ ((Φ E).coeff i).natDegree

Tactic:
·

Goal state after:
case h₂
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (g E).natDegree ≤ (Φ E).support.sup fun i ↦ ((Φ E).coeff i).natDegree
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: case ha
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E) / c E) ≠ 0

pp: case hb
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) ≠ 0

Tactic:
·

Goal state after:
case ha
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E) / c E) ≠ 0
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:
subset_antisymm_iff,

Goal state after:
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) ∧ (convexHull R) (f '' s) ⊆ f '' (convexHull R) s
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: case hb
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) ≠ 0

Tactic:
·

Goal state after:
case hb
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: case e'_4.e'_3
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (f E).natDegree = (Polynomial.C (g E) * Polynomial.map Polynomial.C (f E)).natDegree

pp: case e'_4.e'_4
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (g E).natDegree = (Polynomial.C (f E) * Polynomial.map Polynomial.C (g E)).natDegree

Tactic:
·

Goal state after:
case e'_4.e'_3
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (f E).natDegree = (Polynomial.C (g E) * Polynomial.map Polynomial.C (f E)).natDegree
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: case e'_4.e'_4
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (g E).natDegree = (Polynomial.C (f E) * Polynomial.map Polynomial.C (g E)).natDegree

Tactic:
·

Goal state after:
case e'_4.e'_4
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (g E).natDegree = (Polynomial.C (f E) * Polynomial.map Polynomial.C (g E)).natDegree
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
i : ι
hs : c i • f i + ∑ x ∈ Finset.univ \ {i}, c x • f x ∈ F
hci : 0 < c i
⊢ f i ∈ F

pp: case h
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
⊢ i ∉ Finset.univ → c i • f i = 0

Tactic:
·

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
ι : Type u_4
inst✝ : Fintype ι
f : ι → M
c : ι → R
hF : F.IsFaceOf C
hsC : ∀ (i : ι), f i ∈ C
hc : ∀ (i : ι), 0 ≤ c i
i : ι
hs : c i • f i + ∑ x ∈ Finset.univ \ {i}, c x • f x ∈ F
hci : 0 < c i
⊢ f i ∈ 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
h : A ≤ B
⊢ Module.rank F ↥A * A.relrank B = Module.rank F ↥B

Tactic:
by
  rw [relrank_eq_rank_of_le h]
  let : Algebra A B := (inclusion h).toAlgebra
  exact rank_mul_rank F A B

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

Goal state before:
pp: case h
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
⊢ i ∉ Finset.univ → c i • f i = 0

Tactic:
·

Goal state after:
case h
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
⊢ i ∉ Finset.univ → c i • f i = 0
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case refine_1
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
hF : ∀ {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
x : M
xf : x ∈ F
⊢ x ∈ C

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 : M →ₗ[R] N
hf : Function.Injective ⇑f
sub : map f F ≤ map f C
hF : ∀ {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
x✝ y✝ : M
a✝ : R
hx : x✝ ∈ C
hy : y✝ ∈ C
ha : 0 < a✝
h : a✝ • x✝ + y✝ ∈ F
⊢ x✝ ∈ F

Tactic:
·

Goal state after:
case refine_1
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
hF : ∀ {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
x : M
xf : x ∈ F
⊢ x ∈ C
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 : M →ₗ[R] N
hf : Function.Injective ⇑f
sub : map f F ≤ map f C
hF : ∀ {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
x✝ y✝ : M
a✝ : R
hx : x✝ ∈ C
hy : y✝ ∈ C
ha : 0 < a✝
h : a✝ • x✝ + y✝ ∈ F
⊢ x✝ ∈ F

Tactic:
·

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 : M →ₗ[R] N
hf : Function.Injective ⇑f
sub : map f F ≤ map f C
hF : ∀ {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
x✝ y✝ : M
a✝ : R
hx : x✝ ∈ C
hy : y✝ ∈ C
ha : 0 < a✝
h : a✝ • x✝ + y✝ ∈ F
⊢ x✝ ∈ F
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case refine_1
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 : M
xF : x ∈ F
⊢ x ∈ C

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 : x ∈ C
yC : y ∈ C
a0 : 0 < x✝
h : x✝ • x + y ∈ F
⊢ x ∈ F

Tactic:
·

Goal state after:
case refine_1
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 : M
xF : x ∈ F
⊢ x ∈ C
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 : x ∈ C
yC : y ∈ C
a0 : 0 < x✝
h : x✝ • x + y ∈ F
⊢ x ∈ F

Tactic:
·

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 : x ∈ C
yC : y ∈ C
a0 : 0 < x✝
h : x✝ • x + y ∈ F
⊢ x ∈ F
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case refine_1
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
hF : F.IsFaceOf C
x✝¹ : M
x✝ : x✝¹ ∈ C.lineal
hx : x✝¹ ∈ ↑C.toAddSubmonoid
hx' : x✝¹ ∈ ↑(-C.toAddSubmonoid)
⊢ x✝¹ ∈ ↑F.toAddSubmonoid

pp: case refine_2
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
hF : F.IsFaceOf C
x✝¹ : M
x✝ : x✝¹ ∈ C.lineal
hx : x✝¹ ∈ ↑C.toAddSubmonoid
hx' : x✝¹ ∈ ↑(-C.toAddSubmonoid)
⊢ x✝¹ ∈ ↑(-F.toAddSubmonoid)

Tactic:
·

Goal state after:
case refine_1
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
hF : F.IsFaceOf C
x✝¹ : M
x✝ : x✝¹ ∈ C.lineal
hx : x✝¹ ∈ ↑C.toAddSubmonoid
hx' : x✝¹ ∈ ↑(-C.toAddSubmonoid)
⊢ x✝¹ ∈ ↑F.toAddSubmonoid
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case refine_2
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
hF : F.IsFaceOf C
x✝¹ : M
x✝ : x✝¹ ∈ C.lineal
hx : x✝¹ ∈ ↑C.toAddSubmonoid
hx' : x✝¹ ∈ ↑(-C.toAddSubmonoid)
⊢ x✝¹ ∈ ↑(-F.toAddSubmonoid)

Tactic:
·

Goal state after:
case refine_2
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
hF : F.IsFaceOf C
x✝¹ : M
x✝ : x✝¹ ∈ C.lineal
hx : x✝¹ ∈ ↑C.toAddSubmonoid
hx' : x✝¹ ∈ ↑(-C.toAddSubmonoid)
⊢ x✝¹ ∈ ↑(-F.toAddSubmonoid)
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case le
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₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
⊢ map (LinearMap.fst R M N) F ≤ C₁

pp: case mem_of_smul_add_mem
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₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
⊢ ∀ {x y : M} {a : R},
    x ∈ C₁ → y ∈ C₁ → 0 < a → a • x + y ∈ map (LinearMap.fst R M N) F → x ∈ map (LinearMap.fst R M N) F

Tactic:
·

Goal state after:
case le
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₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
⊢ map (LinearMap.fst R M N) F ≤ C₁
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case mem_of_smul_add_mem
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₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
⊢ ∀ {x y : M} {a : R},
    x ∈ C₁ → y ∈ C₁ → 0 < a → a • x + y ∈ map (LinearMap.fst R M N) F → x ∈ map (LinearMap.fst R M N) F

Tactic:
·

Goal state after:
case mem_of_smul_add_mem
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₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
⊢ ∀ {x y : M} {a : R},
    x ∈ C₁ → y ∈ C₁ → 0 < a → a • x + y ∈ map (LinearMap.fst R M N) F → x ∈ map (LinearMap.fst R M N) F