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

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
⊢ { I₀ := ↑R, X := fun r ↦ Spec (CommRingCat.of (Localization.Away r)),
        f := fun r ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings (Spec R)

Tactic:
rw [presieve₀_mem_precoverage_iff]

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
⊢ (∀ (x : ↥(Spec R)),
      ∃ i,
        x ∈
          Set.range
            ⇑({ I₀ := ↑R, X := fun r ↦ Spec (CommRingCat.of (Localization.Away r)),
                    f := fun r ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) }.f
                i)) ∧
    ∀
      (i :
        { I₀ := ↑R, X := fun r ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun r ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) }.I₀),
      IsOpenImmersion
        ({ I₀ := ↑R, X := fun r ↦ Spec (CommRingCat.of (Localization.Away r)),
              f := fun r ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) }.f
          i)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ IsIso (Hom.appLE U.ι U ⊤ ⋯)

Tactic:
simp only [ι, ofRestrict_appLE]

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ IsIso (X.presheaf.map (homOfLE ⋯).op)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
⊢ { I₀ := s, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.presieve₀ ∈ (precoverage IsOpenImmersion).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := s, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.f i)) ∧
    ∀ (i : { I₀ := s, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.I₀),
      IsOpenImmersion ({ I₀ := s, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.f i)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op

Tactic:
have e₃ := e₂.symm.trans e₁

Goal state after:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
e₁ : Hom.app (X.homOfLE e ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W
e₂ :
  (↑V).presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.homOfLE e) (V.ι ⁻¹ᵁ V.ι ''ᵁ W) =
    Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op
e₃ :
  Hom.app (X.homOfLE e) W ≫ (↑U).presheaf.map ((Opens.map (X.homOfLE e).base).map (eqToIso this).hom.op.unop).op =
    Hom.app U.ι (V.ι ''ᵁ W) ≫ (↑U).presheaf.map (eqToHom ⋯).op
⊢ Hom.app (X.homOfLE e) W = X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
⊢ { I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings ↑(⨆ i, U i)

Tactic:
rw [presieve₀_mem_precoverage_iff]

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
⊢ (∀ (x : ↥↑(⨆ i, U i)), ∃ i, x ∈ Set.range ⇑({ I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.f i)) ∧
    ∀ (i : { I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.I₀),
      IsOpenImmersion ({ I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.f i)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
V : (↑U).Opens
⊢ (Hom.isoImage U.ι V).inv ≫ V.ι = X.homOfLE ⋯

Tactic:
by
  simp [← cancel_mono U.ι]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ (isoImage f (f ⁻¹ᵁ U)).hom ≫ Y.homOfLE ⋯ = f ∣_ U

Tactic:
by
  simp [← cancel_mono U.ι]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
m : ↑(ModuleCat.of R M)
⊢ (ModuleCat.Hom.hom (toStalkₗ' R M x)) m =
    (↑(stalkIsoₗ R M x).toLinearEquiv.symm ∘ₗ LocalizedModule.mkLinearMap x.asIdeal.primeCompl M) m

Tactic:
refine .trans ?_ (localizationtoStalkₗ_mk ..).symm

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
m : ↑(ModuleCat.of R M)
⊢ (ModuleCat.Hom.hom (toStalkₗ' R M x)) m =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen ↑1) x ⋯)) (const m (↑1) (basicOpen ↑1) ⋯)
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasEqualizers C
inst✝² : HasPullbacks C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage C
𝒰 : J.ZeroHypercover S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : (MorphismProperty.isomorphisms C).IsLocalAtTarget J
H :
  ∀ (i : 𝒰.I₀),
    pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯ = pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯
⊢ f = g

Tactic:
suffices IsIso (equalizer.ι f g) from Limits.eq_of_epi_equalizer

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasEqualizers C
inst✝² : HasPullbacks C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage C
𝒰 : J.ZeroHypercover S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : (MorphismProperty.isomorphisms C).IsLocalAtTarget J
H :
  ∀ (i : 𝒰.I₀),
    pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯ = pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯
⊢ IsIso (equalizer.ι f g)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
I J : Ideal ↑Γ(X, U)
⊢ I = J ↔
    ∀ (x : ↥X) (h : x ∈ U),
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I =
        Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J

Tactic:
le_antisymm_iff,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
I J : Ideal ↑Γ(X, U)
⊢ I ≤ J ∧ J ≤ I ↔
    ∀ (x : ↥X) (h : x ∈ U),
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I ≤
          Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J ∧
        Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J ≤
          Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_3
X Y : Scheme
U✝ : X.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X, U✝)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝² : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩) := Y.presheaf.algebra_section_stalk ⟨f x, ⋯⟩
this✝¹ : IsLocalization.AtPrime (↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩)) (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
this✝ : Algebra ↑(X.presheaf.obj (op V)) ↑(X.presheaf.stalk ↑⟨x, hx⟩) := X.presheaf.algebra_section_stalk ⟨x, hx⟩
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) (hV.primeIdealOf ⟨x, hx⟩).asIdeal
a : ↑Γ(Y, U)
⊢ (algebraMap ↑Γ(X, V) ↑(X.presheaf.stalk x)) ((CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) a) =
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)) ((algebraMap ↑Γ(Y, U) ↑(Y.presheaf.stalk (f x))) a)

Tactic:
simp only [RingHom.algebraMap_toAlgebra, Scheme.Hom.germ_stalkMap_apply, Scheme.Hom.appLE,
      homOfLE_leOfHom, CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply,
      X.presheaf.germ_res_apply]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) x =
    (ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
⊢ (ConcreteCategory.hom
        (preservesColimitIso (forget TopCat) (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)).hom)
      ((ConcreteCategory.hom
          (↾⇑(ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one))))
        x) =
    (ConcreteCategory.hom
        (↾⇑(ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) ≫
          (preservesColimitIso (forget TopCat) (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap)).hom))
      y

Tactic:
simp_all

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ IsOpen
    (⇑(ConcreteCategory.hom
          (coequalizer.π ((SheafedSpace.forget CommRingCat).map (Hom.toShHom f))
              ((SheafedSpace.forget CommRingCat).map (Hom.toShHom g)) ≫
            (PreservesCoequalizer.iso (SheafedSpace.forget CommRingCat) (Hom.toShHom f) (Hom.toShHom g)).hom)) ⁻¹'
      ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ''
        (imageBasicOpen f g U s).carrier)

Tactic:
rw [PreservesCoequalizer.iso_hom, ι_comp_coequalizerComparison]

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ IsOpen
    (⇑(ConcreteCategory.hom ((SheafedSpace.forget CommRingCat).map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) ⁻¹'
      ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ''
        (imageBasicOpen f g U s).carrier)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (D.ι i).base)

Tactic:
← show _ = (𝖣.ι i).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) _,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i ≫ (D.gluedIso (forget C)).inv))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D✝ : GlueData
D : GlueData
⊢ { I₀ := D.J, X := D.U, f := D.ι }.presieve₀ ∈ (precoverage IsOpenImmersion).coverings D.glued

Tactic:
rw [presieve₀_mem_precoverage_iff]

Goal state after:
D✝ : GlueData
D : GlueData
⊢ (∀ (x : ↥D.glued), ∃ i, x ∈ Set.range ⇑({ I₀ := D.J, X := D.U, f := D.ι }.f i)) ∧
    ∀ (i : { I₀ := D.J, X := D.U, f := D.ι }.I₀), IsOpenImmersion ({ I₀ := D.J, X := D.U, f := D.ι }.f i)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ (t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ pullback.fst (𝒰.f i ≫ f) g =
    pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ pullback.fst (𝒰.f i ≫ f) g

Tactic:
rw [← cancel_mono (𝒰.f i)]

Goal state after:
case h₀.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ ((t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ pullback.fst (𝒰.f i ≫ f) g) ≫ 𝒰.f i =
    (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ pullback.fst (𝒰.f i ≫ f) g) ≫ 𝒰.f i
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    (((pullback.fst (D.f k i) (D.f k j) ≫ D.t k i).c.app
            (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
          (pullback (D.f k i) (D.f k j)).presheaf.map (eqToHom ⋯)) ≫
        (pullback (D.f k i) (D.f k j)).presheaf.map ((Opens.map (D.t' k i j).base).map (eqToHom ⋯).unop).op) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U)

Tactic:
comp_c_app

Goal state after:
case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    ((((D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
            (pullback.fst (D.f k i) (D.f k j)).c.app
              (op
                ((Opens.map (D.t k i).base).obj
                  (unop (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)))))) ≫
          (pullback (D.f k i) (D.f k j)).presheaf.map (eqToHom ⋯)) ≫
        (pullback (D.f k i) (D.f k j)).presheaf.map ((Opens.map (D.t' k i j).base).map (eqToHom ⋯).unop).op) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
    pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)

Tactic:
rw [← cancel_mono (𝒰.f i)]

Goal state after:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ (t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ 𝒰.f i =
    pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ 𝒰.f i
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
U : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ U x
hU : ∀ (x : ↥X), (U x).ι ≫ f = (U x).ι ≫ g
⊢ { I₀ := ↥X, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.presieve₀ ∈ (precoverage IsOpenImmersion).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Goal state after:
X Y : Scheme
f g : X ⟶ Y
U : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ U x
hU : ∀ (x : ↥X), (U x).ι ≫ f = (U x).ι ≫ g
⊢ (∀ (x : ↥X), ∃ i, x ∈ Set.range ⇑({ I₀ := ↥X, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.f i)) ∧
    ∀ (i : { I₀ := ↥X, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.I₀),
      IsOpenImmersion ({ I₀ := ↥X, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.f i)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst
hlj : l ⟶ k₂.fst
y : (F ⋙ forget).obj l
hy₁ :
  (ConcreteCategory.hom ((F ⋙ forget).map hli)) y =
    (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).inv) x
hy₂ :
  (ConcreteCategory.hom ((F ⋙ forget).map hlj)) y =
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) x
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom)
    (F.map hlj ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).hom) ⋯
⊢ IsOpenImmersion α

Tactic:
have : IsOpenImmersion (α ≫ pullback.fst _ _) := by
      simp only [pullback.lift_fst, α]; infer_instance

Goal state after:
J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst
hlj : l ⟶ k₂.fst
y : (F ⋙ forget).obj l
hy₁ :
  (ConcreteCategory.hom ((F ⋙ forget).map hli)) y =
    (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).inv) x
hy₂ :
  (ConcreteCategory.hom ((F ⋙ forget).map hlj)) y =
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) x
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom)
    (F.map hlj ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).hom) ⋯
this : IsOpenImmersion (α ≫ pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
⊢ IsOpenImmersion α
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst
hlj : l ⟶ k₂.fst
y : (F ⋙ forget).obj l
hy₁ :
  (ConcreteCategory.hom (↾⇑(F.map hli))) y =
    (TopCat.Hom.hom (Hom.isoOpensRange (F.map k₁.snd.1)).inv.base)
      ((TopCat.Hom.hom (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂)).base) x)
hy₂ :
  (ConcreteCategory.hom ((F ⋙ forget).map hlj)) y =
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) x
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom)
    (F.map hlj ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).hom) ⋯
this : IsOpenImmersion α
⊢ (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom) y =
    (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂)) x

Tactic:
simp_all

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_1.refine_1.inl
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥X'
⊢ (coprodMk X' Y') (Sum.inl x) ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) ↔
    (coprodMk X' Y') (Sum.inl x) ∈ ↑(Scheme.Hom.opensRange coprod.inl)

Tactic:
simp_all

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_1.refine_1.inr
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥Y'
⊢ (coprodMk X' Y') (Sum.inr x) ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) ↔
    (coprodMk X' Y') (Sum.inr x) ∈ ↑(Scheme.Hom.opensRange coprod.inl)

Tactic:
simp_all

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_1.refine_2.inl
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥X'
⊢ (coprodMk X' Y') (Sum.inl x) ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) ↔
    (coprodMk X' Y') (Sum.inl x) ∈ ↑(Scheme.Hom.opensRange coprod.inr)

Tactic:
simp_all

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_1.refine_2.inr
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥Y'
⊢ (coprodMk X' Y') (Sum.inr x) ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) ↔
    (coprodMk X' Y') (Sum.inr x) ∈ ↑(Scheme.Hom.opensRange coprod.inr)

Tactic:
simp_all

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
H : Disjoint U V
⊢ ∀ (i : Unit ⊕ Unit), IsAffineOpen (Sum.elim (fun x ↦ U) (fun x ↦ V) i)

Tactic:
simp_all

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

Goal state before:
pp: case basicOpen
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U✝ : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U✝ i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U✝ i))
this : Q.IsLocal := isLocal_affineProperty P
U : ↑Y.affineOpens
r : ↑Γ(Y, ↑U)
h : Q (f ∣_ ↑U)
⊢ Q (f ∣_ ↑(Y.affineBasicOpen r))

Tactic:
have := AffineTargetMorphismProperty.IsLocal.to_basicOpen (f ∣_ U.1) (U.1.topIso.inv r) h

Goal state after:
case basicOpen
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U✝ : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U✝ i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U✝ i))
this✝ : Q.IsLocal := isLocal_affineProperty P
U : ↑Y.affineOpens
r : ↑Γ(Y, ↑U)
h : Q (f ∣_ ↑U)
this : Q (f ∣_ ↑U ∣_ (↑↑U).basicOpen ((ConcreteCategory.hom (↑U).topIso.inv) r))
⊢ Q (f ∣_ ↑(Y.affineBasicOpen r))