mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: 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 : I), CompactSpace ↥(D.obj i)
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i✝ : I
a b : D.obj i✝ ⟶ X
ha : t.app i✝ = a ≫ f
hb : t.app i✝ = b ≫ f
hab : c.π.app i✝ ≫ a = c.π.app i✝ ≫ b
this : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i✝, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := S.affineCover, h𝒰S := ⋯,
    𝒰X := fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i).affineCover, h𝒰X := ⋯ }
𝒰 : (pullback.diagonalObj f).OpenCover := Pullback.diagonalCover f A.𝒰S A.𝒰X
W : (pullback.diagonalObj f).Opens := Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
k : A.𝒰D.I₀ → I
hki' : (j : A.𝒰D.I₀) → k j ⟶ A.i'
heq :
  ∀ (j : A.𝒰D.I₀),
    (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.b
𝒰Df : (D.obj A.i').OpenCover := A.𝒰D.finiteSubcover
h : Nonempty ↥(D.obj A.i')
O : Finset I := {A.i'} ∪ Finset.image (fun i ↦ k (Cover.idx A.𝒰D ↑i)) Finset.univ
o : 𝒰Df.I₀ := ⋯.some
ho : k (Cover.idx A.𝒰D ↑o) ∈ O
i : 𝒰Df.I₀
⊢ k (Cover.idx A.𝒰D ↑i) ∈ O

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Sigma

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : UnivLE.{v, u}
inst✝ : P.IsMultiplicative
𝒰✝ 𝒱 𝒰 : Cover (precoverage P) S
⊢ (Hom.sigma (𝟙 𝒰)).h₀ ≍ (𝟙 𝒰.sigma).h₀

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Sigma

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : UnivLE.{v, u}
inst✝ : P.IsMultiplicative
𝒰 𝒱 X✝ Y✝ Z✝ : Cover (precoverage P) S
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
j : X✝.sigma.I₀
⊢ ∀ (b : X✝.I₀), Sigma.ι X✝.X b ≫ (Hom.sigma (f ≫ g)).h₀ j = Sigma.ι X✝.X b ≫ (Hom.sigma f ≫ Hom.sigma g).h₀ j

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: 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 : I), CompactSpace ↥(D.obj i)
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i✝ : I
a b : D.obj i✝ ⟶ X
ha : t.app i✝ = a ≫ f
hb : t.app i✝ = b ≫ f
hab : c.π.app i✝ ≫ a = c.π.app i✝ ≫ b
this : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i✝, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := S.affineCover, h𝒰S := ⋯,
    𝒰X := fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i).affineCover, h𝒰X := ⋯ }
𝒰 : (pullback.diagonalObj f).OpenCover := Pullback.diagonalCover f A.𝒰S A.𝒰X
W : (pullback.diagonalObj f).Opens := Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
k : A.𝒰D.I₀ → I
hki' : (j : A.𝒰D.I₀) → k j ⟶ A.i'
heq :
  ∀ (j : A.𝒰D.I₀),
    (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.b
𝒰Df : (D.obj A.i').OpenCover := A.𝒰D.finiteSubcover
h : Nonempty ↥(D.obj A.i')
O : Finset I := {A.i'} ∪ Finset.image (fun i ↦ k (Cover.idx A.𝒰D ↑i)) Finset.univ
o : 𝒰Df.I₀ := ⋯.some
ho : k (Cover.idx A.𝒰D ↑o) ∈ O
i : 𝒰Df.I₀
⊢ A.i' ∈ O

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Sigma

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : UnivLE.{v, u}
inst✝ : P.IsMultiplicative
𝒰 𝒱 X✝ Y✝ Z✝ : Cover (precoverage P) S
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (Hom.sigma (f ≫ g)).h₀ ≍ (Hom.sigma f ≫ Hom.sigma g).h₀

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
deg_bound₂ : c'.degBound < c.degBound
⊢ c.degBound * c.degBound ^ c'.degBound = c.degBound ^ (c'.degBound + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.TopCat.EffectiveEpi

Goal state before:
pp: B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
a b : ↑X
hab : (ConcreteCategory.hom π) a = (ConcreteCategory.hom π) b
⊢ ofHom { toFun := fun x ↦ a, continuous_toFun := ⋯ } ≫ π = ofHom { toFun := fun x ↦ b, continuous_toFun := ⋯ } ≫ π

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.TopCat.EffectiveEpi

Goal state before:
pp: B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
a b : ↑X
hab : (ConcreteCategory.hom π) a = (ConcreteCategory.hom π) b
⊢ ofHom { toFun := fun x ↦ a, continuous_toFun := ⋯ } ≫ π = ofHom { toFun := fun x ↦ b, continuous_toFun := ⋯ } ≫ π

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.TopCat.EffectiveEpi

Goal state before:
pp: B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
this : g = ofHom (hπ.liftEquiv ⟨Hom.hom e, ⋯⟩)
⊢ g = ofHom (hπ.lift (Hom.hom e) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.TopCat.EffectiveEpi

Goal state before:
pp: B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
⊢ g = ofHom (hπ.lift (Hom.hom e) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.TopCat.EffectiveEpi

Goal state before:
pp: B X : TopCat
π : X ⟶ B
⊢ EffectiveEpi π ↔ IsQuotientMap ⇑(ConcreteCategory.hom π)

Tactic:
by

Goal state after:
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₂
Z✝ : C
a₁ a₂ : α
g₁ : Z✝ ⟶ X a₁
g₂ : Z✝ ⟶ X a₂
x✝ : g₁ ≫ f a₁ = g₂ ≫ f a₂
⊢ g₁ ≫ i a₁ ≫ e a₁ = g₂ ≫ i a₂ ≫ e a₂

Tactic:
by

Goal state after:
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 ≫ f a) ≫ EffectiveEpiFamily.desc X f (fun a ↦ i a ≫ e a) ⋯ = e a

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: 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 : I), CompactSpace ↥(D.obj i)
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a b : D.obj i ⟶ X
ha : t.app i = a ≫ f
hb : t.app i = b ≫ f
hab : c.π.app i ≫ a = c.π.app i ≫ b
this : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := S.affineCover, h𝒰S := ⋯,
    𝒰X := fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i).affineCover, h𝒰X := ⋯ }
𝒰 : (pullback.diagonalObj f).OpenCover := Pullback.diagonalCover f A.𝒰S A.𝒰X
W : (pullback.diagonalObj f).Opens := Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
k : A.𝒰D.I₀ → I
hki' : (j : A.𝒰D.I₀) → k j ⟶ A.i'
heq :
  ∀ (j : A.𝒰D.I₀),
    (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.b
𝒰Df : (D.obj A.i').OpenCover := A.𝒰D.finiteSubcover
h : Nonempty ↥(D.obj A.i')
O : Finset I := {A.i'} ∪ Finset.image (fun i ↦ k (Cover.idx A.𝒰D ↑i)) Finset.univ
o : 𝒰Df.I₀ := ⋯.some
ho : k (Cover.idx A.𝒰D ↑o) ∈ O
l : I
hl1 : {X : I} → X ∈ O → (l ⟶ X)
hl2 :
  ∀ {X_1 Y : I} (mX : X_1 ∈ O) (mY : Y ∈ O) {f_1 : X_1 ⟶ Y},
    ⟨X_1, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈
        Finset.image (fun i ↦ ⟨k (Cover.idx A.𝒰D ↑i), ⟨A.i', ⟨⋯, ⟨⋯, hki' (Cover.idx A.𝒰D ↑i)⟩⟩⟩⟩) Finset.univ →
      hl1 mX ≫ f_1 = hl1 mY
w v : 𝒰Df.I₀
⊢ k (Cover.idx A.𝒰D ↑w) ∈ O

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: 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 : I), CompactSpace ↥(D.obj i)
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a b : D.obj i ⟶ X
ha : t.app i = a ≫ f
hb : t.app i = b ≫ f
hab : c.π.app i ≫ a = c.π.app i ≫ b
this : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := S.affineCover, h𝒰S := ⋯,
    𝒰X := fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i).affineCover, h𝒰X := ⋯ }
𝒰 : (pullback.diagonalObj f).OpenCover := Pullback.diagonalCover f A.𝒰S A.𝒰X
W : (pullback.diagonalObj f).Opens := Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
k : A.𝒰D.I₀ → I
hki' : (j : A.𝒰D.I₀) → k j ⟶ A.i'
heq :
  ∀ (j : A.𝒰D.I₀),
    (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.b
𝒰Df : (D.obj A.i').OpenCover := A.𝒰D.finiteSubcover
h : Nonempty ↥(D.obj A.i')
O : Finset I := {A.i'} ∪ Finset.image (fun i ↦ k (Cover.idx A.𝒰D ↑i)) Finset.univ
o : 𝒰Df.I₀ := ⋯.some
ho : k (Cover.idx A.𝒰D ↑o) ∈ O
l : I
hl1 : {X : I} → X ∈ O → (l ⟶ X)
hl2 :
  ∀ {X_1 Y : I} (mX : X_1 ∈ O) (mY : Y ∈ O) {f_1 : X_1 ⟶ Y},
    ⟨X_1, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈
        Finset.image (fun i ↦ ⟨k (Cover.idx A.𝒰D ↑i), ⟨A.i', ⟨⋯, ⟨⋯, hki' (Cover.idx A.𝒰D ↑i)⟩⟩⟩⟩) Finset.univ →
      hl1 mX ≫ f_1 = hl1 mY
w v : 𝒰Df.I₀
⊢ k (Cover.idx A.𝒰D ↑v) ∈ O

Tactic:
by

Goal state after:
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
x✝² : (a : α) → Y a ⟶ W✝
x✝¹ :
  ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ x✝² a₁ = g₂ ≫ x✝² a₂
x✝ : B ⟶ W✝
hm : ∀ (a : α), (g a ≫ f a) ≫ x✝ = x✝² a
⊢ x✝ = EffectiveEpiFamily.desc X f (fun a ↦ i a ≫ x✝² a) ⋯

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C✝ : Type u_1
inst✝³ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝² : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst✝¹ : EffectiveEpiFamily Z fun i ↦ g i ≫ f i
inst✝ : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
T : C
i₁ i₂ : I
g₁ : T ⟶ Z i₁
g₂ : T ⟶ Z i₂
eq : g₁ ≫ g i₁ ≫ f i₁ = g₂ ≫ g i₂ ≫ f i₂
⊢ (g₁ ≫ g i₁) ≫ f i₁ = (g₂ ≫ g i₂) ≫ f i₂

Tactic:
by

Goal state after:
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.71} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.71} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
⊢ Cocone D

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C✝ : Type u_1
inst✝³ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝² : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst✝¹ : EffectiveEpiFamily Z fun i ↦ g i ≫ f i
inst✝ : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
T : C
i₁ i₂ : I
g₁ : T ⟶ Z i₁
g₂ : T ⟶ Z i₂
eq : g₁ ≫ g i₁ ≫ f i₁ = g₂ ≫ g i₂ ≫ f i₂
⊢ g₁ ≫ g i₁ ≫ φ i₁ = g₂ ≫ g i₂ ≫ φ i₂

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
deg_bound₂ : c'.degBound < c.degBound
⊢ c.degBound ^ (c'.degBound + 1) ≤ c.degBound ^ c.degBound

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C✝ : Type u_1
inst✝³ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝² : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst✝¹ : EffectiveEpiFamily Z fun i ↦ g i ≫ f i
inst✝ : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
i : I
⊢ f i ≫ EffectiveEpiFamily.desc Z (fun i ↦ g i ≫ f i) (fun i ↦ g i ≫ φ i) ⋯ = φ i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C✝ : Type u_1
inst✝³ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝² : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst✝¹ : EffectiveEpiFamily Z fun i ↦ g i ≫ f i
inst✝ : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
x✝ : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
m : X ⟶ W
hm : ∀ (a : I), f a ≫ m = φ a
i : I
⊢ (g i ≫ f i) ≫ m = g i ≫ φ i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
B B' : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
i : B ⟶ B'
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ g₁ ≫ e a₁ = g₂ ≫ e a₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
B B' : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
i : B ⟶ B'
inst✝¹ : EffectiveEpiFamily X π
inst✝ : IsIso i
W✝ : C
x✝² : (a : α) → X a ⟶ W✝
x✝¹ : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i → g₁ ≫ x✝² a₁ = g₂ ≫ x✝² a₂
x✝ : α
⊢ (π x✝ ≫ i) ≫ inv i ≫ EffectiveEpiFamily.desc X π x✝² ⋯ = x✝² x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
B B' : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
i : B ⟶ B'
inst✝¹ : EffectiveEpiFamily X π
inst✝ : IsIso i
W✝ : C
e : (a : α) → X a ⟶ W✝
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i → g₁ ≫ e a₁ = g₂ ≫ e a₂
m : B' ⟶ W✝
hm : ∀ (a : α), (π a ≫ i) ≫ m = e a
⊢ m = inv i ≫ EffectiveEpiFamily.desc X π e ⋯

Tactic:
by

Goal state after:
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
e : C ≌ D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
this : True → e.functor.map g₁ ≫ ε a₁ = e.functor.map g₂ ≫ ε a₂
⊢ True

Tactic:
by

Goal state after:
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
e : C ≌ D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ g₁ ≫ (fun a ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) a₁ = g₂ ≫ (fun a ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) a₂

Tactic:
by

Goal state after:
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
e : C ≌ D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
W✝ : D
ε : (a : α) → e.functor.obj (X a) ⟶ W✝
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
a : α
⊢ e.functor.map (π a) ≫
      (e.toAdjunction.homEquiv B W✝).symm
        (EffectiveEpiFamily.desc X π (fun a ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯) =
    ε a

Tactic:
by

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

Goal state before:
pp: R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
⊢ coeffSubmodule R₀ c' ^ c'.degBound ^ c'.degBound ≤ coeffSubmodule R₀ c ^ c.degBound ^ c.degBound

Tactic:
by

Goal state after:
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))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, u_2} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
a : J
i : 𝒰.I₀
⊢ pullback.fst (D.obj a).hom (𝒰.f i) ≫ (d.gluedCocone.ι.app a).left =
    ((d.cocone i).ι.app a).left ≫ colimit.ι d.relativeGluingData.functor i

Tactic:
by

Goal state after:
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
e : C ≌ D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
W✝ : D
ε : (a : α) → e.functor.obj (X a) ⟶ W✝
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
m : e.functor.obj B ⟶ W✝
hm : ∀ (a : α), e.functor.map (π a) ≫ m = ε a
⊢ m =
    (e.toAdjunction.homEquiv B W✝).symm (EffectiveEpiFamily.desc X π (fun a ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯)

Tactic:
by

Goal state after:
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
inst✝² : IsRegularEpiCategory D
F : C ⥤ D
inst✝¹ : F.PreservesEpimorphisms
inst✝ : HasPullbacks D
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : EffectiveEpi x✝¹
⊢ EffectiveEpi (F.map x✝¹)

Tactic:
by

Goal state after: