mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
s : Finset S
hs : Submodule.span R ↑s = ⊤
S' : Type u
w✝⁴ : CommRing S'
w✝³ : Algebra R S'
w✝² : Module.Finite R S'
w✝¹ : Free R S'
w✝ : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : ↑s ⊆ ↑f.range
this : Function.Surjective ⇑f.toLinearMap
⊢ Function.Surjective ⇑f

Tactic:
]

Goal state after:
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
s : Finset S
hs : Submodule.span R ↑s = ⊤
S' : Type u
w✝⁴ : CommRing S'
w✝³ : Algebra R S'
w✝² : Module.Finite R S'
w✝¹ : Free R S'
w✝ : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : ↑s ⊆ ↑f.range
this : Function.Surjective ⇑f.toLinearMap
⊢ Function.Surjective ⇑f
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Flat R S
inst✝ : Module.Finite R S
p : PrimeSpectrum R
⊢ p ∈ Set.range (comap (algebraMap R S)) ↔ p ∈ Set.range (comap (algebraMap R S))

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Flat R S
inst✝¹ : Module.Finite R S
h : Function.Surjective (comap (algebraMap R S))
p : Ideal R
inst✝ : p.IsMaximal
⊢ FaithfulSMul (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Flat R S
inst✝¹ : Module.Finite R S
h : Function.Surjective (comap (algebraMap R S))
p : Ideal R
inst✝ : p.IsMaximal
⊢ FaithfulSMul (Localization.AtPrime p) (Localization.AtPrime p ⊗[R] S)
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
⊢ Function.Surjective (PrimeSpectrum.comap (algebraMap R S)) ↔
    Function.Surjective (PrimeSpectrum.comap (algebraMap R S))

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
tfae_1_to_2 : Function.Surjective ⇑(algebraMap R S) → Function.Bijective ⇑(LinearMap.mul' R S)
H : Function.Bijective ⇑(LinearMap.mul' R S)
p : PrimeSpectrum R
h : rankAtStalk (S ⊗[R] S) p = rankAtStalk S p ^ 2
hc : 1 < rankAtStalk S p
⊢ rankAtStalk S p = rankAtStalk S p

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
⊢ rankAtStalk S = 1 ↔ (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ∧ ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
⊢ rankAtStalk S = 1 ↔ (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ∧ ∀ (p : PrimeSpectrum R), rankAtStalk S p ≤ 1
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : 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:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : 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
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : PrimeSpectrum R
⊢ Module.rankAtStalk S x✝ = Module.rankAtStalk S x✝

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).finrank = Module.rankAtStalk S

Tactic:
ext
  rw [RingHom.finrank, toAlgebra_algebraMap]

Goal state after:
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
R' : Type u_5
S' : Type u_6
inst✝¹⁰ : CommRing R'
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra R' S'
inst✝⁵ : Algebra R S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsScalarTower R S S'
inst✝² : IsPushout R S R' S'
inst✝¹ : Module.Flat R S
inst✝ : Module.Finite R S
x : PrimeSpectrum R'
this✝ : IsPushout R R' S S'
this : Module.rankAtStalk S' = Module.rankAtStalk (R' ⊗[R] S)
⊢ Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x) =
    Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X S Y T : Scheme
f : X ⟶ S
inst✝³ : IsAffine S
inst✝² : IsAffine T
f' : Y ⟶ T
g' : Y ⟶ X
g : T ⟶ S
h : IsPullback g' f' f g
inst✝¹ : Flat f
inst✝ : IsFinite f
t : ↥T
this✝ : IsAffine X
this : IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop g') (Scheme.Hom.appTop f')
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank
      (PrimeSpectrum.comap (CommRingCat.Hom.hom (Scheme.Hom.appTop g)) (T.isoSpec.hom t)) =
    (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank ((T.isoSpec.hom ≫ Spec.map (Scheme.Hom.appTop g)) t)

Tactic:
]

Goal state after:
X S Y T : Scheme
f : X ⟶ S
inst✝³ : IsAffine S
inst✝² : IsAffine T
f' : Y ⟶ T
g' : Y ⟶ X
g : T ⟶ S
h : IsPullback g' f' f g
inst✝¹ : Flat f
inst✝ : IsFinite f
t : ↥T
this✝ : IsAffine X
this : IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop g') (Scheme.Hom.appTop f')
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank
      (PrimeSpectrum.comap (CommRingCat.Hom.hom (Scheme.Hom.appTop g)) (T.isoSpec.hom t)) =
    (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).finrank ((T.isoSpec.hom ≫ Spec.map (Scheme.Hom.appTop g)) t)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ (𝟙 c ◁ g₂ ◁ adj₃.unit ≫ adj₂.unit ▷ (g₂ ≫ l₃ ≫ r₃)) ⊗≫
        r₁ ◁ ((g₁ ≫ l₂) ◁ r₂ ◁ β ≫ α ▷ (r₂ ≫ l₂ ≫ h₂)) ▷ r₃ ⊗≫
          (((r₁ ≫ l₁) ≫ h₁) ◁ adj₂.counit ≫ adj₁.counit ▷ h₁ ▷ 𝟙 d) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ l₃) ≫ (l₂ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
          r₁ ◁ (α ▷ (r₂ ≫ l₂) ≫ (l₁ ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ (𝟙 c ◁ g₂ ◁ adj₃.unit ≫ adj₂.unit ▷ (g₂ ≫ l₃ ≫ r₃)) ⊗≫
        r₁ ◁ ((g₁ ≫ l₂) ◁ r₂ ◁ β ≫ α ▷ (r₂ ≫ l₂ ≫ h₂)) ▷ r₃ ⊗≫
          (((r₁ ≫ l₁) ≫ h₁) ◁ adj₂.counit ≫ adj₁.counit ▷ h₁ ▷ 𝟙 d) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ l₃) ≫ (l₂ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
          r₁ ◁ (α ▷ (r₂ ≫ l₂) ≫ (l₁ ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝² : IsAffine S
inst✝¹ : Flat f
inst✝ : IsFinite f
s : ↥S
⊢ IsAffine.finrank f ((𝟙 S) s) = IsAffine.finrank f ((𝟙 S) s)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf₁✝ : IsFinite (Spec.map f)
hf₂✝ : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x✝ : ↥(Spec R)
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Spec R).isoSpec.hom x✝) = (CommRingCat.Hom.hom f).finrank x✝

Tactic:
]

Goal state after:
R S : CommRingCat
f : R ⟶ S
hf₁✝ : IsFinite (Spec.map f)
hf₂✝ : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x✝ : ↥(Spec R)
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Spec R).isoSpec.hom x✝) = (CommRingCat.Hom.hom f).finrank x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf₁✝ : IsFinite (Spec.map f)
hf₂✝ : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x✝ : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Spec R).isoSpec.hom x✝) =
    (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ?m.169

pp: R S : CommRingCat
f : R ⟶ S
hf₁✝ : IsFinite (Spec.map f)
hf₂✝ : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x✝ : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
⊢ PrimeSpectrum ↑Γ(Spec R, ⊤)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ (𝟙 c ◁ β ≫ adj₂.unit ▷ (l₂ ≫ h₂)) ▷ r₃ ⊗≫
          r₁ ◁ ((g₁ ≫ l₂) ◁ adj₂.counit ≫ α ▷ 𝟙 d) ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ β ▷ r₃ ⊗≫
          (r₁ ≫ g₁) ◁ leftZigzag adj₂.unit adj₂.counit ▷ (h₂ ≫ r₃) ⊗≫
            r₁ ◁ α ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ (𝟙 c ◁ β ≫ adj₂.unit ▷ (l₂ ≫ h₂)) ▷ r₃ ⊗≫
          r₁ ◁ ((g₁ ≫ l₂) ◁ adj₂.counit ≫ α ▷ 𝟙 d) ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ β ▷ r₃ ⊗≫
          (r₁ ≫ g₁) ◁ leftZigzag adj₂.unit adj₂.counit ▷ (h₂ ≫ r₃) ⊗≫
            r₁ ◁ α ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Module.Flat R S
x : PrimeSpectrum R
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S))).finrank x = Module.rankAtStalk S x

pp: case hf₁
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Module.Flat R S
x : PrimeSpectrum R
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S))).Finite

pp: case hf₂
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Module.Flat R S
x : PrimeSpectrum R
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S))).Flat

Tactic:
]

Goal state after:
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Module.Flat R S
x : PrimeSpectrum R
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S))).finrank x = Module.rankAtStalk S x

case hf₁
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Module.Flat R S
x : PrimeSpectrum R
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S))).Finite

case hf₂
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Module.Flat R S
x : PrimeSpectrum R
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S))).Flat
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X S Y : Scheme
f : X ⟶ Y
g : Y ⟶ S
inst✝² : IsIso f
inst✝¹ : Flat g
inst✝ : IsFinite g
z : ↥S
e : pullback (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z)) ≅
  pullback g (S.affineOpenCover.f (S.affineOpenCover.idx z)) :=
  (pullbackRightPullbackFstIso g (S.affineOpenCover.f (S.affineOpenCover.idx z)) f).symm ≪≫
    asIso (pullback.snd f (pullback.fst g (S.affineOpenCover.f (S.affineOpenCover.idx z))))
this :
  e.hom ≫ pullback.snd g (S.affineOpenCover.f (S.affineOpenCover.idx z)) =
    pullback.snd (f ≫ g) (S.affineOpenCover.f (S.affineOpenCover.idx z))
