mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: case pos
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝³ : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝² : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝¹ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this✝ : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
hp' : 1 ≤ p.natDegree
e : t ^ m • eval₂ (algebraMap R S) (t ^ n • r) p = 0
this :
  eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) =
    (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p
⊢ (t ^ m) ^ (p.natDegree - 1) • 0 = 0

Tactic:
smul_zero

Goal state after:
case pos
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝³ : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝² : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝¹ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this✝ : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
hp' : 1 ≤ p.natDegree
e : t ^ m • eval₂ (algebraMap R S) (t ^ n • r) p = 0
this :
  eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) =
    (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p
⊢ 0 = 0
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
this :
  ∀ (r : ↑Γ(Y, ⊤)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
      (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen ↑r).ι ≅ Spec Γ(X, X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) ↑r)) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen ↑r) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ (pullbackRestrictIsoRestrict f (Y.basicOpen ↑r)).hom ≫
      (X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯ ≫ f ∣_ Y.basicOpen ↑r ≫ (Y.basicOpen ↑r).toSpecΓ =
    pullback.snd f (Y.basicOpen ↑r).ι ≫ (Y.basicOpen ↑r).toSpecΓ

Tactic:
← Category.assoc

Goal state after:
case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
this :
  ∀ (r : ↑Γ(Y, ⊤)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
      (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen ↑r).ι ≅ Spec Γ(X, X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) ↑r)) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen ↑r) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ ((((pullbackRestrictIsoRestrict f (Y.basicOpen ↑r)).hom ≫ (X.isoOfEq ⋯).hom) ≫ X.homOfLE ⋯) ≫ f ∣_ Y.basicOpen ↑r) ≫
      (Y.basicOpen ↑r).toSpecΓ =
    pullback.snd f (Y.basicOpen ↑r).ι ≫ (Y.basicOpen ↑r).toSpecΓ
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hX
n : Type u
S : Scheme
inst✝ : IsAffine S
i : n
⊢ (CommRingCat.Hom.hom
        (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)) ≫
          Scheme.Hom.app
            (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
              (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
            ⊤))
      (X i) =
    (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) (X i)

Tactic:
rw [CommRingCat.comp_apply, ConcreteCategory.hom_ofHom, coe_eval₂Hom]

Goal state after:
case hX
n : Type u
S : Scheme
inst✝ : IsAffine S
i : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.app
          (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
            (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
          ⊤))
      (eval₂ (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S) (X i)) =
    (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) (X i)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hX
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ ∀ (i : n),
    (CommRingCat.Hom.hom
          (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)) ≫
            Scheme.Hom.app
              (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
                (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
              ⊤))
        (X i) =
      (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) (X i)

Tactic:
· intro i
          rw [CommRingCat.comp_apply, ConcreteCategory.hom_ofHom, coe_eval₂Hom]
          simp only [eval₂_X]
          exact homOfVector_appTop_coord _ _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom
        ((mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv ≫
          (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv))
      (X i) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i)

Tactic:
CommRingCat.comp_apply

Goal state after:
n : Type u
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv)
      ((ConcreteCategory.hom (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv)
        (X i)) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i)
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
pf✝¹ : IsLocalRing ↑(CommRingCat.of K)
h : IsClosed {↑p (IsLocalRing.closedPoint K)}
pf✝ : IsLocalHom (CommRingCat.Hom.hom (Scheme.stalkClosedPointTo ↑p))
⊢ 𝟙 (CommRingCat.of K) =
    (residueFieldIsoBase f (↑p (IsLocalRing.closedPoint K)) h).inv ≫
      Scheme.descResidueField (Scheme.stalkClosedPointTo ↑p)

Tactic:
← Spec.map_injective.eq_iff

Goal state after:
X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
pf✝¹ : IsLocalRing ↑(CommRingCat.of K)
h : IsClosed {↑p (IsLocalRing.closedPoint K)}
pf✝ : IsLocalHom (CommRingCat.Hom.hom (Scheme.stalkClosedPointTo ↑p))
⊢ Spec.map (𝟙 (CommRingCat.of K)) =
    Spec.map
      ((residueFieldIsoBase f (↑p (IsLocalRing.closedPoint K)) h).inv ≫
        Scheme.descResidueField (Scheme.stalkClosedPointTo ↑p))
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
s : Finset ↑R
hs : Ideal.span ↑s = J
hs' : ↑s ⊆ ↑J
x y : ↑R
e : y * x = 0
hy : y ∉ I
⊢ x ∈ (↑R ∙ ↑(∏ x ∈ s.attach, f ↑x ⋯)).annihilator

Tactic:
refine SetLike.le_def.mp ?_ ((hJ x).mpr ⟨⟨y, hy⟩, e⟩)

Goal state after:
X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
s : Finset ↑R
hs : Ideal.span ↑s = J
hs' : ↑s ⊆ ↑J
x y : ↑R
e : y * x = 0
hy : y ∉ I
⊢ J ≤ (↑R ∙ ↑(∏ x ∈ s.attach, f ↑x ⋯)).annihilator
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f g : X.PartialMap Y
W₁ W₂ : X.Opens
hW₁ : Dense ↑W₁
hW₂ : Dense ↑W₂
hW₁' : W₁ ≤ f.domain
hW₂' : W₂ ≤ g.domain
H : f.restrict W₁ hW₁ hW₁' = g.restrict W₂ hW₂ hW₂'
⊢ f.equiv g

Tactic:
have e : W₁ = W₂ := congr($(H).domain)

Goal state after:
X Y : Scheme
f g : X.PartialMap Y
W₁ W₂ : X.Opens
hW₁ : Dense ↑W₁
hW₂ : Dense ↑W₂
hW₁' : W₁ ≤ f.domain
hW₂' : W₂ ≤ g.domain
H : f.restrict W₁ hW₁ hW₁' = g.restrict W₂ hW₂ hW₂'
e : W₁ = W₂
⊢ f.equiv g
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
⊢ (X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯ ≫ (X.isoOfEq ⋯).inv ≫ (g x).hom =
    (X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯ ≫ (X.isoOfEq ⋯).inv ≫ (g y).hom

Tactic:
← Category.assoc

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
⊢ (((X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯) ≫ (X.isoOfEq ⋯).inv) ≫ (g x).hom =
    (((X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯) ≫ (X.isoOfEq ⋯).inv) ≫ (g y).hom
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝⁵ : IsReduced X
inst✝⁴ : Y.IsSeparated
inst✝³ : S.IsSeparated
inst✝² : X.Over S
inst✝¹ : Y.Over S
f : X ⤏ Y
inst✝ : RationalMap.IsOver S f
⊢ PartialMap.IsOver S f.toPartialMap

Tactic:
by
  rw [← PartialMap.isOver_toRationalMap_iff_of_isSeparated, f.toRationalMap_toPartialMap]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y.PartialMap Z
⊢ (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).carrier.Nonempty

Tactic:
by
    simpa [← Set.nonempty_preimage_iff] using
      f.hom.denseRange.inter_open_nonempty _ g.domain.2 g.dense_domain.nonempty

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

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat iX
hUS : IsAffineOpen US
hUX : IsAffineOpen UX
hUT : IsCompact ↑UT
this : Mono (pushoutSection ⋯ hUSX hUST ⋯)
⊢ Mono (pushoutSection H hUST hUSX hUY)

Tactic:
by
    rw [← mono_comp_iff_of_isIso (pushoutSymmetry _ _).hom]; convert! this; cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g₁ g₂ : Y.PartialMap Z
W : Y.Opens
hW : Dense ↑W
hW₁ : W ≤ g₁.domain
hW₂ : W ≤ g₂.domain
e : (f.comp g₁).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ W) ⋯ ⋯ = f.comp (g₂.restrict W hW hW₂)
⊢ (f.comp g₁).equiv (f.comp g₂)

Tactic:
comp_restrict_right

Goal state after:
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g₁ g₂ : Y.PartialMap Z
W : Y.Opens
hW : Dense ↑W
hW₁ : W ≤ g₁.domain
hW₂ : W ≤ g₂.domain
e : (f.comp g₁).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ W) ⋯ ⋯ = (f.comp g₂).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ W) ⋯ ⋯
⊢ (f.comp g₁).equiv (f.comp g₂)
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
| (Hom.isoImage (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).ι
        ((TopologicalSpace.Opens.map (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv.base).obj
          ((TopologicalSpace.Opens.map (f.hom ∣_ g.domain).base).obj
            ((TopologicalSpace.Opens.map g.hom.base).obj h.domain)))).inv ≫
    (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv ∣_ (f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain ≫
      f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom

Tactic:
← Category.assoc

Goal state after:
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
| ((Hom.isoImage (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).ι
          ((TopologicalSpace.Opens.map (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv.base).obj
            ((TopologicalSpace.Opens.map (f.hom ∣_ g.domain).base).obj
              ((TopologicalSpace.Opens.map g.hom.base).obj h.domain)))).inv ≫
      (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv ∣_ (f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain) ≫
    f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUX : IsCompact ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
this : Mono (pushoutSection ⋯ hUSX hUST ⋯)
⊢ Mono (pushoutSection H hUST hUSX hUY)

Tactic:
by
    rw [← mono_comp_iff_of_isIso (pushoutSymmetry _ _).hom]; convert! this; cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
| (((X₁.isoOfEq ⋯).hom ≫ (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)).inv) ≫
      (↑f.domain).homOfLE ⋯) ≫
    (Hom.isoImage (f.hom ⁻¹ᵁ g.domain).ι ((f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
      f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom

Tactic:
← Category.assoc

Goal state after:
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
| ((((X₁.isoOfEq ⋯).hom ≫ (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)).inv) ≫
        (↑f.domain).homOfLE ⋯) ≫
      (Hom.isoImage (f.hom ⁻¹ᵁ g.domain).ι ((f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain)).inv) ≫
    f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_2.refine_2
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
h : ((opensDiagram D i U).map f) x ∈ V
⊢ ⟨(D.map (Over.Hom.left f)) ↑x, ⋯⟩ ∈ ↑V

pp: case e'_2.refine_3
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
⊢ x ∈ ↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V) →
    ((opensDiagram D i U).map f) x ∈ V

Tactic:
· convert! h
      exact Subtype.ext (by simp)

Goal state after:
case e'_2.refine_3
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
⊢ x ∈ ↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V) →
    ((opensDiagram D i U).map f) x ∈ V
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: P : MorphismProperty Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝² : Category.{v_2, u_2} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone i).pt ≅ ((MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).pt :=
  (d.isColimit i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)) (d.isColimit j))
    (D.isoWhiskerLeft (MorphismProperty.Over.pullbackComp (Cover.trans 𝒰 hij) (𝒰.f j) (𝒰.f i) ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))).symm)
a : J
⊢ (pullback.map (D.obj a).hom (𝒰.f i) (D.obj a).hom (Cover.trans 𝒰 hij ≫ 𝒰.f j) (𝟙 (D.obj a).left) (𝟙 (𝒰.X i)) (𝟙 S) ⋯
          ⋯ ≫
        (pullbackLeftPullbackSndIso (D.obj a).hom (𝒰.f j) (Cover.trans 𝒰 hij)).inv) ≫
      pullback.fst (pullback.snd (D.obj a).hom (𝒰.f j)) (Cover.trans 𝒰 hij) ≫
        (Comma.Hom.hom ((d.cocone j).ι.app a)).left =
    pullback.map (D.obj a).hom (𝒰.f i) (D.obj a).hom (𝒰.f j) (𝟙 (D.obj a).left) (Cover.trans 𝒰 hij) (𝟙 S) ⋯ ⋯ ≫
      (Comma.Hom.hom ((d.cocone j).ι.app a)).left

Tactic:
← Category.assoc

Goal state after:
P : MorphismProperty Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝² : Category.{v_2, u_2} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone i).pt ≅ ((MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).pt :=
  (d.isColimit i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)) (d.isColimit j))
    (D.isoWhiskerLeft (MorphismProperty.Over.pullbackComp (Cover.trans 𝒰 hij) (𝒰.f j) (𝒰.f i) ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))).symm)
