mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hp : p ∈ U
s :
  ToType
    (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op U))
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      ((ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).obj).map
            (homOfLE hrU).op))
        s) =
    y
s' : ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
        (structureSheaf ↑S).obj).obj
    (op (PrimeSpectrum.basicOpen r))) :=
  (ConcreteCategory.hom
      (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
            (structureSheaf ↑S).obj).map
        (homOfLE hrU).op))
    s
h :
  s' =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).map
          (homOfLE hrU).op))
      s
⊢ (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      ((ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).obj).map
            (homOfLE hrU).op))
        s) =
    y

Tactic:
exact e

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
h_base : f.base = g.base
h_app : ∀ (U : Y.Opens), app f U ≫ X.presheaf.map (eqToHom ⋯).op = app g U
⊢ f = g

Tactic:
by
  cases f; cases g; congr 1
  apply LocallyRingedSpace.Hom.ext'
  ext : 1
  · exact h_base
  · exact TopCat.Presheaf.ext (fun U ↦ by simpa using! h_app U)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          ⊤ p trivial).hom'
      ((CommRingCat.ofHom
            (algebraMap (↑S)
              ((structureSheafInType ↑S ↑S).obj.obj
                (op ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj ⊤))))).hom'
        x) =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑(CommRingCat.of ↑S)).obj).germ
          ⊤ p trivial))
      0
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ (fun r ↦ ↑(PrimeSpectrum.basicOpen r)) r
hrU : (fun r ↦ ↑(PrimeSpectrum.basicOpen r)) r ⊆ U.carrier
e✝ :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).map
          (homOfLE hrU).op))
      ((ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).obj).map
            i₁.op))
        ((CommRingCat.ofHom
              (algebraMap (↑S)
                ((structureSheafInType ↑S ↑S).obj.obj
                  (op ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj ⊤))))).hom'
          x)) =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).map
          (homOfLE hrU).op))
      ((ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).obj).map
            i₂.op))
        0)
this✝ :
  (algebraMap ↑S
        ↑((structureSheaf ↑S).presheaf.obj
            ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).op.obj
              (op { carrier := {x | r ∉ x.asIdeal}, is_open' := ⋯ }))))
      x =
    0
this : IsLocalization.mk' (↑((structureSheaf ↑S).obj.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) x 1 = 0
n : ℕ
e : ↑⟨(fun x ↦ (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩ * x = 0
⊢ (algebraMap ↑R ↑S) ↑⟨r, hpr⟩ ^ n * x = 0

Tactic:
exact e

Goal state after:
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
⊢ Presieve.singleton f ∈ jointlySurjectivePrecoverage.coverings Y ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
by
  rw [mem_jointlySurjectivePrecoverage_iff]
  refine ⟨fun hf x ↦ ?_, fun hf x ↦ ⟨X, f, ⟨⟩, by simp [hf.range_eq]⟩⟩
  obtain ⟨_, _, ⟨⟩, hx⟩ := hf x
  exact hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈ Set.range ⇑f ∧ Set.range ⇑f ⊆ ↑U

Tactic:
rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp]

Goal state after:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈
      ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } ''
        Set.range ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))) ∧
    ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } ''
        Set.range ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))) ⊆
      ↑U
Module: Mathlib.CategoryTheory.Sites.JointlySurjective

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
⊢ Types.jointlySurjectivePrecoverage.IsStableUnderBaseChange

Tactic:
by
  rw [← Precoverage.comap_id Types.jointlySurjectivePrecoverage]
  apply isStableUnderBaseChange_comap_jointlySurjectivePrecoverage
  intro X Y S f g _
  exact surjective_of_epi _

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
⊢ MorphismProperty.isomorphisms Scheme f → IsOpenImmersion f

Tactic:
(hf : IsIso f)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : Scheme
f : X✝ ⟶ Y✝
hf : IsIso f
⊢ IsOpenImmersion f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ (s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))) → coequalizer f g ⟶ s.pt

Tactic:
refine fun s ↦ coequalizer.desc s.inl ?_
    have H₁ : f ≫ s.inl = s.inr := by simpa using congr(coprod.inl ≫ $s.condition)
    have H₂ : g ≫ s.inl = s.inr := by simpa using congr(coprod.inr ≫ $s.condition)
    exact H₁.trans H₂.symm

Goal state after:
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✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ pullback.lift (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
        (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯) ⋯ ≫
      equalizer.lift (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯)
        ⋯ =
    𝟙 (equalizer lhs rhs)

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ ((locallyRingedSpaceAdjunction.homEquiv X ((𝟭 CommRingCatᵒᵖ).obj (op (CommRingCat.of R)))).symm
          ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f)).unop ≫
      ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
            X.presheaf).map
        (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
Equiv.symm_apply_apply

Goal state after:
X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ f.unop ≫
      ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
            X.presheaf).map
        (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e'_2
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
e_1✝ : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum ↑Γ(X, U))
⊢ ⋃ i, ⇑hU.fromSpec ⁻¹' ↑(X.basicOpen ↑i) = ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier

Tactic:
refine congr_arg (Set.iUnion ·) ?_
        ext1 x
        exact congr_arg Opens.carrier (hU.fromSpec_preimage_basicOpen _)

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ D.t' j i k ≫ D.t' i k j ≫ pullback.snd (D.f k j) (D.f k i) ≫ D.f k i =
    pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j

Tactic:
apply @Epi.left_cancellation _ _ _ _ (D.t' k j i)

Goal state after:
D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ D.t' k j i ≫ D.t' j i k ≫ D.t' i k j ≫ pullback.snd (D.f k j) (D.f k i) ≫ D.f k i =
    D.t' k j i ≫ pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j
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
i : D.J
⊢ ((if hij : i = i then
        (pullbackSymmetry (D.f' i i) (D.f' i i)).hom ≫
          pullback.map (D.f' i i) (D.f' i i) (D.f' i i) (D.f' i i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
      else
        if hik : i = i then
          have this := ⋯;
          pullback.fst (D.f' i i) (D.f' i i) ≫
            eqToHom ⋯ ≫ D.t i i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i i))
        else
          if hjk : i = i then
            have this := ⋯;
            pullback.fst (D.f' i i) (D.f' i i) ≫
              eqToHom ⋯ ≫ D.t i i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i i))
          else
            pullback.map (D.f' i i) (D.f' i i) (D.f i i hij) (D.f i i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
              D.t' i i i hij hik hjk ≫
                pullback.map (D.f i i hjk) (D.f i i ⋯) (D.f' i i) (D.f' i i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯) ≫
      (if hij : i = i then
          (pullbackSymmetry (D.f' i i) (D.f' i i)).hom ≫
            pullback.map (D.f' i i) (D.f' i i) (D.f' i i) (D.f' i i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
        else
          if hik : i = i then
            have this := ⋯;
            pullback.fst (D.f' i i) (D.f' i i) ≫
              eqToHom ⋯ ≫ D.t i i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i i))
          else
            if hjk : i = i then
              have this := ⋯;
              pullback.fst (D.f' i i) (D.f' i i) ≫
                eqToHom ⋯ ≫ D.t i i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i i))
            else
              pullback.map (D.f' i i) (D.f' i i) (D.f i i hij) (D.f i i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                D.t' i i i hij hik hjk ≫
                  pullback.map (D.f i i hjk) (D.f i i ⋯) (D.f' i i) (D.f' i i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                    ⋯) ≫
        if hij : i = i then
          (pullbackSymmetry (D.f' i i) (D.f' i i)).hom ≫
            pullback.map (D.f' i i) (D.f' i i) (D.f' i i) (D.f' i i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
        else
          if hik : i = i then
            have this := ⋯;
            pullback.fst (D.f' i i) (D.f' i i) ≫
              eqToHom ⋯ ≫ D.t i i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i i))
          else
            if hjk : i = i then
              have this := ⋯;
              pullback.fst (D.f' i i) (D.f' i i) ≫
                eqToHom ⋯ ≫ D.t i i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i i))
            else
              pullback.map (D.f' i i) (D.f' i i) (D.f i i hij) (D.f i i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                D.t' i i i hij hik hjk ≫
                  pullback.map (D.f i i hjk) (D.f i i ⋯) (D.f' i i) (D.f' i i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                    ⋯) =
    𝟙 (pullback (D.f' i i) (D.f' i i))

Tactic:
ext <;> simp

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 = ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ↑V ⊆ ↑(⨆ i ∈ s, X.basicOpen i)

Tactic:
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])]

Goal state after:
case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ↑(⨆ f, X.basicOpen ↑f) ⊆ ↑(⨆ 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
i : ι
hi : ↑x ∈ ↑(U i)
f : ↑Γ(X, ↑V)
g : ↑Γ(X, ↑(U i))
e : X.basicOpen f = X.basicOpen g
hf : ↑x ∈ X.basicOpen f
⊢ ↑(X.affineBasicOpen f) = ↑(X.affineBasicOpen g)

Tactic:
exact e

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e_a
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ Spec.map (Spec.homEquiv (IsOpenImmersion.lift U.ι f ⋯ ≫ hU.isoSpec.hom) ≫ φ) =
    Spec.map (Spec.homEquiv (IsOpenImmersion.lift U.ι g ⋯ ≫ hU.isoSpec.hom) ≫ φ)

Tactic:
simp [← cancel_mono U.ι, H]

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
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ IsOpen
    (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ''
      (imageBasicOpen f g U s).carrier)

Tactic:
by
  rw [← (TopCat.homeoOfIso (PreservesCoequalizer.iso (SheafedSpace.forget _) f.toShHom
    g.toShHom)).isOpen_preimage, TopCat.coequalizer_isOpen_iff, ← Set.preimage_comp]
  erw [← TopCat.coe_comp]
  rw [PreservesCoequalizer.iso_hom, ι_comp_coequalizerComparison]
  dsimp only [SheafedSpace.forget]
  rw [imageBasicOpen_image_preimage]
  exact (imageBasicOpen f g U s).2

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasPullbacks C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst✝ : MonObj (mk f)
⊢ Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f)) ≫ pullback.fst (pullback.fst f f ≫ f) (𝟙 X) =
    Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯)

Tactic:
ext <;> simp

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 j k : 𝒰.I₀
⊢ t' 𝒰 f g i j k ≫
      pullback.snd (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k))
        (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) =
    pullback.fst (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
        (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      t 𝒰 f g i j

Tactic:
by
    apply pullback.hom_ext
    on_goal 1 => apply pullback.hom_ext
    all_goals
      simp only [t'_snd_fst_fst, t'_snd_fst_snd, t'_snd_snd, t_fst_fst, t_fst_snd, t_snd,
        Category.assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h₁
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Scheme.Spec.map coprod.inl ≫
      Spec.map
        ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
          (opProdIsoCoprod R S).unop.inv) =
    coprod.inl ≫
      coprod.desc (Spec.map (CommRingCat.ofHom (RingHom.fst ↑R ↑S))) (Spec.map (CommRingCat.ofHom (RingHom.snd ↑R ↑S)))

Tactic:
coprod.inl_desc,

Goal state after:
case h₁
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Scheme.Spec.map coprod.inl ≫
      Spec.map
        ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
          (opProdIsoCoprod R S).unop.inv) =
    Spec.map (CommRingCat.ofHom (RingHom.fst ↑R ↑S))
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:
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.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
⊢ { I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
        f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.presieve₀ ∈
    (precoverage IsOpenImmersion).coverings (pullback f g)

Tactic:
by
    rw [ofArrows_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, fun i ↦ ?_⟩
    · let 𝒱 := ((gluing 𝒰.ulift f g).openCover.pushforwardIso
              (limit.isoLimitCone ⟨_, gluedIsLimit 𝒰.ulift f g⟩).inv).copy
          𝒰.ulift.I₀ (fun i => pullback (𝒰.ulift.f i ≫ f) g)
          (fun i => pullback.map _ _ _ _ (𝒰.ulift.f i) (𝟙 _) (𝟙 _) (Category.comp_id _) (by simp))
          (Equiv.refl 𝒰.ulift.I₀) (fun _ => Iso.refl _) fun i ↦ by
        simp_rw [Cover.pushforwardIso_I₀, Cover.pushforwardIso_f, GlueData.openCover_f,
          GlueData.openCover_I₀, gluing_J]
        exact pullback.hom_ext (by simp [p1]) (by simp [p2])
      obtain ⟨i, x, rfl⟩ := 𝒱.exists_eq x
      exact ⟨_, x, rfl⟩
    · dsimp
      have : pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) (by simp) (by simp) =
        (pullbackSymmetry _ _).hom ≫ (pullbackLeftPullbackSndIso _ _ _).inv ≫
          pullback.fst _ _ ≫ (pullbackSymmetry _ _).hom := by aesop
      rw [this]
      infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullback f g).OpenCover

Tactic:
apply (openCoverOfLeft (𝒰.pullback₁ f) f g).bind

Goal state after:
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
⊢ (i : (openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).I₀) →
    (precoverage IsOpenImmersion).ZeroHypercover ((openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).X i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := isLocal_affineProperty P
⊢ P.RespectsIso

Tactic:
rw [eq_targetAffineLocally P]

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := isLocal_affineProperty P
⊢ (targetAffineLocally Q).RespectsIso
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))
this : Q.IsLocal := isLocal_affineProperty P
⊢ P f

Tactic:
rw [eq_targetAffineLocally P]

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))
this : Q.IsLocal := isLocal_affineProperty P
⊢ targetAffineLocally Q f