awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
s : Set S
spn : Eq (α := Ideal S) (Ideal.span s) ⊤
Mₛ : (↑s : Type u_2) → Type u_5
inst_7 : (r : (↑s : Type u_2)) → AddCommMonoid (Mₛ r)
inst_8 : (r : (↑s : Type u_2)) → Module.{u_1, u_5} R (Mₛ r)
inst_9 : (r : (↑s : Type u_2)) → Module.{u_2, u_5} S (Mₛ r)
inst_10 : ∀ (r : (↑s : Type u_2)), IsScalarTower.{u_1, u_2, u_5} R S (Mₛ r)
g : (r : (↑s : Type u_2)) → LinearMap.{u_2, u_2, u_3, u_5} (RingHom.id S) M (Mₛ r)
inst_11 : ∀ (r : (↑s : Type u_2)), IsLocalizedModule.Away (↑r : S) (g r)
H :
  ∀ (r : (↑s : Type u_2)) ⦃P : Type u_1⦄ [inst_12 : AddCommMonoid P] [inst_13 : Module R P] (N : Submodule R P),
    Function.Injective (α := TensorProduct.{u_1, u_5, u_1} R (Mₛ r) ↥N) (β := TensorProduct.{u_1, u_5, u_1} R (Mₛ r) P)
      (⇑(lTensor (Mₛ r) N.subtype) : (a : Mₛ r ⊗[R] ↥N) → Mₛ r ⊗[R] P)
⊢ ∀ ⦃P : Type u_1⦄ [inst_12 : AddCommMonoid P] [inst_13 : Module R P] (N : Submodule R P),
    Function.Injective (α := M ⊗[R] ↥N) (β := M ⊗[R] P) (⇑(lTensor M N.subtype) : (a : M ⊗[R] ↥N) → M ⊗[R] P)
have simp_rw : ∀ ⦃P : Type u_1⦄ [inst_12 : AddCommMonoid P] [inst_13 : Module R P] (N : Submodule R P),
  Function.Injective (α := M ⊗[R] ↥N) (β := M ⊗[R] P)
    (⇑(((AlgebraTensorModule.lTensor S M : (↥N →ₗ[R] P) →ₗ[R] M ⊗[R] ↥N →ₗ[S] M ⊗[R] P) :
              (a : ↥N →ₗ[R] P) → M ⊗[R] ↥N →ₗ[S] M ⊗[R] P)
            N.subtype :
          M ⊗[R] ↥N →ₗ[S] M ⊗[R] P) :
      (a : M ⊗[R] ↥N) → M ⊗[R] P)
Tactic: simp_rw [← AlgebraTensorModule.coe_lTensor (A := S)]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Localization (goal)
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} (Localization.AtPrime p) (Localization.AtPrime P)
have rw : Module.Flat.{u_4, u_5} A (Localization.AtPrime P)
Tactic: rw [Module.flat_iff_of_isLocalization (Localization.AtPrime p) p.primeCompl]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (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 : Module.Finite R S
p : PrimeSpectrum R
⊢ 0 < Module.rankAtStalk S p ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
have 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
Tactic: rw [Module.rankAtStalk_eq, Module.finrank_pos_iff, p.nontrivial_iff_mem_rangeComap]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (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 : 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
⊢ 0 < Module.rankAtStalk S p ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
have rw₁ : Nontrivial (p.asIdeal.Fiber S) ↔
  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]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (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 : 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
⊢ 0 < Module.rankAtStalk S p ↔
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S))) p
have 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
Tactic: rw [Module.rankAtStalk_eq, Module.finrank_pos_iff, p.nontrivial_iff_mem_rangeComap]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (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 : Module.Finite R S
⊢ (∀ (p : PrimeSpectrum R), 0 < Module.rankAtStalk S p) ↔
    Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S))
have 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))
Tactic: simp_rw [rankAtStalk_pos_iff_mem_range_comap, ← Set.range_eq_univ,
    Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (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 : 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))
⊢ (∀ (p : PrimeSpectrum R), 0 < Module.rankAtStalk S p) ↔
    Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S))
have 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
Tactic: simp_rw [rankAtStalk_pos_iff_mem_range_comap, ← Set.range_eq_univ,
    Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (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 : 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)
have 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)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦
    have : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr h
    Algebra.IsIntegral.comap_surjective _ _⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (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 : Module.Finite R S
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)
have 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)
Tactic: apply injective_of_isLocalization_isMaximal (fun P _ ↦ Localization.AtPrime P)
    (fun P _ ↦ Localization.AtPrime P ⊗[R] S)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (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 : 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)
have rw : FaithfulSMul (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)
Tactic: rw [← faithfulSMul_iff_algebraMap_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (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 : Module.Finite R S
h : Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (comap (algebraMap R S))
p : Ideal R
inst_5 : p.IsMaximal
⊢ FaithfulSMul (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)
have obtain : ∀ (Q : Ideal S) (isPrime : Q.IsPrime)
  (hQ :
    comap (algebraMap R S) { asIdeal := Q, isPrime := isPrime : PrimeSpectrum S } =
      { asIdeal := p, isPrime := sorry : PrimeSpectrum R }),
  FaithfulSMul (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)
Tactic: obtain ⟨⟨Q, _⟩, hQ⟩ := h ⟨p, inferInstance⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (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 : 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 }
⊢ FaithfulSMul (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)
have this : Q.LiesOver p
Tactic: have : Q.LiesOver p := ⟨congr($(hQ).asIdeal).symm⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (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 : 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
⊢ FaithfulSMul (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (goal)
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
⊢ (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
have rw : (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ↔
  Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
Tactic: rw [← PrimeSpectrum.comap_surjective_iff_injective_of_finite,
    PrimeSpectrum.rankAtStalk_pos_iff_comap_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (goal)
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))
⊢ (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ↔
    Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
have rw₁ : Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) ↔
  Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
Tactic: rw [← PrimeSpectrum.comap_surjective_iff_injective_of_finite,
    PrimeSpectrum.rankAtStalk_pos_iff_comap_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (goal)
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
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
have 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)
Tactic: apply surjective_of_isLocalization_isMaximal (fun P _ ↦ Localization.AtPrime P)
    (fun P _ ↦ Localization.AtPrime P ⊗[R] S)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (goal)
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)
have pos : ∀ (hr : rankAtStalk S { asIdeal := p, isPrime := sorry : 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: by_cases hr : Module.rankAtStalk S ⟨p, inferInstance⟩ = 0
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (goal)
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)
⊢ 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)
have neg : ∀ (hr : ¬rankAtStalk S { asIdeal := p, isPrime := sorry : 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: by_cases hr : Module.rankAtStalk S ⟨p, inferInstance⟩ = 0
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (goal)
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)
have apply : Module.rank (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S) = 0
Tactic: apply Module.subsingleton_of_rank_zero (R := Localization.AtPrime p)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
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)
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (goal)
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)
have neg : finrank (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S) = 1
Tactic: refine (Free.bijective_algebraMap_of_finrank_eq_one ?_).2
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
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),
      Function.Bijective (α := S ⊗[R] S) (β := S) (⇑(LinearMap.mul' R S) : (a : S ⊗[R] S) → S),
      ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1].TFAE
have tfae_1_to_2 : ∀ (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 _ _
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
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
tfae_1_to_2 :
  ∀ (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)
H : Function.Bijective (α := S ⊗[R] S) (β := S) (⇑(LinearMap.mul' R S) : (a : S ⊗[R] S) → S)
p : PrimeSpectrum R
⊢ rankAtStalk S p ≤ 1
have h : rankAtStalk.{u_1, u_2} (S ⊗[R] S) p = HPow.hPow (β := ℕ) (rankAtStalk S p) 2
Tactic: have h : rankAtStalk (S ⊗[R] S) p = rankAtStalk S p ^ 2 := by
      simp [rankAtStalk_tensorProduct, sq]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (goal)
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
tfae_1_to_2 :
  ∀ (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)
H : Function.Bijective (α := S ⊗[R] S) (β := S) (⇑(LinearMap.mul' R S) : (a : S ⊗[R] S) → S)
p : PrimeSpectrum R
h : rankAtStalk.{u_1, u_2} (S ⊗[R] S) p = HPow.hPow (β := ℕ) (rankAtStalk S p) 2
⊢ rankAtStalk S p ≤ 1
have by_contra! : ∀ (hc : 1 < rankAtStalk S p), False
Tactic: by_contra! hc
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (goal)
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
tfae_1_to_2 :
  ∀ (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)
H : Function.Bijective (α := S ⊗[R] S) (β := S) (⇑(LinearMap.mul' R S) : (a : S ⊗[R] S) → S)
p : PrimeSpectrum R
h : rankAtStalk.{u_1, u_2} (S ⊗[R] S) p = HPow.hPow (β := ℕ) (rankAtStalk S p) 2
hc : 1 < rankAtStalk S p
⊢ False
have apply : (Nat.succ 0).succ = 1
Tactic: apply Nat.succ_succ_ne_one 0
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (goal)
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
tfae_1_to_2 :
  ∀ (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)
H : Function.Bijective (α := S ⊗[R] S) (β := S) (⇑(LinearMap.mul' R S) : (a : S ⊗[R] S) → S)
p : PrimeSpectrum R
h : rankAtStalk.{u_1, u_2} (S ⊗[R] S) p = HPow.hPow (β := ℕ) (rankAtStalk S p) 2
hc : 1 < rankAtStalk S p
⊢ (Nat.succ 0).succ = 1
have rw : rankAtStalk S p ^ (Nat.succ 0).succ = rankAtStalk S p
Tactic: rw [← Nat.pow_eq_self_iff hc, ← h, Module.rankAtStalk_eq_of_equiv
      (AlgEquiv.ofBijective (Algebra.TensorProduct.lmul' R (S := S)) H).toLinearEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (goal)
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
tfae_1_to_2 :
  ∀ (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)
H : Function.Bijective (α := S ⊗[R] S) (β := S) (⇑(LinearMap.mul' R S) : (a : S ⊗[R] S) → S)
p : PrimeSpectrum R
h : rankAtStalk.{u_1, u_2} (S ⊗[R] S) p = HPow.hPow (β := ℕ) (rankAtStalk S p) 2
hc : 1 < rankAtStalk S p
rw : rankAtStalk S p ^ (Nat.succ 0).succ = rankAtStalk S p
⊢ (Nat.succ 0).succ = 1
have rw₁ : rankAtStalk.{u_1, u_2} (S ⊗[R] S) p = rankAtStalk S p
Tactic: rw [← Nat.pow_eq_self_iff hc, ← h, Module.rankAtStalk_eq_of_equiv
      (AlgEquiv.ofBijective (Algebra.TensorProduct.lmul' R (S := S)) H).toLinearEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (goal)
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
tfae_1_to_2 :
  ∀ (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)
H : Function.Bijective (α := S ⊗[R] S) (β := S) (⇑(LinearMap.mul' R S) : (a : S ⊗[R] S) → S)
p : PrimeSpectrum R
h : rankAtStalk.{u_1, u_2} (S ⊗[R] S) p = HPow.hPow (β := ℕ) (rankAtStalk S p) 2
hc : 1 < rankAtStalk S p
rw : rankAtStalk S p ^ (Nat.succ 0).succ = rankAtStalk S p
rw₁ : rankAtStalk.{u_1, u_2} (S ⊗[R] S) p = rankAtStalk S p
⊢ (Nat.succ 0).succ = 1
have rw₂ : rankAtStalk S p = rankAtStalk S p
Tactic: rw [← Nat.pow_eq_self_iff hc, ← h, Module.rankAtStalk_eq_of_equiv
      (AlgEquiv.ofBijective (Algebra.TensorProduct.lmul' R (S := S)) H).toLinearEquiv]