mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : ι → ↥A
i : (ι →₀ ↥B) →ₗ[R] S := Submodule.mulLeftMap (toSubmodule B) a
j : (ι →₀ ↥B) →ₗ[R] S :=
  ↑(MulOpposite.opLinearEquiv R).symm ∘ₗ
    ↑R (Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)) ∘ₗ
      ↑(Finsupp.mapRange.linearEquiv B.linearEquivOp)
⊢ i = j

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : ι → ↥A
i : (ι →₀ ↥B) →ₗ[R] S := Submodule.mulLeftMap (toSubmodule B) a
j : (ι →₀ ↥B) →ₗ[R] S :=
  ↑(MulOpposite.opLinearEquiv R).symm ∘ₗ
    ↑R (Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)) ∘ₗ
      ↑(Finsupp.mapRange.linearEquiv B.linearEquivOp)
a✝ : ι
x✝ : ↥B
⊢ (i ∘ₗ Finsupp.lsingle a✝) x✝ = (j ∘ₗ Finsupp.lsingle a✝) x✝
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : ι → ↥B
⊢ ((toSubmodule A).mulRightMap b).ker = ⊥ ↔ LinearIndependent (↥A) (⇑B.val ∘ b)

Tactic:
LinearIndependent,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : ι → ↥B
⊢ ((toSubmodule A).mulRightMap b).ker = ⊥ ↔ Function.Injective ⇑(Finsupp.linearCombination (↥A) (⇑B.val ∘ b))
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : ι → ↥B
i : (ι →₀ ↥A) →ₗ[R] S := (toSubmodule A).mulRightMap b
j : (ι →₀ ↥A) →ₗ[R] S := ↑R (Finsupp.linearCombination (↥A) (⇑B.val ∘ b))
⊢ i = j

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : ι → ↥B
i : (ι →₀ ↥A) →ₗ[R] S := (toSubmodule A).mulRightMap b
j : (ι →₀ ↥A) →ₗ[R] S := ↑R (Finsupp.linearCombination (↥A) (⇑B.val ∘ b))
a✝ : ι
x✝ : ↥A
⊢ (i ∘ₗ Finsupp.lsingle a✝) x✝ = (j ∘ₗ Finsupp.lsingle a✝) x✝
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ carrier 0 = {0}

Tactic:
ext

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : L
⊢ x✝ ∈ carrier 0 ↔ x✝ ∈ {0}
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
c : ConjRootClass K L
⊢ (-c).carrier = -c.carrier

Tactic:
ext

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
c : ConjRootClass K L
x✝ : L
⊢ x✝ ∈ (-c).carrier ↔ x✝ ∈ -c.carrier
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : ConjRootClass K L
⊢ (∃ a, mk K a = x ∧ ∃ b, mk K b = y ∧ a + b = 0) ↔ x = -y

Tactic:
constructor

Goal state after:
case mp
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : ConjRootClass K L
⊢ (∃ a, mk K a = x ∧ ∃ b, mk K b = y ∧ a + b = 0) → x = -y

case mpr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x y : ConjRootClass K L
⊢ x = -y → ∃ a, mk K a = x ∧ ∃ b, mk K b = y ∧ a + b = 0
Module: Mathlib.FieldTheory.LinearDisjoint

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
⊢ (IsScalarTower.toAlgHom F (↥B) E).range = B.toSubalgebra

Tactic:
ext

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
x✝ : E
⊢ x✝ ∈ (IsScalarTower.toAlgHom F (↥B) E).range ↔ x✝ ∈ B.toSubalgebra
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: case e'_7
F : Type u
E : Type v
inst✝¹³ : Field F
inst✝¹² : Field E
inst✝¹¹ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint (IsScalarTower.toAlgHom F L E).range
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra L K
inst✝³ : IsScalarTower F L K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsScalarTower L E K
this :
  (Subalgebra.map (IsScalarTower.toAlgHom F E K) A.toSubalgebra).LinearDisjoint
    ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)).range
⊢ IsScalarTower.toAlgHom F L K = (IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)

Tactic:
ext

Goal state after:
case e'_7
F : Type u
E : Type v
inst✝¹³ : Field F
inst✝¹² : Field E
inst✝¹¹ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint (IsScalarTower.toAlgHom F L E).range
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra L K
inst✝³ : IsScalarTower F L K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsScalarTower L E K
this :
  (Subalgebra.map (IsScalarTower.toAlgHom F E K) A.toSubalgebra).LinearDisjoint
    ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)).range
x✝ : L
⊢ (IsScalarTower.toAlgHom F L K) x✝ = ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)) x✝
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
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this✝ : FiniteDimensional F ↥F⟮a⟯
this : FiniteDimensional F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b

Tactic:
have hab : a + b ∈ E := IntermediateField.add_mem E ha hb

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
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this✝ : FiniteDimensional F ↥F⟮a⟯
this : FiniteDimensional F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
hab : a + b ∈ E
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: case e'_6
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
inst✝¹⁵ : Algebra L E
inst✝¹⁴ : IsScalarTower F L E
L' : Type u_1
inst✝¹³ : Field L'
inst✝¹² : Algebra F L'
inst✝¹¹ : Algebra L' E
inst✝¹⁰ : IsScalarTower F L' E
H : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint (IsScalarTower.toAlgHom F L' E).range
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra F K
inst✝⁷ : Algebra L K
inst✝⁶ : IsScalarTower F L K
inst✝⁵ : Algebra L' K
inst✝⁴ : IsScalarTower F L' K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : IsScalarTower L E K
inst✝ : IsScalarTower L' E K
this :
  ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)).range.LinearDisjoint
    ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L' E)).range
⊢ IsScalarTower.toAlgHom F L K = (IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)

Tactic:
ext

Goal state after:
case e'_6
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
inst✝¹⁵ : Algebra L E
inst✝¹⁴ : IsScalarTower F L E
L' : Type u_1
inst✝¹³ : Field L'
inst✝¹² : Algebra F L'
inst✝¹¹ : Algebra L' E
inst✝¹⁰ : IsScalarTower F L' E
H : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint (IsScalarTower.toAlgHom F L' E).range
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra F K
inst✝⁷ : Algebra L K
inst✝⁶ : IsScalarTower F L K
inst✝⁵ : Algebra L' K
inst✝⁴ : IsScalarTower F L' K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : IsScalarTower L E K
inst✝ : IsScalarTower L' E K
this :
  ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)).range.LinearDisjoint
    ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L' E)).range
x✝ : L
⊢ (IsScalarTower.toAlgHom F L K) x✝ = ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)) x✝
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: case e'_7
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
inst✝¹⁵ : Algebra L E
inst✝¹⁴ : IsScalarTower F L E
L' : Type u_1
inst✝¹³ : Field L'
inst✝¹² : Algebra F L'
inst✝¹¹ : Algebra L' E
inst✝¹⁰ : IsScalarTower F L' E
H : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint (IsScalarTower.toAlgHom F L' E).range
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra F K
inst✝⁷ : Algebra L K
inst✝⁶ : IsScalarTower F L K
inst✝⁵ : Algebra L' K
inst✝⁴ : IsScalarTower F L' K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : IsScalarTower L E K
inst✝ : IsScalarTower L' E K
this :
  ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)).range.LinearDisjoint
    ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L' E)).range
⊢ IsScalarTower.toAlgHom F L' K = (IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L' E)

Tactic:
ext

Goal state after:
case e'_7
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
inst✝¹⁵ : Algebra L E
inst✝¹⁴ : IsScalarTower F L E
L' : Type u_1
inst✝¹³ : Field L'
inst✝¹² : Algebra F L'
inst✝¹¹ : Algebra L' E
inst✝¹⁰ : IsScalarTower F L' E
H : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint (IsScalarTower.toAlgHom F L' E).range
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra F K
inst✝⁷ : Algebra L K
inst✝⁶ : IsScalarTower F L K
inst✝⁵ : Algebra L' K
inst✝⁴ : IsScalarTower F L' K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : IsScalarTower L E K
inst✝ : IsScalarTower L' E K
this :
  ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)).range.LinearDisjoint
    ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L' E)).range
x✝ : L'
⊢ (IsScalarTower.toAlgHom F L' K) x✝ = ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L' E)) x✝
Module: Mathlib.FieldTheory.LinearDisjoint

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 w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint L
L' : Type u_1
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L'
inst✝⁴ : Algebra L' L
inst✝³ : IsScalarTower F L' L
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L' E
inst✝ : IsScalarTower L' L E
⊢ IsScalarTower.toAlgHom F L' E = (IsScalarTower.toAlgHom F L E).comp (IsScalarTower.toAlgHom F L' L)

Tactic:
ext

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 w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint L
L' : Type u_1
inst✝⁶ : Field L'
inst✝⁵ : Algebra F L'
inst✝⁴ : Algebra L' L
inst✝³ : IsScalarTower F L' L
inst✝² : Algebra L' E
inst✝¹ : IsScalarTower F L' E
inst✝ : IsScalarTower L' L E
x✝ : L'
⊢ (IsScalarTower.toAlgHom F L' E) x✝ = ((IsScalarTower.toAlgHom F L E).comp (IsScalarTower.toAlgHom F L' L)) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: 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
⊢ ((map f A).mulMap (map f B)).comp (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f)) =
    f.comp (A.mulMap B)

Tactic:
ext

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: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
⊢ B.mulMap A = (A.mulMap B).comp ↑(Algebra.TensorProduct.comm R ↥B ↥A)

Tactic:
ext

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.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
⊢ Function.Surjective ⇑(A.mulMap' B)

Tactic:
simp_rw [mulMap', AlgHom.coe_comp, AlgEquiv.coe_toAlgHom,
    EquivLike.comp_surjective, AlgHom.rangeRestrict_surjective]

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

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
inst✝² : IsGalois F ↥A
inst✝¹ : FiniteDimensional F ↥A
inst✝ : FiniteDimensional F ↥B
h : A ⊓ B = ⊥
C : IntermediateField F E := A ⊔ B
A' : IntermediateField F ↥C := restrict ⋯
B' : IntermediateField F ↥C := restrict ⋯
hA : IntermediateField.map C.val A' = A
hB : IntermediateField.map C.val B' = B
h₁ : A' ⊔ B' = ⊤
h₂ : A' ⊓ B' = ⊥
this : IsGalois F ↥A'
⊢ A'.LinearDisjoint ↥B'

Tactic:
exact of_inf_eq_bot_aux h₁ h₂

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

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 w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
i : L ≃ₐ[F] ↥L' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)
heq : (adjoin L ↑A).toSubsemiring = (Algebra.adjoin ↥L' ↑A).toSubsemiring
a : L
x✝ : ↥(adjoin L ↑A)
x : E
hx : x ∈ adjoin L ↑A
⊢ (RingEquiv.subsemiringCongr heq).toAddEquiv (a • ⟨x, hx⟩) = i a • (RingEquiv.subsemiringCongr heq).toAddEquiv ⟨x, hx⟩

Tactic:
ext

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 w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := ⋯
i : L ≃ₐ[F] ↥L' := ⋯
heq : (adjoin L ↑A).toSubsemiring = (Algebra.adjoin ↥L' ↑A).toSubsemiring
a : L
x✝ : ↥(adjoin L ↑A)
x : E
hx : x ∈ adjoin L ↑A
⊢ ↑((RingEquiv.subsemiringCongr heq).toAddEquiv (a • ⟨x, hx⟩)) =
    ↑(i a • (RingEquiv.subsemiringCongr heq).toAddEquiv ⟨x, hx⟩)
Module: Mathlib.FieldTheory.LinearDisjoint

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 w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := (IsScalarTower.toAlgHom F L E).range
heq : (adjoin L ↑A).toSubsemiring = (Algebra.adjoin ↥A ↑L').toSubsemiring
x✝¹ : ↥A
x✝ : ↥(extendScalars ⋯)
a : E
ha : a ∈ A
x : E
hx : x ∈ extendScalars ⋯
⊢ (RingEquiv.subsemiringCongr heq).toAddEquiv (⟨a, ha⟩ • ⟨x, hx⟩) =
    (RingHom.id ↥A) ⟨a, ha⟩ • (RingEquiv.subsemiringCongr heq).toAddEquiv ⟨x, hx⟩

Tactic:
ext

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 w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := ⋯
heq : (adjoin L ↑A).toSubsemiring = (Algebra.adjoin ↥A ↑L').toSubsemiring
x✝¹ : ↥A
x✝ : ↥(extendScalars ⋯)
a : E
ha : a ∈ A
x : E
hx : x ∈ extendScalars ⋯
⊢ ↑((RingEquiv.subsemiringCongr heq).toAddEquiv (⟨a, ha⟩ • ⟨x, hx⟩)) =
    ↑((RingHom.id ↥A) ⟨a, ha⟩ • (RingEquiv.subsemiringCongr heq).toAddEquiv ⟨x, hx⟩)
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
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)
⊢ i =
    (fa.range.mulMap fb.range).comp
      ↑(Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa ⋯) (AlgEquiv.ofInjective fb ⋯))

Tactic:
ext

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 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)

Tactic:
le_max_iff,

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 ≤
      ↑(x.num * y.denom).natDegree - ↑(x.denom * y.denom).natDegree ∨
    ↑(x.num * y.denom + x.denom * y.num).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]

Tactic:
ext

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✝)
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
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:
ext

Goal state after:
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.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
⊢ Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x

Tactic:
by
  have hi := IsSeparable.isIntegral hsep
  have hi' : IsIntegral E x := IsIntegral.tower_top hi
  refine eq_of_monic_of_dvd_of_natDegree_le (monic hi') ((monic hi).map (algebraMap F E))
    (dvd_map_of_isScalarTower F E x) (le_of_eq ?_)
  have hsep' := IsSeparable.tower_top E hsep
  have := (isSeparable_adjoin_simple_iff_isSeparable _ _).2 hsep
  have := (isSeparable_adjoin_simple_iff_isSeparable _ _).2 hsep'
  have := Algebra.IsSeparable.isAlgebraic F F⟮x⟯
  rw [Polynomial.natDegree_map, ← adjoin.finrank hi, ← adjoin.finrank hi',
    ← finSepDegree_eq_finrank_of_isSeparable F _, ← finSepDegree_eq_finrank_of_isSeparable E _,
    finSepDegree_eq, finSepDegree_eq,
    sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable (F := F) E]

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 : K
hf : (algebraMap K K⟮X⟯) f = ↑((φ E).coeff (generatorIndex h))
⊢ (algebraMap K ↥E) f = (φ E).coeff ⋯.choose

Tactic:
ext

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
f : K
hf : (algebraMap K K⟮X⟯) f = ↑((φ E).coeff (generatorIndex h))
⊢ ↑((algebraMap K ↥E) f) = ↑((φ E).coeff ⋯.choose)
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
  rw [← Φ_coeff_φ_natDegree h]
  exact denom_algebraMap _

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 ≠ ⊥
H : Φ E = 0
this : (c E).num = 0
⊢ False

Tactic:
exact num_ne_zero (c_ne_zero h) this

Goal state after: