awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.Fiber
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] := ⋯
⊢ IsScalarTower 𝓀[R] Pp Sp

Tactic:
have := IsScalarTower.of_algebraMap_eq' φ.comp_algebraMap.symm
-- Module: Mathlib.RingTheory.Smooth.Fiber
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
⊢ IsScalarTower R Sp 𝓀[S]

Tactic:
have := IsScalarTower.of_algebraMap_eq' ψ.comp_algebraMap.symm
-- Module: Mathlib.RingTheory.Smooth.Fiber
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]
⊢ IsScalarTower P S Sp

Tactic:
have : IsScalarTower P S Sp := .of_algebraMap_eq' rfl
-- Module: Mathlib.RingTheory.Smooth.Fiber
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
r : S
⊢ Eq (α := 𝓀[S]) ((algebraMap S 𝓀[S] : (a : S) → 𝓀[S]) r : 𝓀[S])
    ((algebraMap Sp 𝓀[S] : (a : Sp) → 𝓀[S]) ((algebraMap S Sp : (a : S) → Sp) r) : 𝓀[S])

Tactic:
simp [RingHom.algebraMap_toAlgebra, ψ, Sp]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.Smooth.Fiber
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
⊢ IsScalarTower S Sp 𝓀[S]

Tactic:
have : IsScalarTower S Sp 𝓀[S] := .of_algebraMap_eq fun r ↦ by
    simp [RingHom.algebraMap_toAlgebra, ψ, Sp]
-- Module: Mathlib.RingTheory.Smooth.Fiber
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]
⊢ IsScalarTower P Sp 𝓀[S]

Tactic:
have : IsScalarTower P Sp 𝓀[S] := .to₁₃₄ _ S _ _
-- Module: Mathlib.RingTheory.Smooth.Fiber
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]
⊢ IsScalarTower P Pp 𝓀[S]

Tactic:
have : IsScalarTower P Pp 𝓀[S] := .to₁₂₄ _ _ Sp _
-- Module: Mathlib.RingTheory.Smooth.Fiber
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)
⊢ Module.Free Pp Ω[Pp⁄𝓀[R]]

Tactic:
have : Module.Free Pp Ω[Pp⁄𝓀[R]] := .of_equiv e₀.symm
-- Module: Mathlib.RingTheory.Smooth.Fiber
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]]
⊢ Module.Finite Pp Ω[Pp⁄𝓀[R]]

Tactic:
have : Module.Finite Pp Ω[Pp⁄𝓀[R]] := .of_surjective e₀.symm.toLinearMap e₀.symm.surjective
-- Module: Mathlib.RingTheory.Smooth.Fiber
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₁
⊢ Function.Surjective (α := Pp) (β := Sp) (⇑φ : (a : Pp) → Sp)

Tactic:
have h₁' : Function.Surjective φ := LinearMap.lTensor_surjective _ h₁
-- Module: Mathlib.RingTheory.Smooth.Fiber
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)
suffices : Module.Finite Pp ↥(RingHom.ker φ)
⊢ Ideal.FG (RingHom.ker φ)

Tactic:
suffices Module.Finite Pp (RingHom.ker φ) from (Submodule.fg_top _).mp this.1
-- Module: Mathlib.RingTheory.Smooth.Fiber
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 P ↥(RingHom.ker (F := P →+* S) (algebraMap P S))

Tactic:
have : Module.Finite P (RingHom.ker (algebraMap P S)) := ⟨(Submodule.fg_top _).mpr h₂⟩
-- Module: Mathlib.RingTheory.Smooth.Fiber
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_8 : 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)
this : Module.Finite P ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
⊢ Module.Finite Pp ↥(RingHom.ker φ)

Tactic:
.equiv e₁.symm

Premises used: LinearEquiv.symm, Module.Finite.equiv