awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime →
      q' ≠ Ideal.under (↥(integralClosure R S)) q →
        q'.LiesOver p →
          Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b
hf : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
a' b' : R'[X]
hP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Eq (α := P.ResidueField[X])
    (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯))
      (HPow.hPow (α := p.ResidueField[X]) X (m + 1)))
    (Polynomial.map (algebraMap R' P.ResidueField) a')
hb' :
  Eq (α := P.ResidueField[X]) (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)) b)
    (Polynomial.map (algebraMap R' P.ResidueField) b')
s₀ : ↥(integralClosure R S) :=
  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs
a a₁ a₂ a₃ :
  Eq.{v + 1} (α := S)
    (((aeval ((Subalgebra.val (integralClosure R S) : (a : ↥(integralClosure R S)) → S) s₀) : R[X] →ₐ[R] S) :
          (a : R[X]) → S)
        f :
      S)
    (0 : S)
⊢ Eq (α := S)
    ((Subalgebra.val (integralClosure R S) : (a : ↥(integralClosure R S)) → S)
        ((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f : ↥(integralClosure R S)) :
      S)
    (0 : S)

Tactic:
rwa [← aeval_algHom_apply]

Premises used: Polynomial.aeval_algHom_apply
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime →
      q' ≠ Ideal.under (↥(integralClosure R S)) q →
        q'.LiesOver p →
          Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b
hf : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
a' b' : R'[X]
hP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Eq (α := P.ResidueField[X])
    (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯))
      (HPow.hPow (α := p.ResidueField[X]) X (m + 1)))
    (Polynomial.map (algebraMap R' P.ResidueField) a')
hb' :
  Eq (α := P.ResidueField[X]) (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)) b)
    (Polynomial.map (algebraMap R' P.ResidueField) b')
s₀ : ↥(integralClosure R S) :=
  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs
⊢ Eq.{v + 1} (α := ↥(integralClosure R S)) ((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f : ↥(integralClosure R S))
    (0 : ↥(integralClosure R S))

Tactic:
have hfs₀ : aeval s₀ f = 0 := by
    ext1; change (integralClosure R S).val (aeval s₀ f) = 0; rwa [← aeval_algHom_apply]
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime →
      q' ≠ Ideal.under (↥(integralClosure R S)) q →
        q'.LiesOver p →
          Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b
hf : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
a' b' : R'[X]
hP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Eq (α := P.ResidueField[X])
    (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯))
      (HPow.hPow (α := p.ResidueField[X]) X (m + 1)))
    (Polynomial.map (algebraMap R' P.ResidueField) a')
hb' :
  Eq (α := P.ResidueField[X]) (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)) b)
    (Polynomial.map (algebraMap R' P.ResidueField) b')
s₀ : ↥(integralClosure R S) :=
  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs
hfs₀ :
  Eq.{v + 1} (α := ↥(integralClosure R S)) ((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f : ↥(integralClosure R S))
    (0 : ↥(integralClosure R S))
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
rw :
  Eq (α := R' ⊗[R] S) ((TensorProduct.includeRight : (a : S) → R' ⊗[R] S) ((aeval s : (a : R[X]) → S) f) : R' ⊗[R] S)
    (0 : R' ⊗[R] S)
rw₁ : Eq (α := R' ⊗[R] S) ((TensorProduct.includeRight : (a : S) → R' ⊗[R] S) 0) 0
rw₂ rw₃ : Eq (α := R' ⊗[R] S) 0 0
⊢ Eq (α := R' ⊗[R] S)
    (((aeval ((TensorProduct.includeRight : (a : S) → R' ⊗[R] S) s) : R[X] →ₐ[R] R' ⊗[R] S) : (a : R[X]) → R' ⊗[R] S)
        f :
      R' ⊗[R] S)
    (0 : R' ⊗[R] S)

Tactic:
rw [aeval_algHom_apply, hf, map_zero]

Premises used: map_zero, Polynomial.aeval_algHom_apply
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime →
      q' ≠ Ideal.under (↥(integralClosure R S)) q →
        q'.LiesOver p →
          Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b
hf : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
a' b' : R'[X]
hP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Eq (α := P.ResidueField[X])
    (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯))
      (HPow.hPow (α := p.ResidueField[X]) X (m + 1)))
    (Polynomial.map (algebraMap R' P.ResidueField) a')
hb' :
  Eq (α := P.ResidueField[X]) (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)) b)
    (Polynomial.map (algebraMap R' P.ResidueField) b')
s₀ : ↥(integralClosure R S) :=
  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs
hfs₀ :
  Eq.{v + 1} (α := ↥(integralClosure R S)) ((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f : ↥(integralClosure R S))
    (0 : ↥(integralClosure R S))
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
⊢ Eq (α := R' ⊗[R] S) ((aeval s' : (a : R[X]) → R' ⊗[R] S) f : R' ⊗[R] S) (0 : R' ⊗[R] S)

Tactic:
have hs'f : aeval s' f = 0 :=
    show aeval (Algebra.TensorProduct.includeRight s) f = 0 by rw [aeval_algHom_apply, hf, map_zero]
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime →
      q' ≠ Ideal.under (↥(integralClosure R S)) q →
        q'.LiesOver p →
          Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b
hf : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
a' b' : R'[X]
hP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Eq (α := P.ResidueField[X])
    (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯))
      (HPow.hPow (α := p.ResidueField[X]) X (m + 1)))
    (Polynomial.map (algebraMap R' P.ResidueField) a')
hb' :
  Eq (α := P.ResidueField[X]) (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)) b)
    (Polynomial.map (algebraMap R' P.ResidueField) b')
s₀ : ↥(integralClosure R S) :=
  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs
hfs₀ :
  Eq.{v + 1} (α := ↥(integralClosure R S)) ((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f : ↥(integralClosure R S))
    (0 : ↥(integralClosure R S))
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
hs'f : Eq (α := R' ⊗[R] S) ((aeval s' : (a : R[X]) → R' ⊗[R] S) f : R' ⊗[R] S) (0 : R' ⊗[R] S)
⊢ Eq (α := TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    ((aeval (1 ⊗ₜ[R] s₀) : (a : R[X]) → R' ⊗[R] ↥(integralClosure R S)) f :
      TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    (0 : TensorProduct.{u, u, v} R R' ↥(integralClosure R S))

Tactic:
have hs₀'f : aeval (A := R' ⊗[R] integralClosure R S) (1 ⊗ₜ s₀) f = 0 :=
    show aeval (Algebra.TensorProduct.includeRight s₀) f = 0 by
    rw [aeval_algHom_apply, hfs₀, map_zero]
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime →
      q' ≠ Ideal.under (↥(integralClosure R S)) q →
        q'.LiesOver p →
          Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b
hf : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
a' b' : R'[X]
hP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Eq (α := P.ResidueField[X])
    (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯))
      (HPow.hPow (α := p.ResidueField[X]) X (m + 1)))
    (Polynomial.map (algebraMap R' P.ResidueField) a')
hb' :
  Eq (α := P.ResidueField[X]) (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)) b)
    (Polynomial.map (algebraMap R' P.ResidueField) b')
s₀ : ↥(integralClosure R S) :=
  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs
hfs₀ :
  Eq.{v + 1} (α := ↥(integralClosure R S)) ((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f : ↥(integralClosure R S))
    (0 : ↥(integralClosure R S))
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
hs'f : Eq (α := R' ⊗[R] S) ((aeval s' : (a : R[X]) → R' ⊗[R] S) f : R' ⊗[R] S) (0 : R' ⊗[R] S)
hs₀'f :
  Eq (α := TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    ((aeval (1 ⊗ₜ[R] s₀) : (a : R[X]) → R' ⊗[R] ↥(integralClosure R S)) f :
      TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    (0 : TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
e₀ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S) :=
  (aeval (1 ⊗ₜ[R] s₀) : (a : R'[X]) → R' ⊗[R] ↥(integralClosure R S)) (c * a')
dsimp :
  HMul.hMul (α := TensorProduct.{u, u, v} R R' ↥(integralClosure R S)) (β :=
      TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
      ((aeval (1 ⊗ₜ[R] s₀) : (a : R'[X]) → R' ⊗[R] ↥(integralClosure R S)) (c * a') :
        TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
      ((aeval (1 ⊗ₜ[R] s₀) : (a : R'[X]) → R' ⊗[R] ↥(integralClosure R S)) (c * a') :
        TensorProduct.{u, u, v} R R' ↥(integralClosure R S)) =
    (aeval (1 ⊗ₜ[R] s₀) : (a : R'[X]) → R' ⊗[R] ↥(integralClosure R S)) (c * a')
⊢ IsIdempotentElem e₀

Tactic:
dsimp only [e₀, IsIdempotentElem]

Premises used: IsIdempotentElem
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime →
      q' ≠ Ideal.under (↥(integralClosure R S)) q →
        q'.LiesOver p →
          Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b
hf : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
a' b' : R'[X]
hP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Eq (α := P.ResidueField[X])
    (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯))
      (HPow.hPow (α := p.ResidueField[X]) X (m + 1)))
    (Polynomial.map (algebraMap R' P.ResidueField) a')
hb' :
  Eq (α := P.ResidueField[X]) (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)) b)
    (Polynomial.map (algebraMap R' P.ResidueField) b')
s₀ : ↥(integralClosure R S) :=
  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs
hfs₀ :
  Eq.{v + 1} (α := ↥(integralClosure R S)) ((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f : ↥(integralClosure R S))
    (0 : ↥(integralClosure R S))
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
hs'f : Eq (α := R' ⊗[R] S) ((aeval s' : (a : R[X]) → R' ⊗[R] S) f : R' ⊗[R] S) (0 : R' ⊗[R] S)
hs₀'f :
  Eq (α := TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    ((aeval (1 ⊗ₜ[R] s₀) : (a : R[X]) → R' ⊗[R] ↥(integralClosure R S)) f :
      TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    (0 : TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
e₀ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S) :=
  (aeval (1 ⊗ₜ[R] s₀) : (a : R'[X]) → R' ⊗[R] ↥(integralClosure R S)) (c * a')
⊢ Eq (α := TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    ((aeval (1 ⊗ₜ[R] s₀) : (a : R'[X]) → R' ⊗[R] ↥(integralClosure R S))
        (c * a' - c * d * Polynomial.map (algebraMap R R') f) :
      TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    ((aeval (1 ⊗ₜ[R] s₀) : (a : R'[X]) → R' ⊗[R] ↥(integralClosure R S)) (c * a') :
      TensorProduct.{u, u, v} R R' ↥(integralClosure R S))

Tactic:
simp only [map_mul, map_sub, aeval_map_algebraMap, hs₀'f, mul_zero, sub_zero]

Premises used: Polynomial.aeval_map_algebraMap, map_sub, sub_zero, MulZeroClass.mul_zero, map_mul
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime →
      q' ≠ Ideal.under (↥(integralClosure R S)) q →
        q'.LiesOver p →
          Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b
hf : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
a' b' : R'[X]
hP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Eq (α := P.ResidueField[X])
    (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯))
      (HPow.hPow (α := p.ResidueField[X]) X (m + 1)))
    (Polynomial.map (algebraMap R' P.ResidueField) a')
hb' :
  Eq (α := P.ResidueField[X]) (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)) b)
    (Polynomial.map (algebraMap R' P.ResidueField) b')
s₀ : ↥(integralClosure R S) :=
  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs
hfs₀ :
  Eq.{v + 1} (α := ↥(integralClosure R S)) ((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f : ↥(integralClosure R S))
    (0 : ↥(integralClosure R S))
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
hs'f : Eq (α := R' ⊗[R] S) ((aeval s' : (a : R[X]) → R' ⊗[R] S) f : R' ⊗[R] S) (0 : R' ⊗[R] S)
hs₀'f :
  Eq (α := TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    ((aeval (1 ⊗ₜ[R] s₀) : (a : R[X]) → R' ⊗[R] ↥(integralClosure R S)) f :
      TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    (0 : TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
e₀ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S) :=
  (aeval (1 ⊗ₜ[R] s₀) : (a : R'[X]) → R' ⊗[R] ↥(integralClosure R S)) (c * a')
⊢ IsIdempotentElem e₀

Tactic:
have he₀ : IsIdempotentElem e₀ := by
    dsimp only [e₀, IsIdempotentElem]
    nth_rw 2 [eq_sub_iff_add_eq.mpr hcd]
    rw [← map_mul, mul_sub, mul_one, mul_mul_mul_comm, ← hfab']
    simp only [map_mul, map_sub, aeval_map_algebraMap, hs₀'f, mul_zero, sub_zero]
-- Module: Mathlib.RingTheory.Etale.QuasiFinite
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FiniteType R S
p : Ideal R
inst_4 : p.IsPrime
q : Ideal S
inst_5 : q.IsPrime
inst_6 : q.LiesOver p
inst_7 : QuasiFiniteAt R q
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime →
      q' ≠ Ideal.under (↥(integralClosure R S)) q →
        q'.LiesOver p →
          Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (HPow.hPow (α := p.ResidueField[X]) X (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = HPow.hPow (α := p.ResidueField[X]) X (m + 1) * b
hf : Eq.{v + 1} (α := S) ((aeval s : (a : R[X]) → S) f : S) (0 : S)
R' : Type u
w : CommRing R'
w_1 : Algebra R R'
w_2 : Etale R R'
P : Ideal R'
w_3 : P.IsPrime
w_4 : P.LiesOver p
a' b' : R'[X]
hP :
  Function.Bijective (α := p.ResidueField) (β := P.ResidueField)
    (⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) : (a : p.ResidueField) → P.ResidueField)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Eq (α := P.ResidueField[X])
    (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯))
      (HPow.hPow (α := p.ResidueField[X]) X (m + 1)))
    (Polynomial.map (algebraMap R' P.ResidueField) a')
hb' :
  Eq (α := P.ResidueField[X]) (Polynomial.map (AlgHom.toRingHom (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)) b)
    (Polynomial.map (algebraMap R' P.ResidueField) b')
s₀ : ↥(integralClosure R S) :=
  Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) s hRs
hfs₀ :
  Eq.{v + 1} (α := ↥(integralClosure R S)) ((aeval s₀ : (a : R[X]) → ↥(integralClosure R S)) f : ↥(integralClosure R S))
    (0 : ↥(integralClosure R S))
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
hs'f : Eq (α := R' ⊗[R] S) ((aeval s' : (a : R[X]) → R' ⊗[R] S) f : R' ⊗[R] S) (0 : R' ⊗[R] S)
hs₀'f :
  Eq (α := TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    ((aeval (1 ⊗ₜ[R] s₀) : (a : R[X]) → R' ⊗[R] ↥(integralClosure R S)) f :
      TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
    (0 : TensorProduct.{u, u, v} R R' ↥(integralClosure R S))
e₀ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S) :=
  (aeval (1 ⊗ₜ[R] s₀) : (a : R'[X]) → R' ⊗[R] ↥(integralClosure R S)) (c * a')
he₀ : IsIdempotentElem e₀
e : R' ⊗[R] S := (aeval s' : (a : R'[X]) → R' ⊗[R] S) (c * a')
φ : TensorProduct.{u, u, v} R R' ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S :=
  TensorProduct.map (AlgHom.id R' R') (Subalgebra.val (integralClosure R S))
simp :
  ((aeval ((φ : (a : R' ⊗[R] ↥(integralClosure R S)) → R' ⊗[R] S) (1 ⊗ₜ[R] s₀)) : R'[X] →ₐ[R'] R' ⊗[R] S) :
        (a : R'[X]) → R' ⊗[R] S)
      (c * a') =
    e
⊢ (φ : (a : R' ⊗[R] ↥(integralClosure R S)) → R' ⊗[R] S) e₀ = e

Tactic:
simp only [e₀, ← aeval_algHom_apply]

Premises used: Polynomial.aeval_algHom_apply