awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
S : Type u_5
inst_7 : CommRing S
inst_8 : Algebra.{u_5, u_2} S ↥F
inst_9 : Algebra S M
inst_10 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
s : S
rw :
  Membership.mem (α := M) (γ := IntermediateField K M) (F.extendRight M)
    ((algebraMap L M : (a : L) → M) ((algebraMap (↥F) L : (a : ↥F) → L) ((algebraMap S ↥F : (a : S) → ↥F) s : ↥F) : L) :
      M)
⊢ Membership.mem (α := M) (γ := IntermediateField K M) (F.extendRight M) ((algebraMap S M : (a : S) → M) s : M)

Tactic:
rw [IsScalarTower.algebraMap_apply S F M, IsScalarTower.algebraMap_apply F L M]

Premises used: Membership.mem, Subtype, IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
S : Type u_5
inst_7 : CommRing S
inst_8 : Algebra.{u_5, u_2} S ↥F
inst_9 : Algebra S M
inst_10 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
s : S
⊢ Membership.mem (α := L) (↑F.toSubsemiring : Set L)
    ((algebraMap (↥F) L : (a : ↥F) → L) ((algebraMap S ↥F : (a : S) → ↥F) s : ↥F) : L)

Tactic:
simp
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
S : Type u_5
inst_7 : CommRing S
inst_8 : Algebra.{u_5, u_2} S ↥F
inst_9 : Algebra S M
inst_10 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
s : S
⊢ Membership.mem (α := M) (γ := IntermediateField K M) (F.extendRight M)
    ((algebraMap L M : (a : L) → M) ((algebraMap (↥F) L : (a : ↥F) → L) ((algebraMap S ↥F : (a : S) → ↥F) s : ↥F) : L) :
      M)

Tactic:
exact ⟨algebraMap F L (algebraMap S F s), by simp, rfl⟩
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
s : S
x : ↥(F.extendRight M)
refine : Membership.mem (γ := IntermediateField K M) (F.extendRight M) (s • (↑x : M))
⊢ ↥(F.extendRight M)

Tactic:
refine ⟨s • x, ?_⟩
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
s : S
x : ↥(F.extendRight M)
rw :
  Membership.mem (γ := IntermediateField K M) (F.extendRight M)
    (HMul.hMul (α := M) ((algebraMap S M : (a : S) → M) s : M) (↑x : M))
⊢ Membership.mem (γ := IntermediateField K M) (F.extendRight M) (s • (↑x : M))

Tactic:
rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
s : S
x : ↥(F.extendRight M)
⊢ Membership.mem (γ := IntermediateField K M) (F.extendRight M)
    (HMul.hMul (α := M) ((algebraMap S M : (a : S) → M) s : M) (↑x : M))

Tactic:
(F.extendRight M).mul_mem (algebraMap_mem F M s) x.prop

Premises used: IntermediateField.extendRight.algebraMap_mem, IntermediateField.extendRight, Subtype.prop, IntermediateField.mul_mem
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
s : S
x : ↥(F.extendRight M)
⊢ Membership.mem (γ := IntermediateField K M) (F.extendRight M)
    (HMul.hMul (α := M) ((algebraMap S M : (a : S) → M) s : M) (↑x : M))

Tactic:
exact (F.extendRight M).mul_mem (algebraMap_mem F M s) x.prop

Premises used: IntermediateField.extendRight.algebraMap_mem, IntermediateField.extendRight, Subtype.prop, IntermediateField.mul_mem
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
S : Type u_5
inst_7 : CommRing S
inst_8 : Algebra.{u_5, u_2} S ↥F
inst_9 : Algebra S M
inst_10 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
s : S
x : ↥(F.extendRight M)
⊢ (↑(s • x) : M) = s • (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
x : S
x_1 : ↥(F.extendRight M)
⊢ (↑(HMul.hMul (α := ↥(F.extendRight M))
          (((RingHom.codRestrict (algebraMap S M) (toSubalgebra (F.extendRight M)) ⋯ :
                  RingHom.{u_5, u_3} S ↥(toSubalgebra (F.extendRight M))) :
                (a : S) → ↥(F.extendRight M))
              x :
            ↥(F.extendRight M))
          x_1) :
      M) =
    (↑(HMul.hMul (β := ↥(F.extendRight M)) x_1
          (((RingHom.codRestrict (algebraMap S M) (toSubalgebra (F.extendRight M)) ⋯ :
                  RingHom.{u_5, u_3} S ↥(toSubalgebra (F.extendRight M))) :
                (a : S) → ↥(F.extendRight M))
              x :
            ↥(F.extendRight M))) :
      M)

Tactic:
simp [Algebra.commutes]

Premises used: Algebra.commutes
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
s : S
x : ↥(F.extendRight M)
convert_2 :
  s • (↑x : M) =
    (↑(HMul.hMul (α := ↥(F.extendRight M))
          (((RingHom.codRestrict (algebraMap S M) (toSubalgebra (F.extendRight M)) ⋯ :
                  RingHom.{u_5, u_3} S ↥(toSubalgebra (F.extendRight M))) :
                (a : S) → ↥(F.extendRight M))
              s :
            ↥(F.extendRight M))
          x) :
      M)
⊢ (↑(s • x) : M) =
    (↑(HMul.hMul (α := ↥(F.extendRight M))
          (((RingHom.codRestrict (algebraMap S M) (toSubalgebra (F.extendRight M)) ⋯ :
                  RingHom.{u_5, u_3} S ↥(toSubalgebra (F.extendRight M))) :
                (a : S) → ↥(F.extendRight M))
              s :
            ↥(F.extendRight M))
          x) :
      M)

Tactic:
convert_to s • (x : M) = _

Premises used: Subtype.val
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
s : S
x : ↥(F.extendRight M)
convert_2 :
  s • (↑x : M) =
    (↑(((RingHom.codRestrict (algebraMap S M) (toSubalgebra (F.extendRight M)) ⋯ :
                RingHom.{u_5, u_3} S ↥(toSubalgebra (F.extendRight M))) :
              (a : S) → ↥(F.extendRight M))
            s) :
        M) *
      (↑x : M)
convert_2₁ : s • (↑x : M) = HMul.hMul (α := M) ((algebraMap S M : (a : S) → M) s : M) (↑x : M)
convert_2₂ convert_2₃ : s • (↑x : M) = s • (↑x : M)
⊢ s • (↑x : M) =
    (↑(HMul.hMul (α := ↥(F.extendRight M))
          (((RingHom.codRestrict (algebraMap S M) (toSubalgebra (F.extendRight M)) ⋯ :
                  RingHom.{u_5, u_3} S ↥(toSubalgebra (F.extendRight M))) :
                (a : S) → ↥(F.extendRight M))
              s :
            ↥(F.extendRight M))
          x) :
      M)

Tactic:
rw [MulMemClass.coe_mul, RingHom.codRestrict_apply, ← Algebra.smul_def]

Premises used: RingHom.codRestrict_apply, MulMemClass.coe_mul, Algebra.smul_def
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
inst_12 : Algebra S K
inst_13 : IsScalarTower S K M
⊢ Eq (α := Algebra.{u_5, u_3} S ↥(F.extendRight M)) (algebra' (F.extendRight M)) (algebra F M)

Tactic:
rfl
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
inst_12 : Algebra S K
inst_13 : IsScalarTower S K M
⊢ Eq (α := Algebra.{u_5, u_3} S ↥(F.extendRight M)) (algebra' (F.extendRight M)) (algebra F M)

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
⊢ IsScalarTower S (↥(F.extendRight M)) M

Tactic:
IsScalarTower.of_algebraMap_eq' rfl

Premises used: IsScalarTower.of_algebraMap_eq', rfl
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
⊢ IsScalarTower.{u_5, u_2, u_3} S ↥F ↥(F.extendRight M)

Tactic:
IsScalarTower.to₁₂₃ S F (F.extendRight M) M

Premises used: Membership.mem, Subtype, IntermediateField.extendRight, IsScalarTower.to₁₂₃
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
inst_12 : Algebra R S
inst_13 : Algebra.{u_4, u_2} R ↥F
inst_14 : Algebra R M
inst_15 : IsScalarTower.{u_4, u_2, u_3} R (↥F) M
inst_16 : IsScalarTower R S M
⊢ IsScalarTower.{u_4, u_5, u_3} R S ↥(F.extendRight M)

Tactic:
IsScalarTower.to₁₂₃ R S (F.extendRight M) M

Premises used: Membership.mem, Subtype, IntermediateField.extendRight, IsScalarTower.to₁₂₃
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
S : Type u_5
inst_7 : CommRing S
inst_8 : Algebra.{u_5, u_2} S ↥F
inst_9 : Algebra S M
inst_10 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
a : ↥F
⊢ Eq.{u_3 + 1} (α := M)
    ((↑(((F.extendRightEquiv' M S : AlgEquiv.{u_5, u_2, u_3} S ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
            a) :
        M) :
      M)
    ((algebraMap (↥F) M : (a : ↥F) → M) a : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
S : Type u_5
inst_7 : CommRing S
inst_8 : Algebra.{u_5, u_2} S ↥F
inst_9 : Algebra S M
inst_10 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
a : ↥F
⊢ Eq (α := M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        (((F.extendRightEquiv' M S : AlgEquiv.{u_5, u_2, u_3} S ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
            a :
          ↥(F.extendRight M)) :
      M)
    ((algebraMap (↥F) M : (a : ↥F) → M) a : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
S : Type u_5
inst_7 : CommRing S
inst_8 : Algebra.{u_5, u_2} S ↥F
inst_9 : Algebra S M
inst_10 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
a : ↥(F.extendRight M)
rw :
  (algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
      (((F.extendRightEquiv' M S : AlgEquiv.{u_5, u_2, u_3} S ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
          (((AlgEquiv.symm (F.extendRightEquiv' M S) : AlgEquiv.{u_5, u_3, u_2} S ↥(F.extendRight M) ↥F) :
              (a : ↥(F.extendRight M)) → ↥F)
            a) :
        ↥(F.extendRight M)) =
    (↑a : M)
rw₁ : (algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M) a = (↑a : M)
rw₂ rw₃ : (↑a : M) = (↑a : M)
⊢ (algebraMap (↥F) M : (a : ↥F) → M)
      (((AlgEquiv.symm (F.extendRightEquiv' M S) : AlgEquiv.{u_5, u_3, u_2} S ↥(F.extendRight M) ↥F) :
            (a : ↥(F.extendRight M)) → ↥F)
          a :
        ↥F) =
    (↑a : M)

Tactic:
rw [← algebraMap_extendRightEquiv' F M S, AlgEquiv.apply_symm_apply, algebraMap_apply]

Premises used: AlgEquiv.apply_symm_apply, IntermediateField.extendRight.algebraMap_extendRightEquiv', IntermediateField.algebraMap_apply
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
inst_12 : IsFractionRing.{u_5, u_2} S ↥F
⊢ IsFractionRing.{u_5, u_3} S ↥(F.extendRight M)

Tactic:
.of_algEquiv (R := S) (L := F.extendRight M) (K := F) <| F.extendRightEquiv' M S

Premises used: IsFractionRing.of_algEquiv, IntermediateField.extendRightEquiv'
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
inst_12 : Algebra.{u_4, u_2} R ↥F
inst_13 : Algebra R M
inst_14 : IsScalarTower.{u_4, u_2, u_3} R (↥F) M
inst_15 : IsIntegralClosure.{u_5, u_4, u_2} S R ↥F
⊢ IsIntegralClosure.{u_5, u_4, u_3} S R ↥(F.extendRight M)

Tactic:
.of_algEquiv S (F.extendRightEquiv' M R) fun x ↦ ?_

Premises used: IsIntegralClosure.of_algEquiv, IntermediateField.extendRightEquiv'
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
inst_12 : Algebra.{u_4, u_2} R ↥F
inst_13 : Algebra R M
inst_14 : IsScalarTower.{u_4, u_2, u_3} R (↥F) M
inst_15 : IsIntegralClosure.{u_5, u_4, u_2} S R ↥F
refine :
  ∀ (x : S),
    Eq.{u_3 + 1} (α := ↥(F.extendRight M))
      ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M))
      (((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
          ((algebraMap S ↥F : (a : S) → ↥F) x) :
        ↥(F.extendRight M))
⊢ IsIntegralClosure.{u_5, u_4, u_3} S R ↥(F.extendRight M)

Tactic:
refine .of_algEquiv S (F.extendRightEquiv' M R) fun x ↦ ?_
-- Module: Mathlib.FieldTheory.IntermediateField.ExtendRight
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : IntermediateField K L
M : Type u_3
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : Algebra L M
inst_6 : IsScalarTower K L M
R : Type u_4
S : Type u_5
inst_7 : CommRing R
inst_8 : CommRing S
inst_9 : Algebra.{u_5, u_2} S ↥F
inst_10 : Algebra S M
inst_11 : IsScalarTower.{u_5, u_2, u_3} S (↥F) M
inst_12 : Algebra.{u_4, u_2} R ↥F
inst_13 : Algebra R M
inst_14 : IsScalarTower.{u_4, u_2, u_3} R (↥F) M
inst_15 : IsIntegralClosure.{u_5, u_4, u_2} S R ↥F
x : S
rw :
  Eq.{u_3 + 1} (α := M) (↑((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x) : M)
    (↑(((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
          ((algebraMap S ↥F : (a : S) → ↥F) x)) :
      M)
rw₁ :
  Eq (α := M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M)) :
      M)
    ((↑(((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
            ((algebraMap S ↥F : (a : S) → ↥F) x)) :
        M) :
      M)
rw₂ :
  Eq (α := M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M)) :
      M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        (((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
            ((algebraMap S ↥F : (a : S) → ↥F) x) :
          ↥(F.extendRight M)) :
      M)
rw₃ :
  Eq (α := M)
    ((algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
        ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M)) :
      M)
    ((algebraMap (↥F) M : (a : ↥F) → M) ((algebraMap S ↥F : (a : S) → ↥F) x : ↥F) : M)
rw₄ :
  Eq.{u_3 + 1} (α := M) ((algebraMap S M : (a : S) → M) x : M)
    ((algebraMap (↥F) M : (a : ↥F) → M) ((algebraMap S ↥F : (a : S) → ↥F) x : ↥F) : M)
rw₅ rw₆ : Eq.{u_3 + 1} (α := M) ((algebraMap S M : (a : S) → M) x : M) ((algebraMap S M : (a : S) → M) x : M)
⊢ Eq.{u_3 + 1} (α := ↥(F.extendRight M))
    ((algebraMap S ↥(F.extendRight M) : (a : S) → ↥(F.extendRight M)) x : ↥(F.extendRight M))
    (((F.extendRightEquiv' M R : AlgEquiv.{u_4, u_2, u_3} R ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
        ((algebraMap S ↥F : (a : S) → ↥F) x) :
      ↥(F.extendRight M))

Tactic:
rw [Subtype.ext_iff, ← algebraMap_apply (F.extendRight M), ← algebraMap_apply (F.extendRight M),
    algebraMap_extendRightEquiv', ← IsScalarTower.algebraMap_apply,
    ← IsScalarTower.algebraMap_apply]

Premises used: IntermediateField.extendRight.algebraMap_extendRightEquiv', IntermediateField.algebraMap_apply, Subtype.ext_iff, IntermediateField.extendRight, IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
K : Type u_1
inst_1 : Field K
inst_2 : DecidableEq K
i : k →+* K
f : Monics k
hf : (map i (↑f : k[X])).Splits
rwa :
  ∀ (hf : (map i (↑f : k[X])).roots.card = (map i (↑f : k[X])).natDegree),
    (map i (↑f : k[X])).roots.toEnumFinset.card = (↑f : k[X]).natDegree
rwa₁ :
  ∀ (hf : (map i (↑f : k[X])).roots.toEnumFinset.card = (map i (↑f : k[X])).natDegree),
    (map i (↑f : k[X])).roots.toEnumFinset.card = (↑f : k[X]).natDegree
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (hf : (map i (↑f : k[X])).roots.toEnumFinset.card = (↑f : k[X]).natDegree),
    (map i (↑f : k[X])).roots.toEnumFinset.card = (↑f : k[X]).natDegree
⊢ (map i (↑f : k[X])).roots.toEnumFinset.card = (↑f : k[X]).natDegree

Tactic:
rwa [splits_iff_card_roots,
      ← Multiset.card_toEnumFinset, f.2.natDegree_map] at hf

Premises used: Polynomial.splits_iff_card_roots, Polynomial.Monic.natDegree_map, Multiset.card_toEnumFinset, Subtype.property
-- Module: Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Goal:
k : Type u
inst : Field k
s : Finset (Monics k)
f : Monics k
hf : f ∈ s
⊢ Splits (R := SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))
    (∏ x ∈ s, map (algebraMap k (SplittingField (K := k) (∏ f ∈ s, (↑f : k[X])))) (↑x : k[X]))

Tactic:
simpa [Polynomial.map_prod] using SplittingField.splits (∏ f ∈ s, f.1)

Premises used: Polynomial.SplittingField.splits, Finset.prod, Polynomial.map_prod, Subtype.val