awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : FinitePresentation R S
p : Ideal R
q : Ideal S
inst_5 : p.IsPrime
inst_6 : q.IsPrime
inst_7 : q.LiesOver p
inst_8 : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom (R := S) (M := algebraMapSubmonoid S p.primeCompl) (f := ofId S Sq) ⋯
algInst : Algebra Sp Sq := f.toAlgebra
this_2 : IsScalarTower R Sp Sq
this_3 : IsScalarTower Rp Sp Sq
this_4 : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
this_5 : FinitePresentation Rp Sp
this : Algebra S (𝓀[Rp] ⊗[R] S) := TensorProduct.rightAlgebra
⊢ FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[Rp] Sq)
have this₁ : FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[R] S ⊗[S] Sq)
Tactic: have : FormallySmooth 𝓀[Rp] ((𝓀[Rp] ⊗[R] S) ⊗[S] Sq) :=
      .comp _ (𝓀[Rp] ⊗[R] S) _
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : FinitePresentation R S
p : Ideal R
q : Ideal S
inst_5 : p.IsPrime
inst_6 : q.IsPrime
inst_7 : q.LiesOver p
inst_8 : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom (R := S) (M := algebraMapSubmonoid S p.primeCompl) (f := ofId S Sq) ⋯
algInst : Algebra Sp Sq := f.toAlgebra
this_2 : IsScalarTower R Sp Sq
this_3 : IsScalarTower Rp Sp Sq
this_4 : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
this_5 : FinitePresentation Rp Sp
this_6 : Algebra S (𝓀[Rp] ⊗[R] S) := TensorProduct.rightAlgebra
this : FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[R] S ⊗[S] Sq)
e : 𝓀[Rp] ⊗[R] S ≃ₐ[S] S ⊗[R] 𝓀[Rp] :=
  let __spread.0 : 𝓀[Rp] ⊗[R] S ≃ₐ[R] S ⊗[R] 𝓀[Rp] := TensorProduct.comm R 𝓀[Rp] S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e' : 𝓀[Rp] ⊗[R] S ⊗[S] Sq ≃ₐ[R] 𝓀[Rp] ⊗[Rp] Sq :=
  AlgEquiv.trans (AlgEquiv.restrictScalars R (TensorProduct.comm S (𝓀[Rp] ⊗[R] S) Sq))
    (AlgEquiv.trans (A₂ := Sq ⊗[S] (S ⊗[R] 𝓀[Rp]))
      (AlgEquiv.restrictScalars R (S := S)
        (TensorProduct.congr AlgEquiv.refl e : Sq ⊗[S] (𝓀[Rp] ⊗[R] S) ≃ₐ[S] Sq ⊗[S] (S ⊗[R] 𝓀[Rp])))
      (AlgEquiv.trans (A₂ := Sq ⊗[R] 𝓀[Rp])
        (AlgEquiv.restrictScalars R
          (TensorProduct.cancelBaseChange R S S Sq 𝓀[Rp] : Sq ⊗[S] (S ⊗[R] 𝓀[Rp]) ≃ₐ[S] Sq ⊗[R] 𝓀[Rp]))
        (AlgEquiv.trans (TensorProduct.comm R Sq 𝓀[Rp]) (TensorProduct.equivOfCompatibleSMul Rp R R 𝓀[Rp] Sq))))
