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

Goal state before:
pp: K : Type u
inst✝³ : Field K
n : ℕ
hζ✝ : (primitiveRoots n K).Nonempty
a : K
H✝ : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα✝ : α ^ n = (algebraMap K L) a
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (X ^ n - C a)
hα : α ^ n = (algebraMap K L) a
this✝ : Fact (Irreducible (X ^ n - C a))
this : IsSplittingField K K[n√a] (X ^ n - C a) := isSplittingField_AdjoinRoot_X_pow_sub_C hζ H
⊢ (liftAlgHom (X ^ n - C a) (Algebra.ofId K L) α ⋯).range = ⊤

Tactic:
← IsSplittingField.adjoin_rootSet _ (X ^ n - C a),

Goal state after:
K : Type u
inst✝³ : Field K
n : ℕ
hζ✝ : (primitiveRoots n K).Nonempty
a : K
H✝ : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα✝ : α ^ n = (algebraMap K L) a
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (X ^ n - C a)
hα : α ^ n = (algebraMap K L) a
this✝ : Fact (Irreducible (X ^ n - C a))
this : IsSplittingField K K[n√a] (X ^ n - C a) := isSplittingField_AdjoinRoot_X_pow_sub_C hζ H
⊢ (liftAlgHom (X ^ n - C a) (Algebra.ofId K L) α ⋯).range = Algebra.adjoin K ((X ^ n - C a).rootSet L)
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case adjoin_rootSet'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ α ∈ (X ^ finrank K L - C a).rootSet L

Tactic:
mem_rootSet_of_ne (X_pow_sub_C_ne_zero finrank_pos a),

Goal state after:
case adjoin_rootSet'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ (aeval α) (X ^ finrank K L - C a) = 0
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
m : F
a : K
E : IntermediateField F K := F⟮a⟯
this : FiniteDimensional F ↥F⟮a⟯
ha : a ∈ E
hma : m • a ∈ E
a' : ↥E := ⟨a, ha⟩
ma' : ↥E := ⟨m • a, hma⟩
⊢ normalizedTraceAux F K (m • a) = m • normalizedTraceAux F (↥E) a'

Tactic:
normalizedTraceAux_intermediateField F K ma',

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
m : F
a : K
E : IntermediateField F K := F⟮a⟯
this : FiniteDimensional F ↥F⟮a⟯
ha : a ∈ E
hma : m • a ∈ E
a' : ↥E := ⟨a, ha⟩
ma' : ↥E := ⟨m • a, hma⟩
⊢ normalizedTraceAux F (↥E) ma' = m • normalizedTraceAux F (↥E) a'
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A B : Subalgebra R S
f : S →ₐ[R] T
x✝ : ↥A
⊢ ((((map f A).mulMap (map f B)).comp
            (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f))).comp
        Algebra.TensorProduct.includeLeft)
      x✝ =
    ((f.comp (A.mulMap B)).comp Algebra.TensorProduct.includeLeft) x✝

pp: case hb
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A B : Subalgebra R S
f : S →ₐ[R] T
x✝ : ↥B
⊢ ((AlgHom.restrictScalars R
            (((map f A).mulMap (map f B)).comp
              (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f)))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R (f.comp (A.mulMap B))).comp Algebra.TensorProduct.includeRight) x✝

Tactic:
<;>

Goal state after:
case ha
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A B : Subalgebra R S
f : S →ₐ[R] T
x✝ : ↥A
⊢ ((((map f A).mulMap (map f B)).comp
            (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f))).comp
        Algebra.TensorProduct.includeLeft)
      x✝ =
    ((f.comp (A.mulMap B)).comp Algebra.TensorProduct.includeLeft) x✝

case hb
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A B : Subalgebra R S
f : S →ₐ[R] T
x✝ : ↥B
⊢ ((AlgHom.restrictScalars R
            (((map f A).mulMap (map f B)).comp
              (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f)))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R (f.comp (A.mulMap B))).comp Algebra.TensorProduct.includeRight) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
x✝ : ↥B
⊢ ((B.mulMap A).comp Algebra.TensorProduct.includeLeft) x✝ =
    (((A.mulMap B).comp ↑(Algebra.TensorProduct.comm R ↥B ↥A)).comp Algebra.TensorProduct.includeLeft) x✝

