awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1

Tactic:
3

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
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)
⊢ ∀ (a : Function.Bijective (α := S ⊗[R] S) (β := S) (⇑(LinearMap.mul' R S) : (a : S ⊗[R] S) → S))
    (p : PrimeSpectrum R), rankAtStalk S p ≤ 1

Tactic:
2 → 3

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
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.{u_1, u_2} (S ⊗[R] S) p = HPow.hPow (β := ℕ) (rankAtStalk S p) 2

Tactic:
simp [rankAtStalk_tensorProduct, sq]

Premises used: sq, Module.rankAtStalk_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
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.{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]
-- 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
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
by_contra! : ∀ (hc : 1 < rankAtStalk S p), False
⊢ rankAtStalk S p ≤ 1

Tactic:
by_contra! hc
-- 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
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
apply : (Nat.succ 0).succ = 1
⊢ False

Tactic:
apply Nat.succ_succ_ne_one 0

Premises used: Nat.succ_succ_ne_one, OfNat.ofNat
-- 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
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
rw₂ rw₃ : rankAtStalk S p = rankAtStalk S p
⊢ (Nat.succ 0).succ = 1

Tactic:
rw [← Nat.pow_eq_self_iff hc, ← h, Module.rankAtStalk_eq_of_equiv
      (AlgEquiv.ofBijective (Algebra.TensorProduct.lmul' R (S := S)) H).toLinearEquiv]

Premises used: AlgEquiv.ofBijective, Module.rankAtStalk_eq_of_equiv, Algebra.TensorProduct.lmul', Nat.pow_eq_self_iff, AlgEquiv.toLinearEquiv
-- 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
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)
⊢ ∀ (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]
-- 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
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
⊢ ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1

Tactic:
3

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
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)

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
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
⊢ ∀ (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:
3 → 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
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
⊢ ∀ (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

Premises used: Module.algebraMap_surjective_of_rankAtStalk_le_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
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
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)
⊢ [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

Tactic:
tfae_finish
-- 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
⊢ (∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1) ↔
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
(Module.Flat.tfae_algebraMap_surjective R S).out 2 0

Premises used: Module.Flat.tfae_algebraMap_surjective, List.TFAE.out, OfNat.ofNat
-- 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 :
  Eq.{u_1 + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk S) 1 ↔
    (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ∧ ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
⊢ 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)

Tactic:
rw [Function.Bijective, ← rankAtStalk_pos_iff_algebraMap_injective,
    ← rankAtStalk_le_one_iff_surjective]

Premises used: Module.rankAtStalk_pos_iff_algebraMap_injective, Module.rankAtStalk_le_one_iff_surjective, Function.Bijective
-- 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 : 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:
simp [h]
-- 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
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
⊢ 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:
refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩
-- 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), 0 < rankAtStalk S p) ∧ ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
h₁ : ∀ (p : PrimeSpectrum R), rankAtStalk S p = 1 p
⊢ Eq.{u_1 + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk S) 1

Tactic:
ext p
-- 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), 0 < rankAtStalk S p) ∧ ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
p : PrimeSpectrum R
⊢ rankAtStalk S p = 1

Tactic:
grind
-- 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
h : ∀ (x : PrimeSpectrum R), finrank (algebraMap R S) x = Module.rankAtStalk S x
⊢ Eq (α := (x : PrimeSpectrum R) → ℕ) (finrank (algebraMap R S)) (Module.rankAtStalk S)

Tactic:
ext
-- 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
x : PrimeSpectrum R
h : Module.rankAtStalk S x = Module.rankAtStalk S x
h₁ h₂ : Module.rankAtStalk S x = Module.rankAtStalk S x
⊢ finrank (algebraMap R S) x = Module.rankAtStalk S x

Tactic:
rw [RingHom.finrank, toAlgebra_algebraMap]

Premises used: RingHom.finrank, toAlgebra_algebraMap
-- Module: Mathlib.RingTheory.Flat.Rank
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'
⊢ IsPushout R R' S S'

Tactic:
have : IsPushout R R' S S' := Algebra.IsPushout.symm inferInstance
-- Module: Mathlib.RingTheory.Flat.Rank
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'
⊢ 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
-- Module: Mathlib.RingTheory.Flat.Rank
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)
rw₁ rw₂ :
  Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x) =
    Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x)
⊢ Module.rankAtStalk 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]

Premises used: AlgEquiv.symm, Algebra.IsPushout.equiv, Module.rankAtStalk_baseChange, Module.rankAtStalk_eq_of_equiv, AlgEquiv.toLinearEquiv
-- Module: Mathlib.RingTheory.Flat.Rank
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
⊢ Module.Finite R S

Tactic:
algebraize [f, g, (g.comp f)]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.Flat.Rank
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
⊢ Module.Flat R S

Tactic:
algebraize [f, g, (g.comp f)]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.Flat.Rank
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
⊢ Algebra.IsPushout R S R T

Tactic:
have : Algebra.IsPushout R S R T := .of_bijective_right _ _ hf
-- Module: Mathlib.RingTheory.Flat.Rank
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
this : Algebra.IsPushout R S R T
⊢ (g.comp f).finrank x = f.finrank x

Tactic:
apply Algebra.rankAtStalk_eq_of_isPushout

Premises used: Algebra.rankAtStalk_eq_of_isPushout
-- Module: Mathlib.RingTheory.Flat.Rank
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
subst : (g.comp f).finrank (PrimeSpectrum.comap f x) = g.finrank x
⊢ (g.comp f).finrank y = g.finrank x

Tactic:
subst hy
-- Module: Mathlib.RingTheory.Flat.Rank
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
⊢ Module.Finite S T

Tactic:
algebraize [f, g, (g.comp f)]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.Flat.Rank
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
⊢ Module.Flat S T

Tactic:
algebraize [f, g, (g.comp f)]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.Flat.Rank
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
⊢ Module.Finite R T

Tactic:
have : Module.Finite R T := h1.comp <| .of_surjective _ hg.2
-- Module: Mathlib.RingTheory.Flat.Rank
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
⊢ Module.Flat R T

Tactic:
have : Module.Flat R T := (RingHom.Flat.of_bijective hg).comp h2
-- Module: Mathlib.RingTheory.Flat.Rank
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
⊢ Algebra.IsPushout R T S T

Tactic:
have : Algebra.IsPushout R T S T := .of_bijective_left _ _ hg
-- Module: Mathlib.RingTheory.Flat.Rank
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_2 : Module.Flat R T
this : Algebra.IsPushout R T S T
⊢ (g.comp f).finrank (PrimeSpectrum.comap f x) = g.finrank x

Tactic:
(Algebra.rankAtStalk_eq_of_isPushout _ _ _ _ _).symm

Premises used: Algebra.rankAtStalk_eq_of_isPushout, RingHom.finrank, Eq.symm
-- Module: Mathlib.RingTheory.Flat.Rank
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_2 : Module.Flat R T
this : Algebra.IsPushout R T S T
⊢ (g.comp f).finrank (PrimeSpectrum.comap f x) = g.finrank x

Tactic:
exact (Algebra.rankAtStalk_eq_of_isPushout _ _ _ _ _).symm

Premises used: Algebra.rankAtStalk_eq_of_isPushout, Eq.symm
-- Module: Mathlib.RingTheory.Flat.Rank
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)
⊢ 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]

Premises used: CommRingCat.Hom.hom, RingHom.comp
-- Module: Mathlib.RingTheory.Flat.Rank
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)
⊢ 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]

Premises used: CommRingCat.Hom.hom, RingHom.comp