⊢ FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[Rp] Sq)
have this₁ : Eq (α := p.ResidueField →ₐ[R] 𝓀[Rp] ⊗[Rp] Sq)
  ((↑e' : 𝓀[Rp] ⊗[R] S ⊗[S] Sq →ₐ[R] 𝓀[Rp] ⊗[Rp] Sq).comp
    (IsScalarTower.toAlgHom R p.ResidueField (𝓀[Rp] ⊗[R] S ⊗[S] Sq)))
  (IsScalarTower.toAlgHom R p.ResidueField (𝓀[Rp] ⊗[Rp] Sq))
Tactic: have : e'.toAlgHom.comp (IsScalarTower.toAlgHom R p.ResidueField _) =
        IsScalarTower.toAlgHom _ _ _ := by ext
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : FinitePresentation R S
p : Ideal R
q : Ideal S
inst_5 : p.IsPrime
inst_6 : q.IsPrime
inst_7 : q.LiesOver p
inst_8 : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom (R := S) (M := algebraMapSubmonoid S p.primeCompl) (f := ofId S Sq) ⋯
algInst : Algebra Sp Sq := f.toAlgebra
this_2 : IsScalarTower R Sp Sq
this_3 : IsScalarTower Rp Sp Sq
this_4 : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
this : FinitePresentation Rp Sp
⊢ IsSmoothAt R q
have this₁ : FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[Rp] Sq)
Tactic: have : FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[Rp] Sq) := by
    let : Algebra S (𝓀[Rp] ⊗[R] S) := TensorProduct.rightAlgebra
    have : FormallySmooth 𝓀[Rp] ((𝓀[Rp] ⊗[R] S) ⊗[S] Sq) :=
      .comp _ (𝓀[Rp] ⊗[R] S) _
    let e : 𝓀[Rp] ⊗[R] S ≃ₐ[S] S ⊗[R] 𝓀[Rp] :=
      { __ := TensorProduct.comm _ _ _, commutes' _ := rfl }
    let e' : (𝓀[Rp] ⊗[R] S) ⊗[S] Sq ≃ₐ[R] 𝓀[Rp] ⊗[Rp] Sq :=
      ((TensorProduct.comm _ _ _).restrictScalars R).trans <|
      ((TensorProduct.congr (.refl (R := S)) e).restrictScalars R).trans <|
      ((TensorProduct.cancelBaseChange _ _ S _ _).restrictScalars R).trans <|
      (TensorProduct.comm _ _ _).trans (TensorProduct.equivOfCompatibleSMul ..)
    have : e'.toAlgHom.comp (IsScalarTower.toAlgHom R p.ResidueField _) =
        IsScalarTower.toAlgHom _ _ _ := by ext
    let e'' : (𝓀[Rp] ⊗[R] S) ⊗[S] Sq ≃ₐ[𝓀[Rp]] 𝓀[Rp] ⊗[Rp] Sq :=
      { __ := e', commutes' r := congr($this r) }
    exact .of_equiv e''
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : FinitePresentation R S
p : Ideal R
q : Ideal S
inst_5 : p.IsPrime
inst_6 : q.IsPrime
inst_7 : q.LiesOver p
inst_8 : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom (R := S) (M := algebraMapSubmonoid S p.primeCompl) (f := ofId S Sq) ⋯
algInst : Algebra Sp Sq := f.toAlgebra
this_2 : IsScalarTower R Sp Sq
this_3 : IsScalarTower Rp Sp Sq
this_4 : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
this_5 : FinitePresentation Rp Sp
this : FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[Rp] Sq)
⊢ IsSmoothAt R q
have this₁ : FormallySmooth Rp Sq
Tactic: have := FormallySmooth.of_formallySmooth_residueField_tensor
    (R := Rp) (S := Sq) (P := Sp) (algebraMapSubmonoid _ q.primeCompl)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : FinitePresentation R S
H : ∀ (I : Ideal R) [inst_5 : I.IsPrime], FormallySmooth I.ResidueField (I.Fiber S)
⊢ Smooth R S
have refine : ∀ (q : PrimeSpectrum S), Membership.mem (γ := Set (PrimeSpectrum S)) (smoothLocus R S) q
Tactic: refine ⟨smoothLocus_eq_univ_iff.mp (Set.eq_univ_iff_forall.mpr fun q ↦ ?_), ‹_›⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : FinitePresentation R S
q : Ideal S
inst_5 : q.IsPrime
inst_6 : IsUnramifiedAt R q
⊢ IsEtaleAt R q
have obtain : ∀ (f : S) (hfp : f ∉ q) (H : Unramified.{u_1, u_2} R (Localization.Away f)), IsEtaleAt R q
Tactic: obtain ⟨f, hfp, H⟩ := exists_unramified_of_isUnramifiedAt (R := R) q
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : FinitePresentation R S
q : Ideal S
inst_5 : q.IsPrime
inst_6 : IsUnramifiedAt R q
f : S
hfp : f ∉ q
H : Unramified.{u_1, u_2} R (Localization.Away f)
⊢ IsEtaleAt R q
have change : Membership.mem (γ := Set (PrimeSpectrum S)) (etaleLocus R S) { asIdeal := q, isPrime := inst_5 : PrimeSpectrum S }
Tactic: change ⟨q, ‹_›⟩ ∈ etaleLocus R S
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : FinitePresentation R S
q : Ideal S
inst_5 : q.IsPrime
inst_6 : IsUnramifiedAt R q
f : S
hfp : f ∉ q
H : Unramified.{u_1, u_2} R (Localization.Away f)
⊢ Membership.mem (γ := Set (PrimeSpectrum S)) (etaleLocus R S) { asIdeal := q, isPrime := inst_5 : PrimeSpectrum S }
have suffices : Etale.{u_1, u_2} R (Localization.Away f)
Tactic: suffices Algebra.Etale R (Localization.Away f) from
    (basicOpen_subset_etaleLocus_iff (R := R) (f := f)).mpr inferInstance hfp
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Field (hypothesis)
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
⊢ FormallySmooth.{u_1, u_2} K ↥(IntermediateField.adjoin K (Set.range v))
have this : FormallySmooth.{u_1, u_2} K ↥(adjoin K (Set.range v))
Tactic: have : Algebra.FormallySmooth K (adjoin K (Set.range v)) :=
    .of_equiv hb.aevalEquiv
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Field (hypothesis)
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
this : FormallySmooth.{u_1, u_2} K ↥(adjoin K (Set.range v))
⊢ FormallySmooth.{u_1, u_2} K ↥(IntermediateField.adjoin K (Set.range v))
have this₁ : FormallySmooth.{u_2, u_2} ↥(adjoin K (Set.range v)) ↥(IntermediateField.adjoin K (Set.range v))
Tactic: have : Algebra.FormallySmooth (adjoin K (Set.range v))
      (IntermediateField.adjoin K (Set.range v)) :=
    .of_isLocalization (nonZeroDivisors _)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Field (hypothesis)
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
hb' : Eq (α := IntermediateField K L) (IntermediateField.adjoin K (Set.range v)) ⊤
⊢ FormallySmooth K L
have this : FormallySmooth.{u_1, u_2} K ↥(IntermediateField.adjoin K (Set.range v))
Tactic: have := Algebra.FormallySmooth.adjoin_of_algebraicIndependent hb
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Field (hypothesis)
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
hb' : Eq (α := IntermediateField K L) (IntermediateField.adjoin K (Set.range v)) ⊤
this : FormallySmooth.{u_1, u_2} K ↥(IntermediateField.adjoin K (Set.range v))
⊢ FormallySmooth K L
have this₁ : FormallySmooth.{u_1, u_2} K ↥⊤
Tactic: rw [hb'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Field (hypothesis)
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
inst_3 : Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range v))) L
⊢ FormallySmooth K L
have this : FormallySmooth.{u_1, u_2} K ↥(IntermediateField.adjoin K (Set.range v))
Tactic: have := FormallySmooth.adjoin_of_algebraicIndependent hb
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Field (hypothesis)
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
inst_3 : Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range v))) L
this : FormallySmooth.{u_1, u_2} K ↥(IntermediateField.adjoin K (Set.range v))
⊢ FormallySmooth K L
have this₁ : FormallyEtale (↥(IntermediateField.adjoin K (Set.range v))) L
Tactic: have : FormallyEtale (IntermediateField.adjoin K (Set.range v)) L :=
    Algebra.FormallyEtale.of_isSeparable _ L
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Field (goal)
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
inst_3 : PerfectField K
inst_4 : EssFiniteType K L
⊢ FormallySmooth K L
have obtain : ∀ (s : Finset L) (hs : IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) K (Subtype.val (p := fun (x : L) ↦ x ∈ s)))
  (H : Algebra.IsSeparable (↥(IntermediateField.adjoin K (↑s : Set L))) L), FormallySmooth K L
Tactic: obtain ⟨s, hs, H⟩ := exists_isTranscendenceBasis_and_isSeparable_of_perfectField K L
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Field (goal)
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
inst_3 : PerfectField K
inst_4 : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) K (Subtype.val (p := fun (x : L) ↦ x ∈ s))
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K (↑s : Set L))) L
⊢ Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s))))) L
have h : ∀ (x : L), Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s)) = (↑s : Set L)
Tactic: convert! H
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Field (goal)
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
inst_3 : PerfectField K
inst_4 : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) K (Subtype.val (p := fun (x : L) ↦ x ∈ s))
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K (↑s : Set L))) L
h : ∀ (x : L), Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s)) = (↑s : Set L)
⊢ Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s))))) L
have h₁ : ↥(IntermediateField.adjoin K (Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s)))) =
    ↥(IntermediateField.adjoin K (↑s : Set L)) →
  Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s)) = (↑s : Set L)