⊢ IsAffine.finrank (pullback.snd g (S.affineOpenCover.f (S.affineOpenCover.idx z))) (Exists.choose ⋯) =
    IsAffine.finrank (pullback.snd g (S.affineOpenCover.f (S.affineOpenCover.idx z))) (Exists.choose ⋯)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : Flat f
inst✝ : IsFinite f
R : CommRingCat
i : Spec R ⟶ Y
w✝ : IsOpenImmersion i
y' : ↥(Spec R)
⊢ finrank (pullback.snd f (i ≫ g)) y' = finrank (pullback.snd f (i ≫ g)) y'

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝¹ : Flat f
inst✝ : IsFinite f
y : ↥Y
⊢ finrank f (g y) = finrank f (g y)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
x : ↥X
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X), (∃ R, Y = Spec R) → 1 ≤ finrank f (f x)
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : g y = f x
⊢ 1 ≤ finrank (pullback.snd f g) y

Tactic:
]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
x : ↥X
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X), (∃ R, Y = Spec R) → 1 ≤ finrank f (f x)
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : g y = f x
⊢ 1 ≤ finrank (pullback.snd f g) y
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
x : ↥X
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X), (∃ R, Y = Spec R) → 1 ≤ finrank f (f x)
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : g y = f x
z : ↥(pullback f g)
hzl : (pullback.fst f g) z = x
hzr : (pullback.snd f g) z = y
⊢ 1 ≤ finrank (pullback.snd f g) ((pullback.snd f g) z)

Tactic:
]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
x : ↥X
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X), (∃ R, Y = Spec R) → 1 ≤ finrank f (f x)
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : g y = f x
z : ↥(pullback f g)
hzl : (pullback.fst f g) z = x
hzr : (pullback.snd f g) z = y
⊢ 1 ≤ finrank (pullback.snd f g) ((pullback.snd f g) z)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
this :
  ∀ {X : Scheme} (x : ↥X) (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    (∃ S, X = Spec S) → 1 ≤ finrank f (f x)
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
heq : f x = (X.isoSpec.inv ≫ f) (X.isoSpec.hom x)
⊢ 1 ≤ finrank (X.isoSpec.inv ≫ f) ((X.isoSpec.inv ≫ f) (X.isoSpec.hom x))

Tactic:
]

Goal state after:
case inr
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
this :
  ∀ {X : Scheme} (x : ↥X) (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    (∃ S, X = Spec S) → 1 ≤ finrank f (f x)
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
heq : f x = (X.isoSpec.inv ≫ f) (X.isoSpec.hom x)
⊢ 1 ≤ finrank (X.isoSpec.inv ≫ f) ((X.isoSpec.inv ≫ f) (X.isoSpec.hom x))
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
⊢ 1 ≤ (CommRingCat.Hom.hom φ).finrank ((Spec.map φ) x)

Tactic:
]

Goal state after:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
⊢ 1 ≤ (CommRingCat.Hom.hom φ).finrank ((Spec.map φ) x)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ β ▷ r₃ ⊗≫
          (r₁ ≫ g₁) ◁ ((λ_ l₂).hom ≫ (ρ_ l₂).inv) ▷ (h₂ ≫ r₃) ⊗≫
            r₁ ◁ α ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ (g₁ ≫ g₂) ◁ adj₃.unit ⊗≫
        r₁ ◁ ((α_ g₁ g₂ l₃).hom ≫ g₁ ◁ β ≫ (α_ g₁ l₂ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ r₃ ⊗≫
          adj₁.counit ▷ (h₁ ≫ h₂) ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ β ▷ r₃ ⊗≫
          (r₁ ≫ g₁) ◁ ((λ_ l₂).hom ≫ (ρ_ l₂).inv) ▷ (h₂ ≫ r₃) ⊗≫
            r₁ ◁ α ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ (g₁ ≫ g₂) ◁ adj₃.unit ⊗≫
        r₁ ◁ ((α_ g₁ g₂ l₃).hom ≫ g₁ ◁ β ≫ (α_ g₁ l₂ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ r₃ ⊗≫
          adj₁.counit ▷ (h₁ ≫ h₂) ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ (Spec.map φ) x ∈ Set.range (PrimeSpectrum.comap (algebraMap ↑R ↑S))

Tactic:
]

Goal state after:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ (Spec.map φ) x ∈ Set.range (PrimeSpectrum.comap (algebraMap ↑R ↑S))
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case refine_1.inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], 1 ≤ finrank f → (∃ R, Y = Spec R) → Surjective f
hY : ¬∃ R, Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), Surjective (Cover.pullbackHom Y.affineCover f i)

Tactic:
]

Goal state after:
case refine_1.inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], 1 ≤ finrank f → (∃ R, Y = Spec R) → Surjective f
hY : ¬∃ R, Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), Surjective (Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case refine_1.inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], 1 ≤ finrank f → (∃ R, Y = Spec R) → Surjective f
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ 1 y ≤ finrank f ((Y.affineCover.f i) y)

Tactic:
]

Goal state after:
case refine_1.inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], 1 ≤ finrank f → (∃ R, Y = Spec R) → Surjective f
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ 1 y ≤ finrank f ((Y.affineCover.f i) y)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    1 ≤ finrank f → (∃ S, X = Spec S) → Surjective f
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
⊢ Surjective (X.isoSpec.inv ≫ f)

Tactic:
]

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    1 ≤ finrank f → (∃ S, X = Spec S) → Surjective f
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
⊢ Surjective (X.isoSpec.inv ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    1 ≤ finrank f → (∃ S, X = Spec S) → Surjective f
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
x : ↥(Spec R)
⊢ 1 x ≤ finrank f x

Tactic:
]

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    1 ≤ finrank f → (∃ S, X = Spec S) → Surjective f
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
x : ↥(Spec R)
⊢ 1 x ≤ finrank f x
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
x : ↥(Spec R)
h : 1 x ≤ (CommRingCat.Hom.hom φ).finrank x
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
⊢ ∃ a, (Spec.map φ) a = x

Tactic:
]

Goal state after:
R S : CommRingCat
φ : R ⟶ S
x : ↥(Spec R)
h : 1 x ≤ (CommRingCat.Hom.hom φ).finrank x
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
⊢ ∃ a, (Spec.map φ) a = x
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : IsFinite f
inst✝ : LocallyOfFinitePresentation f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f],
    (∃ R, Y = Spec R) → IsLocallyConstant (finrank f)
hY : ¬∃ R, Y = Spec R
⊢ ∀ (x : ↥Y), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f x

Tactic:
]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : IsFinite f
inst✝ : LocallyOfFinitePresentation f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f],
    (∃ R, Y = Spec R) → IsLocallyConstant (finrank f)
hY : ¬∃ R, Y = Spec R
⊢ ∀ (x : ↥Y), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f x