awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ [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_2_to_3 : ∀ (a : Function.Bijective (α := S ⊗[R] S) (β := S) (⇑(LinearMap.mul' R S) : (a : S ⊗[R] S) → S)) (p : PrimeSpectrum R),
  rankAtStalk S p ≤ 1
Tactic: tfae_have 2 → 3 := fun H p ↦ by
    have h : rankAtStalk (S ⊗[R] S) p = rankAtStalk S p ^ 2 := by
      simp [rankAtStalk_tensorProduct, sq]
    by_contra! hc
    apply Nat.succ_succ_ne_one 0
    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 (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)
tfae_2_to_3 :
  ∀ (a : Function.Bijective (α := S ⊗[R] S) (β := S) (⇑(LinearMap.mul' R S) : (a : S ⊗[R] S) → S))
    (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
⊢ [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_3_to_1 : ∀ (a : ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1),
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
Tactic: tfae_have 3 → 1 := Module.algebraMap_surjective_of_rankAtStalk_le_one
-- 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
⊢ Eq.{u_1 + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk S) 1 ↔
    Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
have rw : Eq.{u_1 + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk S) 1 ↔
  (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ∧ ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
Tactic: rw [Function.Bijective, ← rankAtStalk_pos_iff_algebraMap_injective,
    ← rankAtStalk_le_one_iff_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
⊢ Eq.{u_1 + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk S) 1 ↔
    (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ∧ ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
have refine : ∀ (h : (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ∧ ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1),
  Eq.{u_1 + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk S) 1
Tactic: refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩
-- 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), 0 < rankAtStalk S p) ∧ ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
⊢ Eq.{u_1 + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk S) 1
have h₁ : ∀ (p : PrimeSpectrum R), rankAtStalk S p = 1 p
Tactic: ext p
-- 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
⊢ Eq (α := (x : PrimeSpectrum R) → ℕ) (finrank (algebraMap R S)) (Module.rankAtStalk S)
have h : ∀ (x : PrimeSpectrum R), finrank (algebraMap R S) x = Module.rankAtStalk S x
Tactic: ext
-- 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
x : PrimeSpectrum R
⊢ finrank (algebraMap R S) x = Module.rankAtStalk S x
have h : Module.rankAtStalk S x = Module.rankAtStalk S x
Tactic: rw [RingHom.finrank, toAlgebra_algebraMap]
-- 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
x : PrimeSpectrum R
h : Module.rankAtStalk S x = Module.rankAtStalk S x
⊢ finrank (algebraMap R S) x = Module.rankAtStalk S x
have h₁ : Module.rankAtStalk S x = Module.rankAtStalk S x
Tactic: rw [RingHom.finrank, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' : Type u_5
S' : Type u_6
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
inst_11 : IsPushout R S R' S'
inst_12 : Module.Flat R S
inst_13 : Module.Finite R S
x : PrimeSpectrum R'
⊢ Module.rankAtStalk S' x = Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x)
have this : IsPushout R R' S S'
Tactic: have : IsPushout R R' S S' := Algebra.IsPushout.symm inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' : Type u_5
S' : Type u_6
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
inst_11 : IsPushout R S R' S'
inst_12 : Module.Flat R S
inst_13 : Module.Finite R S
x : PrimeSpectrum R'
this : IsPushout R R' S S'
⊢ Module.rankAtStalk S' x = Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x)
have this₁ : Eq.{u_5 + 1} (α := (p : PrimeSpectrum R') → ℕ) (Module.rankAtStalk S') (Module.rankAtStalk (R' ⊗[R] S))
Tactic: have := Module.rankAtStalk_eq_of_equiv (Algebra.IsPushout.equiv R R' S S').symm.toLinearEquiv
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' : Type u_5
S' : Type u_6
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
inst_11 : IsPushout R S R' S'
inst_12 : Module.Flat R S
inst_13 : Module.Finite R S
x : PrimeSpectrum R'
this_1 : IsPushout R R' S S'
this : Eq.{u_5 + 1} (α := (p : PrimeSpectrum R') → ℕ) (Module.rankAtStalk S') (Module.rankAtStalk (R' ⊗[R] S))
⊢ Module.rankAtStalk S' x = Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x)
have rw : Module.rankAtStalk (R' ⊗[R] S) x = Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x)
Tactic: rw [Module.rankAtStalk_eq_of_equiv (Algebra.IsPushout.equiv R R' S S').symm.toLinearEquiv,
    Module.rankAtStalk_baseChange]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
R' : Type u_5
S' : Type u_6
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
inst_11 : IsPushout R S R' S'
inst_12 : Module.Flat R S
inst_13 : Module.Finite R S
x : PrimeSpectrum R'
this_1 : IsPushout R R' S S'
this : Eq.{u_5 + 1} (α := (p : PrimeSpectrum R') → ℕ) (Module.rankAtStalk S') (Module.rankAtStalk (R' ⊗[R] S))
rw : Module.rankAtStalk (R' ⊗[R] S) x = Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x)
⊢ Module.rankAtStalk S' x = Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x)
have rw₁ : Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x) =
  Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x)
Tactic: rw [Module.rankAtStalk_eq_of_equiv (Algebra.IsPushout.equiv R R' S S').symm.toLinearEquiv,
    Module.rankAtStalk_baseChange]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Bijective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
h1 : f.Finite
h2 : f.Flat
x : PrimeSpectrum R
⊢ (g.comp f).finrank x = f.finrank x
have algebraizeInst : Module.Finite R S
Tactic: algebraize [f, g, (g.comp f)]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Bijective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
h1 : f.Finite
h2 : f.Flat
x : PrimeSpectrum R
algebraizeInst : Module.Finite R S
⊢ (g.comp f).finrank x = f.finrank x
have algebraizeInst₁ : Module.Flat R S
Tactic: algebraize [f, g, (g.comp f)]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Bijective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
h1 : f.Finite
h2 : f.Flat
x : PrimeSpectrum R
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Module.Finite R S
algebraizeInst_1 : Module.Flat R S
⊢ (g.comp f).finrank x = f.finrank x
have this : Algebra.IsPushout R S R T
Tactic: have : Algebra.IsPushout R S R T := .of_bijective_right _ _ hf
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (goal)
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h1 : g.Finite
h2 : g.Flat
y : PrimeSpectrum R
x : PrimeSpectrum S
hy : y = PrimeSpectrum.comap f x
⊢ (g.comp f).finrank y = g.finrank x
have subst : (g.comp f).finrank (PrimeSpectrum.comap f x) = g.finrank x
Tactic: subst hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h1 : g.Finite
h2 : g.Flat
x : PrimeSpectrum S
⊢ (g.comp f).finrank (PrimeSpectrum.comap f x) = g.finrank x
have algebraizeInst : Module.Finite S T
Tactic: algebraize [f, g, (g.comp f)]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h1 : g.Finite
h2 : g.Flat
x : PrimeSpectrum S
algebraizeInst : Module.Finite S T
⊢ (g.comp f).finrank (PrimeSpectrum.comap f x) = g.finrank x
have algebraizeInst₁ : Module.Flat S T
Tactic: algebraize [f, g, (g.comp f)]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h1 : g.Finite
h2 : g.Flat
x : PrimeSpectrum S
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Module.Finite S T
algebraizeInst_1 : Module.Flat S T
⊢ (g.comp f).finrank (PrimeSpectrum.comap f x) = g.finrank x
have this : Module.Finite R T
Tactic: have : Module.Finite R T := h1.comp <| .of_surjective _ hg.2
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h1 : g.Finite
h2 : g.Flat
x : PrimeSpectrum S
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Module.Finite S T
algebraizeInst_1 : Module.Flat S T
this : Module.Finite R T
⊢ (g.comp f).finrank (PrimeSpectrum.comap f x) = g.finrank x
have this₁ : Module.Flat R T
Tactic: have : Module.Flat R T := (RingHom.Flat.of_bijective hg).comp h2
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg : Function.Bijective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h1 : g.Finite
h2 : g.Flat
x : PrimeSpectrum S
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Module.Finite S T
algebraizeInst_1 : Module.Flat S T
this_1 : Module.Finite R T
this : Module.Flat R T
⊢ (g.comp f).finrank (PrimeSpectrum.comap f x) = g.finrank x
have this₁ : Algebra.IsPushout R T S T
Tactic: have : Algebra.IsPushout R T S T := .of_bijective_left _ _ hg
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
Goal:
R S T P : CommRingCat
f : R ⟶ S
g : R ⟶ T
inl : S ⟶ P
inr : T ⟶ P
h : CategoryTheory.IsPushout f g inl inr
hf : (Hom.hom f).Flat
hfin : (Hom.hom f).Finite
x : PrimeSpectrum (↑T : Type u)
⊢ (Hom.hom inr).finrank x = (Hom.hom f).finrank (PrimeSpectrum.comap (Hom.hom g) x)
have algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [f.hom, g.hom, inl.hom, inr.hom, inl.hom.comp f.hom]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
Goal:
R S T P : CommRingCat
f : R ⟶ S
g : R ⟶ T
inl : S ⟶ P
inr : T ⟶ P
h : CategoryTheory.IsPushout f g inl inr
hf : (Hom.hom f).Flat
hfin : (Hom.hom f).Finite
x : PrimeSpectrum (↑T : Type u)
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
⊢ (Hom.hom inr).finrank x = (Hom.hom f).finrank (PrimeSpectrum.comap (Hom.hom g) x)
have algebraizeInst₁ : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [f.hom, g.hom, inl.hom, inr.hom, inl.hom.comp f.hom]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
Goal:
R S T P : CommRingCat
f : R ⟶ S
g : R ⟶ T
inl : S ⟶ P
inr : T ⟶ P
h : CategoryTheory.IsPushout f g inl inr
hf : (Hom.hom f).Flat
hfin : (Hom.hom f).Finite
x : PrimeSpectrum (↑T : Type u)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑T : Type u) := (Hom.hom g).toAlgebra
algInst_2 : Algebra (↑S : Type u) (↑P : Type u) := (Hom.hom inl).toAlgebra
algInst_3 : Algebra (↑T : Type u) (↑P : Type u) := (Hom.hom inr).toAlgebra
algInst_4 : Algebra (↑R : Type u) (↑P : Type u) := ((Hom.hom inl).comp (Hom.hom f)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑R : Type u) (↑S : Type u) (↑P : Type u) := ⋯
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
⊢ (Hom.hom inr).finrank x = (Hom.hom f).finrank (PrimeSpectrum.comap (Hom.hom g) x)
have this : IsScalarTower.{u, u, u} (↑R : Type u) (↑T : Type u) (↑P : Type u)
Tactic: have : IsScalarTower R T P := .of_algebraMap_eq' <| congr($(h.1.1).hom)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Rank (hypothesis)
Goal:
R S T P : CommRingCat
f : R ⟶ S
g : R ⟶ T
inl : S ⟶ P
inr : T ⟶ P
h : CategoryTheory.IsPushout f g inl inr
hf : (Hom.hom f).Flat
hfin : (Hom.hom f).Finite
x : PrimeSpectrum (↑T : Type u)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑T : Type u) := (Hom.hom g).toAlgebra
algInst_2 : Algebra (↑S : Type u) (↑P : Type u) := (Hom.hom inl).toAlgebra
algInst_3 : Algebra (↑T : Type u) (↑P : Type u) := (Hom.hom inr).toAlgebra
algInst_4 : Algebra (↑R : Type u) (↑P : Type u) := ((Hom.hom inl).comp (Hom.hom f)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑R : Type u) (↑S : Type u) (↑P : Type u) := ⋯
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
this : IsScalarTower.{u, u, u} (↑R : Type u) (↑T : Type u) (↑P : Type u)
⊢ (Hom.hom inr).finrank x = (Hom.hom f).finrank (PrimeSpectrum.comap (Hom.hom g) x)
have this₁ : Algebra.IsPushout.{u, u, u, u} (↑R : Type u) (↑S : Type u) (↑T : Type u) (↑P : Type u)
Tactic: have : Algebra.IsPushout R S T P := CommRingCat.isPushout_iff_isPushout.mp h
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Stability (goal)
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : Flat R S
inst_8 : Flat S M
⊢ Flat R M
have rw : ∀ ⦃P : Type u⦄ [inst_9 : AddCommMonoid P] [inst_10 : Module R P] (N : Submodule R P),
  Injective (α := M ⊗[R] ↥N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M N.subtype) : (a : M ⊗[R] ↥N) → M ⊗[R] P)
Tactic: rw [Flat.iff_lTensor_injectiveₛ]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Stability (goal)
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : Flat R S
inst_8 : Flat S M
P : Type u
inst_9 : AddCommMonoid P
inst_10 : Module R P
N : Submodule R P
⊢ Injective (α := M ⊗[R] ↥N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M N.subtype) : (a : M ⊗[R] ↥N) → M ⊗[R] P)
have rw : Injective (α := M ⊗[S] (S ⊗[R] ↥N)) (β := M ⊗[S] (S ⊗[R] P))
  (⇑(((AlgebraTensorModule.lTensor S M : (S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) →ₗ[S] M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P)) :
            (a : S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) → M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P))
          (((AlgebraTensorModule.lTensor S S : (↥N →ₗ[R] P) →ₗ[R] S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) :
              (a : ↥N →ₗ[R] P) → S ⊗[R] ↥N →ₗ[S] S ⊗[R] P)
            N.subtype) :
        M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P)) :
    (a : M ⊗[S] (S ⊗[R] ↥N)) → M ⊗[S] (S ⊗[R] P))
Tactic: rw [← coe_lTensor (A := S), ← EquivLike.injective_comp (cancelBaseChange R S S _ _),
    ← LinearEquiv.coe_coe, ← LinearMap.coe_comp, lTensor_comp_cancelBaseChange,
    LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.comp_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Stability (goal)
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : Flat R S
inst_8 : Flat S M
P : Type u
inst_9 : AddCommMonoid P
inst_10 : Module R P
N : Submodule R P
⊢ Injective (α := M ⊗[S] (S ⊗[R] ↥N)) (β := M ⊗[S] (S ⊗[R] P))
    (⇑(((AlgebraTensorModule.lTensor S M :
                (S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) →ₗ[S] M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P)) :
              (a : S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) → M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P))
            (((AlgebraTensorModule.lTensor S S : (↥N →ₗ[R] P) →ₗ[R] S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) :
                (a : ↥N →ₗ[R] P) → S ⊗[R] ↥N →ₗ[S] S ⊗[R] P)
              N.subtype) :
          M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P)) :
      (a : M ⊗[S] (S ⊗[R] ↥N)) → M ⊗[S] (S ⊗[R] P))
have hf : Injective (α := S ⊗[R] ↥N) (β := S ⊗[R] P)
  (⇑(((AlgebraTensorModule.lTensor S S : (↥N →ₗ[R] P) →ₗ[R] S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) :
            (a : ↥N →ₗ[R] P) → S ⊗[R] ↥N →ₗ[S] S ⊗[R] P)
          N.subtype :
        S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) :
    (a : S ⊗[R] ↥N) → S ⊗[R] P)
Tactic: apply Flat.lTensor_preserves_injective_linearMap
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Stability (goal)
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : Flat R S
inst_8 : Flat S M
P : Type u
inst_9 : AddCommMonoid P
inst_10 : Module R P
N : Submodule R P
⊢ Injective (α := S ⊗[R] ↥N) (β := S ⊗[R] P)
    (⇑(((AlgebraTensorModule.lTensor S S : (↥N →ₗ[R] P) →ₗ[R] S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) :
              (a : ↥N →ₗ[R] P) → S ⊗[R] ↥N →ₗ[S] S ⊗[R] P)
            N.subtype :
          S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) :
      (a : S ⊗[R] ↥N) → S ⊗[R] P)
have hf : Injective (α := ↥N) (β := P) (⇑N.subtype : (a : ↥N) → P)
Tactic: apply Flat.lTensor_preserves_injective_linearMap
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Stability (goal)
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : Flat R S
inst_8 : Flat S M
P : Type u
inst_9 : AddCommMonoid P
inst_10 : Module R P
N : Submodule R P
⊢ Injective (α := M ⊗[S] (S ⊗[R] ↥N)) (β := M ⊗[S] (S ⊗[R] P))
    (⇑(((AlgebraTensorModule.lTensor S M :
                (S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) →ₗ[S] M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P)) :
              (a : S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) → M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P))
            (((AlgebraTensorModule.lTensor S S : (↥N →ₗ[R] P) →ₗ[R] S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) :
                (a : ↥N →ₗ[R] P) → S ⊗[R] ↥N →ₗ[S] S ⊗[R] P)
              N.subtype) :
          M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P)) :
      (a : M ⊗[S] (S ⊗[R] ↥N)) → M ⊗[S] (S ⊗[R] P))
have hf : Injective (α := ↥N) (β := P) (⇑N.subtype : (a : ↥N) → P)
Tactic: iterate 2 apply Flat.lTensor_preserves_injective_linearMap
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Stability (goal)
Goal:
R : Type u
M : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Flat (ULift.{t, u} R) M ↔ Flat R M
have refine : ∀ (h : Flat R M), Flat (ULift.{t, u} R) M
Tactic: refine ⟨fun h ↦ .trans _ (ULift R) _, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Stability (hypothesis)
Goal:
R : Type u
M : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Flat R M
⊢ Flat (ULift.{t, u} R) M
have this : Flat (ULift.{t, u} R) R
Tactic: have : Module.Flat (ULift.{t} R) R := .of_ulift
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Stability (goal)
Goal:
R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring Rp
inst_4 : Algebra R Rp
inst_5 : AddCommMonoid Mp
inst_6 : Module R Mp
inst_7 : Module Rp Mp
inst_8 : IsScalarTower R Rp Mp
inst_9 : Flat R M
S : Submonoid R
⊢ Flat (Localization (M := R) S) (LocalizedModule S M)
have apply : IsBaseChange (N := LocalizedModule S M) (Localization (M := R) S) (LocalizedModule.mkLinearMap S M)
Tactic: apply Flat.isBaseChange (R := R) (S := Localization S)
    (f := LocalizedModule.mkLinearMap S M)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Stability (goal)
Goal:
R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring Rp
inst_4 : Algebra R Rp
inst_5 : AddCommMonoid Mp
inst_6 : Module R Mp
inst_7 : Module Rp Mp
inst_8 : IsScalarTower R Rp Mp
inst_9 : Flat R M
S : Submonoid R
⊢ IsBaseChange (N := LocalizedModule S M) (Localization (M := R) S) (LocalizedModule.mkLinearMap S M)
have rw : IsLocalizedModule (M' := LocalizedModule S M) S (LocalizedModule.mkLinearMap S M)
Tactic: rw [← isLocalizedModule_iff_isBaseChange S]