awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
p_1 : Submonoid R
inst_3 : IsLocalization p_1 S
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module S M
inst_7 : IsScalarTower R S M
A : Type u_4
B : Type u_5
inst_8 : CommRing A
inst_9 : CommRing B
inst_10 : Algebra A B
inst_11 : Module.Flat A B
p : Ideal A
inst_12 : p.IsPrime
P : Ideal B
inst_13 : P.IsPrime
inst_14 : P.LiesOver p
inst_15 : Algebra.{u_4, u_5} (Localization.AtPrime p) (Localization.AtPrime P)
inst_16 : Localization.AtPrime.IsLiesOverAlgebra p P
⊢ Module.Flat.{u_4, u_5} A (Localization.AtPrime P)

Tactic:
exact Module.Flat.trans A B (Localization.AtPrime P)

Premises used: Localization.AtPrime, Module.Flat.trans
-- Module: Mathlib.RingTheory.Flat.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
p : Submonoid R
inst_3 : IsLocalization p S
M : Type u_3
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module S M
inst_7 : IsScalarTower R S M
K : Type u_6
inst_8 : AddCommMonoid K
inst_9 : Module R K
f : K →ₗ[R] M
inst_10 : IsLocalizedModule p f
x : R
reg : IsSMulRegular K x
⊢ IsSMulRegular.{u_2, u_3} (R := S) M ((algebraMap R S : (a : R) → S) x : S)

Tactic:
have : Module.Flat R S := IsLocalization.flat S p
  reg.of_flat_of_isBaseChange (IsLocalizedModule.isBaseChange p S f)

Premises used: IsLocalizedModule.isBaseChange, IsSMulRegular.of_flat_of_isBaseChange, IsLocalization.flat
-- Module: Mathlib.RingTheory.Flat.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
p : Submonoid R
inst_3 : IsLocalization p S
x : R
reg : IsSMulRegular R x
⊢ IsSMulRegular (R := S) S ((algebraMap R S : (a : R) → S) x : S)

Tactic:
reg.of_isLocalizedModule S p (Algebra.linearMap R S)

Premises used: Algebra.linearMap, IsSMulRegular.of_isLocalizedModule
-- Module: Mathlib.RingTheory.Flat.Rank
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 : Module.Finite R S
p : PrimeSpectrum R
rw :
  0 < Module.finrank p.asIdeal.ResidueField (p.asIdeal.Fiber S) ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
rw₁ :
  Nontrivial (p.asIdeal.Fiber S) ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
rw₂ rw₃ :
  Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
⊢ 0 < Module.rankAtStalk S p ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p

Tactic:
rw [Module.rankAtStalk_eq, Module.finrank_pos_iff, p.nontrivial_iff_mem_rangeComap]

Premises used: Module.rankAtStalk_eq, Module.finrank_pos_iff, PrimeSpectrum.nontrivial_iff_mem_rangeComap
-- Module: Mathlib.RingTheory.Flat.Rank
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 : Module.Finite R S
simp_rw :
  (∀ (p : PrimeSpectrum R),
      Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p) ↔
    Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S))
simp_rw₁ :
  (∀ (p : PrimeSpectrum R),
      Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p) ↔
    Eq (α := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) Set.univ
⊢ (∀ (p : PrimeSpectrum R), 0 < Module.rankAtStalk S p) ↔
    Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S))

Tactic:
simp_rw [rankAtStalk_pos_iff_mem_range_comap, ← Set.range_eq_univ,
    Set.eq_univ_iff_forall]

Premises used: Set.range_eq_univ, Set.eq_univ_iff_forall, PrimeSpectrum.rankAtStalk_pos_iff_mem_range_comap
-- Module: Mathlib.RingTheory.Flat.Rank
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 : Module.Finite R S
⊢ Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S)) ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
⟨fun h ↦ ?_, fun h ↦
    have : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr h
    Algebra.IsIntegral.comap_surjective _ _⟩

Premises used: Iff.mpr, faithfulSMul_iff_algebraMap_injective, Iff.intro, Algebra.IsIntegral.comap_surjective
-- Module: Mathlib.RingTheory.Flat.Rank
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 : Module.Finite R S
refine :
  ∀ (h : Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S))),
    Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S)) ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦
    have : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr h
    Algebra.IsIntegral.comap_surjective _ _⟩
-- Module: Mathlib.RingTheory.Flat.Rank
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 : Module.Finite R S
h : Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S))
apply :
  ∀ (p : Ideal R) [inst_5 : p.IsMaximal],
    Function.Injective (α := Localization.AtPrime p) (β := Localization.AtPrime p ⊗[R] S)
      (⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)) :
        (a : Localization.AtPrime p) → Localization.AtPrime p ⊗[R] S)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