Tactic: convert! H
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Field (goal)
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
inst_3 : PerfectField K
inst_4 : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) K (Subtype.val (p := fun (x : L) ↦ x ∈ s))
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K (↑s : Set L))) L
h : ∀ (x : L), Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s)) = (↑s : Set L)
h₁ :
  ↥(IntermediateField.adjoin K (Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s)))) =
      ↥(IntermediateField.adjoin K (↑s : Set L)) →
    Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s)) = (↑s : Set L)
⊢ Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s))))) L
have h₂ : ↥(IntermediateField.adjoin K (Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s)))) =
    ↥(IntermediateField.adjoin K (↑s : Set L)) →
  HEq.{u_2 + 1} (α :=
      CommRing ↥(IntermediateField.adjoin K (Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s)))))
      Field.toCommRing (β := CommRing ↥(IntermediateField.adjoin K (↑s : Set L))) Field.toCommRing →
    Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s)) = (↑s : Set L)
Tactic: convert! H
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Field (hypothesis)
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
inst_3 : PerfectField K
inst_4 : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis.{u_2, u_1, u_2} (ι := ↥s) K (Subtype.val (p := fun (x : L) ↦ x ∈ s))
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K (↑s : Set L))) L
⊢ FormallySmooth K L
have this : Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s))))) L
Tactic: have : Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range ((↑) : s → L)))) L := by
    convert! H <;> simp
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Flat (hypothesis)
Goal:
R : Type u_1
A : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing S
inst_4 : Algebra R S
f : S →ₐ[R] A
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := S) (β := A) (⇑f : (a : S) → A)
inst_5 : Module.Flat R S
inst_6 : IsNoetherianRing S
inst_7 : FormallySmooth R A
⊢ Module.Flat R A
have this : Module.Flat.{u_1, u_3} R (AdicCompletion (RingHom.ker f) S)
Tactic: have : Module.Flat R (AdicCompletion (RingHom.ker f) S) := .trans _ S _
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Flat (goal)
Goal:
R : Type u_1
A : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing S
inst_4 : Algebra R S
f : S →ₐ[R] A
hf : Function.Surjective.{u_3 + 1, u_2 + 1} (α := S) (β := A) (⇑f : (a : S) → A)
inst_5 : Module.Flat R S
inst_6 : IsNoetherianRing S
inst_7 : FormallySmooth R A
this : Module.Flat.{u_1, u_3} R (AdicCompletion (RingHom.ker f) S)
⊢ Module.Flat R A
have obtain : ∀ (g : AlgHom.{u_1, u_2, u_3} R A (AdicCompletion (RingHom.ker f) S))
  (hg : (AdicCompletion.kerProj hf).comp g = AlgHom.id R A), Module.Flat R A
Tactic: obtain ⟨g, hg⟩ := exists_kerProj_comp_eq_id f hf
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Flat (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : IsNoetherianRing R
inst_4 : Smooth R A
⊢ Module.Flat R A
have obtain : ∀ (k : ℕ) (f : MvPolynomial (Fin k) R →ₐ[R] A)
  (hf :
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := MvPolynomial (Fin k) R) (β := A)
      (⇑f : (a : MvPolynomial (Fin k) R) → A)),
  Module.Flat R A
Tactic: obtain ⟨k, f, hf⟩ := (FiniteType.iff_quotient_mvPolynomial'' (R := R) (S := A)).mp inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Flat (goal)
Goal:
R : Type u_1
A : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Smooth R A
⊢ Module.Flat R A
have obtain : ∀ (A₀ B₀ : Type u_1) (w : CommRing A₀) (w_1 : CommRing B₀) (w_2 : Algebra ℤ A₀) (w_3 : Algebra A₀ R)
  (w_4 : Algebra A₀ B₀),
  Function.Injective (α := A₀) (β := R) (⇑(algebraMap A₀ R) : (a : A₀) → R) →
    FiniteType ℤ A₀ → Smooth A₀ B₀ → ∀ (e : A ≃ₐ[R] TensorProduct A₀ R B₀), Module.Flat R A
Tactic: obtain ⟨A₀, B₀, _, _, _, _, _, _, _, _, ⟨e⟩⟩ := exists_finiteType ℤ R A
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Flat (hypothesis)
Goal:
R : Type u_1
A : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Smooth R A
A₀ B₀ : Type u_1
w : CommRing A₀
w_1 : CommRing B₀
w_2 : Algebra ℤ A₀
w_3 : Algebra A₀ R
w_4 : Algebra A₀ B₀
left : Function.Injective (α := A₀) (β := R) (⇑(algebraMap A₀ R) : (a : A₀) → R)
left_1 : FiniteType ℤ A₀
left_2 : Smooth A₀ B₀
e : A ≃ₐ[R] TensorProduct A₀ R B₀
⊢ Module.Flat R A
have this : IsNoetherianRing A₀
Tactic: have : IsNoetherianRing A₀ := Algebra.FiniteType.isNoetherianRing ℤ _
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Flat (hypothesis)
Goal:
R : Type u_1
A : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : Smooth R A
A₀ B₀ : Type u_1
w : CommRing A₀
w_1 : CommRing B₀
w_2 : Algebra ℤ A₀
w_3 : Algebra A₀ R
w_4 : Algebra A₀ B₀
left : Function.Injective (α := A₀) (β := R) (⇑(algebraMap A₀ R) : (a : A₀) → R)
left_1 : FiniteType ℤ A₀
left_2 : Smooth A₀ B₀
e : A ≃ₐ[R] TensorProduct A₀ R B₀
this : IsNoetherianRing A₀
⊢ Module.Flat R A
have this₁ : Module.Flat A₀ B₀
Tactic: have : Module.Flat A₀ B₀ := Smooth.flat_of_isNoetherianRing _ _
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Flat (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Smooth
⊢ f.Flat
have algebraizeInst : Algebra.Smooth R S
Tactic: algebraize [f]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B_1 : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B_1
inst_4 : Algebra R B_1
B : Type u_4
inst_5 : CommRing B
inst_6 : Algebra R B
x y : TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B)
h :
  Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B))
    (((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
            TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
          (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
        x :
      S ⊗[R] B)
h_1 :
  Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B))
    (((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
            TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
          (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
        y :
      S ⊗[R] B)
⊢ Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B))
    (((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
            TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
          (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
        (x + y) :
      S ⊗[R] B)
have add : Membership.mem (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B))
  (HAdd.hAdd (α := S ⊗[R] B) (β := S ⊗[R] B)
    (((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
            TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
          (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
        x :
      S ⊗[R] B)
    (((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
            TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
          (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
        y :
      S ⊗[R] B))
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B_1 : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B_1
inst_4 : Algebra R B_1
B : Type u_4
inst_5 : CommRing B
inst_6 : Algebra R B
x : S
y : ↥(integralClosure R B)
⊢ Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B))
    (((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
            TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
          (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
        (x ⊗ₜ[R] y) :
      S ⊗[R] B)
have h : ((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
        TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
      (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
    (x ⊗ₜ[R] y) =
  HSMul.hSMul (β := S ⊗[R] B) x ((Algebra.TensorProduct.includeRight : (a : B) → S ⊗[R] B) (↑y : B) : S ⊗[R] B)
Tactic: convert!
      ((y.2.map (Algebra.TensorProduct.includeRight (R := R) (A := S))).tower_top (A := S)).smul x
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B_1 : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B_1
inst_4 : Algebra R B_1
B : Type u_4
inst_5 : CommRing B
inst_6 : Algebra R B
x : TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B)
⊢ Membership.mem (α := S ⊗[R] B) (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B))
    (((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
            TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
          (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
        x :
      S ⊗[R] B)
have zero : Membership.mem (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B))
  (((Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
        TensorProduct.{u_1, u_2, u_4} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
      (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
    0)
Tactic: induction x with
  | zero => simp
  | add x y _ _ => rw [map_add]; exact add_mem ‹_› ‹_›
  | tmul x y =>
    convert!
      ((y.2.map (Algebra.TensorProduct.includeRight (R := R) (A := S))).tower_top (A := S)).smul x
    simp [smul_tmul']
Cleared hypotheses: x