awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (hypothesis)
Goal:
R : Type u_4
A : Type u_5
Rₘ : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing Rₘ
inst_3 : CommRing Sₘ
M : Submonoid R
inst_4 : Algebra R A
inst_5 : Algebra R Sₘ
inst_6 : Algebra A Sₘ
inst_7 : Algebra R Rₘ
inst_8 : Algebra Rₘ Sₘ
inst_9 : IsScalarTower R Rₘ Sₘ
inst_10 : IsScalarTower R A Sₘ
inst_11 : IsLocalization M Rₘ
inst_12 : IsLocalization (Submonoid.map (F := R →+* A) (algebraMap R A) M) Sₘ
inst_13 : FormallySmooth R A
this : FormallySmooth A Sₘ
⊢ FormallySmooth Rₘ Sₘ
have this₁ : FormallySmooth R Sₘ
Tactic: haveI : FormallySmooth R Sₘ := FormallySmooth.comp R A Sₘ
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : IsLocalRing R
inst_9 : IsLocalRing S
inst_10 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_11 : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst : Algebra Pp Sp := φ.toAlgebra
algInst_1 : Algebra P Sp := RingHom.toAlgebra (φ.comp (algebraMap P Pp))
algInst_2 : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst_3 : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst : IsScalarTower P Pp Sp := ⋯
scalarTowerInst_1 : IsScalarTower Pp Sp 𝓀[S] := ⋯
⊢ FormallySmooth R S
have this : IsScalarTower 𝓀[R] Pp Sp
Tactic: have := IsScalarTower.of_algebraMap_eq' φ.comp_algebraMap.symm
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : IsLocalRing R
inst_9 : IsLocalRing S
inst_10 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_11 : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst : Algebra Pp Sp := φ.toAlgebra
algInst_1 : Algebra P Sp := RingHom.toAlgebra (φ.comp (algebraMap P Pp))
algInst_2 : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst_3 : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst : IsScalarTower P Pp Sp := ⋯
scalarTowerInst_1 : IsScalarTower Pp Sp 𝓀[S] := ⋯
this : IsScalarTower 𝓀[R] Pp Sp
⊢ FormallySmooth R S
have this₁ : IsScalarTower R Sp 𝓀[S]
Tactic: have := IsScalarTower.of_algebraMap_eq' ψ.comp_algebraMap.symm
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : IsLocalRing R
inst_9 : IsLocalRing S
inst_10 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_11 : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst : Algebra Pp Sp := φ.toAlgebra
algInst_1 : Algebra P Sp := RingHom.toAlgebra (φ.comp (algebraMap P Pp))
algInst_2 : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst_3 : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst : IsScalarTower P Pp Sp := ⋯
scalarTowerInst_1 : IsScalarTower Pp Sp 𝓀[S] := ⋯
this_1 : IsScalarTower 𝓀[R] Pp Sp
this : IsScalarTower R Sp 𝓀[S]
⊢ FormallySmooth R S
have this₁ : IsScalarTower P S Sp
Tactic: have : IsScalarTower P S Sp := .of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : IsLocalRing R
inst_9 : IsLocalRing S
inst_10 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_11 : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst : Algebra Pp Sp := φ.toAlgebra
algInst_1 : Algebra P Sp := RingHom.toAlgebra (φ.comp (algebraMap P Pp))
algInst_2 : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst_3 : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst : IsScalarTower P Pp Sp := ⋯
scalarTowerInst_1 : IsScalarTower Pp Sp 𝓀[S] := ⋯
this_1 : IsScalarTower 𝓀[R] Pp Sp
this_2 : IsScalarTower R Sp 𝓀[S]
this : IsScalarTower P S Sp
⊢ FormallySmooth R S
have this₁ : IsScalarTower S Sp 𝓀[S]
Tactic: have : IsScalarTower S Sp 𝓀[S] := .of_algebraMap_eq fun r ↦ by
    simp [RingHom.algebraMap_toAlgebra, ψ, Sp]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : IsLocalRing R
