Module: Mathlib.RingTheory.Invariant.Galois

Goal state before:
pp: case intro
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Finite G
inst✝¹⁵ : Group G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝¹² : Q.LiesOver P
inst✝¹¹ : P.IsPrime
inst✝¹⁰ : Q.IsPrime
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra (A ⧸ P) K
inst✝⁵ : IsFractionRing (A ⧸ P) K
inst✝⁴ : Algebra (B ⧸ Q) L
inst✝³ : IsFractionRing (B ⧸ Q) L
inst✝² : Algebra (A ⧸ P) L
inst✝¹ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝ : IsScalarTower (A ⧸ P) K L
this✝ : Algebra.IsIntegral A B
this : Algebra.IsAlgebraic K L
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
a : A
ha : (algebraMap A (A ⧸ P)) a ≠ 0
b : B
h : (algebraMap A (A ⧸ P)) a • x = y * (algebraMap B (B ⧸ Q)) b
val✝ : Fintype G
p : A[X]
hp : Polynomial.map (algebraMap A B) p = MulSemiringAction.charpoly G b
h_monic : p.Monic
h_eval : (aeval b) p = 0
q : A[X] := p.comp (C a * X)
d : L := (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
comm₁ : (algebraMap K L).comp (algebraMap (A ⧸ P) K) = (algebraMap (B ⧸ Q) L).comp (algebraMap (A ⧸ P) (B ⧸ Q))
comm₂ : (algebraMap (A ⧸ P) (B ⧸ Q)).comp (algebraMap A (A ⧸ P)) = (algebraMap B (B ⧸ Q)).comp (algebraMap A B)
⊢ (Polynomial.map (algebraMap K L) (minpoly K ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y))).Splits

Tactic:
replace h_eval : ((q.map (algebraMap A (A ⧸ P))).map (algebraMap (A ⧸ P) K)).aeval d = 0 := by
    simp_rw [q, map_comp, Polynomial.map_mul, map_C, map_X, aeval_comp, aeval_mul, aeval_C, aeval_X,
      ← RingHom.comp_apply, ← RingHom.comp_assoc, comm₁, RingHom.comp_apply, d, mul_div, ← map_mul]
    rw [← Algebra.smul_def, h, map_mul, mul_div_cancel_left₀ _ (by simpa using hy),
      aeval_map_algebraMap, aeval_algebraMap_apply, aeval_map_algebraMap, aeval_algebraMap_apply,
      h_eval, map_zero, map_zero]

Goal state after:
case intro
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Finite G
inst✝¹⁵ : Group G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝¹² : Q.LiesOver P
inst✝¹¹ : P.IsPrime
inst✝¹⁰ : Q.IsPrime
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra (A ⧸ P) K
inst✝⁵ : IsFractionRing (A ⧸ P) K
inst✝⁴ : Algebra (B ⧸ Q) L
inst✝³ : IsFractionRing (B ⧸ Q) L
inst✝² : Algebra (A ⧸ P) L
inst✝¹ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝ : IsScalarTower (A ⧸ P) K L
this✝ : Algebra.IsIntegral A B
this : Algebra.IsAlgebraic K L
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
a : A
ha : (algebraMap A (A ⧸ P)) a ≠ 0
b : B
h : (algebraMap A (A ⧸ P)) a • x = y * (algebraMap B (B ⧸ Q)) b
val✝ : Fintype G
p : A[X]
hp : Polynomial.map (algebraMap A B) p = MulSemiringAction.charpoly G b
h_monic : p.Monic
q : A[X] := p.comp (C a * X)
d : L := (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
comm₁ : (algebraMap K L).comp (algebraMap (A ⧸ P) K) = (algebraMap (B ⧸ Q) L).comp (algebraMap (A ⧸ P) (B ⧸ Q))
comm₂ : (algebraMap (A ⧸ P) (B ⧸ Q)).comp (algebraMap A (A ⧸ P)) = (algebraMap B (B ⧸ Q)).comp (algebraMap A B)
h_eval : (aeval d) (Polynomial.map (algebraMap (A ⧸ P) K) (Polynomial.map (algebraMap A (A ⧸ P)) q)) = 0
⊢ (Polynomial.map (algebraMap K L) (minpoly K ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y))).Splits