mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case mp
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
x✝ : ↑↑X.toPresheafedSpace
y : ↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Y)
eq :
  (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)) x✝ =
    (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) y
⊢ x✝ ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
exact ⟨y, eq.symm⟩

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

Goal state before:
pp: case mpr
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
x✝ : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
eq : (ConcreteCategory.hom g.base) y = (ConcreteCategory.hom f.base) x✝
⊢ x✝ ∈
    {x |
      ∃ y,
        (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)) x =
          (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) y}

Tactic:
exact ⟨y, eq.symm⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(X, U)
⊢ U.ι ''ᵁ (↑U).basicOpen ((ConcreteCategory.hom U.topIso.inv) r) = X.basicOpen r

Tactic:
rw [ι_image_basicOpen', basicOpen_res_eq, topIso_inv, basicOpen_res_eq X]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
this : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f}
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑(Ideal.span (Set.range b)))

Tactic:
PrimeSpectrum.zeroLocus_span,

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
this : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f}
⊢ f ∈ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (Set.range b))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompact ↑U

Tactic:
by
  convert! @IsCompact.image _ _ _ _ Set.univ hU.fromSpec PrimeSpectrum.compactSpace.1 (by fun_prop)
  convert! hU.range_fromSpec.symm
  exact Set.image_univ

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ⁻¹ᵁ X.basicOpen f = PrimeSpectrum.basicOpen f

Tactic:
by
  rw [fromSpec_preimage_basicOpen', ← basicOpen_eq_of_affine]

Goal state after:
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) ⋯ ⋯
⊢ IsIso (equalizer.ι f g)

Tactic:
change MorphismProperty.isomorphisms C _

Goal state after:
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) ⋯ ⋯
⊢ MorphismProperty.isomorphisms C (equalizer.ι f g)
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: 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
x : X
⊢ (hom f) x ∈ U ↔ (hom g) x ∈ U

Tactic:
change x ∈ f ⁻¹' U ↔ x ∈ g ⁻¹' U

Goal state after:
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
x : X
⊢ x ∈ ⇑(hom f) ⁻¹' U ↔ x ∈ ⇑(hom g) ⁻¹' U
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom
        (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap ≫ (Multicoequalizer.isoCoequalizer D.diagram).inv))
      x =
    (ConcreteCategory.hom
        (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap ≫ (Multicoequalizer.isoCoequalizer D.diagram).inv))
      y
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y

Tactic:
replace h : coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap x =
      coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap y :=
    (TopCat.mono_iff_injective (Multicoequalizer.isoCoequalizer 𝖣.diagram).inv).mp
    inferInstance h

Goal state after:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) x =
    (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) y
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y
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
this✝ :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
this : IsIso (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      ((PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c.app
          (op U) ≫
        (PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit (parallelPair f.toHom g.toHom)
              ((Opens.map
                    (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                          (Hom.toShHom g)).hom.base).obj
                (unop (op U)))).hom ≫
          limit.π
            (PresheafedSpace.componentwiseDiagram (parallelPair f.toHom g.toHom)
              ((Opens.map
                    (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                          (Hom.toShHom g)).hom.base).obj
                (unop (op U))))
            (op WalkingParallelPair.one)))

Tactic:
apply +allowSynthFailures RingHom.isLocalHom_comp

Goal state after:
case inst
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this✝ :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
this : IsIso (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c
⊢ IsLocalHom
    ((PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit (parallelPair f.toHom g.toHom)
            ((Opens.map
                  (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                        (Hom.toShHom g)).hom.base).obj
              (unop (op U)))).hom ≫
        limit.π
          (PresheafedSpace.componentwiseDiagram (parallelPair f.toHom g.toHom)
            ((Opens.map
                  (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                        (Hom.toShHom g)).hom.base).obj
              (unop (op U))))
          (op WalkingParallelPair.one)).hom'

case inst
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this✝ :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
this : IsIso (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c
⊢ IsLocalHom
    ((PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c.app
        (op U)).hom'
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: case inst
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this✝ :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
this : IsIso (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c
⊢ IsLocalHom
    ((PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit (parallelPair f.toHom g.toHom)
            ((Opens.map
                  (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                        (Hom.toShHom g)).hom.base).obj
              (unop (op U)))).hom ≫
        limit.π
          (PresheafedSpace.componentwiseDiagram (parallelPair f.toHom g.toHom)
            ((Opens.map
                  (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                        (Hom.toShHom g)).hom.base).obj
              (unop (op U))))
          (op WalkingParallelPair.one)).hom'

Tactic:
apply +allowSynthFailures RingHom.isLocalHom_comp

Goal state after:
case inst.inst
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this✝ :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
this : IsIso (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c
⊢ IsLocalHom
    (limit.π
        (PresheafedSpace.componentwiseDiagram (parallelPair f.toHom g.toHom)
          ((Opens.map
                (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                      (Hom.toShHom g)).hom.base).obj
            (unop (op U))))
        (op WalkingParallelPair.one)).hom'

case inst.inst
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this✝ :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
this : IsIso (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c
⊢ IsLocalHom
    (PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit (parallelPair f.toHom g.toHom)
          ((Opens.map
                (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                      (Hom.toShHom g)).hom.base).obj
            (unop (op U)))).hom.hom'
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mpr
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
z : ↑(D.V (⟨i, x⟩.fst, ⟨j, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f i j)) z = x
e₂ : (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z) = y
⊢ (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι j)) y

Tactic:
rw [← e₁, ← e₂] at *

Goal state after:
case mpr
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
z : ↑(D.V (⟨i, x⟩.fst, ⟨j, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f i j)) z = (ConcreteCategory.hom (D.f i j)) z
e₂ :
  (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z) =
    (ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z)
⊢ (ConcreteCategory.hom (D.ι i)) ((ConcreteCategory.hom (D.f i j)) z) =
    (ConcreteCategory.hom (D.ι j)) ((ConcreteCategory.hom (D.f j i)) ((ConcreteCategory.hom (D.t i j)) z))
Module: Mathlib.Topology.Gluing

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

Tactic:
apply Set.inter_eq_self_of_subset_left

Goal state after:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U ⊆ Set.range ⇑(ConcreteCategory.hom (D.f j i))
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:
← Scheme.localRingHom_comp_stalkIso

Goal state after:
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
          ((Spec.stalkIso R (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p)).hom ≫
            CommRingCat.ofHom
                (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p).asIdeal p.asIdeal
                  (CommRingCat.Hom.hom f) ⋯) ≫
              (Spec.stalkIso S p).inv)).hom ≫
      (Spec.stalkIso S p).hom
Module: Mathlib.Topology.Gluing

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

Tactic:
h.V_id

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

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
x : ↑(h.U i)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ ↑((ConcreteCategory.hom (h.t k i))
        ⟨↑((ConcreteCategory.hom (h.t j k)) ⟨↑((ConcreteCategory.hom (h.t i j)) ⟨x, hx⟩), ⋯⟩), ⋯⟩) =
    x

Tactic:
convert! congr_arg Subtype.val (h.t_inv k i ⟨x, hx'⟩) using 3

Goal state after:
D : GlueData
h : MkCore
i j k : h.J
x : ↑(h.U i)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ ⟨↑((ConcreteCategory.hom (h.t j k)) ⟨↑((ConcreteCategory.hom (h.t i j)) ⟨x, hx⟩), ⋯⟩), ⋯⟩ =
    (ConcreteCategory.hom (h.t i k)) ⟨x, hx'⟩
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
g : σ → Scheme
inst✝¹ : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst✝ : ∀ (i : σ), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ Sigma.desc α = (Sigma.reindex e.symm g).inv ≫ Sigma.desc fun i ↦ α (e.symm i)

pp: σ : Type v
g : σ → Scheme
inst✝¹ : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst✝ : ∀ (i : σ), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ IsOpenImmersion (Sigma.desc fun i ↦ α (e.symm i))

Tactic:
· refine Sigma.hom_ext _ _ fun i ↦ ?_
    obtain ⟨i, rfl⟩ := e.symm.surjective i
    simp

Goal state after:
σ : Type v
g : σ → Scheme
inst✝¹ : Small.{u, v} σ
X : Scheme
α : (i : σ) → g i ⟶ X
inst✝ : ∀ (i : σ), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ι : Type u
e : σ ≃ ι
⊢ IsOpenImmersion (Sigma.desc fun i ↦ α (e.symm i))
Module: Mathlib.AlgebraicGeometry.Limits

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

Tactic:
change ((TopCat.binaryCofan X Y).inr ≫
    (colimit.isoColimitCocone ⟨_, TopCat.binaryCofanIsColimit _ _⟩).inv ≫ _) x =
      Scheme.forgetToTop.map coprod.inr x
  congr 2
  refine (colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.binaryCofanIsColimit _ _⟩ _ _).trans ?_
  exact coprodComparison_inr Scheme.forgetToTop

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
X : Scheme
inst✝ : Finite σ
U : σ → X.Opens
hU : ∀ (i : σ), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
⊢ IsAffineOpen (iSup U)

Tactic:
by
  obtain ⟨ι, ⟨e⟩⟩ := Small.equiv_small.{u} (α := σ)
  have : Finite ι := e.finite_iff.mp ‹_›
  rw [← e.symm.iSup_congr fun _ ↦ rfl]
  exact .iSup_of_disjoint_aux (by simp [*]) fun i j h ↦ hU' (e.symm.injective.ne h)

Goal state after:
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)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        D.ιInvApp U ≫
          limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
            𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
      𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))

Tactic:
limit.lift_π_assoc

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)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        { pt := (D.U i).presheaf.obj (op U), π := { app := fun j ↦ D.ιInvAppπApp U (unop j), naturality := ⋯ } }.π.app
            (op (WalkingMultispan.left (i, j))) ≫
          𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
      𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))
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)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        (D.f i i).c.app (op U) ≫
          (D.V (i, i)).presheaf.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯) ≫
            invApp (D.f i i) ((Opens.map (D.t i i).base).1 (unop ((Opens.map (D.f i i).base).op.obj (op U)))) ≫
              (D.U i).presheaf.map (eqToHom ⋯).op ≫
                (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫
                  (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))

Tactic:
IsOpenImmersion.inv_naturality_assoc

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)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        (D.f i i).c.app (op U) ≫
          invApp (D.f i i) (unop ((Opens.map (D.f i i).base).op.obj (op U))) ≫
            (D.U i).presheaf.map
                ((opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫
              (D.U i).presheaf.map (eqToHom ⋯).op ≫
                (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫
                  (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
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
s : PullbackCone (D.ι i) (D.ι j)
this : (s.fst ≫ D.ι i).base = (s.snd ≫ D.ι j).base
⊢ s.fst.base ≫ (forget C).map (D.ι i) ≫ (D.gluedIso (forget C)).hom =
    s.snd.base ≫ (forget C).map (D.ι j) ≫ (D.gluedIso (forget C)).hom

Tactic:
rw [comp_base, comp_base] at this

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
this : s.fst.base ≫ (D.ι i).base = s.snd.base ≫ (D.ι j).base
⊢ s.fst.base ≫ (forget C).map (D.ι i) ≫ (D.gluedIso (forget C)).hom =
    s.snd.base ≫ (forget C).map (D.ι j) ≫ (D.gluedIso (forget C)).hom
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 : D.J
⊢ IsOpenImmersion (D.ι i)

Tactic:
dsimp [IsOpenImmersion]
  rw [← D.ι_isoPresheafedSpace_inv]
  have := D.toPresheafedSpaceGlueData.ιIsOpenImmersion i
  infer_instance

Goal state after: