mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
A : Type u_6
C : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalNonAssocSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : StarRing A
inst✝⁵ : StarModule R A
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : StarAddMonoid C
inst✝¹ : StarModule R C
inst✝ : CoalgebraStruct R C
h : star (toConv comul) = toConv (↑(TensorProduct.comm R C C) ∘ₗ comul)
f g : WithConv (C →ₗ[R] A)
⊢ toConv
      (mul' R A ∘ₗ
        ↑(TensorProduct.comm R A A) ∘ₗ
          TensorProduct.map (star f).ofConv (star g).ofConv ∘ₗ ↑(TensorProduct.comm R C C) ∘ₗ comul) =
    toConv (mul' R A ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv ∘ₗ comul)

Tactic:
← comp_assoc _ _ (map _ _),

Goal state after:
R : Type u_5
A : Type u_6
C : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalNonAssocSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : StarRing A
inst✝⁵ : StarModule R A
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : StarAddMonoid C
inst✝¹ : StarModule R C
inst✝ : CoalgebraStruct R C
h : star (toConv comul) = toConv (↑(TensorProduct.comm R C C) ∘ₗ comul)
f g : WithConv (C →ₗ[R] A)
⊢ toConv
      (mul' R A ∘ₗ
        ↑(TensorProduct.comm R A A) ∘ₗ
          (TensorProduct.map (star f).ofConv (star g).ofConv ∘ₗ ↑(TensorProduct.comm R C C)) ∘ₗ comul) =
    toConv (mul' R A ∘ₗ TensorProduct.map (star g).ofConv (star f).ofConv ∘ₗ comul)
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).map
            (X.ofRestrict h).c).app
        (op V) ≫
      (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv) (X.restrict h).presheaf).app
          (op V) ≫
        colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op ⋙ X.presheaf)
          ((h.functorNhds x).op.obj ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)))

Tactic:
erw [← X.presheaf.map_comp_assoc]

Goal state after:
case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    X.presheaf.map
        ((⋯.adjunction.counit.app
              (unop ((OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op.obj (op V)))).op ≫
          h.functor.op.map ((NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv).app (op V))) ≫
      colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op ⋙ X.presheaf)
        ((h.functorNhds x).op.obj ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
⊢ g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf = g₂.c

Tactic:
ext V
    have hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V := by
      ext1
      exact Set.preimage_image_eq _ hf.injective
    have :
      IsIso (hf.isOpenMap.adjunction.counit.app (unop (op (hf.functor.obj V)))) :=
        NatIso.isIso_app_of_isIso
          (whiskerLeft hf.functor hf.isOpenMap.adjunction.counit) V
    have := PresheafedSpace.congr_app eq (op (hf.functor.obj V))
    rw [PresheafedSpace.comp_c_app, PresheafedSpace.comp_c_app,
      PresheafedSpace.ofRestrict_c_app, Category.assoc, cancel_epi] at this
    have h : _ ≫ _ = _ ≫ _ ≫ _ :=
      congr_arg (fun f => (X.restrict hf).presheaf.map (eqToHom hV).op ≫ f) this
    simp only [g₁.c.naturality, g₂.c.naturality_assoc] at h
    simp only [eqToHom_op, eqToHom_map, eqToHom_trans,
      ← IsIso.comp_inv_eq, inv_eqToHom, Category.assoc] at h
    simpa using h

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

Goal state before:
pp: J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ m.base = colimit.desc (F ⋙ forget C) ((forget C).mapCocone s)

Tactic:
apply colimit.hom_ext fun j => ?_

Goal state after:
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
⊢ colimit.ι (F ⋙ forget C) j ≫ m.base =
    colimit.ι (F ⋙ forget C) j ≫ colimit.desc (F ⋙ forget C) ((forget C).mapCocone s)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (𝟙
          ((sheafedSpaceObj T).presheaf.obj
            ((TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).hom.base).op.obj (op U✝)))))
      ((CommRingCat.Hom.hom
          (CommRingCat.ofHom
            (comap ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f)) U✝
              ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj U✝) ⋯)))
        x✝) =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c.app (op U✝))) x✝

Tactic:
comap_comp

Goal state after:
case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (𝟙
          ((sheafedSpaceObj T).presheaf.obj
            ((TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).hom.base).op.obj (op U✝)))))
      ((CommRingCat.Hom.hom
          (CommRingCat.ofHom
            ((comap (CommRingCat.Hom.hom g) ?h.V ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj U✝) ?h.hVW).comp
              (comap (CommRingCat.Hom.hom f) U✝ ?h.V ?h.hUV))))
        x✝) =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c.app (op U✝))) x✝

case h.V
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ TopologicalSpace.Opens ↑(PrimeSpectrum.Top ↑S)

case h.hUV
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ ∀ p ∈ ?h.V, PrimeSpectrum.comap (CommRingCat.Hom.hom f) p ∈ U✝

case h.hVW
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ ∀ p ∈ (TopologicalSpace.Opens.map (topMap (f ≫ g))).obj U✝, PrimeSpectrum.comap (CommRingCat.Hom.hom g) p ∈ ?h.V
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
f : ↑Γ(Spec R, ⊤)
⊢ (Spec R).basicOpen f = PrimeSpectrum.basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso R).hom) f)

Tactic:
convert! basicOpen_eq_of_affine ((Scheme.ΓSpecIso R).hom f)

Goal state after:
R : CommRingCat
f : ↑Γ(Spec R, ⊤)
⊢ f = (ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ((ConcreteCategory.hom (Scheme.ΓSpecIso R).hom) f)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
f : ↑Γ(Spec R, ⊤)
⊢ f = (ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ((ConcreteCategory.hom (Scheme.ΓSpecIso R).hom) f)

Tactic:
exact (Iso.hom_inv_id_apply (Scheme.ΓSpecIso R) f).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥↑U
hxW : x ∈ W
⊢ (↑U).presheaf.germ W x hxW = X.presheaf.germ (U.ι ''ᵁ W) ↑x ⋯ ≫ Hom.stalkMap U.ι x

Tactic:
convert! (Scheme.Hom.germ_stalkMap U.ι (U.ι ''ᵁ W) x ⟨_, hxW, rfl⟩).symm

Goal state after:
case e'_2
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥↑U
hxW : x ∈ W
e_1✝ : ((↑U).presheaf.obj (op W) ⟶ (↑U).presheaf.stalk x) = (X.presheaf.obj (op (U.ι ''ᵁ W)) ⟶ (↑U).presheaf.stalk x)
⊢ (↑U).presheaf.germ W x hxW = Hom.app U.ι (U.ι ''ᵁ W) ≫ (↑U).presheaf.germ (U.ι ⁻¹ᵁ U.ι ''ᵁ W) x ⋯
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))
⊢ CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)))
            ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))) ≫
        f =
      X.toToΓSpecMapBasicOpen r ↔
    f = X.toΓSpecCApp r

Tactic:
refine ConcreteCategory.ext_iff.trans ?_

Goal state after:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))
⊢ ConcreteCategory.hom
        (CommRingCat.ofHom
            (algebraMap (↑(Γ.obj (op X)))
              ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))) ≫
          f) =
      ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r) ↔
    f = X.toΓSpecCApp r
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
⊢ Scheme.Hom.app hU.fromSpec V =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Tactic:
have : U.ι ⁻¹ᵁ V = ⊤ := eq_top_iff.mpr fun x _ ↦ h x.2

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ Scheme.Hom.app hU.fromSpec V =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ X.presheaf.map (homOfLE ⋯).op ≫
      (↑U).presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.app hU.isoSpec.inv ⊤ ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Tactic:
← Scheme.Hom.appTop,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ X.presheaf.map (homOfLE ⋯).op ≫
      (↑U).presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.appTop hU.isoSpec.inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : X ⟶ Y
H : IsOpenImmersion f
⊢ IsAffineOpen (f ''ᵁ U)

Tactic:
f.isAffineOpen_iff_of_isOpenImmersion

Goal state after:
X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : X ⟶ Y
H : IsOpenImmersion f
⊢ IsAffineOpen U
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ⁻¹ᵁ X.basicOpen f = (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f)

Tactic:
by
  rw [Scheme.preimage_basicOpen, hU.fromSpec_app_self]
  exact Scheme.basicOpen_res_eq _ _ (eqToHom hU.fromSpec_preimage_self).op

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: ⊢ IsIso adjunction.counit

Tactic:
apply +allowSynthFailures NatIso.isIso_of_isIso_app

Goal state after:
⊢ ∀ (X : CommRingCatᵒᵖ), IsIso (adjunction.counit.app X)
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' j i i = pullback.fst (D.f j i) (D.f j i) ≫ D.t j i ≫ inv (pullback.snd (D.f i i) (D.f i j))

Tactic:
rw [← Category.assoc, ← D.t_fac]

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' j i i = (D.t' j i i ≫ pullback.snd (D.f i i) (D.f i j)) ≫ inv (pullback.snd (D.f i i) (D.f i j))
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' i j i = pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ inv (pullback.snd (D.f j i) (D.f j i))

Tactic:
rw [← Category.assoc, ← D.t_fac]

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' i j i = (D.t' i j i ≫ pullback.snd (D.f j i) (D.f j i)) ≫ inv (pullback.snd (D.f j i) (D.f j i))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ hU.fromSpec (hU.primeIdealOf x) = ↑x

Tactic:
dsimp only [IsAffineOpen.fromSpec, Subtype.coe_mk, IsAffineOpen.primeIdealOf]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (hU.isoSpec.inv ≫ U.ι) (hU.isoSpec.hom x) = ↑x
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (LaxMonoidal.μ (pullback f) R S) ≫ pullback.fst (R ⊗ S).hom f ≫ pullback.fst R.hom S.hom =
    pullback.fst ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst R.hom f

Tactic:
rw [Monoidal.μ_of_cartesianMonoidalCategory,
    ← cancel_epi (prodComparisonIso (Over.pullback f) R S).hom.left, ← Over.comp_left_assoc,
    Iso.hom_inv_id]
  simp [CartesianMonoidalCategory.prodComparison, fst]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x : ↥X
y : ↥(𝒰.X (idx 𝒰 x))
h : (𝒰.f (idx 𝒰 x)) y = x
⊢ ∃ a, (fromGlued 𝒰) a = x

Tactic:
use 𝒰.gluedCover.ι (𝒰.idx x) y

Goal state after:
case h
X : Scheme
𝒰 : X.OpenCover
x : ↥X
y : ↥(𝒰.X (idx 𝒰 x))
h : (𝒰.f (idx 𝒰 x)) y = x
⊢ (fromGlued 𝒰) (((gluedCover 𝒰).ι (idx 𝒰 x)) y) = x
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
Y : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ
X : WalkingMultispan (MultispanShape.prod D.J)
f' : op X ⟶ Y
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop Y) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map f'

Tactic:
induction Y with | op Y => ?_

Goal state after:
case op.op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
X Y : WalkingMultispan (MultispanShape.prod D.J)
f' : op X ⟶ op Y
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop (op Y)) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map f'
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_1
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' : Scheme
⊢ ∀ {Y' : Scheme} (αX : X' ⟶ X) (αY : Y' ⟶ Y)
    (f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt),
    αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = (BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f →
      αY ≫ (BinaryCofan.mk coprod.inl coprod.inr).inr = (BinaryCofan.mk coprod.inl coprod.inr).inr ≫ f →
        IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inl αX f (BinaryCofan.mk coprod.inl coprod.inr).inl ∧
          IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inr αY f (BinaryCofan.mk coprod.inl coprod.inr).inr

Tactic:
Y'

Goal state after:
case refine_1
ι : 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),
    αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = (BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f →
      αY ≫ (BinaryCofan.mk coprod.inl coprod.inr).inr = (BinaryCofan.mk coprod.inl coprod.inr).inr ≫ f →
        IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inl αX f (BinaryCofan.mk coprod.inl coprod.inr).inl ∧
          IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inr αY f (BinaryCofan.mk coprod.inl coprod.inr).inr
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case inv_hom_id
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
⊢ autoParam
    (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ =
      𝟙 (pullback (𝒰.f i ≫ f) g))
    Iso.inv_hom_id._autoParam

Tactic:
· apply pullback.hom_ext
    · simp_rw [Category.assoc, pullback.lift_fst, pullback.lift_snd, Category.id_comp]
    · simp [p2]

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : P.RespectsRight IsOpenImmersion
U : ↥X → Y.Opens
V : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
⊢ P f

Tactic:
IsZariskiLocalAtSource.iff_of_iSup_eq_top (fun x : X ↦ V x) (P := P)

Goal state after:
P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : P.RespectsRight IsOpenImmersion
U : ↥X → Y.Opens
V : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
⊢ ∀ (i : ↥X), P ((V i).ι ≫ f)

P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : P.RespectsRight IsOpenImmersion
U : ↥X → Y.Opens
V : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
⊢ ⨆ x, V x = ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
e : pullback (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅
  pullback (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
    pullbackRightPullbackFstIso f g ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
      asIso
          (pullback.map ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g
            (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g
            (𝟙 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        (pullbackRightPullbackFstIso (S.affineCover.f i) g (pullback.snd f (S.affineCover.f i))).symm
this :
  e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) =
    pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i)
⊢ P (pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g))

Tactic:
apply HasAffineProperty.pullback_fst_of_right hP'

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
e : pullback (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅
  pullback (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) := ⋯
this :
  e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) =
    pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i)
⊢ Q (pullback.fst (S.affineCover.f i) g)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hs : Ideal.span s = ⊤
h : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
⊢ s ⊆ ↑(Ideal.span {g | P ((algebraMap S (Localization.Away g)).comp f)})

Tactic:
intro g hg

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
s : Set S
hs : Ideal.span s = ⊤
h : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
g : S
hg : g ∈ s
⊢ g ∈ ↑(Ideal.span {g | P ((algebraMap S (Localization.Away g)).comp f)})
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case of_sSup_eq_top
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (f ∣_ U i)
X' : Scheme
⊢ ∀ ⦃Y' : Scheme⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → P f'

Tactic:
Y'

Goal state after:
case of_sSup_eq_top
P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P.universally (f ∣_ U i)
X' Y' : Scheme
⊢ ∀ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → P f'