-- Mathlib/FieldTheory/PolynomialGaloisGroup.lean
theorem restrictProd_injective : Function.Injective (restrictProd p q)

Proof state:
case neg.h.inl
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ p.aroots (p * q).SplittingField
this : Fact (Splits (algebraMap F (p * q).SplittingField) p)
key :
  x = (algebraMap p.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots p (p * q).SplittingField).invFun ⟨x, ⋯⟩)
⊢ f x = g x

Tactic:
rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]

Result:
case neg.h.inl
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ p.aroots (p * q).SplittingField
this : Fact (Splits (algebraMap F (p * q).SplittingField) p)
key :
  x = (algebraMap p.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots p (p * q).SplittingField).invFun ⟨x, ⋯⟩)
⊢ (algebraMap p.SplittingField (p * q).SplittingField)
      ((AlgEquiv.restrictNormal f p.SplittingField) ↑((rootsEquivRoots p (p * q).SplittingField).invFun ⟨x, ⋯⟩)) =
    (algebraMap p.SplittingField (p * q).SplittingField)
      ((AlgEquiv.restrictNormal g p.SplittingField) ↑((rootsEquivRoots p (p * q).SplittingField).invFun ⟨x, ⋯⟩))

Proof state:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : p * q = 0
⊢ Unique (Gal 0)

Tactic:
infer_instance

Result:
no goals

Proof state:
case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
⊢ f = g

Tactic:
ext (x hx)

Result:
case neg.h
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ (p * q).rootSet (p * q).SplittingField
⊢ f x = g x

Proof state:
case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  ((if hq : p * q = 0 then 1 else restrict p (p * q).SplittingField).prod
        (if hq : p * q = 0 then 1 else restrict q (p * q).SplittingField))
      f =
    ((if hq : p * q = 0 then 1 else restrict p (p * q).SplittingField).prod
        (if hq : p * q = 0 then 1 else restrict q (p * q).SplittingField))
      g
⊢ f = g

Tactic:
simp only [dif_neg hpq, MonoidHom.prod_apply, Prod.mk.inj_iff] at hfg

Result:
case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
⊢ f = g

Proof state:
case neg.h.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ q.aroots (p * q).SplittingField
this : Fact (Splits (algebraMap F (p * q).SplittingField) q)
⊢ f x = g x

Tactic:
have key :
  x =
    algebraMap q.SplittingField (p * q).SplittingField
      ((rootsEquivRoots q _).invFun
        ⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr h⟩) :=
  Subtype.ext_iff.mp (Equiv.apply_symm_apply (rootsEquivRoots q _) ⟨x, _⟩).symm

Result:
case neg.h.inr
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ q.aroots (p * q).SplittingField
this : Fact (Splits (algebraMap F (p * q).SplittingField) q)
key :
  x = (algebraMap q.SplittingField (p * q).SplittingField) ↑((rootsEquivRoots q (p * q).SplittingField).invFun ⟨x, ⋯⟩)
⊢ f x = g x

Proof state:
case neg.h.inl
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ p.aroots (p * q).SplittingField
⊢ f x = g x

Tactic:
haveI : Fact (p.Splits (algebraMap F (p * q).SplittingField)) :=
  ⟨splits_of_splits_of_dvd _ hpq (SplittingField.splits (p * q)) (dvd_mul_right p q)⟩

Result:
case neg.h.inl
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
h : x ∈ p.aroots (p * q).SplittingField
this : Fact (Splits (algebraMap F (p * q).SplittingField) p)
⊢ f x = g x

Proof state:
case neg.h
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ (p * q).rootSet (p * q).SplittingField
⊢ f x = g x

Tactic:
rw [rootSet_def, aroots_mul hpq] at hx

Result:
case neg.h
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  (restrict p (p * q).SplittingField) f = (restrict p (p * q).SplittingField) g ∧
    (restrict q (p * q).SplittingField) f = (restrict q (p * q).SplittingField) g
x : (p * q).SplittingField
hx : x ∈ ↑(p.aroots (p * q).SplittingField + q.aroots (p * q).SplittingField).toFinset
⊢ f x = g x

Proof state:
case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg : (restrictProd p q) f = (restrictProd p q) g
⊢ f = g

Tactic:
simp only [restrictProd, restrictDvd_def] at hfg

Result:
case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : ¬p * q = 0
f g : (p * q).Gal
hfg :
  ((if hq : p * q = 0 then 1 else restrict p (p * q).SplittingField).prod
        (if hq : p * q = 0 then 1 else restrict q (p * q).SplittingField))
      f =
    ((if hq : p * q = 0 then 1 else restrict p (p * q).SplittingField).prod
        (if hq : p * q = 0 then 1 else restrict q (p * q).SplittingField))
      g
⊢ f = g