pp: case hb
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
x✝ : ↥A
⊢ ((AlgHom.restrictScalars R (B.mulMap A)).comp Algebra.TensorProduct.includeRight) x✝ =
    ((AlgHom.restrictScalars R ((A.mulMap B).comp ↑(Algebra.TensorProduct.comm R ↥B ↥A))).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
<;>

Goal state after:
case ha
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
x✝ : ↥B
⊢ ((B.mulMap A).comp Algebra.TensorProduct.includeLeft) x✝ =
    (((A.mulMap B).comp ↑(Algebra.TensorProduct.comm R ↥B ↥A)).comp Algebra.TensorProduct.includeLeft) x✝

case hb
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
x✝ : ↥A
⊢ ((AlgHom.restrictScalars R (B.mulMap A)).comp Algebra.TensorProduct.includeRight) x✝ =
    ((AlgHom.restrictScalars R ((A.mulMap B).comp ↑(Algebra.TensorProduct.comm R ↥B ↥A))).comp
        Algebra.TensorProduct.includeRight)
      x✝
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
x✝ : ∃ n, i x ^ ringExpChar F ^ n ∈ (algebraMap F K).range
n : ℕ
y : F
h : (algebraMap F K) y = i x ^ ringExpChar F ^ n
⊢ (algebraMap F E) y = x ^ ringExpChar F ^ n

pp: case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
x✝ : ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F E).range
n : ℕ
y : F
h : (algebraMap F E) y = x ^ ringExpChar F ^ n
⊢ (algebraMap F K) y = i x ^ ringExpChar F ^ n

Tactic:
· apply_fun i using i.injective
    rwa [AlgHom.commutes, map_pow]

Goal state after:
case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
x✝ : ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F E).range
n : ℕ
y : F
h : (algebraMap F E) y = x ^ ringExpChar F ^ n
⊢ (algebraMap F K) y = i x ^ ringExpChar F ^ n
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
H :
  ∀ (K : Type (max v w)) [inst : Field K] [inst_1 : Algebra F K] (fa : A →ₐ[F] K) (fb : B →ₐ[F] K),
    fa.fieldRange.LinearDisjoint ↥fb.fieldRange
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
⊢ M = ⊥

Tactic:
let K : Type (max v w) := A ⊗[F] B ⧸ M

Goal state after:
F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
H :
  ∀ (K : Type (max v w)) [inst : Field K] [inst_1 : Algebra F K] (fa : A →ₐ[F] K) (fb : B →ₐ[F] K),
    fa.fieldRange.LinearDisjoint ↥fb.fieldRange
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
⊢ M = ⊥
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: case ha
F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
this : Field K := Ideal.Quotient.field M
i : A ⊗[F] B →ₐ[F] K := IsScalarTower.toAlgHom F (A ⊗[F] B) K
fa : A →ₐ[F] K := i.comp Algebra.TensorProduct.includeLeft
fb : B →ₐ[F] K := i.comp Algebra.TensorProduct.includeRight
H : Function.Injective ⇑(fa.range.mulMap fb.range)
x✝ : A
⊢ (i.comp Algebra.TensorProduct.includeLeft) x✝ =
    (((fa.range.mulMap fb.range).comp
            ↑(Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa ⋯) (AlgEquiv.ofInjective fb ⋯))).comp
        Algebra.TensorProduct.includeLeft)
      x✝

pp: case hb
F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
this : Field K := Ideal.Quotient.field M
i : A ⊗[F] B →ₐ[F] K := IsScalarTower.toAlgHom F (A ⊗[F] B) K
fa : A →ₐ[F] K := i.comp Algebra.TensorProduct.includeLeft
fb : B →ₐ[F] K := i.comp Algebra.TensorProduct.includeRight
H : Function.Injective ⇑(fa.range.mulMap fb.range)
x✝ : B
⊢ ((AlgHom.restrictScalars F i).comp Algebra.TensorProduct.includeRight) x✝ =
    ((AlgHom.restrictScalars F
            ((fa.range.mulMap fb.range).comp
              ↑(Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa ⋯) (AlgEquiv.ofInjective fb ⋯)))).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
<;>

Goal state after:
case ha
F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
this : Field K := Ideal.Quotient.field M
i : A ⊗[F] B →ₐ[F] K := IsScalarTower.toAlgHom F (A ⊗[F] B) K
fa : A →ₐ[F] K := i.comp Algebra.TensorProduct.includeLeft
fb : B →ₐ[F] K := i.comp Algebra.TensorProduct.includeRight
H : Function.Injective ⇑(fa.range.mulMap fb.range)
x✝ : A
⊢ (i.comp Algebra.TensorProduct.includeLeft) x✝ =
    (((fa.range.mulMap fb.range).comp
            ↑(Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa ⋯) (AlgEquiv.ofInjective fb ⋯))).comp
        Algebra.TensorProduct.includeLeft)
      x✝

case hb
F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
this : Field K := Ideal.Quotient.field M
i : A ⊗[F] B →ₐ[F] K := IsScalarTower.toAlgHom F (A ⊗[F] B) K
fa : A →ₐ[F] K := i.comp Algebra.TensorProduct.includeLeft
fb : B →ₐ[F] K := i.comp Algebra.TensorProduct.includeRight
H : Function.Injective ⇑(fa.range.mulMap fb.range)
x✝ : B
⊢ ((AlgHom.restrictScalars F i).comp Algebra.TensorProduct.includeRight) x✝ =
    ((AlgHom.restrictScalars F
            ((fa.range.mulMap fb.range).comp
              ↑(Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa ⋯) (AlgEquiv.ofInjective fb ⋯)))).comp
        Algebra.TensorProduct.includeRight)
      x✝
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: case pos
K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x = 0
⊢ x⁻¹.intDegree = -x.intDegree

pp: case neg
K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : ¬x = 0
⊢ x⁻¹.intDegree = -x.intDegree

Tactic:
<;>

Goal state after:
case pos
K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x = 0
⊢ x⁻¹.intDegree = -x.intDegree

case neg
K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : ¬x = 0
⊢ x⁻¹.intDegree = -x.intDegree
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: case hx
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ x ≠ 0

pp: case hy
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ y⁻¹ ≠ 0

Tactic:
<;>

Goal state after:
case hx
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ x ≠ 0

case hy
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ y⁻¹ ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ ↑(x.num * y.denom + x.denom * y.num).natDegree - ↑(x.denom * y.denom).natDegree ≤
    max (↑(x.num * y.denom).natDegree - ↑(x.denom * y.denom).natDegree) y.intDegree

Tactic:
←
    natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree hy x.denom_ne_zero,

Goal state after:
case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ ↑(x.num * y.denom + x.denom * y.num).natDegree - ↑(x.denom * y.denom).natDegree ≤
    max (↑(x.num * y.denom).natDegree - ↑(x.denom * y.denom).natDegree)
      (↑(y.num * x.denom).natDegree - ↑(x.denom * y.denom).natDegree)
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: case e_a.e_f
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num - Polynomial.C Polynomial.X * Polynomial.map (algebraMap K K[X]) f.denom
⊢ (↑(aeval ⟨f, ⋯⟩)).comp Polynomial.C = algebraMap K ↥K[f]

pp: case e_a.e_a
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num - Polynomial.C Polynomial.X * Polynomial.map (algebraMap K K[X]) f.denom
⊢ Polynomial.map ((↑(aeval ⟨f, ⋯⟩)).comp Polynomial.C) f.denom = Polynomial.map (algebraMap K ↥K[f]) f.denom

Tactic:
<;>

Goal state after:
case e_a.e_f
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num - Polynomial.C Polynomial.X * Polynomial.map (algebraMap K K[X]) f.denom
⊢ (↑(aeval ⟨f, ⋯⟩)).comp Polynomial.C = algebraMap K ↥K[f]

case e_a.e_a
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num - Polynomial.C Polynomial.X * Polynomial.map (algebraMap K K[X]) f.denom
⊢ Polynomial.map ((↑(aeval ⟨f, ⋯⟩)).comp Polynomial.C) f.denom = Polynomial.map (algebraMap K ↥K[f]) f.denom
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: case e_a.e_f
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := ⋯
φ : K[X][X] := ⋯
x✝ : K
⊢ ↑(((↑(aeval ⟨f, ⋯⟩)).comp Polynomial.C) x✝) = ↑((algebraMap K ↥K[f]) x✝)

pp: case e_a.e_a
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := ⋯
φ : K[X][X] := ⋯
n✝ : ℕ
⊢ ↑((Polynomial.map ((↑(aeval ⟨f, ⋯⟩)).comp Polynomial.C) f.denom).coeff n✝) =
    ↑((Polynomial.map (algebraMap K ↥K[f]) f.denom).coeff n✝)

Tactic:
<;>

Goal state after:
case e_a.e_f
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := ⋯
φ : K[X][X] := ⋯
x✝ : K
⊢ ↑(((↑(aeval ⟨f, ⋯⟩)).comp Polynomial.C) x✝) = ↑((algebraMap K ↥K[f]) x✝)

