mathlib-initiative/mathlib-tactics huggingface dataset:
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)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
⊢ Set.range
      ⇑(ConcreteCategory.hom
          (((inv (pullback.snd f g)).base ≫
              (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom) ≫
            pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
              ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g))) =
    ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
TopCat.coe_comp,

Goal state after:
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)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
⊢ Set.range
      (⇑(ConcreteCategory.hom
            (pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
              ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g))) ∘
        ⇑(ConcreteCategory.hom
            ((inv (pullback.snd f g)).base ≫
              (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom))) =
    ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)
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
S : (x : ↑X) → Submonoid ↑(F.stalk x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : ↑(F.obj U)
hs : ∀ (i : ↥(unop U)), (CommRingCat.Hom.hom (F.germ (unop U) ↑i ⋯)) s ∈ S ↑i
⊢ ∀ (i_1 : ↥(unop V)), (CommRingCat.Hom.hom (F.germ (unop V) ↑i_1 ⋯)) ((CommRingCat.Hom.hom (F.map i)) s) ∈ S ↑i_1

Tactic:
intro x

Goal state after:
X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
S : (x : ↑X) → Submonoid ↑(F.stalk x)
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
s : ↑(F.obj U)
hs : ∀ (i : ↥(unop U)), (CommRingCat.Hom.hom (F.germ (unop U) ↑i ⋯)) s ∈ S ↑i
x : ↥(unop V)
⊢ (CommRingCat.Hom.hom (F.germ (unop V) ↑x ⋯)) ((CommRingCat.Hom.hom (F.map i)) s) ∈ S ↑x
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)ᵒᵖ
m : Submonoid ↑(F.presheaf.obj U) := ⋯
s : ↑(F.presheaf.obj U)
hs : s ∈ m
t : ↑(F.presheaf.obj U)
e : t * s = 0
⊢ ∀ (x : ↑X) (hx : x ∈ unop U),
    (ConcreteCategory.hom (F.presheaf.germ (unop U) x hx)) t = (ConcreteCategory.hom (F.presheaf.germ (unop U) x hx)) 0

Tactic:
intro x

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)ᵒᵖ
m : Submonoid ↑(F.presheaf.obj U) := (F.presheaf.submonoidPresheafOfStalk fun x ↦ (↑(F.presheaf.stalk x))⁰).obj U
s : ↑(F.presheaf.obj U)
hs : s ∈ m
t : ↑(F.presheaf.obj U)
e : t * s = 0
x : ↑X
⊢ ∀ (hx : x ∈ unop U),
    (ConcreteCategory.hom (F.presheaf.germ (unop U) x hx)) t = (ConcreteCategory.hom (F.presheaf.germ (unop U) x hx)) 0
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
this : V.ι ''ᵁ V.ι ⁻¹ᵁ U = U
⊢ Set.range ⇑(ConcreteCategory.hom ((V.ι ⁻¹ᵁ U).ι.base ≫ V.ι.base)) = Set.range ⇑U.ι

Tactic:
TopCat.coe_comp,

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
this : V.ι ''ᵁ V.ι ⁻¹ᵁ U = U
⊢ Set.range (⇑V.ι ∘ ⇑(V.ι ⁻¹ᵁ U).ι) = Set.range ⇑U.ι
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
⊢ Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯ =
    CommRingCat.ofHom
      (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))))
        (↑(X.presheaf.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)))))
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) r)

Tactic:
let := hU.isLocalization_basicOpen r

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : ↑Γ(Y, U)
this : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r
⊢ Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)) ⋯ =
    CommRingCat.ofHom
      (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))))
        (↑(X.presheaf.1 (op (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appLE f U V e)) r)))))
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) r)
Module: Mathlib.CategoryTheory.MorphismProperty.Local

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasEqualizers C
inst✝² : HasPullbacks C
X Y S : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
J : Precoverage C
𝒰 : J.ZeroHypercover S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : (MorphismProperty.isomorphisms C).IsLocalAtTarget J
H :
  ∀ (i : 𝒰.I₀),
    pullback.map s (𝒰.f i) t (𝒰.f i) f (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯ = pullback.map s (𝒰.f i) t (𝒰.f i) g (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯
⊢ f = g

Tactic:
suffices IsIso (equalizer.ι f g) from Limits.eq_of_epi_equalizer
  change MorphismProperty.isomorphisms C _
  rw [(MorphismProperty.isomorphisms C).iff_of_zeroHypercover_target (𝒰.pullback₁ s)]
  intro i
  have : pullback.snd (equalizer.ι f g) (pullback.fst s (𝒰.f i)) =
      (equalizerPullbackMapIso hf hg _).inv ≫ equalizer.ι _ _ := by
    ext <;> simp [pullback.condition]
  simpa [this] using equalizer.ι_of_eq (H i)

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
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
f' : M →ₗ[R] N :=
  let __spread.0 := f;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
⊢ ∀ (x : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl),
    IsUnit ((algebraMap R (Module.End R (LocalizedModule y.asIdeal.primeCompl N))) ↑x)

Tactic:
intro x

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
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
this✝¹ : Module R N := Module.compHom N σ
this✝ : Algebra R S := σ.toAlgebra
this : IsScalarTower R S N
f' : M →ₗ[R] N :=
  let __spread.0 := f;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
x : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
⊢ IsUnit ((algebraMap R (Module.End R (LocalizedModule y.asIdeal.primeCompl N))) ↑x)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
x✝ : ↑(CommRingCat.of R)
x : ↥(unop (op ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U)))
⊢ (Localization.localRingHom (PrimeSpectrum.comap f ↑x).asIdeal (↑x).asIdeal f ⋯)
      (↑((algebraMap R ↑((structureSheaf R).obj.obj (op U))) x✝) ⟨PrimeSpectrum.comap f ↑x, ⋯⟩) =
    ↑((algebraMap S
            ↑((structureSheaf S).obj.obj
                (op ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U))))
          (f x✝))
      x

Tactic:
exact Localization.localRingHom_to_map _ _ _ _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
⊢ ∀ x ∈ s, ↑(X.basicOpen x) ⊆ ↑U

Tactic:
intro x

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
x : ↑Γ(X, U)
⊢ x ∈ s → ↑(X.basicOpen x) ⊆ ↑U
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : U ≤ ⨆ f, X.basicOpen ↑f
⊢ ∀ x ∈ s, X.basicOpen x ≤ U

Tactic:
intro x

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : U ≤ ⨆ f, X.basicOpen ↑f
x : ↑Γ(X, U)
⊢ x ∈ s → X.basicOpen x ≤ U
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
⊢ ∀ (x : ↑(coproductCofan F).pt.toTopCat),
    IsLocalHom
      (CommRingCat.Hom.hom
        (PresheafedSpace.Hom.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom
          x))

Tactic:
intro x

Goal state after:
ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
s : Cocone F
x : ↑(coproductCofan F).pt.toTopCat
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap (colimit.desc (F ⋙ forgetToSheafedSpace) (forgetToSheafedSpace.mapCocone s)).hom x))
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

Goal state after:
case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↥X
⊢ x ∈ U → x ∈ ⨆ i ∈ s, X.basicOpen i
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
⊢ ∀ (x : ↥↑V), ∃ f, ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)

Tactic:
intro x

Goal state after:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
x : ↥↑V
⊢ ∃ f, ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
⊢ ↑V ≤ ⨆ f_1, X.basicOpen ↑f_1

Tactic:
intro x

Goal state after:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
x : ↥X
⊢ x ∈ ↑V → x ∈ ⨆ f_1, X.basicOpen ↑f_1
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
⊢ (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι j)) y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩

Tactic:
by
  constructor
  · delta GlueData.ι
    simp_rw [← Multicoequalizer.ι_sigmaπ]
    intro h
    rw [←
      show _ = Sigma.mk i x from ConcreteCategory.congr_hom (sigmaIsoSigma.{_, u} D.U).inv_hom_id _]
    rw [←
      show _ = Sigma.mk j y from ConcreteCategory.congr_hom (sigmaIsoSigma.{_, u} D.U).inv_hom_id _]
    change InvImage D.Rel (sigmaIsoSigma.{_, u} D.U).hom _ _
    rw [← (InvImage.equivalence _ _ D.rel_equiv).eqvGen_iff]
    refine Relation.EqvGen.mono ?_ _ _ (D.eqvGen_of_π_eq h :)
    rintro _ _ ⟨x⟩
    obtain ⟨⟨⟨i, j⟩, y⟩, rfl⟩ :=
      (ConcreteCategory.bijective_of_isIso (sigmaIsoSigma.{u, u} _).inv).2 x
    unfold InvImage MultispanIndex.fstSigmaMap MultispanIndex.sndSigmaMap
    rw [sigmaIsoSigma_inv_apply]
    -- `rw [← ConcreteCategory.comp_apply]` succeeds but rewrites the wrong expression
    erw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, colimit.ι_desc_assoc,
      ← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, colimit.ι_desc_assoc]
      -- previous line now `erw` after https://github.com/leanprover-community/mathlib4/pull/13170
    erw [sigmaIsoSigma_hom_ι_apply, sigmaIsoSigma_hom_ι_apply]
    exact ⟨y, ⟨rfl, rfl⟩⟩
  · rintro ⟨z, e₁, e₂⟩
    dsimp only at *
    -- Porting note: there were `subst e₁` and `subst e₂`, instead of the `rw`
    rw [← e₁, ← e₂] at *
    rw [D.glue_condition_apply]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ Function.Injective ⇑(ConcreteCategory.hom (D.ι i))

Tactic:
intro x

Goal state after:
D : GlueData
i : D.J
x : ↑(D.U i)
⊢ ∀ ⦃a₂ : ↑(D.U i)⦄, (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι i)) a₂ → x = a₂
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
⊢ Set.range ⇑(ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(ConcreteCategory.hom (D.ι j)) =
    Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))

Tactic:
ext x
  constructor
  · rintro ⟨⟨x₁, eq₁⟩, ⟨x₂, eq₂⟩⟩
    obtain ⟨y, e₁, -⟩ := (D.ι_eq_iff_rel _ _ _ _).mp (eq₁.trans eq₂.symm)
    · subst eq₁
      exact ⟨y, by simp [e₁]⟩
  · rintro ⟨x, hx⟩
    refine ⟨⟨D.f i j x, hx⟩, ⟨D.f j i (D.t _ _ x), ?_⟩⟩
    rw [D.glue_condition_apply]
    exact hx

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' Set.univ =
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) '' Set.range ⇑(ConcreteCategory.hom (D.f j i))

Tactic:
←
    Set.image_univ,

Goal state after:
D : GlueData
i j : D.J
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' Set.univ =
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) '' ⇑(ConcreteCategory.hom (D.f j i)) '' Set.univ
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R✝ S✝ : CommRingCat
f✝ : R✝ ⟶ S✝
p✝ : PrimeSpectrum ↑S✝
x : PrimeSpectrum ↑R✝
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ (Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).hom ≫
      (Arrow.mk
          (CommRingCat.ofHom
            (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
              (CommRingCat.Hom.hom f) ⋯))).hom =
    (Arrow.mk (Hom.stalkMap (Spec.map f) p)).hom ≫ (Spec.stalkIso S p).hom

Tactic:
by
    rw [← Scheme.localRingHom_comp_stalkIso]
    simp

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case refine_2
h : MkCore
i j : h.J
x : ↥(h.V j i)
this :
  ↑((ConcreteCategory.hom (h.t i j)) ⟨↑((ConcreteCategory.hom (h.t j i)) x), ⋯⟩) =
    ↑((ConcreteCategory.hom (h.t j j)) ⟨↑x, ?refine_1⟩)
⊢ (ConcreteCategory.hom (h.t i j)) ((ConcreteCategory.hom (h.t j i)) x) = x

pp: case refine_1
h : MkCore
i j : h.J
x : ↥(h.V j i)
⊢ ↑x ∈ h.V j j

Tactic:
· rw [h.t_id] at this
    · convert! Subtype.ext this

Goal state after:
case refine_1
h : MkCore
i j : h.J
x : ↥(h.V j i)
⊢ ↑x ∈ h.V j j
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case refine_1
D : GlueData
h : MkCore
i j k : h.J
⊢ { p // (ConcreteCategory.hom (h.V i j).inclusion') p.1 = (ConcreteCategory.hom (h.V i k).inclusion') p.2 } →
    { p // (ConcreteCategory.hom (h.V j k).inclusion') p.1 = (ConcreteCategory.hom (h.V j i).inclusion') p.2 }

Tactic:
intro x

Goal state after:
case refine_1
D : GlueData
h : MkCore
i j k : h.J
x : { p // (ConcreteCategory.hom (h.V i j).inclusion') p.1 = (ConcreteCategory.hom (h.V i k).inclusion') p.2 }
⊢ { p // (ConcreteCategory.hom (h.V j k).inclusion') p.1 = (ConcreteCategory.hom (h.V j i).inclusion') p.2 }
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
⊢ Function.Injective ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Tactic:
intro x

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x : ↑(ofOpenSubsets U).glued
⊢ ∀ ⦃a₂ : ↑(ofOpenSubsets U).glued⦄,
    (ConcreteCategory.hom (fromOpenSubsetsGlue U)) x = (ConcreteCategory.hom (fromOpenSubsetsGlue U)) a₂ → x = a₂
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
⊢ ∀ (x : ↑D.toLocallyRingedSpaceGlueData.glued.toTopCat),
    ∃ R f, x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ LocallyRingedSpace.IsOpenImmersion f

Tactic:
intro x

Goal state after:
D : GlueData
x : ↑D.toLocallyRingedSpaceGlueData.glued.toTopCat
⊢ ∃ R f, x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ LocallyRingedSpace.IsOpenImmersion f
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
          ((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)))) ''
      ⇑(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:
TopCat.coe_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: 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:
TopCat.coe_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 (pullback.fst ((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) ⁻¹'
          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.refine_1
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)
⊢ Function.LeftInverse ⇑(ConcreteCategory.hom (D.t' k i j).base) ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)

Tactic:
intro x

Goal state after:
case w.refine_1
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)
x : ↑↑(pullback (D.f i j) (D.f i k))
⊢ (ConcreteCategory.hom (D.t' k i j).base) ((TopCat.Hom.hom (inv (D.t' k i j)).base) x) = x
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w.refine_2
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)
⊢ Function.RightInverse ⇑(ConcreteCategory.hom (D.t' k i j).base) ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)

Tactic:
intro x

Goal state after:
case w.refine_2
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)
x : ↑↑(pullback (D.f k i) (D.f k j))
⊢ (TopCat.Hom.hom (inv (D.t' k i j)).base) ((ConcreteCategory.hom (D.t' k i j).base) x) = x
Module: Mathlib.AlgebraicGeometry.Gluing

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

Tactic:
intro x

Goal state after:
X : Scheme
𝒰 : X.OpenCover
x : ↥(gluedCover 𝒰).glued
⊢ ∀ ⦃a₂ : ↥(gluedCover 𝒰).glued⦄, (fromGlued 𝒰) x = (fromGlued 𝒰) a₂ → x = a₂