mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: case mpr.refine_3
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
e₁ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) =
    (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2

Tactic:
← TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd

Goal state after:
case mpr.refine_3
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
e₁ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) =
    (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x))
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
⊢ ∃ ι x a b,
    ∃ (ibU : ∀ (i : ι), basicOpen (b i) ≤ U),
      U ≤ ⨆ i, basicOpen (b i) ∧
        (∀ (i j : ι), b j • a i = b i • a j) ∧
          ∀ (i : ι),
            (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s =
              const (a i) (b i) (basicOpen (b i)) ⋯

Tactic:
have (i j : _) : LocalizedModule.mk (g i • f j) ⟨g i * g j, Submonoid.mem_powers _⟩ =
      LocalizedModule.mk (g j • f i) ⟨g i * g j, Submonoid.mem_powers _⟩ := by
    refine toBasicOpenₗ_injective (g i * g j) ?_
    simp only [toBasicOpenₗ_mk]
    have := H i
    trans (structureSheafInType R M).obj.map (homOfLE ?_).op s
    · refine .trans (Subtype.ext <| funext fun a ↦ ?_) congr((structureSheafInType R M).obj.map
        (homOfLE ((PrimeSpectrum.basicOpen_mul (g i) (g j)).trans_le inf_le_right)).op $(H j))
      exact LocalizedModule.mk_eq.mpr ⟨1, by simp [Submonoid.smul_def, ← smul_assoc]; ring_nf⟩
    · refine congr((structureSheafInType R M).obj.map (homOfLE ((PrimeSpectrum.basicOpen_mul (g i)
        (g j)).trans_le inf_le_left)).op $(H i)).symm.trans (Subtype.ext <| funext fun a ↦ ?_)
      exact LocalizedModule.mk_eq.mpr ⟨1, by simp [Submonoid.smul_def, ← smul_assoc]⟩
    · exact ((PrimeSpectrum.basicOpen_mul (g i) (g j)).trans_le inf_le_right).trans (igU _)

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
this : ∀ (i j : ↥U), LocalizedModule.mk (g i • f j) ⟨g i * g j, ⋯⟩ = LocalizedModule.mk (g j • f i) ⟨g i * g j, ⋯⟩
⊢ ∃ ι x a b,
    ∃ (ibU : ∀ (i : ι), basicOpen (b i) ≤ U),
      U ≤ ⨆ i, basicOpen (b i) ∧
        (∀ (i j : ι), b j • a i = b i • a j) ∧
          ∀ (i : ι),
            (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s =
              const (a i) (b i) (basicOpen (b i)) ⋯
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
W : (↑(f ⁻¹ᵁ U)).Opens
e : W ≤ (f ∣_ U) ⁻¹ᵁ V
⊢ Scheme.Hom.appLE (f ∣_ U) V W e = Scheme.Hom.appLE f (U.ι ''ᵁ V) ((f ⁻¹ᵁ U).ι ''ᵁ W) ⋯

Tactic:
by
  rw [Scheme.Hom.appLE, morphismRestrict_app', Scheme.Opens.toScheme_presheaf_map,
    Scheme.Hom.appLE_map]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : TopologicalSpace.Opens ↥X
x : ↥X
hU : x ∈ ↑U
S : Set ↥X
hS : S ∈ {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}
hxS : x ∈ S
hSU : S ⊆ ↑U
⊢ ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U

Tactic:
refine ⟨⟨S, X.affineBasisCover_is_basis.isOpen hS⟩, ?_, hxS, hSU⟩

Goal state after:
X : Scheme
U : TopologicalSpace.Opens ↥X
x : ↥X
hU : x ∈ ↑U
S : Set ↥X
hS : S ∈ {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}
hxS : x ∈ S
hSU : S ⊆ ↑U
⊢ { carrier := S, is_open' := ⋯ } ∈ X.affineOpens
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit t

Tactic:
apply isUnit_of_mul_isUnit_left (y := t')

Goal state after:
X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := ⋯
S : CommRingCat := ⋯
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := ⋯
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit (t * t')
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCat
this : (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv = 𝟙 (Spec R)
⊢ Spec.map (Scheme.ΓSpecIso R).hom = (Spec R).toSpecΓ

Tactic:
rwa [← IsIso.eq_comp_inv, Category.id_comp, ← Spec.map_inv, IsIso.Iso.inv_inv, eq_comm] at this

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
⊢ U ≤ ⨆ i ∈ s, X.basicOpen i

Tactic:
intro x hx
    obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open hx U.2
    refine SetLike.mem_of_subset ?_ hxV
    rw [← (hV.iSup_basicOpen_eq_self_iff (s := X.presheaf.map (homOfLE hVU).op '' s)).mpr
      (by rw [← Ideal.map_span, hs, Ideal.map_top])]
    simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Set.iUnion_coe_set, Set.mem_image,
      Set.iUnion_exists, Set.biUnion_and', Set.iUnion_iUnion_eq_right, Scheme.basicOpen_res,
      Opens.coe_inf, Opens.coe_mk, Set.iUnion_subset_iff]
    exact fun i hi ↦ (Set.inter_subset_right.trans
      (Set.subset_iUnion₂ (s := fun x _ ↦ (X.basicOpen x : Set X)) i hi))

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
⊢ ⨆ i ∈ s, X.basicOpen i = U

Tactic:
by
  apply le_antisymm
  · rw [iSup₂_le_iff]
    exact fun i _ ↦ X.basicOpen_le i
  · intro x hx
    obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open hx U.2
    refine SetLike.mem_of_subset ?_ hxV
    rw [← (hV.iSup_basicOpen_eq_self_iff (s := X.presheaf.map (homOfLE hVU).op '' s)).mpr
      (by rw [← Ideal.map_span, hs, Ideal.map_top])]
    simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Set.iUnion_coe_set, Set.mem_image,
      Set.iUnion_exists, Set.biUnion_and', Set.iUnion_iUnion_eq_right, Scheme.basicOpen_res,
      Opens.coe_inf, Opens.coe_mk, Set.iUnion_subset_iff]
    exact fun i hi ↦ (Set.inter_subset_right.trans
      (Set.subset_iUnion₂ (s := fun x _ ↦ (X.basicOpen x : Set X)) i hi))

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑X.isoSpec.inv '' ⇑X.isoSpec.inv ⁻¹' X.zeroLocus s = X.zeroLocus s

Tactic:
Set.image_preimage_eq

Goal state after:
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ X.zeroLocus s = X.zeroLocus s

case h
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ Function.Surjective ⇑X.isoSpec.inv
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
⊢ IsOpen[inst✝] (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s)

Tactic:
isOpen_iff_forall_mem_open

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
⊢ ∀ x ∈ ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s,
    ∃ t ⊆ ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s, IsOpen[inst✝] t ∧ x ∈ t
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case left
D : GlueData
i : D.toLocallyRingedSpaceGlueData.J
y : ↑(D.toLocallyRingedSpaceGlueData.U i).toTopCat
j : (D.U i).affineCover.I₀
z : ↥((D.U i).affineCover.X j)
hz : ((D.U i).affineCover.f j) z = y
⊢ (ConcreteCategory.hom (D.toLocallyRingedSpaceGlueData.ι i).base) y ∈
    Set.range ⇑(ConcreteCategory.hom (Hom.toLRSHom ((D.U i).affineCover.f j) ≫ D.toLocallyRingedSpaceGlueData.ι i).base)

Tactic:
simp only [LocallyRingedSpace.comp_toHom, PresheafedSpace.comp_base,
      TopCat.hom_comp, ContinuousMap.coe_comp, Set.range_comp]

Goal state after:
case left
D : GlueData
i : D.toLocallyRingedSpaceGlueData.J
y : ↑(D.toLocallyRingedSpaceGlueData.U i).toTopCat
j : (D.U i).affineCover.I₀
z : ↥((D.U i).affineCover.X j)
hz : ((D.U i).affineCover.f j) z = y
⊢ (ConcreteCategory.hom ((D.mapGlueData forgetToLocallyRingedSpace).ι i).base) y ∈
    ⇑(TopCat.Hom.hom ((D.mapGlueData forgetToLocallyRingedSpace).ι i).base) ''
      Set.range ⇑(TopCat.Hom.hom (Hom.toLRSHom ((D.U i).affineCover.f j)).base)
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))
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
eq₂ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.snd (D.f i j) (D.f i k)).base
⊢ ⇑(ConcreteCategory.hom (pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)))) ''
      ⇑(ConcreteCategory.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom) ''
        ⇑(ConcreteCategory.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom) ⁻¹'
          ⇑(ConcreteCategory.hom (pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)))) ⁻¹' S =
    ⇑(ConcreteCategory.hom (D.f i k).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) '' S