a : J
⊢ ((pullback.map (D.obj a).hom (𝒰.f i) (D.obj a).hom (Cover.trans 𝒰 hij ≫ 𝒰.f j) (𝟙 (D.obj a).left) (𝟙 (𝒰.X i)) (𝟙 S) ⋯
            ⋯ ≫
          (pullbackLeftPullbackSndIso (D.obj a).hom (𝒰.f j) (Cover.trans 𝒰 hij)).inv) ≫
        pullback.fst (pullback.snd (D.obj a).hom (𝒰.f j)) (Cover.trans 𝒰 hij)) ≫
      (Comma.Hom.hom ((d.cocone j).ι.app a)).left =
    pullback.map (D.obj a).hom (𝒰.f i) (D.obj a).hom (𝒰.f j) (𝟙 (D.obj a).left) (Cover.trans 𝒰 hij) (𝟙 S) ⋯ ⋯ ≫
      (Comma.Hom.hom ((d.cocone j).ι.app a)).left
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst✝ : EffectiveEpiFamily X f
W✝ : C
e : (a : α) → Y a ⟶ W✝
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ (g a ≫ i a) ≫ 𝟙 (Y a) ≫ e a = 𝟙 (Y a) ≫ e a

Tactic:
← Category.assoc

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst✝ : EffectiveEpiFamily X f
W✝ : C
e : (a : α) → Y a ⟶ W✝
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ ((g a ≫ i a) ≫ 𝟙 (Y a)) ≫ e a = 𝟙 (Y a) ≫ e a
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B X : C
f : X ⟶ B
inst✝ : IsSplitEpi f
⊢ CategoryTheory.EffectiveEpi f

Tactic:
← Category.comp_id f

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B X : C
f : X ⟶ B
inst✝ : IsSplitEpi f
⊢ CategoryTheory.EffectiveEpi (f ≫ 𝟙 B)
Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
inst✝¹ : F.ReflectsEffectiveEpiFamilies
α✝ : Type
inst✝ : Finite α✝
B✝ : C
x✝¹ : α✝ → C
x✝ : (a : α✝) → x✝¹ a ⟶ B✝
h : EffectiveEpiFamily (fun a ↦ F.obj (x✝¹ a)) fun a ↦ F.map (x✝ a)
⊢ EffectiveEpiFamily x✝¹ x✝

Tactic:
by
    have := F.effectiveEpiFamily_of_map _ _ h
    infer_instance

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
          ((k₀ * k) ^ (k₀ * k) • D) n) ^
        (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
          ((k₀ * k) ^ (k₀ * k) • D) n) *
      ((k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n) =
    (k₀ * k) ^ (k₀ * k) *
      ((numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
            ((k₀ * k) ^ (k₀ * k) • D) n) ^
          (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
            ((k₀ * k) ^ (k₀ * k) • D) n) *
        degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n)

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
        ((k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n) *
      D n =
    numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
      ((k₀ * k) ^ (k₀ * k) * D n)

Tactic:
ring

Goal state after: