mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Pullback

Goal state before:
pp: C : Type v₁
inst✝¹¹ : SmallCategory C
D : Type v₁
inst✝¹⁰ : SmallCategory D
G : C ⥤ D
A : Type u₁
inst✝⁹ : Category.{v₁, u₁} A
J : GrothendieckTopology C
K : GrothendieckTopology D
FA : A → A → Type u_1
CA : A → Type v₁
inst✝⁸ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁷ : ConcreteCategory A FA
inst✝⁶ : PreservesLimits (forget A)
inst✝⁵ : HasColimits A
inst✝⁴ : HasLimits A
inst✝³ : PreservesFilteredColimits (forget A)
inst✝² : (forget A).ReflectsIsomorphisms
inst✝¹ : G.IsContinuous J K
inst✝ : RepresentablyFlat G
⊢ PreservesFiniteLimits (G.sheafPullback A J K)

Tactic:
apply sheafPullbackConstruction.preservesFiniteLimits

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: 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
⊢ (X.restrictStalkIso h x).inv = Hom.stalkMap (X.ofRestrict h) x

Tactic:
refine colimit.hom_ext fun V => ?_
  induction V with | op V => ?_
  let i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
    homOfLE (Set.image_preimage_subset f _)
  erw [Iso.comp_inv_eq, colimit.ι_map_assoc, colimit.ι_map_assoc, colimit.ι_pre]
  simp_rw [Category.assoc]
  erw [colimit.ι_pre ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf)
      (h.functorNhds x).op]
  erw [← X.presheaf.map_comp_assoc]
  exact (colimit.w ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf) i.op).symm

Goal state after:
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
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
⊢ IsIso ((f ≫ g).c.app (op (⋯.functor.obj U)))

Tactic:
by
    generalize_proofs h
    dsimp only [AlgebraicGeometry.PresheafedSpace.comp_c_app, unop_op, Functor.op, comp_base,
      Opens.map_comp_obj]
    apply IsIso.comp_isIso'
    · exact c_iso' g ((opensFunctor f).obj U) (by ext; simp)
    · apply c_iso' f U
      ext1
      dsimp only [Opens.map_coe, IsOpenMap.coe_functor_obj, comp_base, TopCat.coe_comp]
      rw [Set.image_comp, Set.preimage_image_eq _ hg.base_open.injective]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ (app g U ≫ Y.presheaf.map (homOfLE e₁).op) ≫ app f V ≫ X.presheaf.map (homOfLE e₂).op =
    (app g U ≫ app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
rw [Category.assoc, f.naturality_assoc, ← Functor.map_comp]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ app g U ≫ app f (g ⁻¹ᵁ U) ≫ X.presheaf.map (((Opens.map f.base).map (homOfLE e₁).op.unop).op ≫ (homOfLE e₂).op) =
    (app g U ≫ app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).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 ∈ p.asIdeal.primeCompl,
    IsUnit
      ((algebraMap ↑R
          ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                  (structureSheaf ↑S).obj).stalk
              p))
        x)

pp: case h₂
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀
    (y :
      ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).stalk
          p)),
    ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

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 [algebraMap_pushforward_stalk, toPushforwardStalk_comp]
    change IsUnit ((TopCat.Presheaf.stalkFunctor CommRingCat p).map
      (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap ↑R ↑S))).hom.c _)
    exact (IsLocalization.map_units ((structureSheaf R).presheaf.stalk p) ⟨x, hx⟩).map _

Goal state after:
case h₂
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀
    (y :
      ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).stalk
          p)),
    ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

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
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: case h
P✝ P : MorphismProperty Scheme
inst✝¹ : IsJointlySurjectivePreserving P
inst✝ : P.IsStableUnderBaseChange
ι : Type (u + 1)
S : Scheme
X : ι → Scheme
f : (i : ι) → X i ⟶ S
hf : (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑(f i)) ∧ ∀ (i : ι), P (f i)
Y : Scheme
g : Y ⟶ S
T : ι → Scheme
p₁ : (i : ι) → T i ⟶ Y
p₂ : (i : ι) → T i ⟶ X i
H : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
x : ↥Y
i : ι
y : ↥(X i)
hy : (f i) y = g x
this : HasPullback g (f i)
w : ↥(pullback g (f i))
hw : (pullback.fst g (f i)) w = x
⊢ (p₁ i) (⋯.isoPullback.inv w) = x

Tactic:
simpa [← Scheme.Hom.comp_apply]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom g.base)
⊢ lift g f ⋯ ≫ lift f g ⋯ = 𝟙 X

Tactic:
by rw [← cancel_mono f]; simp

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f g ⋙ forget) (PresheafedSpace.forget C)

Tactic:
by
      have : PreservesLimit
        (cospan ((cospan f g ⋙ forget).map Hom.inl)
          ((cospan f g ⋙ forget).map Hom.inr)) (PresheafedSpace.forget C) := by
        dsimp
        infer_instance
      apply preservesLimit_of_iso_diagram _ (diagramIsoCospan _).symm

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

Goal state before:
pp: case refine_2
K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
⊢ ∀ (i : { I₀ := J, X := obj, f := map }.I₀), P ({ I₀ := J, X := obj, f := map }.f i)

Tactic:
simp_rw [h, MorphismProperty.cancel_left_of_respectsIso]
      intro i
      exact 𝒰.map_prop _

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
e : Set.range ⇑f = Set.range ⇑g
⊢ lift g f ⋯ ≫ lift f g ⋯ = 𝟙 X

Tactic:
by rw [← cancel_mono f]; simp

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝ : ι
this✝ :
  colimit.ι (F ⋙ forget C) { as := as✝ } =
    (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := { as := as✝ }.as } =
    TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        ((((Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
                TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as) ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv) ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫
          (preservesColimitIso (forget C) F).inv))

Tactic:
simp_rw [TopCat.isOpenEmbedding_iff_comp_isIso, (TopCat.isOpenEmbedding_iff_isIso_comp)]

Goal state after:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝ : ι
this✝ :
  colimit.ι (F ⋙ forget C) { as := as✝ } =
    (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := { as := as✝ }.as } =
    TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) as✝))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
⊢ { l //
    l ≫ (pullbackConeOfLeft f g).fst = s.fst ∧
      l ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
          m ≫ (pullbackConeOfLeft f g).fst = s.fst → m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = l }

Tactic:
refine ⟨LocallyRingedSpace.Hom.mk (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift
        f.1 g.1 (PullbackCone.mk _ _ (congr_arg LocallyRingedSpace.Hom.toHom s.condition))) ?_,
      LocallyRingedSpace.Hom.ext'
        (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_fst f.1 g.1 _),
      LocallyRingedSpace.Hom.ext'
          (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift_snd f.1 g.1 _), ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
⊢ ∀ (x : ↑↑s.pt.toPresheafedSpace),
    IsLocalHom
      (CommRingCat.Hom.hom
        (PresheafedSpace.Hom.stalkMap
          (PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
            (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯))
          x))

case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
s : PullbackCone f g
⊢ ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
    m ≫ (pullbackConeOfLeft f g).fst = s.fst →
      m ≫ (pullbackConeOfLeft f g).snd = s.snd →
        m =
          {
            toHom :=
              PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftLift f.toHom g.toHom
                (PullbackCone.mk s.fst.toHom s.snd.toHom ⋯),
            prop := ?refine_1 }
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
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
r : ↥(sectionsSubalgebra R U)
a : (x : ↥U) → Localizations M ↑x
ha : a ∈ (sectionsSubmodule M U).carrier
x : ↥U
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal R M).pred fun x ↦ (r • a) (i x)

Tactic:
by
    obtain ⟨V, hxV, hVU, rx, rs, hr⟩ := r.2 x
    obtain ⟨W, hxW, hWU, ax, as, ha⟩ := ha x
    refine ⟨V ⊓ W, ⟨hxV, hxW⟩, homOfLE (inf_le_left.trans hVU.le), rx • ax, as * rs, fun y ↦ ?_⟩
    obtain ⟨hrsy, hry⟩ := hr ⟨y.1, y.2.1⟩
    obtain ⟨hasy, hay⟩ := ha ⟨y.1, y.2.2⟩
    exact ⟨y.1.asIdeal.primeCompl.mul_mem hasy hrsy, congr($hry • $hay)⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ Nonempty ↥↑U ↔ (↑U).Nonempty

Tactic:
by
  simp only [toScheme_carrier, SetLike.coe_sort_coe, nonempty_subtype]
  rfl

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
f : R
⊢ ∀ (x : ↥(Submonoid.powers f)),
    IsUnit ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))) ↑x)

Tactic:
simp only [Subtype.forall]

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
f : R
⊢ ∀ a ∈ Submonoid.powers f,
    IsUnit ((algebraMap R (Module.End R ((structureSheafInType R M).obj.obj (op (basicOpen f))))) a)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ s ^ n •
      (IsLocalizedModule.lift (Submonoid.powers s) (LocalizedModule.mkLinearMap (Submonoid.powers s) M)
          (toOpenₗ R M (basicOpen s)) ⋯)
        (LocalizedModule.mk f ⟨s ^ n, ⋯⟩) =
    s ^ n • const f (s ^ n) (basicOpen s) ⋯

Tactic:
rw [← map_smul, LocalizedModule.smul'_mk, ← Submonoid.mk_smul (S := .powers s) _ ⟨n, rfl⟩,
    LocalizedModule.mk_cancel, ← LocalizedModule.mkLinearMap_apply, IsLocalizedModule.lift_apply,
    smul_const]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : R
f : M
n : ℕ
⊢ (toOpenₗ R M (basicOpen s)) f = const (s ^ n • f) (s ^ n) (basicOpen s) ⋯
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ ↑((resLE f U V e) x) = f ↑x

Tactic:
by
  simp [resLE, morphismRestrict_base]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: ⊢ PreservesLimits forgetToScheme

Tactic:
apply +allowSynthFailures @preservesLimits_of_natIso _ _ _ _ _ _
    (Functor.isoWhiskerRight equivCommRingCat.unitIso forgetToScheme).symm

Goal state after:
⊢ PreservesLimitsOfSize.{u_1, u_1, u_1, u_1, u_1 + 1, u_1 + 1}
    ((equivCommRingCat.functor ⋙ equivCommRingCat.inverse) ⋙ forgetToScheme)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⋂ i ∈ s, ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ

Tactic:
← Set.preimage_iInter₂,

Goal state after:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ⋂ i ∈ s, (basicOpen i).carrierᶜ
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
⊢ IsUnit ((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) f)

Tactic:
have := (isUnit_toStalk x f hf).map (algebraMap _
    (Module.End ((structurePresheafInCommRingCat R).stalk x)
      ((structurePresheafInModuleCat R M).stalk x)))

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
this :
  IsUnit
    ((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
        (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
      ((ConcreteCategory.hom (toStalk R x)) f))
⊢ IsUnit ((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) f)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
⊢ toStalkₗ' R M x ≫ stalkToLocalizationₗ R M x = ModuleCat.ofHom (LocalizedModule.mkLinearMap x.asIdeal.primeCompl M)

Tactic:
rw [toStalkₗ', Category.assoc, germ_stalkToLocalizationₗ]; rfl

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i j : D.J
x : ↑D.glued
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j)) →
    x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))

pp: case mpr
D : GlueData
i j : D.J
x : ↑D.glued
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i)) →
    x ∈ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j))

Tactic:
· rintro ⟨⟨x₁, eq₁⟩, ⟨x₂, eq₂⟩⟩
    obtain ⟨y, e₁, -⟩ := (D.ι_eq_iff_rel _ _ _ _).mp (eq₁.trans eq₂.symm)
    · subst eq₁
      exact ⟨y, by simp [e₁]⟩

Goal state after:
case mpr
D : GlueData
i j : D.J
x : ↑D.glued
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i)) →
    x ∈ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j))
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U ⊆ Set.range ⇑(ConcreteCategory.hom (D.f j i))

Tactic:
rw [← D.preimage_range i j]

Goal state after:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U ⊆
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' Set.range ⇑(ConcreteCategory.hom (D.ι i))
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U =
    (fun x ↦
        (⇑(ConcreteCategory.hom (D.f i j)) ∘ ⇑(ConcreteCategory.hom (D.t j i)))
          ((ConcreteCategory.hom (D.t i j)) x)) ⁻¹'
      U

Tactic:
change _ = (D.t i j ≫ D.t j i ≫ _) ⁻¹' _

Goal state after:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U = ⇑(ConcreteCategory.hom (D.t i j ≫ D.t j i ≫ D.f i j)) ⁻¹' U
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ PreservesColimit F forgetToSheafedSpace

Tactic:
by
    -- Porting note: was `apply preservesColimitOfIsoDiagram ...` and the proof that preservation
    -- of colimit is provided later
    suffices PreservesColimit (parallelPair (F.map WalkingParallelPairHom.left)
        (F.map WalkingParallelPairHom.right)) forgetToSheafedSpace from
      preservesColimit_of_iso_diagram _ (diagramIsoParallelPair F).symm
    apply preservesColimit_of_preserves_colimit_cocone (coequalizerCoforkIsColimit _ _)
    apply (isColimitMapCoconeCoforkEquiv _ _).symm _
    dsimp only [forgetToSheafedSpace]
    exact coequalizerIsCoequalizer _ _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : BinaryFan 0 X
m : s.pt ⟶ X
x✝ : m ≫ 0 = s.fst
h₂ : m ≫ 𝟙 X = s.snd
⊢ m = s.snd

Tactic:
by simpa using h₂

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : BinaryCofan 0 X
m : X ⟶ s.pt
x✝ : 0 ≫ m = s.inl
h₂ : 𝟙 X ≫ m = s.inr
⊢ m = s.inr

Tactic:
by simpa using h₂

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ IsOpenMap ⇑(fromGlued 𝒰)

Tactic:
intro U hU
  rw [isOpen_iff_forall_mem_open]
  intro x hx
  rw [𝒰.gluedCover.isOpen_iff] at hU
  use 𝒰.fromGlued '' U ∩ Set.range (𝒰.f (𝒰.idx x))
  use Set.inter_subset_left
  constructor
  · rw [← Set.image_preimage_eq_inter_range]
    apply (𝒰.f (𝒰.idx x)).isOpenEmbedding.isOpenMap
    convert! hU (𝒰.idx x) using 1
    simp only [← ι_fromGlued, gluedCover_U, Hom.comp_base, TopCat.hom_comp, ContinuousMap.coe_comp,
      Set.preimage_comp]
    congr! 1
    exact Set.preimage_image_eq _ 𝒰.fromGlued_injective
  · exact ⟨hx, 𝒰.covers x⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
i : ι
x : ↥(f i)
⊢ (sigmaMk f) ⟨i, x⟩ = (Sigma.ι f i) x

Tactic:
change ((TopCat.sigmaCofan (fun x ↦ (f x).toTopCat)).inj i ≫
    (colimit.isoColimitCocone ⟨_, TopCat.sigmaCofanIsColimit _⟩).inv ≫ _) x =
      Scheme.forgetToTop.map (Sigma.ι f i) x

Goal state after:
ι : Type u
f : ι → Scheme
i : ι
x : ↥(f i)
⊢ (ConcreteCategory.hom
        ((TopCat.sigmaCofan fun x ↦ (f x).toTopCat).inj i ≫
          (colimit.isoColimitCocone
                { cocone := TopCat.sigmaCofan fun x ↦ (f x).toTopCat,
                  isColimit := TopCat.sigmaCofanIsColimit fun x ↦ (f x).toTopCat }).inv ≫
            (PreservesCoproduct.iso Scheme.forgetToTop f).symm.hom))
      x =
    (ConcreteCategory.hom (Scheme.forgetToTop.map (Sigma.ι f i))) x
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
x : ↥X
⊢ (coprodMk X Y) (Sum.inl x) = coprod.inl x

Tactic:
change ((TopCat.binaryCofan X Y).inl ≫
    (colimit.isoColimitCocone ⟨_, TopCat.binaryCofanIsColimit _ _⟩).inv ≫ _) x =
      Scheme.forgetToTop.map coprod.inl x

Goal state after:
X Y : Scheme
x : ↥X
⊢ (ConcreteCategory.hom
        (((↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace).inl ≫
          (colimit.isoColimitCocone
                { cocone := (↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace,
                  isColimit := (↑X.toPresheafedSpace).binaryCofanIsColimit ↑Y.toPresheafedSpace }).inv ≫
            (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom))
      x =
    (ConcreteCategory.hom (Scheme.forgetToTop.map coprod.inl)) x
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
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      pullback.fst s.fst (𝒰.f i) ≫ s.snd =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      pullback.fst s.fst (𝒰.f j) ≫ s.snd

Tactic:
exact pullback.condition_assoc _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
h₁ : ι₁ ''ᵁ ι₁ ⁻¹ᵁ U ⊔ ι₂ ''ᵁ ι₂ ⁻¹ᵁ U = U
⊢ ι₁ ''ᵁ ι₁ ⁻¹ᵁ U ⊓ ι₂ ''ᵁ ι₂ ⁻¹ᵁ U = ⊥

Tactic:
by
    simp_rw [Scheme.Hom.image_preimage_eq_opensRange_inf]
    rw [← inf_inf_distrib_right, (isCompl_opensRange_inl_inr X Y).inf_eq_bot, bot_inf_eq]

Goal state after: