-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsStandardSmoothOfRelativeDimension n R S
let let₁ let₂ : ∃ (g : MvPolynomial (Fin n) R →ₐ[R] S), g.Etale
let₃ let₄ let₅ let₆ let₇ :
  ∀ (ι σ : Type) (w : _root_.Finite σ),
    _root_.Finite ι →
      ∀ (P : Algebra.SubmersivePresentation R S ι σ) (e : P.dimension = n),
        ∃ (g : MvPolynomial (Fin n) R →ₐ[R] S), g.Etale
let₈ :
  let this := Fintype.ofFinite;
  ∀ (ι σ : Type) (w : _root_.Finite σ) (w_1 : _root_.Finite ι) (P : Algebra.SubmersivePresentation R S ι σ)
    (e : P.dimension = n),
    let e₀ : σ ⊕ Fin n ≃ ι :=
      Equiv.trans ((Equiv.ofInjective P.map ⋯).sumCongr (Equiv.symm (Finite.equivFinOfCardEq ⋯)))
        (Equiv.Set.sumCompl (Set.range P.map));
    let e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
      AlgEquiv.trans (AlgEquiv.symm (MvPolynomial.sumAlgEquiv R σ (Fin n))) (MvPolynomial.renameEquiv R e₀);
    let φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
      (↑e : MvPolynomial σ (MvPolynomial (Fin n) R) →ₐ[R] P.Ring).comp
        (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)));
    let algInst := φ.toAlgebra;
    ∀ (this : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring), ∃ (g : MvPolynomial (Fin n) R →ₐ[R] S), g.Etale
let₉ :
  let this := Fintype.ofFinite;
  ∀ (ι σ : Type) (w : _root_.Finite σ) (w_1 : _root_.Finite ι) (P : Algebra.SubmersivePresentation R S ι σ)
    (e : P.dimension = n),
    let e₀ : σ ⊕ Fin n ≃ ι :=
      Equiv.trans ((Equiv.ofInjective P.map ⋯).sumCongr (Equiv.symm (Finite.equivFinOfCardEq ⋯)))
        (Equiv.Set.sumCompl (Set.range P.map));
    let e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
      AlgEquiv.trans (AlgEquiv.symm (MvPolynomial.sumAlgEquiv R σ (Fin n))) (MvPolynomial.renameEquiv R e₀);
    let φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
      (↑e : MvPolynomial σ (MvPolynomial (Fin n) R) →ₐ[R] P.Ring).comp
        (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)));
    let algInst := φ.toAlgebra;
    let algInst_1 : Algebra.{u, v} (MvPolynomial (Fin n) R) S := toAlgebra (comp (algebraMap P.Ring S) φ.toRingHom);
    ∀ (this : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring) (this : IsScalarTower R (MvPolynomial (Fin n) R) S),
      ∃ (g : MvPolynomial (Fin n) R →ₐ[R] S), g.Etale
⊢ ∃ (g : MvPolynomial (Fin n) R →ₐ[R] S), g.Etale
have let₁₀ : let this := Fintype.ofFinite;
∀ (ι σ : Type) (w : _root_.Finite σ) (w_1 : _root_.Finite ι) (P : Algebra.SubmersivePresentation R S ι σ)
  (e : P.dimension = n),
  let e₀ : σ ⊕ Fin n ≃ ι :=
    Equiv.trans ((Equiv.ofInjective P.map sorry).sumCongr (Equiv.symm (Finite.equivFinOfCardEq sorry)))
      (Equiv.Set.sumCompl (Set.range P.map));
  let e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
    AlgEquiv.trans (AlgEquiv.symm (MvPolynomial.sumAlgEquiv R σ (Fin n))) (MvPolynomial.renameEquiv R e₀);
  let φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
    (↑e : MvPolynomial σ (MvPolynomial (Fin n) R) →ₐ[R] P.Ring).comp
      (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)));
  let algInst := φ.toAlgebra;
  let algInst_1 : Algebra.{u, v} (MvPolynomial (Fin n) R) S := toAlgebra (comp (algebraMap P.Ring S) φ.toRingHom);
  ∀ (this : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring) (this : IsScalarTower R (MvPolynomial (Fin n) R) S),
    Etale (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) S))
Tactic: classical
  let := Fintype.ofFinite
  obtain ⟨ι, σ, _, _, P, e⟩ :=
    Algebra.IsStandardSmoothOfRelativeDimension.out (R := R) (S := S) (n := n)
  let e₀ : σ ⊕ Fin n ≃ ι := ((Equiv.ofInjective _ P.map_inj).sumCongr
      (Finite.equivFinOfCardEq (by rw [Nat.card_coe_set_eq, Set.ncard_compl,
        Set.ncard_range_of_injective P.map_inj, ← e, Algebra.Presentation.dimension])).symm).trans
      (Equiv.Set.sumCompl _)
  let e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
    (MvPolynomial.sumAlgEquiv R _ _).symm.trans (MvPolynomial.renameEquiv _ e₀)
  let φ := e.toAlgHom.comp (IsScalarTower.toAlgHom _ (MvPolynomial (Fin n) R) _)
  algebraize [φ.toRingHom, (algebraMap P.Ring S).comp φ.toRingHom]
  have := IsScalarTower.of_algebraMap_eq' φ.comp_algebraMap.symm
  have : IsScalarTower R (MvPolynomial (Fin n) R) S := .to₁₂₄ _ _ P.Ring _
  refine ⟨IsScalarTower.toAlgHom _ _ _, ?_⟩
  have H : (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom =
      (algebraMap P.Ring S).comp e.toRingHom := by
    ext
    · simp [e, IsScalarTower.algebraMap_eq R (MvPolynomial (Fin n) R) S]
    · simp [e, @RingHom.algebraMap_toAlgebra (MvPolynomial (Fin n) R) S, φ]
    · simp [e]
  let P' : Algebra.PreSubmersivePresentation (MvPolynomial (Fin n) R) S σ σ :=
  { toGenerators := .ofSurjective (algebraMap _ _ <| e <| .X ·) <| by
      convert! P.algebraMap_surjective.comp e.surjective
      exact congr($H)
    relation := e.symm ∘ P.relation
    span_range_relation_eq_ker := by
      rw [Set.range_comp, ← AlgEquiv.coe_ringEquiv e.symm, AlgEquiv.symm_toRingEquiv,
        ← Ideal.map_span, P.span_range_relation_eq_ker, Ideal.map_symm]
      exact congr(RingHom.ker $H).symm
    map := _
    map_inj := Function.injective_id }
  let P' : Algebra.SubmersivePresentation (MvPolynomial (Fin n) R) S σ σ :=
  { __ := P'
    jacobian_isUnit := by
      convert! P.jacobian_isUnit using 1
      simp_rw [Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det, map_det]
      congr 1
      ext i j
      trans algebraMap P.Ring S (e ((e.symm (P.relation j)).pderiv i))
      · simpa [Algebra.PreSubmersivePresentation.jacobiMatrix_apply, P',
          Algebra.Generators.ofSurjective] using congr($H _)
      suffices e ((e.symm (P.relation j)).pderiv i) = (P.relation j).pderiv (P.map i) by
        simp [Algebra.PreSubmersivePresentation.jacobiMatrix_apply, this]
      simp [e, MvPolynomial.pderiv_sumToIter, ← MvPolynomial.pderiv_rename e₀.injective,
        show e₀ (Sum.inl i) = P.map i from rfl] }
  exact etale_algebraMap.mpr (Algebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero.mpr
    ⟨_, _, _, inferInstance, P', by simp [Algebra.Presentation.dimension]⟩)