mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens ↑↑Y)ᵒᵖ
⊢ (((isoRestrict f).hom ≫ Y.ofRestrict ⋯).c ≫
          𝟙 ((Opens.map ((isoRestrict f).hom ≫ Y.ofRestrict ⋯).base).op ⋙ X.presheaf)).app
      x =
    f.c.app x

Tactic:
erw [Category.comp_id, comp_c_app, f.c.naturality_assoc, ← X.presheaf.map_comp]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens ↑↑Y)ᵒᵖ
⊢ f.c.app x ≫ X.presheaf.map ((Opens.map f.base).op.map (⋯.adjunction.counit.app (unop x)).op ≫ (eqToIso ⋯).hom) =
    f.c.app x
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
⊢ IsIso (Y.presheaf.map (⋯.adjunction.counit.app (hf.functor.obj U)).op)

Tactic:
have : (Opens.map f).obj (hf.functor.obj U) = U := by
      ext1
      exact Set.preimage_image_eq _ hf.injective

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
⊢ IsIso (Y.presheaf.map (⋯.adjunction.counit.app (hf.functor.obj U)).op)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀ (x : ↑S), (toPushforwardStalkAlgHom R S p) x = 0 → ∃ m, m • x = 0

Tactic:
· intro x hx
    rw [toPushforwardStalkAlgHom_apply,
      ← (toPushforwardStalk (CommRingCat.ofHom (algebraMap ↑R ↑S)) p).hom.map_zero,
      toPushforwardStalk] at hx
    rw [CommRingCat.comp_apply, map_zero] at hx
    obtain ⟨U, hpU, i₁, i₂, e⟩ := TopCat.Presheaf.germ_eq (C := CommRingCat) _ _ _ _ _ _ hx
    obtain ⟨_, ⟨r, rfl⟩, hpr, hrU⟩ :=
      PrimeSpectrum.isTopologicalBasis_basic_opens.exists_subset_of_mem_open (show p ∈ U.1 from hpU)
        U.2
    apply_fun (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).map
        (homOfLE hrU).op at e
    have : algebraMap S ((structureSheaf S).presheaf.obj _) x = 0 := e
    have :=
      (@IsLocalization.mk'_one _ _ _ _ _ _
            (StructureSheaf.IsLocalization.to_basicOpen S <| algebraMap R S r) x).trans
        this
    obtain ⟨⟨_, n, rfl⟩, e⟩ := (IsLocalization.mk'_eq_zero_iff _ _).mp this
    refine ⟨⟨r, hpr⟩ ^ n, ?_⟩
    rw [Submonoid.smul_def, Algebra.smul_def, SubmonoidClass.coe_pow, map_pow]
    exact e

Goal state after:
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P✝ Q P : MorphismProperty C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ P.precoverage.coverings X
⊢ ∃ T ∈ P.precoverage.coverings Y, T.FactorsThruAlong S f

Tactic:
have : S.HasPullbacks f := ⟨fun {W} h hh ↦ P.hasPullback _ (hS hh)⟩

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P✝ Q P : MorphismProperty C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ P.precoverage.coverings X
this : S.HasPullbacks f
⊢ ∃ T ∈ P.precoverage.coverings Y, T.FactorsThruAlong S f
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
⊢ Presieve.singleton f ∈ (precoverage P).coverings S ↔ Function.Surjective ⇑f ∧ P f

Tactic:
← Presieve.ofArrows_pUnit.{0},

Goal state after:
P : MorphismProperty Scheme
X S : Scheme
f : X ⟶ S
⊢ (Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∈ (precoverage P).coverings S ↔ Function.Surjective ⇑f ∧ P f
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace C
Y : SheafedSpace C
f : X ⟶ Y.toPresheafedSpace
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ X.presheaf.IsSheaf

Tactic:
apply TopCat.Presheaf.isSheaf_of_iso (sheafIsoOfIso (isoRestrict f).symm).symm

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace C
Y : SheafedSpace C
f : X ⟶ Y.toPresheafedSpace
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ((TopCat.Presheaf.pushforward C (isoRestrict f).symm.hom.base).obj (Y.restrict ⋯).presheaf).IsSheaf
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
H :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
⊢ IsIso
    ((colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).c.app
      (op (H.functor.obj U)))

Tactic:
PresheafedSpace.comp_c_app,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
H :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
⊢ IsIso
    ((preservesColimitIso forgetToPresheafedSpace F).inv.c.app (op (H.functor.obj U)) ≫
      (colimit.ι (F ⋙ forgetToPresheafedSpace) i).c.app
        (op ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (unop (op (H.functor.obj U))))))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
⊢ Set.range
      ⇑(ConcreteCategory.hom
          (pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
            ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g))) =
    ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
TopCat.pullback_fst_range

Goal state after:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
⊢ {x |
      ∃ y,
        (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)) x =
          (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) y} =
    ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ (asIso t ≪≫ pullbackRestrictIsoRestrict f V).hom ≫ (Arrow.mk (f ∣_ Scheme.Hom.opensRange g)).hom =
    (Arrow.mk (pullback.snd f g)).hom ≫ e.hom

Tactic:
rw [Iso.trans_hom, asIso_hom, ← Iso.comp_inv_eq, ← cancel_mono g]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ (Arrow.mk (f ∣_ Scheme.Hom.opensRange g)).hom) ≫ e.inv) ≫ g =
    (Arrow.mk (pullback.snd f g)).hom ≫ g
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
⊢ Arrow.mk (f ∣_ Scheme.Hom.opensRange g) ≅ Arrow.mk (pullback.snd f g)

Tactic:
let V : Y.Opens := g.opensRange
  let e :=
    IsOpenImmersion.isoOfRangeEq g V.ι Subtype.range_coe.symm
  let t : pullback f g ⟶ pullback f V.ι :=
    pullback.map _ _ _ _ (𝟙 _) e.hom (𝟙 _) (by rw [Category.comp_id, Category.id_comp])
      (by rw [Category.comp_id, IsOpenImmersion.isoOfRangeEq_hom_fac])
  symm
  refine Arrow.isoMk (asIso t ≪≫ pullbackRestrictIsoRestrict f V) e ?_
  rw [Iso.trans_hom, asIso_hom, ← Iso.comp_inv_eq, ← cancel_mono g]
  dsimp
  rw [Category.assoc, Category.assoc, Category.assoc, IsOpenImmersion.isoOfRangeEq_inv_fac,
    ← pullback.condition, morphismRestrict_ι,
    pullbackRestrictIsoRestrict_hom_ι_assoc, pullback.lift_fst_assoc, Category.comp_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
⊢ IsTopologicalBasis (SetLike.coe '' X.affineOpens)

Tactic:
exact X.isBasis_affineOpens

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ Set.range ⇑(U.ι ≫ f) = Set.range ⇑(f ''ᵁ U).ι

Tactic:
simp [Scheme.Hom.comp_base, Set.range_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).obj.obj (op (PrimeSpectrum.basicOpen f)))
e_2✝ : CommRing.toCommSemiring ≍ CommRing.toCommSemiring
r✝ : ↑Γ(X, U)
⊢ algebraMap ↑Γ(X, U) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) =
    algebraMap ↑Γ(X, U) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)

Tactic:
dsimp [CommRingCat.ofHom, RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp,
    basicOpenSectionsToAffine]

Goal state after:
case e'_3
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).obj.obj (op (PrimeSpectrum.basicOpen f)))
e_2✝ : CommRing.toCommSemiring ≍ CommRing.toCommSemiring
r✝ : ↑Γ(X, U)
⊢ CommRingCat.Hom.hom
      (X.presheaf.map (homOfLE ⋯).op ≫
        Scheme.Hom.app hU.fromSpec (X.basicOpen f) ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) =
    algebraMap ↑Γ(X, U) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
⊢ ((identityToΓSpec.app X).c.app (op ⊤)).op ≫ (toSpecΓ (unop (Γ.rightOp.obj X))).op = 𝟙 (Γ.rightOp.obj X)

