awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
h₂' : Ideal.FG (RingHom.ker φ)
x : Sp
hx : Membership.mem (γ := Submodule Sp Sp) 𝓂[Sp] x
⊢ Membership.mem (γ := Submodule Sp Sp) (RingHom.ker ψ) x
have 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)
Tactic: obtain ⟨x, rfl⟩ := TensorProduct.mk_surjective _ _ _ (by exact residue_surjective) x
Cleared hypotheses: x, hx
-- 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)
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)
⊢ 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)
have this₁ : ¬IsUnit x
Tactic: have : ¬IsUnit x := fun h ↦ hx <| h.map TensorProduct.includeRight
-- 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)
h₂' : Ideal.FG (RingHom.ker φ)
⊢ FormallySmooth R S
have h₃ : 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]
-- 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)
h₂' : Ideal.FG (RingHom.ker φ)
h₃ : LE.le (α := Ideal Sp) 𝓂[Sp] (RingHom.ker ψ)
⊢ FormallySmooth R S
have 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])
Tactic: rw [Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField (P := P) h₁ 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)
h₂' : Ideal.FG (RingHom.ker φ)
h₃ : LE.le (α := Ideal Sp) 𝓂[Sp] (RingHom.ker ψ)
⊢ 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])
have this₁ : 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
-- 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)
M : Submonoid P
inst_12 : IsLocalization M S
inst_13 : FinitePresentation R P
⊢ FormallySmooth R S
have obtain : ∀ (n : ℕ) (f₀ : MvPolynomial (Fin n) R →ₐ[R] P)
  (hf₀ :
    Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin n) R) (β := P)
      (⇑f₀ : (a : MvPolynomial (Fin n) R) → P)),
  FormallySmooth R S
Tactic: obtain ⟨n, f₀, hf₀⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp
    (inferInstance : Algebra.FiniteType R P)
-- 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)
M : Submonoid P
inst_12 : IsLocalization M S
inst_13 : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin n) R) (β := P) (⇑f₀ : (a : MvPolynomial (Fin n) R) → P)
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S :=
  IsLocalization.liftAlgHom (R := MvPolynomial (Fin n) R) (M := M') (f := AlgHom.comp (IsScalarTower.toAlgHom R P S) f₀)
    ⋯
x : S
⊢ ∃ (a : P'), (fP : (a : P') → S) a = x
have obtain : ∀ (x s : P) (hs : s ∈ M),
  ∃ (a : P'), (fP : (a : P') → S) a = IsLocalization.mk' S x (Subtype.mk (p := fun (x : P) ↦ x ∈ M) s hs)
Tactic: obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M x
Cleared hypotheses: x
-- 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)
M : Submonoid P
inst_12 : IsLocalization M S
inst_13 : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin n) R) (β := P) (⇑f₀ : (a : MvPolynomial (Fin n) R) → P)
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S :=
  IsLocalization.liftAlgHom (R := MvPolynomial (Fin n) R) (M := M') (f := AlgHom.comp (IsScalarTower.toAlgHom R P S) f₀)
    ⋯
x s : P
hs : s ∈ M
⊢ ∃ (a : P'), (fP : (a : P') → S) a = IsLocalization.mk' S x (Subtype.mk (p := fun (x : P) ↦ x ∈ M) s hs)
have obtain : ∀ (x : MvPolynomial (Fin n) R),
  ∃ (a : P'),
    (fP : (a : P') → S) a =
      IsLocalization.mk' S ((f₀ : (a : MvPolynomial (Fin n) R) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ M) s hs)
Tactic: obtain ⟨x, rfl⟩ := hf₀ x
Cleared hypotheses: x
-- 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)
M : Submonoid P
inst_12 : IsLocalization M S
inst_13 : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin n) R) (β := P) (⇑f₀ : (a : MvPolynomial (Fin n) R) → P)
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S :=
  IsLocalization.liftAlgHom (R := MvPolynomial (Fin n) R) (M := M') (f := AlgHom.comp (IsScalarTower.toAlgHom R P S) f₀)
    ⋯
s : P
hs : s ∈ M
x : MvPolynomial (Fin n) R
⊢ ∃ (a : P'),
    (fP : (a : P') → S) a =
      IsLocalization.mk' S ((f₀ : (a : MvPolynomial (Fin n) R) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ M) s hs)
have obtain : ∀ (s : MvPolynomial (Fin n) R) (hs : Membership.mem (α := P) M ((f₀ : (a : MvPolynomial (Fin n) R) → P) s : P)),
  ∃ (a : P'),
    (fP : (a : P') → S) a =
      IsLocalization.mk'.{u_3, u_2} (R := P) (M := M) S ((f₀ : (a : MvPolynomial (Fin n) R) → P) x : P)
        (Subtype.mk (p := fun (x : P) ↦ x ∈ M) ((f₀ : (a : MvPolynomial (Fin n) R) → P) s) hs : ↥M)
Tactic: obtain ⟨s, rfl⟩ := hf₀ s
Cleared hypotheses: s, hs
-- 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)
M : Submonoid P
inst_12 : IsLocalization M S
inst_13 : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin n) R) (β := P) (⇑f₀ : (a : MvPolynomial (Fin n) R) → P)
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S :=
  IsLocalization.liftAlgHom (R := MvPolynomial (Fin n) R) (M := M') (f := AlgHom.comp (IsScalarTower.toAlgHom R P S) f₀)
    ⋯
x s : MvPolynomial (Fin n) R
hs : Membership.mem (α := P) M ((f₀ : (a : MvPolynomial (Fin n) R) → P) s : P)
⊢ ∃ (a : P'),
    (fP : (a : P') → S) a =
      IsLocalization.mk'.{u_3, u_2} (R := P) (M := M) S ((f₀ : (a : MvPolynomial (Fin n) R) → P) x : P)
        (Subtype.mk (p := fun (x : P) ↦ x ∈ M) ((f₀ : (a : MvPolynomial (Fin n) R) → P) s) hs : ↥M)
have refine : (fP : (a : P') → S)
    (IsLocalization.mk' (M := M') P' x (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦ x ∈ M') s hs)) =
  IsLocalization.mk'.{u_3, u_2} (R := P) (M := M) S ((f₀ : (a : MvPolynomial (Fin n) R) → P) x : P)
    (Subtype.mk (p := fun (x : P) ↦ x ∈ M) ((f₀ : (a : MvPolynomial (Fin n) R) → P) s) hs : ↥M)
Tactic: refine ⟨IsLocalization.mk' (M := M') _ x ⟨s, hs⟩, ?_⟩
-- 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)
M : Submonoid P
inst_12 : IsLocalization M S
inst_13 : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin n) R) (β := P) (⇑f₀ : (a : MvPolynomial (Fin n) R) → P)
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S :=
  IsLocalization.liftAlgHom (R := MvPolynomial (Fin n) R) (M := M') (f := AlgHom.comp (IsScalarTower.toAlgHom R P S) f₀)
    ⋯
⊢ FormallySmooth R S
have hf₁ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := P') (β := S) (⇑fP : (a : P') → S)
Tactic: have hf₁ : Function.Surjective fP := by
    intro x
    obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M x
    obtain ⟨x, rfl⟩ := hf₀ x
    obtain ⟨s, rfl⟩ := hf₀ s
    refine ⟨IsLocalization.mk' (M := M') _ x ⟨s, hs⟩, ?_⟩
    simp [fP, IsLocalization.lift_mk', Units.mul_inv_eq_iff_eq_mul, IsUnit.liftRight]
-- 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)
M : Submonoid P
inst_12 : IsLocalization M S
inst_13 : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin n) R) (β := P) (⇑f₀ : (a : MvPolynomial (Fin n) R) → P)
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S :=
  IsLocalization.liftAlgHom (R := MvPolynomial (Fin n) R) (M := M') (f := AlgHom.comp (IsScalarTower.toAlgHom R P S) f₀)
    ⋯
hf₁ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := P') (β := S) (⇑fP : (a : P') → S)
⊢ Ideal.FG (RingHom.ker fP)
have this : Ideal.FG (RingHom.ker f₀.toRingHom)
Tactic: have := Algebra.FinitePresentation.ker_fG_of_surjective _ hf₀
-- 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)
M : Submonoid P
inst_12 : IsLocalization M S
inst_13 : FinitePresentation R P
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin n) R) (β := P) (⇑f₀ : (a : MvPolynomial (Fin n) R) → P)
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S :=
  IsLocalization.liftAlgHom (R := MvPolynomial (Fin n) R) (M := M') (f := AlgHom.comp (IsScalarTower.toAlgHom R P S) f₀)
    ⋯
hf₁ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := P') (β := S) (⇑fP : (a : P') → S)
this : Ideal.FG (RingHom.ker f₀.toRingHom)
⊢ Ideal.FG (RingHom.ker fP)
have h : Eq (α := Ideal P') (RingHom.ker fP)
  (Ideal.map (F := MvPolynomial (Fin n) R →+* P') (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker f₀.toRingHom))
Tactic: convert! this.map (algebraMap _ P')