inst_9 : IsLocalRing S
inst_10 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_11 : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst : Algebra Pp Sp := φ.toAlgebra
algInst_1 : Algebra P Sp := RingHom.toAlgebra (φ.comp (algebraMap P Pp))
algInst_2 : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst_3 : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst : IsScalarTower P Pp Sp := ⋯
scalarTowerInst_1 : IsScalarTower Pp Sp 𝓀[S] := ⋯
this_1 : IsScalarTower 𝓀[R] Pp Sp
this_2 : IsScalarTower R Sp 𝓀[S]
this_3 : IsScalarTower P S Sp
this : IsScalarTower S Sp 𝓀[S]
⊢ FormallySmooth R S
have this₁ : IsScalarTower P Sp 𝓀[S]
Tactic: have : IsScalarTower P Sp 𝓀[S] := .to₁₃₄ _ S _ _
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : IsLocalRing R
inst_9 : IsLocalRing S
inst_10 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_11 : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst : Algebra Pp Sp := φ.toAlgebra
algInst_1 : Algebra P Sp := RingHom.toAlgebra (φ.comp (algebraMap P Pp))
algInst_2 : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst_3 : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst : IsScalarTower P Pp Sp := ⋯
scalarTowerInst_1 : IsScalarTower Pp Sp 𝓀[S] := ⋯
this_1 : IsScalarTower 𝓀[R] Pp Sp
this_2 : IsScalarTower R Sp 𝓀[S]
this_3 : IsScalarTower P S Sp
this_4 : IsScalarTower S Sp 𝓀[S]
this : IsScalarTower P Sp 𝓀[S]
⊢ FormallySmooth R S
have this₁ : IsScalarTower P Pp 𝓀[S]
Tactic: have : IsScalarTower P Pp 𝓀[S] := .to₁₂₄ _ _ Sp _
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : IsLocalRing R
inst_9 : IsLocalRing S
inst_10 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_11 : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst : Algebra Pp Sp := φ.toAlgebra
algInst_1 : Algebra P Sp := RingHom.toAlgebra (φ.comp (algebraMap P Pp))
algInst_2 : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst_3 : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst : IsScalarTower P Pp Sp := ⋯
scalarTowerInst_1 : IsScalarTower Pp Sp 𝓀[S] := ⋯
this_1 : IsScalarTower 𝓀[R] Pp Sp
this_2 : IsScalarTower R Sp 𝓀[S]
this_3 : IsScalarTower P S Sp
this_4 : IsScalarTower S Sp 𝓀[S]
this_5 : IsScalarTower P Sp 𝓀[S]
this : IsScalarTower P Pp 𝓀[S]
ePp : Pp ≃ₐ[P] P ⊗[R] 𝓀[R] :=
  let __spread.0 : 𝓀[R] ⊗[R] P ≃ₐ[R] P ⊗[R] 𝓀[R] := TensorProduct.comm R 𝓀[R] P;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₀ : Ω[Pp⁄𝓀[R]] ≃ₗ[Pp] Pp ⊗[P] Ω[P⁄R] := LinearEquiv.symm (KaehlerDifferential.tensorKaehlerEquiv R 𝓀[R] P Pp)
⊢ FormallySmooth R S
have this₁ : Module.Free Pp Ω[Pp⁄𝓀[R]]
Tactic: have : Module.Free Pp Ω[Pp⁄𝓀[R]] := .of_equiv e₀.symm
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : IsLocalRing R
inst_9 : IsLocalRing S
inst_10 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_11 : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst : Algebra Pp Sp := φ.toAlgebra
algInst_1 : Algebra P Sp := RingHom.toAlgebra (φ.comp (algebraMap P Pp))
algInst_2 : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst_3 : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst : IsScalarTower P Pp Sp := ⋯
scalarTowerInst_1 : IsScalarTower Pp Sp 𝓀[S] := ⋯
this_1 : IsScalarTower 𝓀[R] Pp Sp
this_2 : IsScalarTower R Sp 𝓀[S]
this_3 : IsScalarTower P S Sp
this_4 : IsScalarTower S Sp 𝓀[S]
this_5 : IsScalarTower P Sp 𝓀[S]
this_6 : IsScalarTower P Pp 𝓀[S]
ePp : Pp ≃ₐ[P] P ⊗[R] 𝓀[R] :=
  let __spread.0 : 𝓀[R] ⊗[R] P ≃ₐ[R] P ⊗[R] 𝓀[R] := TensorProduct.comm R 𝓀[R] P;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₀ : Ω[Pp⁄𝓀[R]] ≃ₗ[Pp] Pp ⊗[P] Ω[P⁄R] := LinearEquiv.symm (KaehlerDifferential.tensorKaehlerEquiv R 𝓀[R] P Pp)
this : Module.Free Pp Ω[Pp⁄𝓀[R]]
⊢ FormallySmooth R S
have this₁ : Module.Finite Pp Ω[Pp⁄𝓀[R]]
Tactic: have : Module.Finite Pp Ω[Pp⁄𝓀[R]] := .of_surjective e₀.symm.toLinearMap e₀.symm.surjective
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : IsLocalRing R
inst_9 : IsLocalRing S
inst_10 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_11 : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst : Algebra Pp Sp := φ.toAlgebra
algInst_1 : Algebra P Sp := RingHom.toAlgebra (φ.comp (algebraMap P Pp))
algInst_2 : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst_3 : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst : IsScalarTower P Pp Sp := ⋯
scalarTowerInst_1 : IsScalarTower Pp Sp 𝓀[S] := ⋯
this_1 : IsScalarTower 𝓀[R] Pp Sp
this_2 : IsScalarTower R Sp 𝓀[S]
this_3 : IsScalarTower P S Sp
this_4 : IsScalarTower S Sp 𝓀[S]
this_5 : IsScalarTower P Sp 𝓀[S]
this_6 : IsScalarTower P Pp 𝓀[S]
ePp : Pp ≃ₐ[P] P ⊗[R] 𝓀[R] :=
  let __spread.0 : 𝓀[R] ⊗[R] P ≃ₐ[R] P ⊗[R] 𝓀[R] := TensorProduct.comm R 𝓀[R] P;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₀ : Ω[Pp⁄𝓀[R]] ≃ₗ[Pp] Pp ⊗[P] Ω[P⁄R] := LinearEquiv.symm (KaehlerDifferential.tensorKaehlerEquiv R 𝓀[R] P Pp)
this_7 : Module.Free Pp Ω[Pp⁄𝓀[R]]
this : Module.Finite Pp Ω[Pp⁄𝓀[R]]
e₁ : ↥(RingHom.ker φ) ≃ₗ[Pp] Pp ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) :=
  kerTensorProductMapIdToAlgHomEquiv R P S 𝓀[R] h₁
⊢ FormallySmooth R S
have h₁' : Function.Surjective (α := Pp) (β := Sp) (⇑φ : (a : Pp) → Sp)
Tactic: have h₁' : Function.Surjective φ := LinearMap.lTensor_surjective _ h₁
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (goal)
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : IsLocalRing R
inst_9 : IsLocalRing S
inst_10 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_11 : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst : Algebra Pp Sp := φ.toAlgebra
algInst_1 : Algebra P Sp := RingHom.toAlgebra (φ.comp (algebraMap P Pp))
algInst_2 : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst_3 : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst : IsScalarTower P Pp Sp := ⋯
scalarTowerInst_1 : IsScalarTower Pp Sp 𝓀[S] := ⋯
this_1 : IsScalarTower 𝓀[R] Pp Sp
this_2 : IsScalarTower R Sp 𝓀[S]
this_3 : IsScalarTower P S Sp
this_4 : IsScalarTower S Sp 𝓀[S]
this_5 : IsScalarTower P Sp 𝓀[S]
this_6 : IsScalarTower P Pp 𝓀[S]
ePp : Pp ≃ₐ[P] P ⊗[R] 𝓀[R] :=
  let __spread.0 : 𝓀[R] ⊗[R] P ≃ₐ[R] P ⊗[R] 𝓀[R] := TensorProduct.comm R 𝓀[R] P;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₀ : Ω[Pp⁄𝓀[R]] ≃ₗ[Pp] Pp ⊗[P] Ω[P⁄R] := LinearEquiv.symm (KaehlerDifferential.tensorKaehlerEquiv R 𝓀[R] P Pp)
this_7 : Module.Free Pp Ω[Pp⁄𝓀[R]]
this : Module.Finite Pp Ω[Pp⁄𝓀[R]]
e₁ : ↥(RingHom.ker φ) ≃ₗ[Pp] Pp ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) :=
  kerTensorProductMapIdToAlgHomEquiv R P S 𝓀[R] h₁
h₁' : Function.Surjective (α := Pp) (β := Sp) (⇑φ : (a : Pp) → Sp)
⊢ Ideal.FG (RingHom.ker φ)
have suffices : Module.Finite Pp ↥(RingHom.ker φ)
Tactic: suffices Module.Finite Pp (RingHom.ker φ) from (Submodule.fg_top _).mp this.1
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : IsLocalRing R
inst_9 : IsLocalRing S
inst_10 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_11 : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst : Algebra Pp Sp := φ.toAlgebra
algInst_1 : Algebra P Sp := RingHom.toAlgebra (φ.comp (algebraMap P Pp))
algInst_2 : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst_3 : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst : IsScalarTower P Pp Sp := ⋯
scalarTowerInst_1 : IsScalarTower Pp Sp 𝓀[S] := ⋯
this_1 : IsScalarTower 𝓀[R] Pp Sp
this_2 : IsScalarTower R Sp 𝓀[S]
this_3 : IsScalarTower P S Sp
this_4 : IsScalarTower S Sp 𝓀[S]
this_5 : IsScalarTower P Sp 𝓀[S]
this_6 : IsScalarTower P Pp 𝓀[S]
ePp : Pp ≃ₐ[P] P ⊗[R] 𝓀[R] :=
  let __spread.0 : 𝓀[R] ⊗[R] P ≃ₐ[R] P ⊗[R] 𝓀[R] := TensorProduct.comm R 𝓀[R] P;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₀ : Ω[Pp⁄𝓀[R]] ≃ₗ[Pp] Pp ⊗[P] Ω[P⁄R] := LinearEquiv.symm (KaehlerDifferential.tensorKaehlerEquiv R 𝓀[R] P Pp)
this_7 : Module.Free Pp Ω[Pp⁄𝓀[R]]
this : Module.Finite Pp Ω[Pp⁄𝓀[R]]
e₁ : ↥(RingHom.ker φ) ≃ₗ[Pp] Pp ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) :=
  kerTensorProductMapIdToAlgHomEquiv R P S 𝓀[R] h₁
h₁' : Function.Surjective (α := Pp) (β := Sp) (⇑φ : (a : Pp) → Sp)
⊢ Module.Finite Pp ↥(RingHom.ker φ)
have this₁ : Module.Finite P ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
Tactic: have : Module.Finite P (RingHom.ker (algebraMap P S)) := ⟨(Submodule.fg_top _).mpr h₂⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : IsLocalRing R
inst_9 : IsLocalRing S
inst_10 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_11 : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst : Algebra Pp Sp := φ.toAlgebra
algInst_1 : Algebra P Sp := RingHom.toAlgebra (φ.comp (algebraMap P Pp))
algInst_2 : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst_3 : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst : IsScalarTower P Pp Sp := ⋯
scalarTowerInst_1 : IsScalarTower Pp Sp 𝓀[S] := ⋯
this_1 : IsScalarTower 𝓀[R] Pp Sp
this_2 : IsScalarTower R Sp 𝓀[S]
this_3 : IsScalarTower P S Sp
this_4 : IsScalarTower S Sp 𝓀[S]
this_5 : IsScalarTower P Sp 𝓀[S]
this_6 : IsScalarTower P Pp 𝓀[S]
ePp : Pp ≃ₐ[P] P ⊗[R] 𝓀[R] :=
  let __spread.0 : 𝓀[R] ⊗[R] P ≃ₐ[R] P ⊗[R] 𝓀[R] := TensorProduct.comm R 𝓀[R] P;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₀ : Ω[Pp⁄𝓀[R]] ≃ₗ[Pp] Pp ⊗[P] Ω[P⁄R] := LinearEquiv.symm (KaehlerDifferential.tensorKaehlerEquiv R 𝓀[R] P Pp)
this_7 : Module.Free Pp Ω[Pp⁄𝓀[R]]
this : Module.Finite Pp Ω[Pp⁄𝓀[R]]
e₁ : ↥(RingHom.ker φ) ≃ₗ[Pp] Pp ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) :=
  kerTensorProductMapIdToAlgHomEquiv R P S 𝓀[R] h₁
h₁' : Function.Surjective (α := Pp) (β := Sp) (⇑φ : (a : Pp) → Sp)
⊢ FormallySmooth R S
have h₂' : Ideal.FG (RingHom.ker φ)
Tactic: have h₂' : (RingHom.ker φ).FG := by
    suffices Module.Finite Pp (RingHom.ker φ) from (Submodule.fg_top _).mp this.1
    have : Module.Finite P (RingHom.ker (algebraMap P S)) := ⟨(Submodule.fg_top _).mpr h₂⟩
    exact .equiv e₁.symm