awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.Field
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 ↥⊤
⊢ FormallySmooth K L

Tactic:
exact .of_equiv IntermediateField.topEquiv
-- Module: Mathlib.RingTheory.Smooth.Field
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.{u_1, u_2} K ↥(IntermediateField.adjoin K (Set.range v))

Tactic:
have := FormallySmooth.adjoin_of_algebraicIndependent hb
-- Module: Mathlib.RingTheory.Smooth.Field
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))
⊢ FormallyEtale (↥(IntermediateField.adjoin K (Set.range v))) L

Tactic:
have : FormallyEtale (IntermediateField.adjoin K (Set.range v)) L :=
    Algebra.FormallyEtale.of_isSeparable _ L
-- Module: Mathlib.RingTheory.Smooth.Field
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_1 : FormallySmooth.{u_1, u_2} K ↥(IntermediateField.adjoin K (Set.range v))
this : FormallyEtale (↥(IntermediateField.adjoin K (Set.range v))) L
⊢ FormallySmooth K L

Tactic:
.comp _ (IntermediateField.adjoin K (Set.range v)) _

Premises used: Membership.mem, Subtype, IntermediateField.adjoin, Set.range, Algebra.FormallySmooth.comp
-- Module: Mathlib.RingTheory.Smooth.Field
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_1 : FormallySmooth.{u_1, u_2} K ↥(IntermediateField.adjoin K (Set.range v))
this : FormallyEtale (↥(IntermediateField.adjoin K (Set.range v))) L
⊢ FormallySmooth K L

Tactic:
exact .comp _ (IntermediateField.adjoin K (Set.range v)) _
-- Module: Mathlib.RingTheory.Smooth.Field
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
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
⊢ FormallySmooth K L

Tactic:
obtain ⟨s, hs, H⟩ := exists_isTranscendenceBasis_and_isSeparable_of_perfectField K L

Premises used: exists_isTranscendenceBasis_and_isSeparable_of_perfectField
-- Module: Mathlib.RingTheory.Smooth.Field
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 (↑s : Set L))) L

Tactic:
H
-- Module: Mathlib.RingTheory.Smooth.Field
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)
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)
⊢ Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s))))) L

Tactic:
convert! H
-- Module: Mathlib.RingTheory.Smooth.Field
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
x : L
⊢ Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s)) = (↑s : Set L)

Tactic:
simp
-- Module: Mathlib.RingTheory.Smooth.Field
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
e_1 :
  ↥(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:
simp
-- Module: Mathlib.RingTheory.Smooth.Field
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
e_1 :
  ↥(IntermediateField.adjoin K (Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s)))) =
    ↥(IntermediateField.adjoin K (↑s : Set L))
e_3 :
  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:
simp
-- Module: Mathlib.RingTheory.Smooth.Field
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

Tactic:
have : Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range ((↑) : s → L)))) L := by
    convert! H <;> simp
-- Module: Mathlib.RingTheory.Smooth.Field
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
this :
  Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s))))) L
⊢ FormallySmooth K L

Tactic:
.of_algebraicIndependent_of_isSeparable hs.1

Premises used: Algebra.FormallySmooth.of_algebraicIndependent_of_isSeparable, And.left
-- Module: Mathlib.RingTheory.Smooth.Field
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
this :
  Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range (ι := ↥s) (Subtype.val (p := fun (x : L) ↦ x ∈ s))))) L
⊢ FormallySmooth K L

Tactic:
exact .of_algebraicIndependent_of_isSeparable hs.1
-- Module: Mathlib.RingTheory.Smooth.Flat
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.{u_1, u_3} R (AdicCompletion (RingHom.ker f) S)

Tactic:
have : Module.Flat R (AdicCompletion (RingHom.ker f) S) := .trans _ S _
-- Module: Mathlib.RingTheory.Smooth.Flat
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)
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
⊢ Module.Flat R A

Tactic:
obtain ⟨g, hg⟩ := exists_kerProj_comp_eq_id f hf

Premises used: Algebra.FormallySmooth.exists_kerProj_comp_eq_id
-- Module: Mathlib.RingTheory.Smooth.Flat
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)
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:
.of_retract g.toLinearMap
    (AdicCompletion.kerProj hf).toLinearMap (LinearMap.ext fun x ↦ congr($hg x))

Premises used: AlgHom.toLinearMap, LinearMap.ext, congrArg, AdicCompletion.kerProj, id, Module.Flat.of_retract, DFunLike.coe
-- Module: Mathlib.RingTheory.Smooth.Flat
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)
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:
exact .of_retract g.toLinearMap
    (AdicCompletion.kerProj hf).toLinearMap (LinearMap.ext fun x ↦ congr($hg x))
-- Module: Mathlib.RingTheory.Smooth.Flat
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
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
⊢ Module.Flat R A

Tactic:
obtain ⟨k, f, hf⟩ := (FiniteType.iff_quotient_mvPolynomial'' (R := R) (S := A)).mp inferInstance

Premises used: inferInstance, Iff.mp, Algebra.FiniteType.iff_quotient_mvPolynomial''
-- Module: Mathlib.RingTheory.Smooth.Flat
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
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:
FormallySmooth.flat_of_algHom_of_isNoetherianRing f hf

Premises used: Algebra.FormallySmooth.flat_of_algHom_of_isNoetherianRing
-- Module: Mathlib.RingTheory.Smooth.Flat
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
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:
exact FormallySmooth.flat_of_algHom_of_isNoetherianRing f hf

Premises used: Algebra.FormallySmooth.flat_of_algHom_of_isNoetherianRing
-- Module: Mathlib.RingTheory.Smooth.Flat
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
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
⊢ Module.Flat R A

Tactic:
obtain ⟨A₀, B₀, _, _, _, _, _, _, _, _, ⟨e⟩⟩ := exists_finiteType ℤ R A

Premises used: Int, Algebra.Smooth.exists_finiteType
-- Module: Mathlib.RingTheory.Smooth.Flat
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₀
⊢ IsNoetherianRing A₀

Tactic:
have : IsNoetherianRing A₀ := Algebra.FiniteType.isNoetherianRing ℤ _
-- Module: Mathlib.RingTheory.Smooth.Flat
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 A₀ B₀

Tactic:
have : Module.Flat A₀ B₀ := Smooth.flat_of_isNoetherianRing _ _
-- Module: Mathlib.RingTheory.Smooth.Flat
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_1 : IsNoetherianRing A₀
this : Module.Flat A₀ B₀
⊢ Module.Flat R A

Tactic:
.of_linearEquiv e.toLinearEquiv

Premises used: AlgEquiv.toLinearEquiv, Module.Flat.of_linearEquiv
-- Module: Mathlib.RingTheory.Smooth.Flat
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_1 : IsNoetherianRing A₀
this : Module.Flat A₀ B₀
⊢ Module.Flat R A

Tactic:
exact .of_linearEquiv e.toLinearEquiv
-- Module: Mathlib.RingTheory.Smooth.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Smooth
⊢ Algebra.Smooth R S

Tactic:
algebraize [f]
-- Module: Mathlib.RingTheory.Smooth.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Smooth
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.Smooth R S
⊢ f.Flat

Tactic:
Algebra.Smooth.flat R S

Premises used: RingHom.Flat, Algebra.Smooth.flat
-- Module: Mathlib.RingTheory.Smooth.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Smooth
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.Smooth R S
⊢ f.Flat

Tactic:
exact Algebra.Smooth.flat R S

Premises used: Algebra.Smooth.flat
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
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
⊢ 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:
simp
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
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)
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))
⊢ 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)

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
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 (γ := 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:
add_mem ‹_› ‹_›

Premises used: Set.Mem, AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
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 (γ := 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:
exact add_mem ‹_› ‹_›

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
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)
⊢ IsIntegral S
    (HSMul.hSMul (β := S ⊗[R] B) x ((Algebra.TensorProduct.includeRight : (a : B) → S ⊗[R] B) (↑y : B) : S ⊗[R] B))

Tactic:
((y.2.map (Algebra.TensorProduct.includeRight (R := R) (A := S))).tower_top (A := S)).smul x

Premises used: IsIntegral.smul, IsIntegral.map, IsIntegral.tower_top, Subtype.property, Algebra.TensorProduct.includeRight