case e_a.e_a
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := ⋯
φ : K[X][X] := ⋯
n✝ : ℕ
⊢ ↑((Polynomial.map ((↑(aeval ⟨f, ⋯⟩)).comp Polynomial.C) f.denom).coeff n✝) =
    ↑((Polynomial.map (algebraMap K ↥K[f]) f.denom).coeff n✝)
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ ∃ i, (φ E).coeff i ∉ (algebraMap K ↥E).range

Tactic:
rw [← notMem_map_range]
  intro ⟨f, hf⟩
  rw [coe_mapRingHom] at hf
  refine transcendental_X ⟨f, ?_, ?_⟩
  · apply (Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective K E)).mp
    exact hf ▸ φ_ne_zero h
  · simpa using congr(aeval (X : K⟮X⟯) $(hf))

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

Goal state before:
pp: case mpr
𝕜 : 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 ∈ s → ↑((orthogonalProjection s) p) = p

Tactic:
· intro h
    have hp : p ∈ (s : Set P) ∩ mk' p s.directionᗮ := ⟨h, self_mem_mk' p _⟩
    rw [inter_eq_singleton_orthogonalProjection p] at hp
    symm
    exact hp

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

Goal state before:
pp: case zero
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : NeZero 0
s : Simplex ℝ P 0
i : Fin (0 + 1)
h :
  finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))
this : 0 ≠ 0
⊢ 0 - 1 + 1 = 0

pp: case succ
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
s : Simplex ℝ P (n✝ + 1)
i : Fin (n✝ + 1 + 1)
h :
  finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))
this : n✝ + 1 ≠ 0
⊢ n✝ + 1 - 1 + 1 = n✝ + 1

Tactic:
<;>

Goal state after:
case zero
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : NeZero 0
s : Simplex ℝ P 0
i : Fin (0 + 1)
h :
  finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))
this : 0 ≠ 0
⊢ 0 - 1 + 1 = 0

case succ
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
s : Simplex ℝ P (n✝ + 1)
i : Fin (n✝ + 1 + 1)
h :
  finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))
this : n✝ + 1 ≠ 0
⊢ n✝ + 1 - 1 + 1 = n✝ + 1
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case mp
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
⊢ vectorSpan ℝ {p, s.points i} = (s.altitude i).direction →
    p ≠ s.points i ∧
      p -ᵥ s.points i ∈ vectorSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ

pp: case mpr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
⊢ p ≠ s.points i ∧
      p -ᵥ s.points i ∈ vectorSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ →
    vectorSpan ℝ {p, s.points i} = (s.altitude i).direction

Tactic:
· intro h
    constructor
    · intro heq
      rw [heq, Set.pair_eq_singleton, vectorSpan_singleton] at h
      have hd : finrank ℝ (s.altitude i).direction = 0 := by rw [← h, finrank_bot]
      simp at hd
    · rw [← Submodule.mem_inf, _root_.inf_comm, ← direction_altitude, ← h]
      exact
        vsub_mem_vectorSpan ℝ (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_singleton _))

Goal state after:
case mpr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
⊢ p ≠ s.points i ∧
      p -ᵥ s.points i ∈ vectorSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ →
    vectorSpan ℝ {p, s.points i} = (s.altitude i).direction
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : x = 0
⊢ o.oangle ((o.rotation θ) x) ((o.rotation θ) y) = o.oangle x y

pp: case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : ¬x = 0
⊢ o.oangle ((o.rotation θ) x) ((o.rotation θ) y) = o.oangle x y

Tactic:
<;>

Goal state after:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : x = 0
⊢ o.oangle ((o.rotation θ) x) ((o.rotation θ) y) = o.oangle x y

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : ¬x = 0
⊢ o.oangle ((o.rotation θ) x) ((o.rotation θ) y) = o.oangle x y
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case pos
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
⊢ 2 • o.oangle (-x) x = 0

pp: case neg
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
⊢ 2 • o.oangle (-x) x = 0

Tactic:
<;>

Goal state after:
case pos
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
⊢ 2 • o.oangle (-x) x = 0

case neg
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
⊢ 2 • o.oangle (-x) x = 0
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case pos
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
⊢ 2 • o.oangle x (-x) = 0

pp: case neg
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
⊢ 2 • o.oangle x (-x) = 0

Tactic:
<;>

Goal state after:
case pos
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
⊢ 2 • o.oangle x (-x) = 0

case neg
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
⊢ 2 • o.oangle x (-x) = 0