apply injective_of_isLocalization_isMaximal (fun P _ ↦ Localization.AtPrime P)
    (fun P _ ↦ Localization.AtPrime P ⊗[R] S)

Premises used: Localization.AtPrime, injective_of_isLocalization_isMaximal, TensorProduct
-- Module: Mathlib.RingTheory.Flat.Rank
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 : Module.Finite R S
h : Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S))
p : Ideal R
_ :
  ∀ [inst_5 : p.IsMaximal],
    Function.Injective (α := Localization.AtPrime p) (β := Localization.AtPrime p ⊗[R] S)
      (⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)) :
        (a : Localization.AtPrime p) → Localization.AtPrime p ⊗[R] S)
⊢ ∀ [inst_5 : p.IsMaximal],
    Function.Injective (α := Localization.AtPrime p) (β := Localization.AtPrime p ⊗[R] S)
      (⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)) :
        (a : Localization.AtPrime p) → Localization.AtPrime p ⊗[R] S)

Tactic:
_
-- Module: Mathlib.RingTheory.Flat.Rank
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 : Module.Finite R S
h : Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S))
p : Ideal R
inst_5 : p.IsMaximal
rw : FaithfulSMul (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)
⊢ Function.Injective (α := Localization.AtPrime p) (β := Localization.AtPrime p ⊗[R] S)
    (⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)) :
      (a : Localization.AtPrime p) → Localization.AtPrime p ⊗[R] S)

Tactic:
rw [← faithfulSMul_iff_algebraMap_injective]

Premises used: faithfulSMul_iff_algebraMap_injective
-- Module: Mathlib.RingTheory.Flat.Rank
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 : Module.Finite R S
h : Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S))
p : Ideal R
inst_5 : p.IsMaximal
obtain :
  ∀ (Q : Ideal S) (isPrime : Q.IsPrime)
    (hQ :
      comap (algebraMap R S) { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S } =
        { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }),
    FaithfulSMul (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)
⊢ FaithfulSMul (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)

Tactic:
obtain ⟨⟨Q, _⟩, hQ⟩ := h ⟨p, inferInstance⟩

Premises used: PrimeSpectrum.mk, inferInstance
-- Module: Mathlib.RingTheory.Flat.Rank
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 : Module.Finite R S
h : Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S))
p : Ideal R
inst_5 : p.IsMaximal
Q : Ideal S
isPrime : Q.IsPrime
hQ :
  comap (algebraMap R S) { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S } =
    { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }
⊢ Q.LiesOver p

Tactic:
have : Q.LiesOver p := ⟨congr($(hQ).asIdeal).symm⟩
-- Module: Mathlib.RingTheory.Flat.Rank
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 : Module.Finite R S
h : Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S))
p : Ideal R
inst_5 : p.IsMaximal
Q : Ideal S
isPrime : Q.IsPrime
hQ :
  comap (algebraMap R S) { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S } =
    { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }
this_1 : Q.LiesOver p
this : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver p Q
f : Localization.AtPrime p ⊗[R] S →ₐ[R] Localization.AtPrime Q :=
  Algebra.TensorProduct.lift (IsScalarTower.toAlgHom R (Localization.AtPrime p) (Localization.AtPrime Q))
    (IsScalarTower.toAlgHom R S (Localization.AtPrime Q)) ⋯
⊢ Nontrivial (Localization.AtPrime p ⊗[R] S)

Tactic:
f.domain_nontrivial

Premises used: AlgHom.toRingHom, RingHom.domain_nontrivial
-- Module: Mathlib.RingTheory.Flat.Rank
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 : Module.Finite R S
h : Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S))
p : Ideal R
inst_5 : p.IsMaximal
Q : Ideal S
isPrime : Q.IsPrime
hQ :
  comap (algebraMap R S) { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S } =
    { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }
this_1 : Q.LiesOver p
this : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver p Q
f : Localization.AtPrime p ⊗[R] S →ₐ[R] Localization.AtPrime Q :=
  Algebra.TensorProduct.lift (IsScalarTower.toAlgHom R (Localization.AtPrime p) (Localization.AtPrime Q))
    (IsScalarTower.toAlgHom R S (Localization.AtPrime Q)) ⋯
⊢ Nontrivial (Localization.AtPrime p ⊗[R] S)

Tactic:
exact f.domain_nontrivial

Premises used: AlgHom.toRingHom, RingHom.domain_nontrivial
-- Module: Mathlib.RingTheory.Flat.Rank
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 : Module.Finite R S
h : Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S))
p : Ideal R
inst_5 : p.IsMaximal
Q : Ideal S
isPrime : Q.IsPrime
hQ :
  comap (algebraMap R S) { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S } =
    { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }
this_1 : Q.LiesOver p
this : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver p Q
⊢ Nontrivial (Localization.AtPrime p ⊗[R] S)

Tactic:
have : Nontrivial (Localization.AtPrime p ⊗[R] S) := by
    let f : Localization.AtPrime p ⊗[R] S →ₐ[R] Localization.AtPrime Q :=
      Algebra.TensorProduct.lift (IsScalarTower.toAlgHom R _ _)
        (IsScalarTower.toAlgHom R S _) (fun _ _ ↦ Commute.all _ _)
    exact f.domain_nontrivial
-- Module: Mathlib.RingTheory.Flat.Rank
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 : Module.Finite R S
h : Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S))
p : Ideal R
inst_5 : p.IsMaximal
Q : Ideal S
isPrime : Q.IsPrime
hQ :
  comap (algebraMap R S) { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S } =
    { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }
this_1 : Q.LiesOver p
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver p Q
this : Nontrivial (Localization.AtPrime p ⊗[R] S)
⊢ FaithfulSMul (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
inst_4 : Module.Finite R S
rw :
  (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ↔
    Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
rw₁ rw₂ :
  Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) ↔
    Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
⊢ (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
rw [← PrimeSpectrum.comap_surjective_iff_injective_of_finite,
    PrimeSpectrum.rankAtStalk_pos_iff_comap_surjective]

Premises used: PrimeSpectrum.rankAtStalk_pos_iff_comap_surjective, PrimeSpectrum.comap_surjective_iff_injective_of_finite
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
inst_4 : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
apply :
  ∀ (p : Ideal R) [inst_5 : p.IsMaximal],
    Function.Surjective (α := Localization.AtPrime p) (β := Localization.AtPrime p ⊗[R] S)
      (⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)) :
        (a : Localization.AtPrime p) → Localization.AtPrime p ⊗[R] S)
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
apply surjective_of_isLocalization_isMaximal (fun P _ ↦ Localization.AtPrime P)
    (fun P _ ↦ Localization.AtPrime P ⊗[R] S)

Premises used: Localization.AtPrime, surjective_of_isLocalization_isMaximal, TensorProduct
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
inst_4 : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
_ :
  ∀ [inst_5 : p.IsMaximal],
    Function.Surjective (α := Localization.AtPrime p) (β := Localization.AtPrime p ⊗[R] S)
      (⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)) :
        (a : Localization.AtPrime p) → Localization.AtPrime p ⊗[R] S)
⊢ ∀ [inst_5 : p.IsMaximal],
    Function.Surjective (α := Localization.AtPrime p) (β := Localization.AtPrime p ⊗[R] S)
      (⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)) :
        (a : Localization.AtPrime p) → Localization.AtPrime p ⊗[R] S)

Tactic:
_
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
inst_4 : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst_5 : p.IsMaximal
pos :
  ∀ (hr : rankAtStalk S { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R } = 0),
    Function.Surjective (α := Localization.AtPrime p) (β := Localization.AtPrime p ⊗[R] S)
      (⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)) :
        (a : Localization.AtPrime p) → Localization.AtPrime p ⊗[R] S)
neg :
  ∀ (hr : ¬rankAtStalk S { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R } = 0),
    Function.Surjective (α := Localization.AtPrime p) (β := Localization.AtPrime p ⊗[R] S)
      (⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)) :
        (a : Localization.AtPrime p) → Localization.AtPrime p ⊗[R] S)
⊢ Function.Surjective (α := Localization.AtPrime p) (β := Localization.AtPrime p ⊗[R] S)
    (⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)) :
      (a : Localization.AtPrime p) → Localization.AtPrime p ⊗[R] S)

Tactic:
by_cases hr : Module.rankAtStalk S ⟨p, inferInstance⟩ = 0

Premises used: PrimeSpectrum.mk, Module.rankAtStalk, inferInstance
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
inst_4 : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst_5 : p.IsMaximal
hr : rankAtStalk S { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R } = 0
apply : Module.rank (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S) = 0
⊢ Subsingleton (Localization.AtPrime p ⊗[R] S)

Tactic:
apply Module.subsingleton_of_rank_zero (R := Localization.AtPrime p)

Premises used: Module.subsingleton_of_rank_zero
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
inst_4 : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst_5 : p.IsMaximal
hr : rankAtStalk S { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R } = 0
⊢ Module.rank (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S) = 0

Tactic:
simp [← finrank_eq_rank, ← rankAtStalk_eq_finrank_tensorProduct ⟨p, inferInstance⟩, hr]

Premises used: PrimeSpectrum.mk, inferInstance, Module.rankAtStalk_eq_finrank_tensorProduct, Module.finrank_eq_rank
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
inst_4 : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst_5 : p.IsMaximal
hr : rankAtStalk S { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R } = 0
⊢ Subsingleton (Localization.AtPrime p ⊗[R] S)

Tactic:
have : Subsingleton (Localization.AtPrime p ⊗[R] S) := by
      apply Module.subsingleton_of_rank_zero (R := Localization.AtPrime p)
      simp [← finrank_eq_rank, ← rankAtStalk_eq_finrank_tensorProduct ⟨p, inferInstance⟩, hr]
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
inst_4 : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst_5 : p.IsMaximal
hr : rankAtStalk S { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R } = 0
this : Subsingleton (Localization.AtPrime p ⊗[R] S)
⊢ Function.Surjective (α := Localization.AtPrime p) (β := Localization.AtPrime p ⊗[R] S)
    (⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)) :
      (a : Localization.AtPrime p) → Localization.AtPrime p ⊗[R] S)

Tactic:
Function.surjective_to_subsingleton _

Premises used: Function.surjective_to_subsingleton
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
inst_4 : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst_5 : p.IsMaximal
hr : rankAtStalk S { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R } = 0
this : Subsingleton (Localization.AtPrime p ⊗[R] S)
⊢ Function.Surjective (α := Localization.AtPrime p) (β := Localization.AtPrime p ⊗[R] S)
    (⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)) :
      (a : Localization.AtPrime p) → Localization.AtPrime p ⊗[R] S)

Tactic:
exact Function.surjective_to_subsingleton _

Premises used: Function.surjective_to_subsingleton
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
inst_4 : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst_5 : p.IsMaximal
hr : ¬rankAtStalk S { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R } = 0
⊢ Function.Surjective (α := Localization.AtPrime p) (β := Localization.AtPrime p ⊗[R] S)
    (⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)) :
      (a : Localization.AtPrime p) → Localization.AtPrime p ⊗[R] S)

Tactic:
(Free.bijective_algebraMap_of_finrank_eq_one ?_).2

Premises used: And.right, Module.Free.bijective_algebraMap_of_finrank_eq_one
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
inst_4 : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst_5 : p.IsMaximal
hr : ¬rankAtStalk S { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R } = 0
neg : finrank (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S) = 1
⊢ Function.Surjective (α := Localization.AtPrime p) (β := Localization.AtPrime p ⊗[R] S)
    (⇑(algebraMap (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)) :
      (a : Localization.AtPrime p) → Localization.AtPrime p ⊗[R] S)

Tactic:
refine (Free.bijective_algebraMap_of_finrank_eq_one ?_).2

Premises used: And.right, Module.Free.bijective_algebraMap_of_finrank_eq_one
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
inst_4 : Module.Finite R S
h : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : Ideal R
inst_5 : p.IsMaximal
hr : ¬rankAtStalk S { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R } = 0
⊢ finrank (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S) = 1

Tactic:
grind [rankAtStalk_eq_finrank_tensorProduct ⟨p, inferInstance⟩]

Premises used: PrimeSpectrum.mk, inferInstance, Module.rankAtStalk_eq_finrank_tensorProduct
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
inst_4 : Module.Finite R S
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
inst_4 : Module.Finite R S
⊢ Function.Bijective (α := S ⊗[R] S) (β := S) (⇑(LinearMap.mul' R S) : (a : S ⊗[R] S) → S)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
inst_4 : Module.Finite R S
⊢ ∀ (a : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)),
    Function.Bijective (α := S ⊗[R] S) (β := S) (⇑(LinearMap.mul' R S) : (a : S ⊗[R] S) → S)

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Flat R S
inst_4 : Module.Finite R S
⊢ ∀ (a : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)),
    Function.Bijective (α := S ⊗[R] S) (β := S) (⇑(LinearMap.mul' R S) : (a : S ⊗[R] S) → S)

Tactic:
tfae_have 1 → 2 := LinearMap.mul'_bijective_of_surjective _ _

Premises used: LinearMap.mul'_bijective_of_surjective