mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this✝⁵ : p.IsPrime
this✝⁴ : Module p.ResidueField (p.Fiber S) := leftModule
this✝³ : SMul p.ResidueField (p.Fiber S) := this✝⁴.toSMul
this✝² : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝¹ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this✝ : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
hsQ' : (algebraMap R Q.ResidueField) s ≠ 0
hrQ' : φ r = 1
e' : (algebraMap R Q.ResidueField) s * φ x = (algebraMap S Q.ResidueField) t
Q' : Ideal S
left✝ : Q'.IsPrime
right✝ : Q'.LiesOver (Ideal.under R Q)
H : Q' ≠ Q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver p Q'
⊢ s ∉ Ideal.under R Q'

Tactic:
rwa [← Q'.over_def p]

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
H : (aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R')) = (algebraMap S S').comp ↑φ
q : R[X][X]
hqm : q.Monic
hq : eval₂ φ.toRingHom t q = 0
⊢ eval₂ (aeval ((algebraMap S S') (φ X))).toRingHom ((algebraMap S S') t) (map (mapRingHom (algebraMap R R')) q) = 0

Tactic:
rw [eval₂_map, H, ← hom_eval₂, ← AlgHom.toRingHom_eq_coe, hq, map_zero]

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
this✝⁴ : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective ⇑f
hx : IsStronglyTranscendental R (f X)
hf : aeval (f X) = f
this✝³ : Algebra R[X] S := f.toAlgebra
this✝² : IsScalarTower R R[X] S
this✝¹ : Module.Finite R[X] S
this✝ : FaithfulSMul R[X] S
this : Ideal.map C (Ideal.under R P) < Ideal.under R[X] P
Q : Ideal S
hQ : Q < P
left✝ : Q.IsPrime
e : Ideal.map C (Ideal.under R P) = Ideal.under R[X] Q
⊢ Ideal.under R Q = Ideal.under R P

Tactic:
rw [← Ideal.under_under (B := R[X]), ← e]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
this✝⁴ : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective ⇑f
hx : IsStronglyTranscendental R (f X)
hf : aeval (f X) = f
this✝³ : Algebra R[X] S := f.toAlgebra
this✝² : IsScalarTower R R[X] S
this✝¹ : Module.Finite R[X] S
this✝ : FaithfulSMul R[X] S
this : Ideal.map C (Ideal.under R P) < Ideal.under R[X] P
Q : Ideal S
hQ : Q < P
left✝ : Q.IsPrime
e : Ideal.map C (Ideal.under R P) = Ideal.under R[X] Q
⊢ Ideal.under R (Ideal.map C (Ideal.under R P)) = Ideal.under R P
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
⊢ ↑((addLinearEquiv R m n).symm PQ) = ↑((addLinearEquiv R m n).symm ((PQ.1, 0).1, (PQ.1, 0).2 + (0, PQ.2).2))

Tactic:
zero_add

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
PQ : ↥R[X]_m × ↥R[X]_n
⊢ ↑((addLinearEquiv R m n).symm PQ) = ↑((addLinearEquiv R m n).symm ((PQ.1, 0).1, (0, PQ.2).2))
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
⊢ ∏ i, (LinearMap.toMatrix (degreeLT.basis R n) (degreeLT.basis R n)) (↑(taylorLinearEquiv r n)) i i = 1

pp: R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
⊢ ((LinearMap.toMatrix (degreeLT.basis R n) (degreeLT.basis R n)) ↑(taylorLinearEquiv r n)).IsUpperTriangular

Tactic:
Fintype.prod_eq_one

Goal state after:
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
⊢ 1 = 1

case h
R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
⊢ ∀ (a : Fin n), (LinearMap.toMatrix (degreeLT.basis R n) (degreeLT.basis R n)) (↑(taylorLinearEquiv r n)) a a = 1

R : Type u_1
inst✝ : CommRing R
r : R
n : ℕ
a✝ : Nontrivial R
⊢ ((LinearMap.toMatrix (degreeLT.basis R n) (degreeLT.basis R n)) ↑(taylorLinearEquiv r n)).IsUpperTriangular
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case left
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f g : R[X]
m n : ℕ
φ : R →+* S
i : Fin (m + n)
i✝ : Fin m
⊢ (map φ f).sylvester (map φ g) m n i (Fin.castAdd n i✝) = φ.mapMatrix (f.sylvester g m n) i (Fin.castAdd n i✝)

Tactic:
simp [sylvester, apply_ite φ]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case right
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f g : R[X]
m n : ℕ
φ : R →+* S
i : Fin (m + n)
i✝ : Fin n
⊢ (map φ f).sylvester (map φ g) m n i (Fin.natAdd m i✝) = φ.mapMatrix (f.sylvester g m n) i (Fin.natAdd m i✝)

Tactic:
simp [sylvester, apply_ite φ]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
e : ↑(fromNormalization f ⁻¹ᵁ ↑U) ≅ (normalizationOpenCover f).X U :=
  IsOpenImmersion.isoOfRangeEq (fromNormalization f ⁻¹ᵁ ↑U).ι ((normalizationOpenCover f).f U) ⋯
⊢ IsIntegralHom (e.inv ≫ fromNormalization f ∣_ ↑U)

Tactic:
← MorphismProperty.cancel_right_of_respectsIso @IsIntegralHom _ U.2.isoSpec.hom

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : ↑Y.affineOpens
e : ↑(fromNormalization f ⁻¹ᵁ ↑U) ≅ (normalizationOpenCover f).X U :=
  IsOpenImmersion.isoOfRangeEq (fromNormalization f ⁻¹ᵁ ↑U).ι ((normalizationOpenCover f).f U) ⋯
⊢ IsIntegralHom ((e.inv ≫ fromNormalization f ∣_ ↑U) ≫ (IsAffineOpen.isoSpec ⋯).hom)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case succ.e_a.e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ (if m ≤ m + 1 + n ∧ m + 1 + n ≤ m + (n + 1) then g.coeff (m + 1 + n - m) else 0) = g.coeff (n + 1)

Tactic:
rw [if_pos (by lia)]

Goal state after:
case succ.e_a.e_a
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m : ℕ
hf : f.natDegree ≤ m
n : ℕ
⊢ g.coeff (m + 1 + n - m) = g.coeff (n + 1)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
m n : ℕ
r : R
⊢ f.resultant (C r) m (0 + n) = f.coeff m ^ (0 + n) * r ^ m

Tactic:
resultant_add_right_deg _ _ _ _ _ (by simp)

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
m n : ℕ
r : R
⊢ f.coeff m ^ n * f.resultant (C r) m 0 = f.coeff m ^ (0 + n) * r ^ m
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FiniteType R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
this✝ : Small.{u, v} S
this : ZariskisMainProperty R (Ideal.comap (Shrink.algEquiv R S).toRingEquiv.toRingHom p)
⊢ ZariskisMainProperty R p

Tactic:
rw [zariskisMainProperty_iff'] at this ⊢

Goal state after:
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FiniteType R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
this✝ : Small.{u, v} S
this :
  ∃ r ∉ Ideal.comap (Shrink.algEquiv R S).toRingEquiv.toRingHom p,
    ∀ (x : Shrink.{u, v} S), ∃ m, IsIntegral R (r ^ m * x)
⊢ ∃ r ∉ p, ∀ (x : S), ∃ m, IsIntegral R (r ^ m * x)
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
⊢ ∀ ⦃X_1 Y_1 : (directedCover Y).I₀⦄ (f_1 : X_1 ⟶ Y_1),
    (normalizationGlueData f).functor.map f_1 ≫
        Spec.map
            (CommRingCat.ofHom
              ((CommRingCat.Hom.hom
                    (appLE f₁ (f₂ ⁻¹ᵁ ↑Y_1) (f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op Y_1)))
                      ⋯)).codRestrict
                (integralClosure ↑Γ(Y, Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op Y_1)))
                  ↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op Y_1))))
                ⋯)) ≫
          ⋯.fromSpec =
      (Spec.map
            (CommRingCat.ofHom
              ((CommRingCat.Hom.hom
                    (appLE f₁ (f₂ ⁻¹ᵁ ↑X_1) (f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op X_1)))
                      ⋯)).codRestrict
                (integralClosure ↑Γ(Y, Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op X_1)))
                  ↑Γ(X, f ⁻¹ᵁ Opposite.unop ((toOpensFunctor Y).op.obj (Opposite.op X_1))))
                ⋯)) ≫
          ⋯.fromSpec) ≫
        ((Functor.const (directedCover Y).I₀).obj T).map f_1

Tactic:
· intros U V i
    dsimp [normalizationGlueData, relativeGluingData]
    rw [Category.comp_id, ← Spec.map_comp_assoc, ← (V.2.preimage f₂).map_fromSpec (U.2.preimage f₂)
      (homOfLE (f₂.preimage_mono (Scheme.AffineZariskiSite.toOpens_mono i.le))).op,
      ← Spec.map_comp_assoc]
    congr 2
    ext i
    apply Subtype.ext
    dsimp [normalizationDiagram]
    simp only [← CommRingCat.comp_apply, appLE_map, map_appLE]

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FiniteType R S
p : Ideal S
inst✝ : p.IsPrime
H✝ : ZariskisMainProperty R p
S' : Subalgebra R S
hS' : (Subalgebra.toSubmodule S').FG
r : ↥S'
hrp : ↑r ∉ p
H : Function.Bijective ⇑(Localization.awayMap S'.val.toRingHom r)
this✝¹ : Module.Finite R ↥S'
this✝ : QuasiFinite R (Localization.Away r)
this : QuasiFinite R (Localization.Away ↑r)
f : Localization.Away ↑r →ₐ[S] Localization.AtPrime p := IsLocalization.Away.liftAlgHom ↑r ⋯
x s : S
hs : s ∈ p.primeCompl
⊢ ∃ s_1,
    IsUnit ((AlgHom.restrictScalars R f) s_1) ∧
      IsLocalization.mk' (Localization.AtPrime p) x ⟨s, hs⟩ * (AlgHom.restrictScalars R f) s_1 ∈
        (AlgHom.restrictScalars R f).range

Tactic:
exact ⟨algebraMap _ _ s, by simpa using IsLocalization.map_units _ ⟨s, hs⟩,
    algebraMap _ _ x, by simp⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case e_a
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
i : ↑Γ(Y, ↑U)
⊢ (CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ ↑U) (f ⁻¹ᵁ toOpens U) ⋯))
      ((CommRingCat.Hom.hom (appLE f₂ (↑U) (f₂ ⁻¹ᵁ ↑U) ⋯)) i) =
    (CommRingCat.Hom.hom (app f (toOpens U))) i

Tactic:
rw [← CommRingCat.comp_apply, Hom.appLE_comp_appLE, app_eq_appLE]

Goal state after:
case e_a
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
i : ↑Γ(Y, ↑U)
⊢ (ConcreteCategory.hom (appLE (f₁ ≫ f₂) (↑U) (f ⁻¹ᵁ toOpens U) ⋯)) i =
    (CommRingCat.Hom.hom (appLE f (toOpens U) (f ⁻¹ᵁ toOpens U) ⋯)) i
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
n : ℕ
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg : natDegree 0 ≤ n
hf' : f.natDegree = 0
⊢ f.resultant 0 f.natDegree n = (Multiset.map (fun x ↦ eval x 0) f.roots).prod

Tactic:
obtain ⟨r, rfl⟩ := hfm.natDegree_eq_zero.mp hf'; simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂

Tactic:
obtain ⟨g₁', hg₁, e₁⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g₁)

Goal state after:
case surjective
R✝ : Type u_1
inst✝² : CommRing R✝
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
φ : R →+* S
hφ : Function.Surjective ⇑φ
f : S[X]
IH :
  ∀ (q g₁ g₂ : R[X]), q.resultant (g₁ * g₂) q.natDegree (g₁.natDegree + g₂.natDegree) = q.resultant g₁ * q.resultant g₂
g₁ g₂ : S[X]
f' : R[X]
hf' : map φ f' = f
e : f'.degree = f.degree
g₁' : R[X]
hg₁ : map φ g₁' = g₁
e₁ : g₁'.degree = g₁.degree
⊢ f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree) = f.resultant g₁ * f.resultant g₂
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
⊢ toNormalization (pullback.snd f g) ≫ normalizationPullback f g ≫ pullback.fst (fromNormalization f) g =
    pullback.fst f g ≫ toNormalization f

Tactic:
by
  simp [normalizationPullback]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: ⊢ CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ FinitePresentation) fun {R S} [CommRing R] [CommRing S] ↦
    FaithfullyFlat

