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
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ IsIso ((f ≫ g).c.app (op (h.functor.obj U)))

Tactic:
dsimp only [AlgebraicGeometry.PresheafedSpace.comp_c_app, unop_op, Functor.op, comp_base,
      Opens.map_comp_obj]

Goal state after:
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
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ IsIso (g.c.app (op (h.functor.obj U)) ≫ f.c.app (op ((Opens.map g.base).obj (h.functor.obj U))))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ f ⁻¹ᵁ f ''ᵁ U = U

Tactic:
by
  apply Opens.ext
  simp [Set.preimage_image_eq _ f.isOpenEmbedding.injective]

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

Goal state before:
pp: case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : Opens ↑↑X
⊢ ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app
      (op x) =
    s.fst.c.app (op x)

Tactic:
| op x =>

Goal state after:
case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : Opens ↑↑X
⊢ ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app
      (op x) =
    s.fst.c.app (op x)
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
⊢ IsOpenImmersion (limit.π (cospan f g) one)

Tactic:
rw [← limit.w (cospan f g) WalkingCospan.Hom.inl]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ IsOpenImmersion (limit.π (cospan f g) left ≫ (cospan f g).map Hom.inl)
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 : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ IsLimit ((forget C).mapCone (pullbackConeOfLeft f g))

Tactic:
apply (IsLimit.postcomposeHomEquiv (diagramIsoCospan _) _).toFun
      refine (IsLimit.equivIsoLimit ?_).toFun (limit.isLimit (cospan f.base g.base))
      fapply Cone.ext
      · exact Iso.refl _
      change ∀ j, _ = 𝟙 _ ≫ _ ≫ _
      simp_rw [Category.id_comp]
      rintro (_ | _ | _) <;> symm
      · simp only [limit.cone_x, cospan_one, Functor.mapCone_π_app, PullbackCone.condition_one,
        forget_map,
          comp_base, cospan_left, cospan_right, Functor.comp_map, cospan_map_inl, cospan_map_inr,
          diagramIsoCospan_hom_app, PullbackCone.fst_limit_cone]
        tauto
      · exact Category.comp_id _
      · exact Category.comp_id _

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (pullback.snd (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g))) ''
      ⇑(ConcreteCategory.hom (pullback.fst f.base g.base)) ⁻¹' Set.univ =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

Tactic:
TopCat.pullback_snd_image_fst_preimage

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map g)) ⁻¹'
      ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map f)) '' Set.univ =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: 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.ContainsIdentities
inst✝¹ : P.RespectsIso
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
x : ↥Y
⊢ f ((inv f) x) = x

Tactic:
by simp [← Hom.comp_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
⊢ f x = g (snd p)

Tactic:
← hx,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
⊢ f (fst p) = g (snd p)
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)
⊢ IsIso
    ((PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g).hom ≫
      pullback.snd ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map g))

Tactic:
exact IsIso.comp_isIso' inferInstance <|
    PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset _ _ H'

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_3
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ∣_ W.ι ⁻¹ᵁ U ≫ (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom =
    (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

pp: case refine_4
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U).ι ≫ (Iso.refl ↑V).hom =
    (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

pp: case refine_5
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (W.ι ⁻¹ᵁ U).ι ≫ (Iso.refl ↑W).hom = (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE hU

pp: case refine_6
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ≫ (Iso.refl ↑W).hom = (Iso.refl ↑V).hom ≫ X.homOfLE hV

Tactic:
all_goals { simp [← cancel_mono (Scheme.Opens.ι _)] }

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: case mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
x✝ : (fun X ↦ X) Y
⊢ x✝ ∈ ⇑(hom π) ⁻¹' ⇑(hom π) '' U → x✝ ∈ U

Tactic:
rw [←
      show _ = π from
        h.comp_coconePointUniqueUpToIso_inv (coequalizerColimit f g).2
          WalkingParallelPair.one]

Goal state after:
case mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
x✝ : (fun X ↦ X) Y
⊢ x✝ ∈
      ⇑(hom
            ((coequalizerColimit f g).cocone.ι.app WalkingParallelPair.one ≫
              (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)) ⁻¹'
        ⇑(hom
              ((coequalizerColimit f g).cocone.ι.app WalkingParallelPair.one ≫
                (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)) ''
          U →
    x✝ ∈ U
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
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s t : (structureSheafInType R M).obj.obj (op U)
x✝ : ↥(unop (op V))
⊢ (Localizations.comapFun f ↑x✝) (↑s ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩ + ↑t ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩) =
    (Localizations.comapFun f ↑x✝) (↑s ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩) +
      (Localizations.comapFun f ↑x✝) (↑t ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩)

Tactic:
rw [map_add]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
⊢ X.zeroLocus ↑(⨅ i ∈ t, I i) = (⋃ i ∈ t, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ

Tactic:
refine ht.induction_on _ (by simp) fun {i t} hit ht IH ↦ ?_
  simp only [Set.mem_insert_iff, Set.iUnion_iUnion_eq_or_left, ← IH, ← zeroLocus_inf,
    Submodule.coe_inf, Set.union_assoc]
  congr!
  simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
S : Set ↑↑(D.V (i, j))
⊢ ⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) ''
      ⇑(ConcreteCategory.hom (pullback.fst (D.f i j) (D.f i k)).base) ⁻¹' S =
    ⇑(ConcreteCategory.hom (D.f i k).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) '' S

Tactic:
have eq₁ : _ = (π₁ i, j, k).base := PreservesPullback.iso_hom_fst (forget C) _ _

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
S : Set ↑↑(D.V (i, j))
eq₁ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.fst (D.f i j) (D.f i k)).base
⊢ ⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) ''
      ⇑(ConcreteCategory.hom (pullback.fst (D.f i j) (D.f i k)).base) ⁻¹' S =
    ⇑(ConcreteCategory.hom (D.f i k).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) '' S
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
i j : 𝒰.I₀
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) =
    pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      (pullbackSymmetry s.fst (𝒰.f i)).hom ≫ pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯

Tactic:
by
  simp [gluedLiftPullbackMap]

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
i j : 𝒰.I₀
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      pullback.snd s.fst (𝒰.f j)

Tactic:
by
  simp [gluedLiftPullbackMap]

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
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨l, fi, fj, fk, α, z, hα, hα₁, hα₂, rfl⟩ := exists_of_pullback_V_V F x

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
i j k : Shrink.{u, w} J
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
this :
  Scheme.Hom.stalkMap (coprod.inr ≫ coprodSpec R S) x ≫ inv (Scheme.Hom.stalkMap coprod.inr x) =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inr x)
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inr x)))

Tactic:
Scheme.Hom.stalkMap_congr_hom _ (Spec.map _) (coprodSpec_inr R S)

Goal state after:
case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
this :
  (((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inr x) =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inr x)
⊢ IsIso
    (Scheme.Hom.stalkMap (coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inr x)))
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
i : ι
⊢ P (IsOpenImmersion.lift (⨆ i, U i).ι f ⋯ ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i)

Tactic:
have heq : g ⁻¹ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = f ⁻¹ᵁ U i := by
      change (g ≫ (⨆ i, U i).ι) ⁻¹ᵁ U i = _
      simp [g]

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
i : ι
heq : g ⁻¹ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = f ⁻¹ᵁ U i
⊢ P (IsOpenImmersion.lift (⨆ i, U i).ι f ⋯ ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case hpostcomp
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y), targetAffineLocally P f → targetAffineLocally P (f ≫ e.hom)

Tactic:
introv H
    rintro ⟨U, hU : IsAffineOpen U⟩; dsimp
    have : IsAffine _ := hU.preimage_of_isIso e.hom
    rw [morphismRestrict_comp, P.cancel_right_of_respectsIso]
    exact H ⟨(Opens.map e.hom.base).obj U, hU.preimage_of_isIso e.hom⟩

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
i j : (glueData F).J
k : (Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).I₀
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [Opens.iSupOpenCover, V, Scheme.homOfLE_ι_assoc]

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
i j : (glueData F).J
k : (Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).I₀
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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)
j : WalkingMultispan (MultispanShape.prod D.J)
⊢ (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ limit.π (D.diagramOverOpen U) (op j) =
    𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op j)

