mathlib-initiative/mathlib-tactics huggingface dataset:
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
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
x : ↥(Spec R)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f],
    (∃ R, Y = Spec R) → ∀ (x : ↥Y), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f x
U : Set ↥(Spec R)
hU : IsOpen U
hxU : x ∈ U
H : ∀ x' ∈ U, finrank (pullback.snd f g) x' = finrank (pullback.snd f g) x
y' : ↥(Spec R)
hyU : y' ∈ U
⊢ finrank (pullback.snd f g) y' = finrank (pullback.snd f g) x

Tactic:
]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : IsFinite f
inst✝ : LocallyOfFinitePresentation f
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
x : ↥(Spec R)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f],
    (∃ R, Y = Spec R) → ∀ (x : ↥Y), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f x
U : Set ↥(Spec R)
hU : IsOpen U
hxU : x ∈ U
H : ∀ x' ∈ U, finrank (pullback.snd f g) x' = finrank (pullback.snd f g) x
y' : ↥(Spec R)
hyU : y' ∈ U
⊢ finrank (pullback.snd f g) y' = finrank (pullback.snd f g) x
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
inst✝ : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f],
    (∃ S, X = Spec S) → IsLocallyConstant (finrank f)
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
⊢ IsLocallyConstant (finrank (X.isoSpec.inv ≫ f))

Tactic:
]

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

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
inst✝² : (CommRingCat.Hom.hom φ).Flat
inst✝¹ : (CommRingCat.Hom.hom φ).Finite
inst✝ : (CommRingCat.Hom.hom φ).FinitePresentation
⊢ IsLocallyConstant (CommRingCat.Hom.hom φ).finrank

Tactic:
]

Goal state after:
R S : CommRingCat
φ : R ⟶ S
inst✝² : (CommRingCat.Hom.hom φ).Flat
inst✝¹ : (CommRingCat.Hom.hom φ).Finite
inst✝ : (CommRingCat.Hom.hom φ).FinitePresentation
⊢ IsLocallyConstant (CommRingCat.Hom.hom φ).finrank
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial ↑R
⊢ Module.rankAtStalk (↑R) y = 1

pp: case hf₁
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial ↑R
⊢ (CommRingCat.Hom.hom (𝟙 R)).Finite

pp: case hf₂
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial ↑R
⊢ (CommRingCat.Hom.hom (𝟙 R)).Flat

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial ↑R
⊢ Module.rankAtStalk (↑R) y = 1

case hf₁
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial ↑R
⊢ (CommRingCat.Hom.hom (𝟙 R)).Finite

case hf₂
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial ↑R
⊢ (CommRingCat.Hom.hom (𝟙 R)).Flat
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
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 : finrank f = 1
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f], finrank f = 1 → (∃ S, X = Spec S) → IsIso f
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
⊢ IsIso (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 : finrank f = 1
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f], finrank f = 1 → (∃ S, X = Spec S) → IsIso f
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
⊢ IsIso (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 : finrank f = 1
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f], finrank f = 1 → (∃ S, X = Spec S) → IsIso f
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
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
⊢ Function.Bijective ⇑(ConcreteCategory.hom φ)

Tactic:
]

Goal state after:
R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
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
⊢ Function.Bijective ⇑(ConcreteCategory.hom φ)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
h : (CommRingCat.Hom.hom φ).finrank = 1
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
⊢ Module.rankAtStalk ↑S = 1

Tactic:
]

Goal state after:
R S : CommRingCat
φ : R ⟶ S
h : (CommRingCat.Hom.hom φ).finrank = 1
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
⊢ Module.rankAtStalk ↑S = 1
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), Smooth (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), Smooth (Scheme.Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: case inr.sq
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ IsPullback ?inr.f' (Scheme.Hom.fiberToSpecResidueField (pullback.snd f (Y.affineCover.f i)) y) ?g ?inr.f

Tactic:
exact isPullback_fiberToSpecResidueField_of_isPullback (IsPullback.of_hasPullback _ _) _

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

Goal state before:
pp: case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X : Scheme} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ S, X = Spec S) → Smooth f
h : ¬∃ S, X = Spec S
⊢ ∀ (i : X.affineCover.I₀), Smooth (X.affineCover.f i ≫ f)

Tactic:
]

Goal state after:
case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X : Scheme} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ S, X = Spec S) → Smooth f
h : ¬∃ S, X = Spec S
⊢ ∀ (i : X.affineCover.I₀), Smooth (X.affineCover.f i ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X : Scheme} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ S, X = Spec S) → Smooth f
h : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x✝ : ∀ (y : ↥(Spec R)), Smooth (pullback.snd f ((Spec R).fromSpecResidueField y))
y : ↥(Spec R)
⊢ Smooth
    ((pullbackRightPullbackFstIso f ((Spec R).fromSpecResidueField y) (X.affineCover.f i)).inv ≫
      pullback.snd (X.affineCover.f i) (pullback.fst f ((Spec R).fromSpecResidueField y)) ≫
        pullback.snd f ((Spec R).fromSpecResidueField y))

Tactic:
]

Goal state after:
case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X : Scheme} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ S, X = Spec S) → Smooth f
h : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x✝ : ∀ (y : ↥(Spec R)), Smooth (pullback.snd f ((Spec R).fromSpecResidueField y))
y : ↥(Spec R)
⊢ Smooth
    ((pullbackRightPullbackFstIso f ((Spec R).fromSpecResidueField y) (X.affineCover.f i)).inv ≫
      pullback.snd (X.affineCover.f i) (pullback.fst f ((Spec R).fromSpecResidueField y)) ≫
        pullback.snd f ((Spec R).fromSpecResidueField y))
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst✝¹ : (CommRingCat.Hom.hom φ).FinitePresentation
inst✝ : (CommRingCat.Hom.hom φ).Flat
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Algebra.FinitePresentation ↑R ↑S
algebraizeInst✝ : Module.Flat ↑R ↑S
p : Ideal ↑R
hp : p.IsPrime
⊢ (algebraMap p.ResidueField (p.Fiber ↑S)).FormallySmooth

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst✝¹ : (CommRingCat.Hom.hom φ).FinitePresentation
inst✝ : (CommRingCat.Hom.hom φ).Flat
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Algebra.FinitePresentation ↑R ↑S
algebraizeInst✝ : Module.Flat ↑R ↑S
p : Ideal ↑R
hp : p.IsPrime
⊢ (algebraMap p.ResidueField (p.Fiber ↑S)).FormallySmooth
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst✝¹ : (CommRingCat.Hom.hom φ).FinitePresentation
inst✝ : (CommRingCat.Hom.hom φ).Flat
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Algebra.FinitePresentation ↑R ↑S
algebraizeInst✝ : Module.Flat ↑R ↑S
p : Ideal ↑R
hp : p.IsPrime
⊢ Smooth
    (Scheme.Hom.fiberToSpecResidueField (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S)))
      { asIdeal := p, isPrime := hp })

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst✝¹ : (CommRingCat.Hom.hom φ).FinitePresentation
inst✝ : (CommRingCat.Hom.hom φ).Flat
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Algebra.FinitePresentation ↑R ↑S
algebraizeInst✝ : Module.Flat ↑R ↑S
p : Ideal ↑R
hp : p.IsPrime
⊢ Smooth
    (Scheme.Hom.fiberToSpecResidueField (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S)))
      { asIdeal := p, isPrime := hp })
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).RespectsIso

Tactic:
]

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).RespectsIso
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).IsMultiplicative

Tactic:
]

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).IsMultiplicative
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).IsStableUnderBaseChange

Tactic:
]

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).IsStableUnderBaseChange
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtSource (@Flat ⊓ MorphismProperty.diagonal @Flat)

Tactic:
]

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtSource (@Flat ⊓ MorphismProperty.diagonal @Flat)
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget (@Flat ⊓ MorphismProperty.diagonal @Flat)

Tactic:
]

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget (@Flat ⊓ MorphismProperty.diagonal @Flat)
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ @WeaklyEtale ≤ MorphismProperty.diagonal @WeaklyEtale

Tactic:
]

Goal state after:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ @WeaklyEtale ≤ MorphismProperty.diagonal @WeaklyEtale
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ Order.krullDim ↑(PrimeSpectrum.zeroLocus ↑I) = Order.krullDim ↑(PrimeSpectrum.zeroLocus ↑I)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ringKrullDim (R ⧸ I) = Order.krullDim ↑(PrimeSpectrum.zeroLocus ↑I)

Tactic:
by
  rw [ringKrullDim, Order.krullDim_eq_of_orderIso I.primeSpectrumQuotientOrderIsoZeroLocus]

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : Ideal.span {r} = ⊤
⊢ ⊥ + 1 ≤ ringKrullDim R

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : Ideal.span {r} = ⊤
⊢ ⊥ + 1 ≤ ringKrullDim R
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
⊢ ¬Ideal.span {r} = ⊤

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
⊢ ¬Ideal.span {r} = ⊤
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
this✝¹ : Nonempty ↑(PrimeSpectrum.zeroLocus ↑(Ideal.span {r}))
this✝ : Nontrivial (R ⧸ Ideal.span {r})
this : Nontrivial R
⊢ ∀ (i : LTSeries ↑(PrimeSpectrum.zeroLocus ↑(Ideal.span {r}))), ↑i.length + 1 ≤ ⨆ p, ↑p.length

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
this✝¹ : Nonempty ↑(PrimeSpectrum.zeroLocus ↑(Ideal.span {r}))
this✝ : Nontrivial (R ⧸ Ideal.span {r})
this : Nontrivial R
⊢ ∀ (i : LTSeries ↑(PrimeSpectrum.zeroLocus ↑(Ideal.span {r}))), ↑i.length + 1 ≤ ⨆ p, ↑p.length
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case e'_3
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
inst✝ : Finite σ
α✝ β✝ : Type u_3
e : α✝ ≃ β✝
H : ringKrullDim R + ↑(Nat.card α✝) ≤ ringKrullDim (MvPolynomial α✝ R)
⊢ ringKrullDim R + ↑(Nat.card β✝) = ringKrullDim R + ↑(Nat.card β✝)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case h_option
R : Type u_1
inst✝² : CommRing R
σ : Type u_3
inst✝¹ : Finite σ
α✝ : Type u_3
inst✝ : Fintype α✝
IH : ringKrullDim R + ↑(Fintype.card α✝) ≤ ringKrullDim (MvPolynomial α✝ R)
⊢ ringKrullDim (Polynomial (MvPolynomial α✝ R)) ≤ ringKrullDim (MvPolynomial (Option α✝) R)

Tactic:
]

Goal state after:
case h_option
R : Type u_1
inst✝² : CommRing R
σ : Type u_3
inst✝¹ : Finite σ
α✝ : Type u_3
inst✝ : Fintype α✝
IH : ringKrullDim R + ↑(Fintype.card α✝) ≤ ringKrullDim (MvPolynomial α✝ R)
⊢ ringKrullDim (Polynomial (MvPolynomial α✝ R)) ≤ ringKrullDim (MvPolynomial (Option α✝) R)
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Finite σ
⊢ ringKrullDim R + ↑↑(Nat.card σ) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
]

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Finite σ
⊢ ringKrullDim R + ↑↑(Nat.card σ) ≤ ringKrullDim (MvPolynomial σ R)
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
⊢ ∀ (m : ℕ), ↑m ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
]

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
⊢ ∀ (m : ℕ), ↑m ≤ ringKrullDim (MvPolynomial σ R)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
this : Submodule.map ((mul R R) a) I = a • I
⊢ ⊥ = ⊥

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 ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ (α ▷ 𝟙 e ≫ (l₁ ≫ h) ◁ adj₄.unit) ▷ r₂ ⊗≫
          r₃ ◁ (adj₁.counit ▷ (h ≫ l₄) ≫ 𝟙 b ◁ β) ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
hb : b ∈ nonZeroDivisors R
this✝ : Module.length R (R ⧸ b • span {a}) = Module.length R (R ⧸ span {a}) + Module.length R (R ⧸ span {b})
lem : b • span {a} = span {b * a}
this : {b} • span {a} = b • span {a}
⊢ Module.length R (R ⧸ span {a * b}) = Module.length R (R ⧸ b • span {a})

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
hb : b ∈ nonZeroDivisors R
this✝ : Module.length R (R ⧸ b • span {a}) = Module.length R (R ⧸ span {a}) + Module.length R (R ⧸ span {b})
lem : b • span {a} = span {b * a}
this : {b} • span {a} = b • span {a}
⊢ Module.length R (R ⧸ span {a * b}) = Module.length R (R ⧸ b • span {a})
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
hb : b ∈ nonZeroDivisors R
this✝ : Module.length R (R ⧸ b • span {a}) = Module.length R (R ⧸ span {a}) + Module.length R (R ⧸ span {b})
lem : b • span {a} = span {b * a}
this : {b} • span {a} = b • span {a}
⊢ Module.length R (R ⧸ span {b * a}) = Module.length R (R ⧸ span {b * a})

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
ha : a ∈ nonZeroDivisors R
⊢ ord R a + ord R b = ord R a + ord R b

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
n : ℕ
ih : ord R (x ^ n) = n • ord R x
⊢ n • ord R x + ord R x = n • ord R x + ord R x

pp: case succ.hb
R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
n : ℕ
ih : ord R (x ^ n) = n • ord R x
⊢ x ∈ nonZeroDivisors R

Tactic:
]

Goal state after:
case succ.hb
R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
n : ℕ
ih : ord R (x ^ n) = n • ord R x
⊢ x ∈ nonZeroDivisors R
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
h : IsUnit a
x : R
⊢ Module.length R (R ⧸ span {x}) = Module.length R (R ⧸ span {x})

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra S R
a : S
h : IsUnit a
x : R
⊢ ord R ((algebraMap S R) a * x) = ord R x

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra S R
a : S
h : IsUnit a
x : R
⊢ ord R ((algebraMap S R) a * x) = ord R x
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a x : R
⊢ x ∣ a * x

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a x : R
⊢ x ∣ a * x