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
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
⊢ IsIso f.base

Tactic:
let t : X ≃ₜ Y := H.base_open.isEmbedding.toHomeomorph.trans
    { toFun := Subtype.val
      invFun := fun x =>
        ⟨x, by rw [Set.range_eq_univ.mpr ((TopCat.epi_iff_surjective _).mp h')]; trivial⟩ }

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
t : ↑↑X ≃ₜ ↑↑Y :=
  ⋯.toHomeomorph.trans
    { toFun := Subtype.val, invFun := fun x ↦ ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
      continuous_invFun := ⋯ }
⊢ IsIso f.base
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
V : Y.Opens
hV : V ≤ opensRange f
⊢ IsIso (app f V)

Tactic:
rw [show V = f ''ᵁ f ⁻¹ᵁ V from Opens.ext (Set.image_preimage_eq_of_subset hV).symm]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case neg
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
x : ↥Y
hx : x ∉ Set.range ⇑f
⊢ x ∉ (fun a ↦ f a) '' X.zeroLocus s

Tactic:
exact fun H ↦ hx (Set.image_subset_range _ _ H)

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

Goal state before:
pp: X : Scheme
⊢ IsTopologicalBasis {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}

Tactic:
apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds

Goal state after:
case h_open
X : Scheme
⊢ ∀ u ∈ {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}, IsOpen u

case h_nhds
X : Scheme
⊢ ∀ (a : ↥X) (u : Set ↥X), a ∈ u → IsOpen u → ∃ v ∈ {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}, a ∈ v ∧ v ⊆ u
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
⊢ Mono (F.presheaf.toTotalQuotientPresheaf.app U)

Tactic:
apply ConcreteCategory.mono_of_injective

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
⊢ Function.Injective ⇑(ConcreteCategory.hom (F.presheaf.toTotalQuotientPresheaf.app U))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ IsPullback (equalizer.ι f g) (equalizer.ι f g ≫ f) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))

Tactic:
refine ⟨⟨by ext <;> simp [equalizer.condition f g]⟩, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ (s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))) → s.pt ⟶ equalizer f g

case refine_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ ∀ (s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))), ?refine_1 s ≫ equalizer.ι f g = s.fst

case refine_3
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ ∀ (s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))), ?refine_1 s ≫ equalizer.ι f g ≫ f = s.snd

case refine_4
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ ∀ (s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))) (m : s.pt ⟶ equalizer f g),
    m ≫ equalizer.ι f g = s.fst → m ≫ equalizer.ι f g ≫ f = s.snd → m = ?refine_1 s
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (hU.isoSpec.hom ≫ hU.isoSpec.inv ≫ U.ι) x = ↑x

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ U.ι x = ↑x
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
⊢ IsLimit (D.vPullbackCone i j)

Tactic:
by
  apply isLimitOfReflects F
  apply (isLimitMapConePullbackConeEquiv _ _).symm _
  let e : cospan (F.map (D.ι i)) (F.map (D.ι j)) ≅
      cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
    NatIso.ofComponents
      (fun x => by
        cases x
        exacts [D.gluedIso F, Iso.refl _])
      (by rintro (_ | _) (_ | _) (_ | _ | _) <;> simp)
  apply IsLimit.postcomposeHomEquiv e _ _
  apply hc.ofIsoLimit
  refine Cone.ext (Iso.refl _) ?_
  rintro (_ | _ | _)
  all_goals simp [e]; rfl

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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U)))

Tactic:
have := ι_comp_coequalizerComparison f.toShHom g.toShHom SheafedSpace.forgetToPresheafedSpace

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this :
  coequalizer.π (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom f))
        (SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom g)) ≫
      coequalizerComparison (Hom.toShHom f) (Hom.toShHom g) SheafedSpace.forgetToPresheafedSpace =
    SheafedSpace.forgetToPresheafedSpace.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))
⊢ IsLocalHom (CommRingCat.Hom.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U)))
Module: Mathlib.Topology.Gluing

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

Tactic:
obtain ⟨y, e₁, -⟩ := (D.ι_eq_iff_rel _ _ _ _).mp (eq₁.trans eq₂.symm)

Goal state after:
case mp
D : GlueData
i j : D.J
x : ↑D.glued
x₁ : ↑(D.U i)
eq₁ : (ConcreteCategory.hom (D.ι i)) x₁ = x
x₂ : ↑(D.U j)
eq₂ : (ConcreteCategory.hom (D.ι j)) x₂ = x
y : ↑(D.V (⟨i, x₁⟩.fst, ⟨j, x₂⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, x₁⟩.fst ⟨j, x₂⟩.fst)) y = ⟨i, x₁⟩.snd
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))
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 ≫
              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_comp,

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 (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 ≫
                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
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
⊢ ⇑(ConcreteCategory.hom (D.t k i).base) ⁻¹'
      ⇑(TopCat.Hom.hom (D.t k i).base) ∘
          ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) ''
        ↑U =
    ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) '' ⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑U

Tactic:
Set.image_comp,

Goal state after:
case w
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
⊢ ⇑(ConcreteCategory.hom (D.t k i).base) ⁻¹'
      ⇑(TopCat.Hom.hom (D.t k i).base) ''
        ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) '' ↑U =
    ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) '' ⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑U
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
⊢ ⇑(ConcreteCategory.hom (D.t k i).base) ⁻¹'
      ⇑(TopCat.Hom.hom (D.t k i).base) ''
        ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) '' ↑U =
    ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) '' ⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑U

Tactic:
Set.image_comp,

Goal state after:
case w
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
⊢ ⇑(ConcreteCategory.hom (D.t k i).base) ⁻¹'
      ⇑(TopCat.Hom.hom (D.t k i).base) ''
        ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) '' ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base) '' ↑U =
    ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) '' ⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑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)
⊢ ⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv) ∘ ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι j)) ⁻¹'
      ⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv) ∘ ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)) ''
        ↑U =
    ⇑(ConcreteCategory.hom (D.f j i).base) ''
      ⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U

Tactic:
Set.image_comp,

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)
⊢ ⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv) ∘ ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι j)) ⁻¹'
      ⇑(ConcreteCategory.hom (D.gluedIso (forget C)).inv) ''
        ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i)) '' ↑U =
    ⇑(ConcreteCategory.hom (D.f j i).base) ''
      ⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inr
X : Scheme
inst✝ : Subsingleton ↥X
x : ↥X
⊢ IsAffine X

Tactic:
obtain ⟨_, ⟨U, hU : IsAffine _, rfl⟩, hxU, -⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open (a := x) (by trivial) isOpen_univ

Goal state after:
case inr
X : Scheme
inst✝ : Subsingleton ↥X
x : ↥X
U : Opens ↥X
hU : IsAffine ↑U
hxU : x ∈ ↑U
⊢ IsAffine X
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ IsPullback f coprod.inl coprod.inl (coprod.map f g)

Tactic:
by
  refine IsOpenImmersion.isPullback _ _ _ _ (by simp) ?_
  apply le_antisymm
  · rintro x ⟨y, hxy⟩
    obtain ⟨(x | x), rfl⟩ := (coprodMk _ _).surjective x
    · rw [← SetLike.mem_coe]; simp -- TODO : add `Scheme.Hom.mem_opensRange`
    · simp only [coprodMk_inr, ← Scheme.Hom.comp_apply, coprod.inr_map] at hxy
      cases Set.disjoint_iff_forall_ne.mp (isCompl_range_inl_inr _ _).1 ⟨y, rfl⟩ ⟨_, rfl⟩ hxy
  · rintro _ ⟨x, rfl⟩
    exact ⟨f x, by simp [← Scheme.Hom.comp_apply, -Scheme.Hom.comp_base]⟩

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
i : 𝒰.I₀
⊢ (pullbackP1Iso 𝒰 f g i).hom ≫ (pullbackP1Iso 𝒰 f g i).inv ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i) =
    pullback.fst (p1 𝒰 f g) (𝒰.f i)

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ pullback.fst (p1 𝒰 f g) (𝒰.f i) = pullback.fst (p1 𝒰 f g) (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
X : Scheme
inst✝ : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this : IsOpenImmersion (Sigma.desc fun i ↦ (U i).ι)
⊢ IsAffineOpen (iSup U)

Tactic:
convert! isAffineOpen_opensRange (Sigma.desc fun i ↦ (U i).ι)

Goal state after:
ι : Type u
X : Scheme
inst✝ : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this : IsOpenImmersion (Sigma.desc fun i ↦ (U i).ι)
⊢ iSup U = Scheme.Hom.opensRange (Sigma.desc fun i ↦ (U i).ι)

ι : Type u
X : Scheme
inst✝ : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this : IsOpenImmersion (Sigma.desc fun i ↦ (U i).ι)
⊢ IsAffine (∐ fun i ↦ ↑(U i))
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
⊢ P f

Tactic:
refine (P.iff_of_zeroHypercover_target
    (Y.openCoverOfIsOpenCover (s := Set.range U) Subtype.val (by ext; simp [← hU]))).mpr fun i ↦ ?_

Goal state after:
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (f ∣_ U i)
i : (Y.openCoverOfIsOpenCover Subtype.val ⋯).I₀
⊢ P (pullback.snd f ((Y.openCoverOfIsOpenCover Subtype.val ⋯).f i))
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P Q : AffineTargetMorphismProperty
H : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f
⊢ P = Q

Tactic:
delta AffineTargetMorphismProperty; ext; exact H _

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine ((𝒰' i).X j)
h𝒰' : ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀), Q (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
⊢ P.diagonal f

Tactic:
have i1 : ∀ i, IsAffine (𝒱.X i) := fun i => by dsimp [𝒱]; infer_instance

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine ((𝒰' i).X j)
h𝒰' : ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀), Q (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
⊢ P.diagonal f
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ (pullbackSpecIso R S T).hom ≫
      (pullbackSpecIso R S T).inv ≫
        pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))) =
    pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T)))

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))) =
    pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T)))
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
h₂ : ∃ y ∈ Ideal.span (Set.range (mulNumerator s p)), ∃ z, mk' (Rₜ ⟨a, ha⟩) 1 1 = mk' (Rₜ ⟨a, ha⟩) y z
⊢ a ∈ ↑(Ideal.span (Set.range (mulNumerator s p))).radical

Tactic:
obtain ⟨y, hy, ⟨-, m, rfl⟩, hyz⟩ := h₂

Goal state after:
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
h₁ : Ideal.span (p ⟨a, ha⟩) ≤ Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p))
y : R
hy : y ∈ Ideal.span (Set.range (mulNumerator s p))
m : ℕ
hyz : mk' (Rₜ ⟨a, ha⟩) 1 1 = mk' (Rₜ ⟨a, ha⟩) y ⟨(fun x ↦ a ^ x) m, ⋯⟩
⊢ a ∈ ↑(Ideal.span (Set.range (mulNumerator s p))).radical
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ (pullbackSpecIso R S T).hom ≫
      (pullbackSpecIso R S T).inv ≫
        pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))) =
    pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T)))

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))) =
    pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T)))
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: case hP₃
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
x✝ : Continuous[inst✝¹, inst✝] f
hsp :
  ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy✝ : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
hy : ⟨y, hi⟩ ∈ closure[instTopologicalSpaceSubtype] {⟨f x, hfx⟩}
a : ↑(f ⁻¹' (U i).carrier)
ha : ↑a ∈ closure[inst✝¹] {x}
hay : ↑((U i).carrier.restrictPreimage f a) = ↑⟨y, hi⟩
⊢ y ∈ f '' closure[inst✝¹] {x}

Tactic:
simp only [Opens.carrier_eq_coe, Set.restrictPreimage_coe] at hay

Goal state after:
case hP₃
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
x✝ : Continuous[inst✝¹, inst✝] f
hsp :
  ∀ (i : ι) (x : ↑(f ⁻¹' (U i).carrier)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy✝ : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
hy : ⟨y, hi⟩ ∈ closure[instTopologicalSpaceSubtype] {⟨f x, hfx⟩}
a : ↑(f ⁻¹' (U i).carrier)
ha : ↑a ∈ closure[inst✝¹] {x}
hay : f ↑a = y
⊢ y ∈ f '' closure[inst✝¹] {x}
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
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
hf : P f
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
(Mathlib.Tactic.useSyntax
 "use"
 []
 (group)
 [(choice
   («term{_}» "{" [(num "1")] "}")
   (Term.structInst
    "{"
    []
    (Term.structInstFields [(Term.structInstField (Term.structInstLVal (fieldIdx "1") []) [])])
    (Term.optEllipsis [])
    []
    "}"))])

Goal state after:
case h
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
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
hf : P f
⊢ ∃ (_ : Ideal.span {1} = ⊤),
    ∀ t ∈ {1}, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
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
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R S)

Tactic:
(Mathlib.Tactic.useSyntax
 "use"
 []
 (group)
 [(choice
   («term{_}» "{" [(num "1")] "}")
   (Term.structInst
    "{"
    []
    (Term.structInstFields [(Term.structInstField (Term.structInstLVal (fieldIdx "1") []) [])])
    (Term.optEllipsis [])
    []
    "}"))])

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
⊢ ∃ (_ : Ideal.span {1} = ⊤),
    ∀ t ∈ {1}, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp (algebraMap R S))