Tactic:
exact congr_arg Quiver.Hom.op (left_triangle X)

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case inr.inr.inr
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
h✝² : i ≠ j
h✝¹ : i ≠ k
h✝ : j ≠ k
⊢ (if hij : i = j then
        (pullbackSymmetry (D.f' i j) (D.f' i k)).hom ≫
          pullback.map (D.f' i k) (D.f' i j) (D.f' j k) (D.f' j i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
      else
        if hik : i = k then
          have this := ⋯;
          pullback.fst (D.f' i j) (D.f' i k) ≫
            eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' j k) (D.f' j i))
        else
          if hjk : j = k then
            have this := ⋯;
            pullback.fst (D.f' i j) (D.f' i k) ≫
              eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' j k) (D.f' j i))
          else
            pullback.map (D.f' i j) (D.f' i k) (D.f i j hij) (D.f i k hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
              D.t' i j k hij hik hjk ≫
                pullback.map (D.f j k hjk) (D.f j i ⋯) (D.f' j k) (D.f' j i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯) ≫
      pullback.snd (D.f' j k) (D.f' j i) =
    pullback.fst (D.f' i j) (D.f' i k) ≫ if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.t i j h ≫ eqToHom ⋯

Tactic:
simp [*, reassoc_of% D.t_fac]

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
this :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      ((coequalizer.π f.toHom g.toHom ≫
              (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom).c.app
        (op U)))

Tactic:
PresheafedSpace.comp_c_app,

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      ((PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c.app
          (op U) ≫
        (coequalizer.π f.toHom g.toHom).c.app
          (op
            ((Opens.map
                  (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                        (Hom.toShHom g)).hom.base).obj
              (unop (op U))))))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e_a
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ IsOpenImmersion.lift U.ι f ⋯ = IsOpenImmersion.lift U.ι g ⋯

Tactic:
rw [← cancel_mono hU.isoSpec.hom, ← Spec.homEquiv.injective.eq_iff,
    ← cancel_mono φ, ← Spec.map_injective.eq_iff]

Goal state after:
case e_a
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ Spec.map (Spec.homEquiv (IsOpenImmersion.lift U.ι f ⋯ ≫ hU.isoSpec.hom) ≫ φ) =
    Spec.map (Spec.homEquiv (IsOpenImmersion.lift U.ι g ⋯ ≫ hU.isoSpec.hom) ≫ φ)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
R S : C
f : R ⟶ S
⊢ (preservesTerminalIso (pullback f)).hom = (isoMk (asIso (pullback.snd (𝟙 S) f)) ⋯).hom

Tactic:
exact toUnit_unique _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰✝ : X.OpenCover
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf : ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y
⊢ X ⟶ Y

Tactic:
refine inv 𝒰.ulift.fromGlued ≫ ?_

Goal state after:
X : Scheme
𝒰✝ : X.OpenCover
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf : ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y
⊢ (ulift 𝒰).gluedCover.glued ⟶ Y
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))
y : ↑↑(pullback (D.f i j) (D.f i k))
⊢ (ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) ((ConcreteCategory.hom (inv (D.t' k i j)).base) y) =
    (ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k) ≫ D.t i k).base) y

Tactic:
change (inv (D.t' k i j) ≫ π₁ k, i, j).base y = _

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))
y : ↑↑(pullback (D.f i j) (D.f i k))
⊢ (ConcreteCategory.hom (inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j)).base) y =
    (ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k) ≫ D.t i k).base) y
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ fst (𝒰.f i) (𝒰.f j) ≫ inv (snd f (𝒰.f i)) ≫ fst f (𝒰.f i) = snd (𝒰.f i) (𝒰.f j) ≫ inv (snd f (𝒰.f j)) ≫ fst f (𝒰.f j)

Tactic:
rw [← cancel_epi ((pullbackRightPullbackFstIso _ _ _).hom ≫ map (fst f (𝒰.f i) ≫ f)
      (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd _ _) (𝟙 _) (𝟙 _) (by simp) (by simp))]

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
H : ∀ (i : 𝒰.I₀), IsIso (snd f (𝒰.f i))
i j : 𝒰.I₀
⊢ ((pullbackRightPullbackFstIso f (𝒰.f j) (fst f (𝒰.f i))).hom ≫
        map (fst f (𝒰.f i) ≫ f) (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd f (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯) ≫
      fst (𝒰.f i) (𝒰.f j) ≫ inv (snd f (𝒰.f i)) ≫ fst f (𝒰.f i) =
    ((pullbackRightPullbackFstIso f (𝒰.f j) (fst f (𝒰.f i))).hom ≫
        map (fst f (𝒰.f i) ≫ f) (𝒰.f j) (𝒰.f i) (𝒰.f j) (snd f (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯) ≫
      snd (𝒰.f i) (𝒰.f j) ≫ inv (snd f (𝒰.f j)) ≫ fst f (𝒰.f j)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case a
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
z : ↥Z
⊢ (a ≫ Sigma.ι g i) z ∈ Scheme.Hom.opensRange (Sigma.ι g i) ⊓ Scheme.Hom.opensRange (Sigma.ι g j)

Tactic:
· exact ⟨⟨a.base z, rfl⟩, ⟨b.base z, by rw [← Scheme.Hom.comp_apply, h.w]⟩⟩

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

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

Tactic:
· simp_rw [Category.assoc]
          dsimp only [Functor.op, unop_op, Quiver.Hom.unop_op]
          rw [eqToHom_map (Opens.map _), eqToHom_op, eqToHom_trans]
          congr

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift 𝒰).I₀
⊢ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ =
    (Iso.refl (pullback ((Cover.ulift 𝒰).f i ≫ f) g)).hom ≫
      (gluing (Cover.ulift 𝒰) f g).ι ((Equiv.refl (Cover.ulift 𝒰).I₀) i) ≫
        (limit.isoLimitCone
            { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
              isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv

Tactic:
GlueData.openCover_I₀,

Goal state after:
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift 𝒰).I₀
⊢ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ =
    (Iso.refl (pullback ((Cover.ulift 𝒰).f i ≫ f) g)).hom ≫
      (gluing (Cover.ulift 𝒰) f g).ι ((Equiv.refl (Cover.ulift 𝒰).I₀) i) ≫
        (limit.isoLimitCone
            { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
              isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
hf : P f
i : 𝒰.I₀
⊢ P (pullback.snd f (𝒰.f i))

pp: case refine_2
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
⊢ P f

Tactic:
· apply hP _ (𝒰.f i)
    rw [← pullback.condition]
    exact IsZariskiLocalAtSource.comp hf _

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
⊢ P f
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: 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))
⊢ P f

Tactic:
by
  let := isLocal_affineProperty P
  rw [eq_targetAffineLocally P]
  classical
  intro V
  induction V using of_affine_open_cover U hU with
  | basicOpen U r h =>
    have := AffineTargetMorphismProperty.IsLocal.to_basicOpen (f ∣_ U.1) (U.1.topIso.inv r) h
    exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r)).mp this
  | openCover U s hs H =>
    apply AffineTargetMorphismProperty.IsLocal.of_basicOpenCover _
      (s.image (Scheme.Opens.topIso _).inv) (by simp [← Ideal.map_span, hs, Ideal.map_top])
    intro ⟨r, hr⟩
    obtain ⟨r, hr', rfl⟩ := Finset.mem_image.mp hr
    exact (Q.arrow_mk_iso_iff
      (morphismRestrictRestrictBasicOpen f _ r).symm).mp (H ⟨r, hr'⟩)
  | hU i => exact hU' i

Goal state after:
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
inst✝ : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [cocone, Functor.mapCocone_ι_app, Scheme.Hom.comp_toLRSHom,
      forgetToLocallyRingedSpace_map, ← GlueData.ι_isoLocallyRingedSpace_inv]

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
inst✝ : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)