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] := ⋯
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:
exact .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_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 φ)

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
-- 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)
h₂' : Ideal.FG (RingHom.ker φ)
x : Sp
hx : Membership.mem (γ := Submodule Sp Sp) 𝓂[Sp] x
⊢ Function.Surjective (α := R) (β := 𝓀[R]) (⇑(algebraMap R 𝓀[R]) : (a : R) → 𝓀[R])

Tactic:
residue_surjective

Premises used: Submodule.Quotient.mk, IsLocalRing.residue_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₁
h₁' : Function.Surjective (α := Pp) (β := Sp) (⇑φ : (a : Pp) → Sp)
h₂' : Ideal.FG (RingHom.ker φ)
x : Sp
hx : Membership.mem (γ := Submodule Sp Sp) 𝓂[Sp] x
⊢ Function.Surjective (α := R) (β := 𝓀[R]) (⇑(algebraMap R 𝓀[R]) : (a : R) → 𝓀[R])

Tactic:
exact residue_surjective

Premises used: IsLocalRing.residue_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₁
h₁' : Function.Surjective (α := Pp) (β := Sp) (⇑φ : (a : Pp) → Sp)
h₂' : Ideal.FG (RingHom.ker φ)
x : Sp
hx : Membership.mem (γ := Submodule Sp Sp) 𝓂[Sp] x
obtain :
  ∀ (x : S)
    (hx :
      Membership.mem (α := Sp) (γ := Submodule Sp Sp) 𝓂[Sp]
        (((TensorProduct.mk R 𝓀[R] S : (a : 𝓀[R]) → S →ₗ[R] 𝓀[R] ⊗[R] S) 1 : (a : S) → 𝓀[R] ⊗[R] S) x : 𝓀[R] ⊗[R] S)),
    Membership.mem (α := Sp) (γ := Submodule Sp Sp) (RingHom.ker ψ)
      (((TensorProduct.mk R 𝓀[R] S : (a : 𝓀[R]) → S →ₗ[R] 𝓀[R] ⊗[R] S) 1 : (a : S) → 𝓀[R] ⊗[R] S) x : 𝓀[R] ⊗[R] S)
⊢ Membership.mem (γ := Submodule Sp Sp) (RingHom.ker ψ) x

Tactic:
obtain ⟨x, rfl⟩ := TensorProduct.mk_surjective _ _ _ (by exact residue_surjective) x

Premises used: TensorProduct.mk_surjective, 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_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)
h₂' : Ideal.FG (RingHom.ker φ)
x : S
hx :
  Membership.mem (α := Sp) (γ := Submodule Sp Sp) 𝓂[Sp]
    (((TensorProduct.mk R 𝓀[R] S : (a : 𝓀[R]) → S →ₗ[R] 𝓀[R] ⊗[R] S) 1 : (a : S) → 𝓀[R] ⊗[R] S) x : 𝓀[R] ⊗[R] S)
⊢ ¬IsUnit x

Tactic:
have : ¬IsUnit x := fun h ↦ hx <| h.map TensorProduct.includeRight
-- 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)
h₂' : Ideal.FG (RingHom.ker φ)
x : S
hx :
  Membership.mem (α := Sp) (γ := Submodule Sp Sp) 𝓂[Sp]
    (((TensorProduct.mk R 𝓀[R] S : (a : 𝓀[R]) → S →ₗ[R] 𝓀[R] ⊗[R] S) 1 : (a : S) → 𝓀[R] ⊗[R] S) x : 𝓀[R] ⊗[R] S)
this : ¬IsUnit x
⊢ Membership.mem (α := Sp) (γ := Submodule Sp Sp) (RingHom.ker ψ)
    (((TensorProduct.mk R 𝓀[R] S : (a : 𝓀[R]) → S →ₗ[R] 𝓀[R] ⊗[R] S) 1 : (a : S) → 𝓀[R] ⊗[R] S) x : 𝓀[R] ⊗[R] S)

Tactic:
simpa [ψ, 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_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)
h₂' : Ideal.FG (RingHom.ker φ)
⊢ LE.le (α := Ideal Sp) 𝓂[Sp] (RingHom.ker ψ)

Tactic:
have h₃ : 𝓂[Sp] ≤ RingHom.ker ψ := by
    intro x hx
    obtain ⟨x, rfl⟩ := TensorProduct.mk_surjective _ _ _ (by exact residue_surjective) x
    have : ¬IsUnit x := fun h ↦ hx <| h.map TensorProduct.includeRight
    simpa [ψ, 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_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)
h₂' : Ideal.FG (RingHom.ker φ)
h₃ : LE.le (α := Ideal Sp) 𝓂[Sp] (RingHom.ker ψ)
rw :
  Function.Injective (α := TensorProduct.{u_3, u_2, u_3} P 𝓀[S] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) (β :=
    TensorProduct.{u_3, u_2, u_3} P 𝓀[S] Ω[P⁄R])
    (⇑(KaehlerDifferential.cotangentComplexBaseChange R S P 𝓀[S]) :
      (a : 𝓀[S] ⊗[P] ↥(RingHom.ker (algebraMap P S))) → 𝓀[S] ⊗[P] Ω[P⁄R])
⊢ FormallySmooth R S

Tactic:
rw [Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField (P := P) h₁ h₂]

Premises used: Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField
-- 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)
h₂' : Ideal.FG (RingHom.ker φ)
h₃ : LE.le (α := Ideal Sp) 𝓂[Sp] (RingHom.ker ψ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have := (Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange
    (R := 𝓀[R]) _ _ h₁' h₂' h₃).mp inferInstance