Tactic:
refine .mk _ finitePresentation_respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_
  rw [finitePresentation_algebraMap] at h' ⊢
  rw [faithfullyFlat_algebraMap_iff] at h
  exact .of_finitePresentation_tensorProduct_of_faithfullyFlat S

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : StrictlyUnitaryLaxFunctor B C
x : B
⊢ F.mapId x ≫ eqToHom ⋯ = 𝟙 (𝟙 (F.obj x))

Tactic:
by simp [F.mapId_eq_eqToHom]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : StrictlyUnitaryLaxFunctor B C
x : B
⊢ eqToHom ⋯ ≫ F.mapId x = 𝟙 (F.map (𝟙 x))

Tactic:
by simp [F.mapId_eq_eqToHom]

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₁ ◁ (adj₂.unit ▷ (g₂ ≫ 𝟙 e) ≫ (l₂ ≫ r₂) ◁ g₂ ◁ adj₃.unit) ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ l₃) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ β) ▷ r₃ ⊗≫
          (adj₁.counit ▷ h₁ ▷ (r₂ ≫ l₂) ≫ (𝟙 b ≫ h₁) ◁ adj₂.counit) ▷ 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:
rw [← whisker_exchange, ← whisker_exchange, ← whisker_exchange]
      bicategory

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 snd y = finrank f (g y)

Tactic:
by
  rw [← h.isoPullback_hom_snd, finrank_comp_left_of_isIso, finrank_pullback_snd]

Goal state after:
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
l : LTSeries ↑(PrimeSpectrum.zeroLocus ↑(Ideal.span {r}))
p : Ideal R
hp : p ∈ ⊥.minimalPrimes
hp'✝ : p ≤ (↑(RelSeries.head l)).asIdeal
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
hp' : p' < ↑(RelSeries.head l)
⊢ ↑l.length + 1 ≤ ⨆ p, ↑p.length

Tactic:
refine le_trans ?_ (le_iSup _ ((l.map Subtype.val (fun _ _ ↦ id)).cons p' hp'))

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
l : LTSeries ↑(PrimeSpectrum.zeroLocus ↑(Ideal.span {r}))
p : Ideal R
hp : p ∈ ⊥.minimalPrimes
hp'✝ : p ≤ (↑(RelSeries.head l)).asIdeal
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
hp' : p' < ↑(RelSeries.head l)
⊢ ↑l.length + 1 ≤ ↑(RelSeries.cons (l.map Subtype.val ⋯) p' hp').length
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : KrullDimLE 1 R
x : R
hx : x ∈ nonZeroDivisors R
⊢ Order.krullDim (PrimeSpectrum (R ⧸ span {x})) + 1 ≤ 0 + 1

Tactic:
zero_add

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : KrullDimLE 1 R
x : R
hx : x ∈ nonZeroDivisors R
⊢ Order.krullDim (PrimeSpectrum (R ⧸ span {x})) + 1 ≤ 1
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
⊢ U = ⊤

Tactic:
by
  obtain ⟨s, hs⟩ := (PrimeSpectrum.isOpen_iff _).mp U.2
  obtain ⟨t, hts, ht, ht'⟩ : ∃ t ⊆ s, t.Finite ∧ V ⊆ ⋃ i ∈ t, (basicOpen i).1 := by
    obtain ⟨t, ht⟩ := hV'.elim_finite_subcover
      (fun i : s ↦ (basicOpen i.1).1) (fun _ ↦ (basicOpen _).2)
      (by simpa [← Set.compl_iInter, ← zeroLocus_iUnion₂ (κ := (· ∈ s)), ← hs])
    exact ⟨t.map (Function.Embedding.subtype _), by simp, Finset.finite_toSet _, by simpa using ht⟩
  replace ht' : V ⊆ (zeroLocus t)ᶜ := by
    simpa [← Set.compl_iInter, ← zeroLocus_iUnion₂ (κ := (· ∈ t))] using ht'
  have (i : _) : Ideal.span (Pi.evalRingHom (R ·) i '' t) = ⊤ := by
    rw [← zeroLocus_empty_iff_eq_top, zeroLocus_span, ← preimage_comap_zeroLocus,
      ← Set.compl_univ_iff, ← Set.preimage_compl, Set.preimage_eq_univ_iff]
    trans (Sigma.ι _ i ≫ sigmaSpec R).opensRange.1
    · simp; rfl
    · rw [Scheme.Hom.opensRange_comp]
      exact (Set.image_subset_range _ _).trans (hV.trans ht')
  have : Ideal.span s = ⊤ := top_le_iff.mp
    ((Ideal.span_eq_top_of_span_image_evalRingHom _ ht this).ge.trans (Ideal.span_mono hts))
  simpa [← zeroLocus_span s, zeroLocus_empty_iff_eq_top.mpr this] using hs

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
g : (j₀ : 𝒰.I₀) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.X j₀
hg :
  ∀ (j₀ : 𝒰.I₀) (x : { i // j i = j₀ }),
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ ↑(R ↑x)) x)) ≫ g j₀ = IsOpenImmersion.lift (𝒰.f j₀) (f ↑x) ⋯
R' : 𝒰.I₀ → CommRingCat := fun j₀ ↦ CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))
e : ((i : ι) → ↑(R i)) ≃+* ((j₀ : 𝒰.I₀) → ↑(R' j₀)) :=
  { toFun := fun f x i ↦ f ↑i, invFun := fun f i ↦ f (j i) ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯ }
i : ι
⊢ pointsPi R X (Spec.map (CommRingCat.ofHom e.symm.toRingHom) ≫ inv (sigmaSpec R') ≫ Sigma.desc fun j₀ ↦ g j₀ ≫ 𝒰.f j₀)
      i =
    f i

Tactic:
have : (Pi.evalRingHom (R ·) i).comp e.symm.toRingHom =
    (Pi.evalRingHom _ ⟨i, rfl⟩).comp (Pi.evalRingHom (R' ·) (j i)) := rfl

Goal state after:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
g : (j₀ : 𝒰.I₀) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.X j₀
hg :
  ∀ (j₀ : 𝒰.I₀) (x : { i // j i = j₀ }),
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ ↑(R ↑x)) x)) ≫ g j₀ = IsOpenImmersion.lift (𝒰.f j₀) (f ↑x) ⋯
R' : 𝒰.I₀ → CommRingCat := fun j₀ ↦ CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))
e : ((i : ι) → ↑(R i)) ≃+* ((j₀ : 𝒰.I₀) → ↑(R' j₀)) :=
  { toFun := fun f x i ↦ f ↑i, invFun := fun f i ↦ f (j i) ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯ }
i : ι
this :
  (Pi.evalRingHom (fun x ↦ ↑(R x)) i).comp e.symm.toRingHom =
    (Pi.evalRingHom (fun i_1 ↦ ↑(R ↑i_1)) ⟨i, ⋯⟩).comp (Pi.evalRingHom (fun x ↦ ↑(R' x)) (j i))
⊢ pointsPi R X (Spec.map (CommRingCat.ofHom e.symm.toRingHom) ≫ inv (sigmaSpec R') ≫ Sigma.desc fun j₀ ↦ g j₀ ≫ 𝒰.f j₀)
      i =
    f i
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ (⨅ x ∈ t, x.asHomogeneousIdeal).toIdeal ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}

Tactic:
HomogeneousIdeal.toIdeal_iInf,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ ⨅ i, (⨅ (_ : i ∈ t), i.asHomogeneousIdeal).toIdeal ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
x : ProjectiveSpectrum 𝒜
⊢ f ∈ (⨅ (_ : x ∈ t), x.asHomogeneousIdeal).toIdeal ↔ x ∈ t → f ∈ x.asHomogeneousIdeal

Tactic:
HomogeneousIdeal.toIdeal_iInf,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
x : ProjectiveSpectrum 𝒜
⊢ f ∈ ⨅ (_ : x ∈ t), x.asHomogeneousIdeal.toIdeal ↔ x ∈ t → f ∈ x.asHomogeneousIdeal
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : f ∈ (vanishingIdeal t).toIdeal
g : A
hg : g ∈ (vanishingIdeal t').toIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asHomogeneousIdeal

Tactic:
HomogeneousIdeal.mem_iff,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : f ∈ vanishingIdeal t
g : A
hg : g ∈ vanishingIdeal t'
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asHomogeneousIdeal