awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
⊢ Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β :=
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))

Tactic:
⟨toIntegralClosure_injective_of_flat, ?_⟩

Premises used: And.intro, TensorProduct.toIntegralClosure_injective_of_flat, Function.Bijective
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
refine :
  Function.Surjective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β :=
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
⊢ Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β :=
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))

Tactic:
refine ⟨toIntegralClosure_injective_of_flat, ?_⟩
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
x : S ⊗[R] B
hx : Membership.mem (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) x
simp :
  Membership.mem (γ := Subalgebra S (S ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
        (Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
          TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
      Subalgebra S (S ⊗[R] B))
    x
⊢ ∃ (a : TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)),
    (toIntegralClosure R S B : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B))) a =
      Subtype.mk (p := fun (x : S ⊗[R] B) ↦
        Membership.mem (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) x) x hx

Tactic:
simp only [toIntegralClosure, Subtype.ext_iff, AlgHom.coe_codRestrict, ← AlgHom.mem_range]

Premises used: AlgHom.mem_range, TensorProduct.toIntegralClosure, Subtype.ext_iff, AlgHom.coe_codRestrict
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
x : S ⊗[R] B
hx : Membership.mem (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) x
⊢ Membership.mem (γ := Subalgebra S (S ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
        (Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
          TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
      Subalgebra S (S ⊗[R] B))
    x

Tactic:
Algebra.adjoin_le ?_ (mem_adjoin_map_integralClosure_of_isStandardEtale x hx)

Premises used: mem_adjoin_map_integralClosure_of_isStandardEtale, Algebra.adjoin_le
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
x : S ⊗[R] B
hx : Membership.mem (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) x
refine :
  (↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)) : Set (S ⊗[R] B)) ⊆
    (↑(AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
            (Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
              TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
          Subalgebra S (S ⊗[R] B)) :
      Set (S ⊗[R] B))
⊢ Membership.mem (γ := Subalgebra S (S ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
        (Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
          TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
      Subalgebra S (S ⊗[R] B))
    x

Tactic:
refine Algebra.adjoin_le ?_ (mem_adjoin_map_integralClosure_of_isStandardEtale x hx)

Premises used: mem_adjoin_map_integralClosure_of_isStandardEtale, Algebra.adjoin_le
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
x : S ⊗[R] B
hx : Membership.mem (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) x
y : B
hy : IsIntegral R y
⊢ Eq (α := S ⊗[R] B)
    ((AlgHom.toRingHom
            (Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
              TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
          (a : S ⊗[R] ↥(integralClosure R B)) → S ⊗[R] B)
        (1 ⊗ₜ[R] Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra R B) (integralClosure R B) x) y hy) :
      S ⊗[R] B)
    (((↑Algebra.TensorProduct.includeRight : B →+* S ⊗[R] B) : (a : B) → S ⊗[R] B) y : S ⊗[R] B)

Tactic:
simp
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
x : S ⊗[R] B
hx : Membership.mem (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) x
y : B
hy : IsIntegral R y
⊢ Membership.mem (α := S ⊗[R] B)
    (↑(AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
            (Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
              TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
          Subalgebra S (S ⊗[R] B)) :
      Set (S ⊗[R] B))
    (((↑Algebra.TensorProduct.includeRight : B →+* S ⊗[R] B) : (a : B) → S ⊗[R] B) y : S ⊗[R] B)

Tactic:
refine ⟨1 ⊗ₜ ⟨y, hy⟩, by simp⟩
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
m : PrimeSpectrum S
obtain :
  ∀ (f : S) (hfm : f ∉ m.asIdeal) (n : ℕ) (w : Algebra.{u_1, u_2} (MvPolynomial (Fin n) R) (Localization.Away f)),
    IsScalarTower.{u_1, u_1, u_2} R (MvPolynomial (Fin n) R) (Localization.Away f) →
      Algebra.IsStandardEtale.{u_1, u_2} (MvPolynomial (Fin n) R) (Localization.Away f) →
        ∃ f ∉ m.asIdeal,
          Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) ↥(integralClosure R B)) (β :=
            ↥(integralClosure (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B) :
                Subalgebra (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B)))
            (⇑(toIntegralClosure R (Localization.Away f) B) :
              (a : Localization.Away f ⊗[R] ↥(integralClosure R B)) →
                ↥(integralClosure (Localization.Away f) (Localization.Away f ⊗[R] B)))
⊢ ∃ f ∉ m.asIdeal,
    Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) ↥(integralClosure R B)) (β :=
      ↥(integralClosure (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B) :
          Subalgebra (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B)))
      (⇑(toIntegralClosure R (Localization.Away f) B) :
        (a : Localization.Away f ⊗[R] ↥(integralClosure R B)) →
          ↥(integralClosure (Localization.Away f) (Localization.Away f ⊗[R] B)))

Tactic:
obtain ⟨f, hfm, n, _, _, _⟩ :=
      Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial (R := R) (p := m.asIdeal)

Premises used: Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
m : PrimeSpectrum S
f : S
hfm : f ∉ m.asIdeal
n : ℕ
w : Algebra.{u_1, u_2} (MvPolynomial (Fin n) R) (Localization.Away f)
left : IsScalarTower.{u_1, u_1, u_2} R (MvPolynomial (Fin n) R) (Localization.Away f)
right : Algebra.IsStandardEtale.{u_1, u_2} (MvPolynomial (Fin n) R) (Localization.Away f)
⊢ ∃ f ∉ m.asIdeal,
    Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) ↥(integralClosure R B)) (β :=
      ↥(integralClosure (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B) :
          Subalgebra (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B)))
      (⇑(toIntegralClosure R (Localization.Away f) B) :
        (a : Localization.Away f ⊗[R] ↥(integralClosure R B)) →
          ↥(integralClosure (Localization.Away f) (Localization.Away f ⊗[R] B)))

Tactic:
⟨f, hfm, toIntegralClosure_bijective_of_tower (S := MvPolynomial (Fin n) R)
      toIntegralClosure_mvPolynomial_bijective toIntegralClosure_bijective_of_isStandardEtale⟩

Premises used: _private.0.TensorProduct.toIntegralClosure_bijective_of_isStandardEtale, TensorProduct.toIntegralClosure_mvPolynomial_bijective, TensorProduct.toIntegralClosure_bijective_of_tower, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
m : PrimeSpectrum S
f : S
hfm : f ∉ m.asIdeal
n : ℕ
w : Algebra.{u_1, u_2} (MvPolynomial (Fin n) R) (Localization.Away f)
left : IsScalarTower.{u_1, u_1, u_2} R (MvPolynomial (Fin n) R) (Localization.Away f)
right : Algebra.IsStandardEtale.{u_1, u_2} (MvPolynomial (Fin n) R) (Localization.Away f)
⊢ ∃ f ∉ m.asIdeal,
    Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) ↥(integralClosure R B)) (β :=
      ↥(integralClosure (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B) :
          Subalgebra (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B)))
      (⇑(toIntegralClosure R (Localization.Away f) B) :
        (a : Localization.Away f ⊗[R] ↥(integralClosure R B)) →
          ↥(integralClosure (Localization.Away f) (Localization.Away f ⊗[R] B)))

Tactic:
exact ⟨f, hfm, toIntegralClosure_bijective_of_tower (S := MvPolynomial (Fin n) R)
      toIntegralClosure_mvPolynomial_bijective toIntegralClosure_bijective_of_isStandardEtale⟩
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
⊢ ∀ (m : PrimeSpectrum S),
    ∃ f ∉ m.asIdeal,
      Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) ↥(integralClosure R B)) (β :=
        ↥(integralClosure (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B) :
            Subalgebra (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B)))
        (⇑(toIntegralClosure R (Localization.Away f) B) :
          (a : Localization.Away f ⊗[R] ↥(integralClosure R B)) →
            ↥(integralClosure (Localization.Away f) (Localization.Away f ⊗[R] B)))

Tactic:
have (m : PrimeSpectrum S) : ∃ f ∉ m.asIdeal,
      Function.Bijective (toIntegralClosure R (Localization.Away f) B) := by
    obtain ⟨f, hfm, n, _, _, _⟩ :=
      Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial (R := R) (p := m.asIdeal)
    exact ⟨f, hfm, toIntegralClosure_bijective_of_tower (S := MvPolynomial (Fin n) R)
      toIntegralClosure_mvPolynomial_bijective toIntegralClosure_bijective_of_isStandardEtale⟩
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
this :
  ∀ (m : PrimeSpectrum S),
    ∃ f ∉ m.asIdeal,
      Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) ↥(integralClosure R B)) (β :=
        ↥(integralClosure (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B) :
            Subalgebra (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B)))
        (⇑(toIntegralClosure R (Localization.Away f) B) :
          (a : Localization.Away f ⊗[R] ↥(integralClosure R B)) →
            ↥(integralClosure (Localization.Away f) (Localization.Away f ⊗[R] B)))
choose :
  ∀ (f : (m : PrimeSpectrum S) → S) (hfm : ∀ (m : PrimeSpectrum S), f m ∉ m.asIdeal)
    (hf :
      ∀ (m : PrimeSpectrum S),
        Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) ↥(integralClosure R B)) (β :=
          ↥(integralClosure (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B) :
              Subalgebra (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B)))
          (⇑(toIntegralClosure R (Localization.Away (f m)) B) :
            (a : Localization.Away (f m) ⊗[R] ↥(integralClosure R B)) →
              ↥(integralClosure (Localization.Away (f m)) (Localization.Away (f m) ⊗[R] B)))),
    Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β :=
      ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
      (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
⊢ Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β :=
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))

Tactic:
choose f hfm hf using this
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
f : (m : PrimeSpectrum S) → S
hfm : ∀ (m : PrimeSpectrum S), f m ∉ m.asIdeal
hf :
  ∀ (m : PrimeSpectrum S),
    Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) ↥(integralClosure R B)) (β :=
      ↥(integralClosure (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B) :
          Subalgebra (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B)))
      (⇑(toIntegralClosure R (Localization.Away (f m)) B) :
        (a : Localization.Away (f m) ⊗[R] ↥(integralClosure R B)) →
          ↥(integralClosure (Localization.Away (f m)) (Localization.Away (f m) ⊗[R] B)))
⊢ Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β :=
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))

Tactic:
TensorProduct.toIntegralClosure_bijective_of_isLocalizationAway (R := R)
    (s := Set.range f) (B := B) ?_ (Localization.Away ·.1) (Set.forall_subtype_range_iff.mpr hf)

Premises used: Iff.mpr, Localization.Away, TensorProduct.toIntegralClosure_bijective_of_isLocalizationAway, Subtype.val, Set.forall_subtype_range_iff
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
f : (m : PrimeSpectrum S) → S
hfm : ∀ (m : PrimeSpectrum S), f m ∉ m.asIdeal
hf :
  ∀ (m : PrimeSpectrum S),
    Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) ↥(integralClosure R B)) (β :=
      ↥(integralClosure (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B) :
          Subalgebra (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B)))
      (⇑(toIntegralClosure R (Localization.Away (f m)) B) :
        (a : Localization.Away (f m) ⊗[R] ↥(integralClosure R B)) →
          ↥(integralClosure (Localization.Away (f m)) (Localization.Away (f m) ⊗[R] B)))
refine : Eq (α := Ideal S) (Ideal.span (Set.range f)) ⊤
⊢ Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β :=
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))

Tactic:
refine TensorProduct.toIntegralClosure_bijective_of_isLocalizationAway (R := R)
    (s := Set.range f) (B := B) ?_ (Localization.Away ·.1) (Set.forall_subtype_range_iff.mpr hf)

Premises used: Iff.mpr, Localization.Away, TensorProduct.toIntegralClosure_bijective_of_isLocalizationAway, Subtype.val, Set.forall_subtype_range_iff
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
f : (m : PrimeSpectrum S) → S
hfm : ∀ (m : PrimeSpectrum S), f m ∉ m.asIdeal
hf :
  ∀ (m : PrimeSpectrum S),
    Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) ↥(integralClosure R B)) (β :=
      ↥(integralClosure (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B) :
          Subalgebra (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B)))
      (⇑(toIntegralClosure R (Localization.Away (f m)) B) :
        (a : Localization.Away (f m) ⊗[R] ↥(integralClosure R B)) →
          ↥(integralClosure (Localization.Away (f m)) (Localization.Away (f m) ⊗[R] B)))
by_contra : ∀ (H : ¬Eq (α := Ideal S) (Ideal.span (Set.range f)) ⊤), False
⊢ Eq (α := Ideal S) (Ideal.span (Set.range f)) ⊤

Tactic:
by_contra H
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
f : (m : PrimeSpectrum S) → S
hfm : ∀ (m : PrimeSpectrum S), f m ∉ m.asIdeal
hf :
  ∀ (m : PrimeSpectrum S),
    Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) ↥(integralClosure R B)) (β :=
      ↥(integralClosure (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B) :
          Subalgebra (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B)))
      (⇑(toIntegralClosure R (Localization.Away (f m)) B) :
        (a : Localization.Away (f m) ⊗[R] ↥(integralClosure R B)) →
          ↥(integralClosure (Localization.Away (f m)) (Localization.Away (f m) ⊗[R] B)))