Tactic:
| op j =>

Goal state after:
case op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j : WalkingMultispan (MultispanShape.prod D.J)
⊢ (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ limit.π (D.diagramOverOpen U) (op j) =
    𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op j)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case mpr
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
i j k : J
fi : k ⟶ i
fj : k ⟶ j
x : ↥(F.obj k)
⊢ (colimit.ι F i) ((F.map fi) x) = (colimit.ι F j) ((F.map fj) x)

Tactic:
simp only [← Scheme.Hom.comp_apply, colimit.w]

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : IsLocalization.Away x S
I J : Ideal R
hle : map (algebraMap R S) I ≤ map (algebraMap R S) J
hxJ : ∀ (y : R), x * y ∈ J → y ∈ J
⊢ I ≤ J

Tactic:
intro y hy

Goal state after:
R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : IsLocalization.Away x S
I J : Ideal R
hle : map (algebraMap R S) I ≤ map (algebraMap R S) J
hxJ : ∀ (y : R), x * y ∈ J → y ∈ J
y : R
hy : y ∈ I
⊢ y ∈ J
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
introv R _
  use {1}
  simp only [Set.mem_singleton_iff, forall_eq, Ideal.span_singleton_one, exists_const]
  let e : S ≃ₐ[R] (Localization.Away (1 : S)) :=
    (IsLocalization.atUnits S (Submonoid.powers 1) (by simp)).restrictScalars R
  have : IsLocalization.Away r (Localization.Away (1 : S)) :=
    IsLocalization.isLocalization_of_algEquiv (Submonoid.powers r) e
  rw [← IsScalarTower.algebraMap_eq]
  apply hPa _ r

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst f g)))

Tactic:
by
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11224): change `rw` to `erw`
  erw [← PreservesPullback.iso_inv_fst AffineScheme.forgetToScheme (AffineScheme.ofHom f)
      (AffineScheme.ofHom g)]
  rw [Scheme.Hom.comp_appTop, CommRingCat.hom_comp, hP'.cancel_right_isIso,
    AffineScheme.forgetToScheme_map]
  have := congr_arg Quiver.Hom.unop
      (PreservesPullback.iso_hom_fst AffineScheme.Γ.rightOp (AffineScheme.ofHom f)
        (AffineScheme.ofHom g))
  simp only [AffineScheme.Γ, Functor.rightOp_obj, Functor.comp_obj, Functor.op_obj, unop_comp,
    AffineScheme.forgetToScheme_obj, Scheme.Γ_obj, Functor.rightOp_map, Functor.comp_map,
    Functor.op_map, Quiver.Hom.unop_op, AffineScheme.forgetToScheme_map, Scheme.Γ_map] at this
  rw [← this, CommRingCat.hom_comp, hP'.cancel_right_isIso, ← pushoutIsoUnopPullback_inl_hom,
    CommRingCat.hom_comp, hP'.cancel_right_isIso]
  exact hP.pushout_inl hP' _ _ H

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

Goal state before:
pp: case refine_1
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) x) = 0

Tactic:
have H : (X.presheaf.map (homOfLE _).op) x = 0 := H

Goal state after:
case refine_1
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H✝ : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) x) = 0
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : Ideal R
hp : p ∈ ⊥.minimalPrimes
⊢ ⨅ J ∈ ⊥.minimalPrimes, J.height = 0

Tactic:
simp only [ENat.iInf_eq_zero]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : Ideal R
hp : p ∈ ⊥.minimalPrimes
⊢ ∃ i, ∃ (_ : i ∈ ⊥.minimalPrimes), i.height = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ P (f ≫ U.ι)

Tactic:
IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := P) V

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ ∀ (i : ↑Us), P ((V i).ι ≫ f ≫ U.ι)

case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ iSup V = ⊤
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ I.ideal V ≤ Ideal.comap (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal U)

Tactic:
by
  rw [← Ideal.map_le_iff_le_comap, ← I.map_ideal h]

Goal state after: