mathlib-initiative/mathlib-tactics huggingface dataset:
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✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝¹ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this✝ : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
i' : 𝒰.I₀ → I
f : (j : 𝒰.I₀) → i' j ⟶ i
hf : ∀ (j : 𝒰.I₀), IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j)
g : (j : I) →
  j ∈ insert i (Finset.image i' Finset.univ) →
    (IsCofiltered.inf (insert i (Finset.image i' Finset.univ))
        (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ) ⟶
      j) :=
  fun j ↦
    IsCofiltered.infTo (insert i (Finset.image i' Finset.univ))
      (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ)
this : ∀ (j : 𝒰.I₀), IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (g i ⋯)) 𝒰).X j)
⊢ i ∈ insert i (Finset.image i' Finset.univ)

Tactic:
simp

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

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X ⤏ Y
x : ↥↑f.domain
⊢ ↑(({ I₀ := ↑{x | ∃ g, ∃ (_ : g.toRationalMap = f), g.domain = x}, X := fun U ↦ ↑↑U, f := fun U ↦ X.homOfLE ⋯ }.f
          ⟨⋯.choose, ⋯⟩)
        ⟨↑x, ⋯⟩) =
    ↑x

Tactic:
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✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝⁴ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := ⋯
this✝³ : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
j : 𝒰.I₀
H : ∀ {i' : I} (f : i' ⟶ i), Nonempty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map f) 𝒰).X j)
F : Over i ⥤ Scheme := ⋯
this✝² : ∀ (i' : Over i), IsAffine (F.obj i')
this✝¹ : ∀ (i' : Over i), Nonempty ↥(F.obj i')
e : F ⟶ (F ⋙ Γ.rightOp) ⋙ Scheme.Spec := ⋯
this✝ : ∀ (i_1 : Over i), IsIso (e.app i_1)
this : IsIso e
c' : LimitCone F := ⋯
i' : (Over i)ᵒᵖ
⊢ Nonempty ↥↑⊤

Tactic:
simp

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ f.toRationalMap.toPartialMap.toRationalMap = (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).toRationalMap

Tactic:
simp

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

Goal state before:
pp: case mp
X Y : Scheme
f : X.PartialIso Y
⊢ ∃ (e : f.source = f.source) (e' : f.target = f.target), f.iso = X.isoOfEq e ≪≫ f.iso ≪≫ Y.isoOfEq e'

Tactic:
simp

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

Goal state before:
pp: case e
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y.PartialMap Z
V : Y.Opens
hV : Dense ↑V
hV' : V ≤ g.domain
x✝ : ↥X
⊢ x✝ ∈ ↑(f.comp (g.restrict V hV hV')).domain ↔ x✝ ∈ ↑((f.comp g).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ V) ⋯ ⋯).domain

Tactic:
simp

Goal state after:
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})
hxT₂ : x ∈ ↑T₂
⊢ {c} ⊆ Set.range { f := f₂ x.f, n := x.n + 1, g := Fin.cons c (g₂ x) }.g

Tactic:
simp

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

Goal state before:
pp: X Y Z : Scheme
inst✝³ : PreirreducibleSpace ↥X
inst✝² : Nonempty ↥Y
f₁ f₂ : X.PartialMap Y
inst✝¹ : IsDominant f₁.hom
inst✝ : IsDominant f₂.hom
h : f₁.equiv f₂
g : Y.PartialMap Z
⊢ (f₁.comp g).equiv (f₂.comp g)

Tactic:
by
  obtain ⟨W, hW, hW₁, hW₂, e⟩ := h
  replace e : f₁.restrict W hW hW₁ = f₂.restrict W hW hW₂ :=
    PartialMap.ext _ _ rfl (by simpa using e)
  replace e := congr($(e).comp g)
  rw [comp_restrict_left, comp_restrict_left] at e
  exact equiv_of_restrict_eq _ _ e

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

Goal state before:
pp: case e
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y ⟶ Z
⊢ (f.comp (Hom.toPartialMap g)).domain = (f.compHom g).domain

Tactic:
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✝ : IsCofiltered I
i : I
U : (D.obj i).Opens
j : Over i
⊢ { hom := (c.π.app i ⁻¹ᵁ U).ι, w := ⋯ }.hom ≫ (Cone.whisker (Over.forget i) c).π.app j =
    (opensCone D c i U).π.app j ≫ (opensDiagramι D i U).app j

Tactic:
simp

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

Goal state before:
pp: X Y : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
⊢ f.comp (PartialMap.id Y) = f

Tactic:
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.67} 𝒰.I₀
inst✝ : 𝒰.LocallyDirected
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
y : ↥(𝒰.X k)
⊢ 𝒰.trans hki ≫ 𝒰.f i = 𝒰.trans hkj ≫ 𝒰.f j

Tactic:
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.75} 𝒰.I₀
inst✝² : 𝒰.LocallyDirected
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
i j : 𝒰.I₀
k : (k : 𝒰.I₀) × (k ⟶ i) × (k ⟶ j)
⊢ 𝒰.trans k.snd.1 ≫ 𝒰.f i = 𝒰.trans k.snd.2 ≫ 𝒰.f j

Tactic:
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)
h : ((opensDiagram D i U).map f) x ∈ V
⊢ ↑⟨(D.map (Over.Hom.left f)) ↑x, ⋯⟩ = ↑(((opensDiagram D i U).map f) x)

Tactic:
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:
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:
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:
simp

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

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
⊢ UniversallyInjective f ≤ diagonal (@Surjective) f

Tactic:
hf

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
⊢ diagonal (@Surjective) f
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:
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:
simp

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

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
⊢ diagonal (@Surjective) f → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] x ↦ Injective x) f

Tactic:
hf

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] x ↦ Injective x) f
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:
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:
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:
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:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: 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)
i : I
U V : (D.obj i).Opens
hU : IsCompact ↑U
hV : IsCompact ↑V
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
j₂ : I
fj₂i : j₂ ⟶ i
e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U
k : I
fkj₁ : k ⟶ j₁
fkj₂ : k ⟶ j₂
e : fkj₁ ≫ fj₁i = fkj₂ ≫ fj₂i
⊢ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ U ≤ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ V

pp: 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)
i : I
U V : (D.obj i).Opens
hU : IsCompact ↑U
hV : IsCompact ↑V
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
j₂ : I
fj₂i : j₂ ⟶ i
e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U
k : I
fkj₁ : k ⟶ j₁
fkj₂ : k ⟶ j₂
e : fkj₁ ≫ fj₁i = fkj₂ ≫ fj₂i
⊢ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ V ≤ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ U

Tactic:
· simpa only [Scheme.Hom.comp_preimage, Functor.map_comp] using Scheme.Hom.preimage_mono _ e₁

Goal state after:
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)
i : I
U V : (D.obj i).Opens
hU : IsCompact ↑U
hV : IsCompact ↑V
H : c.π.app i ⁻¹ᵁ U = c.π.app i ⁻¹ᵁ V
j₁ : I
fj₁i : j₁ ⟶ i
e₁ : D.map fj₁i ⁻¹ᵁ U ≤ D.map fj₁i ⁻¹ᵁ V
j₂ : I
fj₂i : j₂ ⟶ i
e₂ : D.map fj₂i ⁻¹ᵁ V ≤ D.map fj₂i ⁻¹ᵁ U
k : I
fkj₁ : k ⟶ j₁
fkj₂ : k ⟶ j₂
e : fkj₁ ≫ fj₁i = fkj₂ ≫ fj₂i
⊢ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ V ≤ D.map (fkj₁ ≫ fj₁i) ⁻¹ᵁ U
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:
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:
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:
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:
simp

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i : 𝒰.I₀
⊢ IsOpenImmersion.lift (𝒰.f i) (𝒰.f i) ⋯ ≫ 𝒰.f i = 𝟙 (𝒰.X i) ≫ 𝒰.f i

Tactic:
simp

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i✝ j✝ k✝ : 𝒰.I₀
hij : i✝ ⟶ j✝
hjk : j✝ ⟶ k✝
⊢ IsOpenImmersion.lift (𝒰.f k✝) (𝒰.f i✝) ⋯ ≫ 𝒰.f k✝ =
    (IsOpenImmersion.lift (𝒰.f j✝) (𝒰.f i✝) ⋯ ≫ IsOpenImmersion.lift (𝒰.f k✝) (𝒰.f j✝) ⋯) ≫ 𝒰.f k✝

Tactic:
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 : I), CompactSpace ↥(D.obj i)
inst✝⁵ : LocallyOfFiniteType f
inst✝⁴ : IsCofiltered I
inst✝³ : IsAffine S
inst✝² : IsAffine X
inst✝¹ : ∀ (i : I), IsAffine (D.obj i)
inst✝ : IsAffine c.pt
i : I
a : D.obj i ⟶ X
ha : t.app i = a ≫ f
j : I
b : D.obj j ⟶ X
hb : t.app j = b ≫ f
hab : c.π.app i ≫ a = c.π.app j ≫ b
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b

Tactic:
wlog hS : ∃ R, S = Spec R generalizing S

Goal state after:
case inr
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✝³ : IsAffine S
inst✝² : IsAffine X
inst✝¹ : ∀ (i : I), IsAffine (D.obj i)
inst✝ : IsAffine c.pt
i : I
a : D.obj i ⟶ X
ha : t.app i = a ≫ f
j : I
b : D.obj j ⟶ X
hb : t.app j = b ≫ f
hab : c.π.app i ≫ a = c.π.app j ≫ b
this :
  ∀ {S : Scheme} (t : D ⟶ (Functor.const I).obj S) (f : X ⟶ S) [LocallyOfFiniteType f] [IsAffine S],
    t.app i = a ≫ f → t.app j = b ≫ f → (∃ R, S = Spec R) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
hS : ¬∃ R, S = Spec R
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b

I : Type u
inst✝⁷ : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : IsAffine X
inst✝³ : ∀ (i : I), IsAffine (D.obj i)
inst✝² : IsAffine c.pt
i : I
a : D.obj i ⟶ X
j : I
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
S : Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsAffine S
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
hS : ∃ R, S = Spec R
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: J : Type u_1
inst✝² : Category.{u_2, u_1} J
F G : J ⥤ Scheme
s : F ⟶ G
inst✝¹ : Quiver.IsThin J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective ⇑(F.map hij)
inst✝ : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq : (F.map fi) xi = (F.map fj) xj
⊢ (s.app j ≫ G.map fj) xj = (G.map fj) ((s.app j) xj)

Tactic:
simp

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
i✝ j✝ : X.directedAffineCover.I₀
⊢ i✝ ≤ j✝ ↔ Hom.opensRange (X.directedAffineCover.f i✝) ≤ Hom.opensRange (X.directedAffineCover.f j✝)

Tactic:
simp

Goal state after:
P : MorphismProperty Scheme
X : Scheme
i✝ j✝ : X.directedAffineCover.I₀
⊢ i✝ ≤ j✝ ↔ i✝ ≤ j✝
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
⊢ (Set.range fun i ↦ Hom.opensRange (X.directedAffineCover.f i)) = X.affineOpens

Tactic:
simp

Goal state after: