awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
F : Type u_4
inst : Field F
E : Type u_5
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_6
inst_3 : Field K
inst_4 : Algebra F K
L : IntermediateField F E
f : E →ₐ[F] K
rw : (f.comp L.val).fieldRange.toSubalgebra = Subalgebra.map f L.toSubalgebra
rw₁ : (f.comp L.val).range = Subalgebra.map f L.toSubalgebra
rw₂ : Subalgebra.map f L.val.range = Subalgebra.map f L.toSubalgebra
⊢ (f.comp L.val).fieldRange.toSubalgebra = (map f L).toSubalgebra
have rw₃ : Subalgebra.map f L.toSubalgebra = Subalgebra.map f L.toSubalgebra
Tactic: rw [toSubalgebra_map, AlgHom.fieldRange_toSubalgebra, AlgHom.range_comp, range_val]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S : IntermediateField K L
F E_1 E'_1 : Subfield L
h : F ≤ E_1
h' : F ≤ E'_1
x : L
E E' : { E : Subfield L // F ≤ E }
⊢ LE.le (α := IntermediateField (↥F) L)
      (({ toFun := fun (E : { E : Subfield L // F ≤ E }) ↦ extendScalars ⋯,
              invFun := fun (E : IntermediateField (↥F) L) ↦
                Subtype.mk (p := fun (E : Subfield L) ↦ F ≤ E) E.toSubfield ⋯,
              left_inv := ⋯, right_inv := ⋯ : { E : Subfield L // F ≤ E } ≃ IntermediateField (↥F) L } :
            (a : { E : Subfield L // F ≤ E }) → IntermediateField (↥F) L)
          E :
        IntermediateField (↥F) L)
      (({ toFun := fun (E : { E : Subfield L // F ≤ E }) ↦ extendScalars ⋯,
              invFun := fun (E : IntermediateField (↥F) L) ↦
                Subtype.mk (p := fun (E : Subfield L) ↦ F ≤ E) E.toSubfield ⋯,
              left_inv := ⋯, right_inv := ⋯ : { E : Subfield L // F ≤ E } ≃ IntermediateField (↥F) L } :
            (a : { E : Subfield L // F ≤ E }) → IntermediateField (↥F) L)
          E' :
        IntermediateField (↥F) L) ↔
    E ≤ E'
have simp : extendScalars sorry ≤ extendScalars sorry ↔ E ≤ E'
Tactic: simp only [Equiv.coe_fn_mk]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S F E_1 E'_1 : IntermediateField K L
h : F ≤ E_1
h' : F ≤ E'_1
x : L
E E' : { E : IntermediateField K L // F ≤ E }
⊢ LE.le (α := IntermediateField (↥F) L)
      (({ toFun := fun (E : { E : IntermediateField K L // F ≤ E }) ↦ extendScalars ⋯,
              invFun := fun (E : IntermediateField (↥F) L) ↦
                Subtype.mk (p := fun (E : IntermediateField K L) ↦ F ≤ E) (restrictScalars K E) ⋯,
              left_inv := ⋯, right_inv := ⋯ : { E : IntermediateField K L // F ≤ E } ≃ IntermediateField (↥F) L } :
            (a : { E : IntermediateField K L // F ≤ E }) → IntermediateField (↥F) L)
          E :
        IntermediateField (↥F) L)
      (({ toFun := fun (E : { E : IntermediateField K L // F ≤ E }) ↦ extendScalars ⋯,
              invFun := fun (E : IntermediateField (↥F) L) ↦
                Subtype.mk (p := fun (E : IntermediateField K L) ↦ F ≤ E) (restrictScalars K E) ⋯,
              left_inv := ⋯, right_inv := ⋯ : { E : IntermediateField K L // F ≤ E } ≃ IntermediateField (↥F) L } :
            (a : { E : IntermediateField K L // F ≤ E }) → IntermediateField (↥F) L)
          E' :
        IntermediateField (↥F) L) ↔
    E ≤ E'
have simp : extendScalars sorry ≤ extendScalars sorry ↔ E ≤ E'
Tactic: simp only [Equiv.coe_fn_mk]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
h : F ≤ E
⊢ lift (restrict h) = F
have h₁ : ∀ (x : L), x ∈ lift (restrict h) ↔ x ∈ F
Tactic: ext x
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
⊢ x ∈ lift (restrict h) ↔ x ∈ F
have h₁ : ∀ (hx : x ∈ lift (restrict h)), x ∈ F
Tactic: refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Basic (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
h₁ : ∀ (hx : x ∈ lift (restrict h)), x ∈ F
⊢ x ∈ lift (restrict h) ↔ x ∈ F
have h₂ : ∀ (hx : x ∈ F), x ∈ lift (restrict h)
Tactic: refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
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
a : ↥(F.extendRight M)
⊢ (algebraMap (↥F) M : (a : ↥F) → M)
      (((AlgEquiv.symm (F.extendRightEquiv M) : AlgEquiv.{u_1, u_3, u_2} K ↥(F.extendRight M) ↥F) :
            (a : ↥(F.extendRight M)) → ↥F)
          a :
        ↥F) =
    (↑a : M)
have rw : (algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
    (((F.extendRightEquiv M : AlgEquiv.{u_1, u_2, u_3} K ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
        (((AlgEquiv.symm (F.extendRightEquiv M) : AlgEquiv.{u_1, u_3, u_2} K ↥(F.extendRight M) ↥F) :
            (a : ↥(F.extendRight M)) → ↥F)
          a) :
      ↥(F.extendRight M)) =
  (↑a : M)
Tactic: rw [← algebraMap_extendRightEquiv, AlgEquiv.apply_symm_apply, algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
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
a : ↥(F.extendRight M)
rw :
  (algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
      (((F.extendRightEquiv M : AlgEquiv.{u_1, u_2, u_3} K ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
          (((AlgEquiv.symm (F.extendRightEquiv M) : AlgEquiv.{u_1, u_3, u_2} K ↥(F.extendRight M) ↥F) :
              (a : ↥(F.extendRight M)) → ↥F)
            a) :
        ↥(F.extendRight M)) =
    (↑a : M)
⊢ (algebraMap (↥F) M : (a : ↥F) → M)
      (((AlgEquiv.symm (F.extendRightEquiv M) : AlgEquiv.{u_1, u_3, u_2} K ↥(F.extendRight M) ↥F) :
            (a : ↥(F.extendRight M)) → ↥F)
          a :
        ↥F) =
    (↑a : M)
have rw₁ : (algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M) a = (↑a : M)
Tactic: rw [← algebraMap_extendRightEquiv, AlgEquiv.apply_symm_apply, algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
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
a : ↥(F.extendRight M)
rw :
  (algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M)
      (((F.extendRightEquiv M : AlgEquiv.{u_1, u_2, u_3} K ↥F ↥(F.extendRight M)) : (a : ↥F) → ↥(F.extendRight M))
          (((AlgEquiv.symm (F.extendRightEquiv M) : AlgEquiv.{u_1, u_3, u_2} K ↥(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)
⊢ (algebraMap (↥F) M : (a : ↥F) → M)
      (((AlgEquiv.symm (F.extendRightEquiv M) : AlgEquiv.{u_1, u_3, u_2} K ↥(F.extendRight M) ↥F) :
            (a : ↥(F.extendRight M)) → ↥F)
          a :
        ↥F) =
    (↑a : M)
have rw₂ : (↑a : M) = (↑a : M)
Tactic: rw [← algebraMap_extendRightEquiv, AlgEquiv.apply_symm_apply, algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
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 S M : (a : S) → M) s : M)
have 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)
Tactic: rw [IsScalarTower.algebraMap_apply S F M, IsScalarTower.algebraMap_apply F L M]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
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)
⊢ ↥(F.extendRight M)
have refine : Membership.mem (γ := IntermediateField K M) (F.extendRight M) (s • (↑x : M))
Tactic: refine ⟨s • x, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
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) (s • (↑x : M))
have rw : Membership.mem (γ := IntermediateField K M) (F.extendRight M)
  (HMul.hMul (α := M) ((algebraMap S M : (a : S) → M) s : M) (↑x : M))
Tactic: rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
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)
⊢ (↑(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)
have convert_2 : s • (↑x : M) =
  (↑(HMul.hMul (α := ↥(F.extendRight M))
        (((RingHom.codRestrict (algebraMap S M) (toSubalgebra (F.extendRight M)) sorry :
                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) = _
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
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)
⊢ 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)
have convert_2 : s • (↑x : M) =
  (↑(((RingHom.codRestrict (algebraMap S M) (toSubalgebra (F.extendRight M)) sorry :
              RingHom.{u_5, u_3} S ↥(toSubalgebra (F.extendRight M))) :
            (a : S) → ↥(F.extendRight M))
          s) :
      M) *
    (↑x : M)
Tactic: rw [MulMemClass.coe_mul, RingHom.codRestrict_apply, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
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)
⊢ 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)
have convert_2₁ : s • (↑x : M) = HMul.hMul (α := M) ((algebraMap S M : (a : S) → M) s : M) (↑x : M)
Tactic: rw [MulMemClass.coe_mul, RingHom.codRestrict_apply, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
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)
⊢ 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)
have convert_2₂ : s • (↑x : M) = s • (↑x : M)
Tactic: rw [MulMemClass.coe_mul, RingHom.codRestrict_apply, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
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)
⊢ (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)
have 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)
Tactic: rw [← algebraMap_extendRightEquiv' F M S, AlgEquiv.apply_symm_apply, algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
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)
⊢ (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)
have rw₁ : (algebraMap (↥(F.extendRight M)) M : (a : ↥(F.extendRight M)) → M) a = (↑a : M)
Tactic: rw [← algebraMap_extendRightEquiv' F M S, AlgEquiv.apply_symm_apply, algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
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)
⊢ (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)
have rw₂ : (↑a : M) = (↑a : M)
Tactic: rw [← algebraMap_extendRightEquiv' F M S, AlgEquiv.apply_symm_apply, algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
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)
have 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))
Tactic: refine .of_algEquiv S (F.extendRightEquiv' M R) fun x ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
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
⊢ 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))
have 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)
Tactic: rw [Subtype.ext_iff, ← algebraMap_apply (F.extendRight M), ← algebraMap_apply (F.extendRight M),
    algebraMap_extendRightEquiv', ← IsScalarTower.algebraMap_apply,
    ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.ExtendRight (goal)
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)
⊢ 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))
have 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)
Tactic: rw [Subtype.ext_iff, ← algebraMap_apply (F.extendRight M), ← algebraMap_apply (F.extendRight M),
    algebraMap_extendRightEquiv', ← IsScalarTower.algebraMap_apply,
    ← IsScalarTower.algebraMap_apply]