Tactic:
Set.image_preimage_eq

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
eq₂ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.snd (D.f i j) (D.f i k)).base
⊢ ⇑(ConcreteCategory.hom (pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)))) ''
      ⇑(ConcreteCategory.hom (pullback.fst ((forget C).map (D.f i j)) ((forget C).map (D.f i k)))) ⁻¹' S =
    ⇑(ConcreteCategory.hom (D.f i k).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) '' S

case h
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
eq₂ :
  (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom ≫
      pullback.snd ((forget C).map (D.f i j)) ((forget C).map (D.f i k)) =
    (pullback.snd (D.f i j) (D.f i k)).base
⊢ Function.Surjective ⇑(ConcreteCategory.hom (PreservesPullback.iso (forget C) (D.f i j) (D.f i k)).hom)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : IsOpen U
⊢ IsOpen (⇑(fromGlued 𝒰) '' U)

Tactic:
isOpen_iff_forall_mem_open

Goal state after:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : IsOpen U
⊢ ∀ x ∈ ⇑(fromGlued 𝒰) '' U, ∃ t ⊆ ⇑(fromGlued 𝒰) '' U, IsOpen t ∧ x ∈ t
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 left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (Opens.map (D.f j k).base).op.obj (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))) =
    op
      ((Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.left (j, k))))).base).obj
        (⋯.functor.obj U))

Tactic:
Functor.op_obj

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ op ((Opens.map (D.f j k).base).obj (unop (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))))) =
    op
      ((Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.left (j, k))))).base).obj
        (⋯.functor.obj U))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case right
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ Function.Injective
    ⇑(ConcreteCategory.hom ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init WalkingPair.right)))

Tactic:
· simpa using! g.isOpenEmbedding.injective

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

Goal state before:
pp: case restrict
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := isLocal_affineProperty P
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), targetAffineLocally Q f → targetAffineLocally Q (f ∣_ U)

Tactic:
intro X

Goal state after:
case restrict
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X✝ Y : Scheme
f : X✝ ⟶ Y
this : Q.IsLocal := isLocal_affineProperty P
X : Scheme
⊢ ∀ {Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), targetAffineLocally Q f → targetAffineLocally Q (f ∣_ U)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
        (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫
      𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))))

Tactic:
rw [Category.comp_id]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))))
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
y : R
hy : y ∈ I
n : ℕ
h : (fun x_1 ↦ x ^ x_1) n * y ∈ J
⊢ y ∈ J

Tactic:
dsimp at h

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
n : ℕ
h : x ^ n * y ∈ J
⊢ y ∈ J
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U V : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝¹ : IsAffine U
inst✝ : IsOpenImmersion g
iV : V ⟶ X
f' : V ⟶ U
h : IsPullback iV f' f g
H : P.diagonal f
⊢ Q.diagonal f'

Tactic:
by
  let := isLocal_affineProperty P
  rw [← Q.diagonal.cancel_left_of_respectsIso h.isoPullback.inv,
    h.isoPullback_inv_snd]
  rintro U V f₁ f₂ hU hV hf₁ hf₂
  rw [← Q.cancel_left_of_respectsIso (pullbackDiagonalMapIso f _ f₁ f₂).hom]
  convert! HasAffineProperty.of_isPullback (P := P) (.of_hasPullback _ _) H
  · apply pullback.hom_ext <;> simp
  · infer_instance
  · infer_instance

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case h
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
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
e : S ≃ₐ[R] Localization.Away 1 := AlgEquiv.restrictScalars R (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
⊢ P ((algebraMap S (Localization.Away 1)).comp (algebraMap R S))

Tactic:
have : IsLocalization.Away r (Localization.Away (1 : S)) :=
    IsLocalization.isLocalization_of_algEquiv (Submonoid.powers r) e

Goal state after:
case h
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
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
e : S ≃ₐ[R] Localization.Away 1 := AlgEquiv.restrictScalars R (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
this : IsLocalization.Away r (Localization.Away 1)
⊢ P ((algebraMap S (Localization.Away 1)).comp (algebraMap R S))
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x ↦ ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
n' : ℕ
e'' : f (↑r ^ n') * f (↑r ^ n) * x = f (↑r ^ n') * f b
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range

Tactic:
← map_mul,

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x ↦ ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
n' : ℕ
e'' : f (↑r ^ n' * ↑r ^ n) * x = f (↑r ^ n') * f b
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x ↦ ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
n' : ℕ
e'' : f (↑r ^ n' * ↑r ^ n) * x = f (↑r ^ n') * f b
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range

Tactic:
← map_mul,

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
e : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f) (Localization.awayMap f ↑r)
this : Algebra R S := f.toAlgebra
x : S
r : ↑s
b : R
n : ℕ
e' :
  (algebraMap S (Localization.Away (f ↑r))) (x * ↑⟨f ↑⟨(fun x ↦ ↑r ^ x) n, ⋯⟩, ⋯⟩) =
    (algebraMap S (Localization.Away (f ↑r))) (f b)
n' : ℕ
e'' : f (↑r ^ n' * ↑r ^ n) * x = f (↑r ^ n' * b)
⊢ ∃ n, ↑r ^ n • x ∈ (Algebra.linearMap R S).range
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f := ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P (pullback.diagonal f)

Tactic:
exact hf

Goal state after:
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),
    iSup U = ⊤ → (∀ (i : ι), P.universally (f ∣_ U i)) → P.universally f

Tactic:
intro X

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 : Scheme
⊢ ∀ {Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ → (∀ (i : ι), P.universally (f ∣_ U i)) → P.universally f
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X),
    P.universally f ↔ ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)

Tactic:
intro X

Goal state after:
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X : Scheme
⊢ ∀ {Y : Scheme} (f : X ⟶ Y) (𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X),
    P.universally f ↔ ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
hP : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), P ⇑f
⊢ MorphismProperty.isomorphisms Scheme ≤ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P

Tactic:
intro X

Goal state after:
P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
hP : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), P ⇑f
X : Scheme
⊢ ∀ ⦃Y : Scheme⦄ (f : X ⟶ Y),
    MorphismProperty.isomorphisms Scheme f → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f