H : ¬Eq (α := Ideal S) (Ideal.span (Set.range f)) ⊤
obtain : ∀ (m : Ideal S) (hm : m.IsMaximal) (e : Ideal.span (Set.range f) ≤ m), False
⊢ False

Tactic:
obtain ⟨m, hm, e⟩ := Ideal.exists_le_maximal _ H

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
f : (m : PrimeSpectrum S) → S
hfm : ∀ (m : PrimeSpectrum S), f m ∉ m.asIdeal
hf :
  ∀ (m : PrimeSpectrum S),
    Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) ↥(integralClosure R B)) (β :=
      ↥(integralClosure (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B) :
          Subalgebra (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B)))
      (⇑(toIntegralClosure R (Localization.Away (f m)) B) :
        (a : Localization.Away (f m) ⊗[R] ↥(integralClosure R B)) →
          ↥(integralClosure (Localization.Away (f m)) (Localization.Away (f m) ⊗[R] B)))
H : ¬Eq (α := Ideal S) (Ideal.span (Set.range f)) ⊤
m : Ideal S
hm : m.IsMaximal
e : Ideal.span (Set.range f) ≤ m
⊢ False

Tactic:
hfm ⟨m, inferInstance⟩ (e (Ideal.subset_span (Set.mem_range_self ⟨m, inferInstance⟩)) :)

Premises used: Set.mem_range_self, PrimeSpectrum.mk, Ideal.subset_span, inferInstance
-- Module: Mathlib.RingTheory.Smooth.IntegralClosure
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
f : (m : PrimeSpectrum S) → S
hfm : ∀ (m : PrimeSpectrum S), f m ∉ m.asIdeal
hf :
  ∀ (m : PrimeSpectrum S),
    Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) ↥(integralClosure R B)) (β :=
      ↥(integralClosure (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B) :
          Subalgebra (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B)))
      (⇑(toIntegralClosure R (Localization.Away (f m)) B) :
        (a : Localization.Away (f m) ⊗[R] ↥(integralClosure R B)) →
          ↥(integralClosure (Localization.Away (f m)) (Localization.Away (f m) ⊗[R] B)))
H : ¬Eq (α := Ideal S) (Ideal.span (Set.range f)) ⊤
m : Ideal S
hm : m.IsMaximal
e : Ideal.span (Set.range f) ≤ m
⊢ False

Tactic:
exact hfm ⟨m, inferInstance⟩ (e (Ideal.subset_span (Set.mem_range_self ⟨m, inferInstance⟩)) :)

Premises used: Set.mem_range_self, PrimeSpectrum.mk, Ideal.subset_span, inferInstance
-- Module: Mathlib.RingTheory.Smooth.Local
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsLocalRing S
inst_3 : Algebra R S
P : Extension.{u, u_1, u_2} R S
inst_4 : FormallySmooth.{u_1, u} R P.Ring
inst_5 : Module.Free.{u, u} P.Ring Ω[P.Ring⁄R]
inst_6 : Module.Finite.{u, u} P.Ring Ω[P.Ring⁄R]
h' : P.ker.FG
⊢ Module.Finite.{u, u} P.Ring P.Cotangent

Tactic:
have : Module.Finite P.Ring P.Cotangent :=
    have : Module.Finite P.Ring P.ker := .of_fg h'
    .of_surjective _ Extension.Cotangent.mk_surjective
-- Module: Mathlib.RingTheory.Smooth.Local
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsLocalRing S
inst_3 : Algebra R S
P : Extension.{u, u_1, u_2} R S
inst_4 : FormallySmooth.{u_1, u} R P.Ring
inst_5 : Module.Free.{u, u} P.Ring Ω[P.Ring⁄R]
inst_6 : Module.Finite.{u, u} P.Ring Ω[P.Ring⁄R]
h' : P.ker.FG
this : Module.Finite.{u, u} P.Ring P.Cotangent
⊢ Module.Finite.{u_2, u} S P.Cotangent

Tactic:
have : Module.Finite S P.Cotangent := Module.Finite.of_restrictScalars_finite P.Ring _ _