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 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, ⋯⟩ = ↑(((opensDiagram D i U).map f) x)

Tactic:
by simp

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 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)
hU : (D.map (Over.Hom.left f)) ((D.map j.hom ⁻¹ᵁ U).ι x) ∈ D.map k.hom ⁻¹ᵁ U
hV : ⟨(D.map (Over.Hom.left f)) ((D.map j.hom ⁻¹ᵁ U).ι x), hU⟩ ∈ ↑V
⊢ ↑(((opensDiagram D i U).map f) x) = ↑⟨(D.map (Over.Hom.left f)) ((D.map j.hom ⁻¹ᵁ U).ι x), hU⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact ↑U
H : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace ↥((opensDiagram D i U).obj j)
⊢ ⊤ ≤ (c.π.app i ⁻¹ᵁ U).ι ⁻¹ᵁ c.π.app i ⁻¹ᵁ U

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact ↑U
H✝ : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace ↥((opensDiagram D i U).obj j)
H : ((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V = ⊤
⊢ D.map (Over.mk (𝟙 i)).hom ⁻¹ᵁ U = U

Tactic:
by simp

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.61} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
hij : i ⟶ j
⊢ f ≫ 𝟙 X = 𝟙 Y ≫ f

Tactic:
by simp

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.61} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
hij : i ⟶ j
⊢ 𝒰.f i ≫ 𝟙 X = 𝒰.trans hij ≫ 𝒰.f j

Tactic:
by simp

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.61} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
⊢ pullback.map f (𝒰.f i) f (𝒰.f i) (𝟙 Y) (𝒰.trans (𝟙 i)) (𝟙 X) ⋯ ⋯ = 𝟙 ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)

Tactic:
by simp

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅ pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) :=
  pullbackRightPullbackFstIso f (𝒰.f j) (pullback.fst f (𝒰.f i)) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫ pullbackAssoc f (𝒰.f i) (𝒰.f i) (𝒰.f j)
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ f ≫ 𝟙 X = 𝟙 Y ≫ f

Tactic:
by simp

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅ pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) :=
  pullbackRightPullbackFstIso f (𝒰.f j) (pullback.fst f (𝒰.f i)) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫ pullbackAssoc f (𝒰.f i) (𝒰.f i) (𝒰.f j)
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ 𝒰.f k ≫ 𝟙 X = 𝒰.trans hki ≫ 𝒰.f i

Tactic:
by simp

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅ pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) :=
  pullbackRightPullbackFstIso f (𝒰.f j) (pullback.fst f (𝒰.f i)) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫ pullbackAssoc f (𝒰.f i) (𝒰.f i) (𝒰.f j)
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ 𝒰.f k ≫ 𝟙 X = 𝒰.trans hkj ≫ 𝒰.f j

Tactic:
by simp

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅ pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) :=
  pullbackRightPullbackFstIso f (𝒰.f j) (pullback.fst f (𝒰.f i)) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫ pullbackAssoc f (𝒰.f i) (𝒰.f i) (𝒰.f j)
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ pullback.map f (𝒰.f k) f (𝒰.f i) (𝟙 Y) (𝒰.trans hki) (𝟙 X) ⋯ ⋯ ≫ pullback.fst f (𝒰.f i) =
    pullback.map f (𝒰.f k) f (𝒰.f j) (𝟙 Y) (𝒰.trans hkj) (𝟙 X) ⋯ ⋯ ≫ pullback.fst f (𝒰.f j)

Tactic:
by simp

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅ pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) :=
  pullbackRightPullbackFstIso f (𝒰.f j) (pullback.fst f (𝒰.f i)) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫ pullbackAssoc f (𝒰.f i) (𝒰.f i) (𝒰.f j)
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ 𝒰.trans hki ≫ 𝒰.f i = 𝒰.trans hkj ≫ 𝒰.f j

Tactic:
by simp

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.177} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : 𝒰.I₀
x : ↥(pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)))
iso : pullback (pullback.fst f (𝒰.f i)) (pullback.fst f (𝒰.f j)) ≅ pullback f (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) :=
  pullbackRightPullbackFstIso f (𝒰.f j) (pullback.fst f (𝒰.f i)) ≪≫
    pullback.congrHom ⋯ ⋯ ≪≫ pullbackAssoc f (𝒰.f i) (𝒰.f i) (𝒰.f j)
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
⊢ 𝒰.f k ≫ 𝟙 X = pullback.lift (𝒰.trans hki) (𝒰.trans hkj) ⋯ ≫ pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i

Tactic:
by simp

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰✝ : Cover (precoverage P) X
inst✝⁴ : Category.{v_1, ?u.15} 𝒰✝.I₀
inst✝³ : 𝒰✝.LocallyDirected
inst✝² : P.IsStableUnderBaseChange
𝒰 : Cover (precoverage P) X
inst✝¹ : Category.{v_2, ?u.259} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
Y : Scheme
f : Y ⟶ X
i j : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀
hij : i ⟶ j
⊢ 𝒰.f i = 𝒰.trans hij ≫ 𝒰.f j

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x | ∃ i V, ∃ (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact ↑(sSup s)
this : Finite ↑s
i : ↑s → I
V : (x : ↑s) → (D.obj (i x)).Opens
hV : ∀ (x : ↑s), IsAffineOpen (V x)
hVi : ∀ (x : ↑s), c.π.app (i x) ⁻¹ᵁ V x = ↑x
j : I
fj : (b : ↑s) → j ⟶ i b
⊢ ∃ i V, IsCompact ↑V ∧ c.π.app i ⁻¹ᵁ V = sSup s

Tactic:
refine ⟨j, ⨆ (k : s), D.map (fj _) ⁻¹ᵁ V k, ?_, ?_⟩

Goal state after:
case refine_1
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x | ∃ i V, ∃ (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact ↑(sSup s)
this : Finite ↑s
i : ↑s → I
V : (x : ↑s) → (D.obj (i x)).Opens
hV : ∀ (x : ↑s), IsAffineOpen (V x)
hVi : ∀ (x : ↑s), c.π.app (i x) ⁻¹ᵁ V x = ↑x
j : I
fj : (b : ↑s) → j ⟶ i b
⊢ IsCompact ↑(⨆ k, D.map (fj k) ⁻¹ᵁ V k)

case refine_2
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
s : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x | ∃ i V, ∃ (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact ↑(sSup s)
this : Finite ↑s
i : ↑s → I
V : (x : ↑s) → (D.obj (i x)).Opens
hV : ∀ (x : ↑s), IsAffineOpen (V x)
hVi : ∀ (x : ↑s), c.π.app (i x) ⁻¹ᵁ V x = ↑x
j : I
fj : (b : ↑s) → j ⟶ i b
⊢ c.π.app j ⁻¹ᵁ ⨆ k, D.map (fj k) ⁻¹ᵁ V k = sSup s
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n :=
  { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom ↑q₁) ∘ e.val }
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := { val := ⇑(mapRingHom ↑q₂) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (R ⧸ Ideal.span {c}) n e₂
f : R[X]
T₁ : ConstructibleSetData (Localization.Away c)
T₂ : ConstructibleSetData (R ⧸ Ideal.span {c})
hT₁ : comap Polynomial.C '' (zeroLocus (Set.range e₁.val) \ zeroLocus {(mapRingHom ↑q₁) f}) = T₁.toSet
hT₁deg : ∀ x ∈ T₁, x.n ≤ e₁.degBound
hT₂ : comap Polynomial.C '' (zeroLocus (Set.range e₂.val) \ zeroLocus {(mapRingHom ↑q₂) f}) = T₂.toSet
hT₂deg : ∀ x ∈ T₂, x.n ≤ e₂.degBound
x✝ : Invertible (q₁ c) := { invOf := IsLocalization.Away.invSelf c, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
he₁span :
  coeffSubmodule R₀ e₁ ^ e₁.powBound =
    ⅟(q₁ c ^ e₁.powBound) • Submodule.map q₁.toLinearMap (span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
g₁ : (x : BasicConstructibleSetData (Localization.Away c)) → Fin x.n → R
hg₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), g₁ x i ∈ ↑(span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
hq₁g₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), q₁.toLinearMap (g₁ x i) = q₁ c ^ e₁.powBound * x.g i
n₁ : Localization.Away c → ℕ
f₁ : Localization.Away c → R
hf₁ : ∀ (x : Localization.Away c), x * q₁ c ^ n₁ x = q₁ (f₁ x)
g₂ : (x : BasicConstructibleSetData (R ⧸ Ideal.span {c})) → Fin x.n → R
hg₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), g₂ x i ∈ ↑(coeffSubmodule R₀ e ^ e₂.powBound)
hq₂g₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), q₂.toLinearMap (g₂ x i) = x.g i
f₂ : R ⧸ Ideal.span {c} → R
hf₂ : ∀ (x : R ⧸ Ideal.span {c}), q₂ (f₂ x) = x
S₁ : Finset (BasicConstructibleSetData R) := Finset.image (fun x ↦ { f := c * f₁ x.f, n := x.n, g := g₁ x }) T₁
S₂ : Finset (BasicConstructibleSetData R) :=
  Finset.image (fun x ↦ { f := f₂ x.f, n := x.n + 1, g := Fin.cons c (g₂ x) }) T₂
x : BasicConstructibleSetData (R ⧸ Ideal.span {c})
hx : x ∈ T₂
⊢ Fin.cons c (g₂ x) 0 ∈ ⋃ i, coeff(e.val i)

Tactic:
by
        simpa using ⟨_, _, hi.symm⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
⊢ CommSq (d.natTrans.app i) (colimit.ι d.functor i) (𝒰.f i) d.toBase

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁷ : Category.{u, u} I
inst✝⁶ : IsCofiltered I
i j : I
R : CommRingCat
inst✝⁵ : IsAffine (Spec R)
S : CommRingCat
inst✝⁴ : IsAffine (Spec S)
φ : R ⟶ S
inst✝³ : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝² : ∀ (i : I), CompactSpace ↥((D ⋙ Scheme.Spec).obj i)
inst✝¹ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
inst✝ : IsAffine c.pt
t : D ⋙ Scheme.Spec ⟶ (Functor.const I).obj (Spec R)
a : S ⟶ Opposite.unop (D.obj i)
ha : t.app i = Spec.map a ≫ Spec.map φ
b : S ⟶ Opposite.unop (D.obj j)
hb : t.app j = Spec.map b ≫ Spec.map φ
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
⊢ ∀ {X Y : I} (f : X ⟶ Y),
    (((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec).map f ≫
        (Iso.refl ((((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec).obj Y)).hom =
      (Iso.refl ((((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec).obj X)).hom ≫
        ((Functor.const I).obj (Spec R)).map f

Tactic:
by simp

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
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
i : ℕ
hi : i ≤ f.natDegree
⊢ f.natDegree < f.natDegree + 2

Tactic:
by simp

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
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
i : ℕ
hi : f.natDegree < i
⊢ f.natDegree + 1 ∈ Set.Iio (f.natDegree + 2)

Tactic:
by simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case h
I : Type u
inst✝³ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := ⋯
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X))ᶜ).Nonempty
Z : (i' : I) → (i' ⟶ A.i) → Set ↥(D.obj i') := ⋯
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), (A.c.π.app i) s ∈ Z i hij
⊢ (pullback.diagonal f) ((A.c.π.app A.i ≫ A.a) s) = (D.map (𝟙 A.i) ≫ pullback.lift A.a A.b ⋯) ((A.c.π.app A.i) s)

Tactic:
have H : A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f =
      A.c.π.app A.i ≫ pullback.lift A.a A.b (A.ha.symm.trans A.hb) := by ext <;> simp [hab]

Goal state after:
case h
I : Type u
inst✝³ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X))ᶜ).Nonempty
Z : (i' : I) → (i' ⟶ A.i) → Set ↥(D.obj i') := fun i' hii' ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W)ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), (A.c.π.app i) s ∈ Z i hij
H : A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f = A.c.π.app A.i ≫ pullback.lift A.a A.b ⋯
⊢ (pullback.diagonal f) ((A.c.π.app A.i ≫ A.a) s) = (D.map (𝟙 A.i) ≫ pullback.lift A.a A.b ⋯) ((A.c.π.app A.i) s)
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
⊢ ⋃ i, ⋃ (h : i ∈ ∅), f i '' ↑((fun x x_1 ↦ { carrier := ∅, is_open' := ⋯ }) i h) = ∅

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
U : Set S
inst✝ : TopologicalSpace S
x✝ : IsOpen U ∧ IsCompact U
ho : IsOpen U
hc : IsCompact U
⊢ id '' { carrier := U, is_open' := ho }.carrier = U

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
U : Set S
inst✝ : TopologicalSpace S
⊢ (∃ V, IsCompact V.carrier ∧ id '' V.carrier = U) ↔ IsOpen U ∧ IsCompact U

Tactic:
refine ⟨fun ⟨V, hV, heq⟩ ↦ ?_, fun ⟨ho, hc⟩ ↦ ⟨⟨U, ho⟩, hc, by simp⟩⟩

Goal state after:
S : Type u_1
U : Set S
inst✝ : TopologicalSpace S
x✝ : ∃ V, IsCompact V.carrier ∧ id '' V.carrier = U
V : Opens S
hV : IsCompact V.carrier
heq : id '' V.carrier = U
⊢ IsOpen U ∧ IsCompact U
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₃.inr.refine_2
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.n ≤ c.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ coeffSubmodule R₀ c ^ c.powBound

Tactic:
let c' : InductionObj _ _ := ⟨update c.val j (c.val j %ₘ c.val i)⟩

Goal state after:
case hP₃.inr.refine_2
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) }
⊢ C.n ≤ c.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ coeffSubmodule R₀ c ^ c.powBound
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, ↑t = U
H : ∀ t ∈ s, IsCompactOpenCovered f ↑t
t : Finset ↑s
ht : U ⊆ ⋃ i ∈ t, ↑↑i
⊢ ⋃ i ∈ t, ↑↑i ⊆ ⋃ t_1 ∈ SetLike.coe '' ↑(Finset.image Subtype.val t), t_1

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
V : Opens (X i)
hV : IsCompact ↑V
⊢ ⋃ i_1, ⋃ (h : i_1 ∈ {i}), f i_1 '' ↑((fun j hj ↦ ⋯ ▸ V) i_1 h) = f i '' ↑V

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hunion : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
Us : (i : ↑s) → Set (Opens (X ↑i))
UsB : ∀ (i : ↑s), Us i ⊆ B ↑i
hUsf : ∀ (i : ↑s), (Us i).Finite
hUs : ∀ (i : ↑s), V ↑i ⋯ = sSup (Us i)
σ : Type (max u_2 u_3) := (i : ↑s) × ↑(Us i)
this✝ : Finite ↑s
this : ∀ (i : ↑s), Finite ↑(Us i)
i : σ
⊢ (fun i ↦ ↑i.snd) i ∈ Us i.fst

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hunion : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
Us : (i : ↑s) → Set (Opens (X ↑i))
UsB : ∀ (i : ↑s), Us i ⊆ B ↑i
hUsf : ∀ (i : ↑s), (Us i).Finite
hUs : ∀ (i : ↑s), V ↑i ⋯ = sSup (Us i)
σ : Type (max u_2 u_3) := (i : ↑s) × ↑(Us i)
this✝ : Finite ↑s
this : ∀ (i : ↑s), Finite ↑(Us i)
x✝ : σ
⊢ (fun i ↦ ↑i.snd) x✝ ∈ Us x✝.fst

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : Finite ι
inst✝ : TopologicalSpace S
hf : ∀ (i : ι), IsSpectralMap (f i)
U : Set S
hs : ∀ x ∈ U, ∃ i, x ∈ Set.range (f i)
hU : IsOpen U
hc : IsCompact U
⊢ ⋃ i, ⋃ (h : i ∈ Set.univ), f i '' ↑((fun i x ↦ { carrier := f i ⁻¹' U, is_open' := ⋯ }) i h) ⊆ U

Tactic:
by simp

Goal state after: