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

Goal state before:
pp: case op.op.snd
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).c.app (op U) ≫
      invApp (pullback.fst (D.f j k) (D.f j i))
          ((Opens.map (D.t' j k i).base).1
            (unop (op ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 (unop (op U)))))) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
          ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
have :
              D.t' j k i ≫ (π₁ k, i, j) ≫ D.t k i ≫ 𝖣.f i k =
                (pullbackSymmetry _ _).hom ≫ (π₁ j, i, k) ≫ D.t j i ≫ D.f i j := by
              rw [← 𝖣.t_fac_assoc, 𝖣.t'_comp_eq_pullbackSymmetry_assoc,
                pullbackSymmetry_hom_comp_snd_assoc, pullback.condition, 𝖣.t_fac_assoc]

Goal state after:
case op.op.snd
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).c.app (op U) ≫
      invApp (pullback.fst (D.f j k) (D.f j i))
          ((Opens.map (D.t' j k i).base).1
            (unop (op ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 (unop (op U)))))) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
          ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯)
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₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯) ≫
      (gluing 𝒰 f g).ι i =
    ((pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i) ≫ (gluing 𝒰 f g).f i j) ≫ (gluing 𝒰 f g).ι i

Tactic:
congr 1

Goal state after:
case e_a
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
      pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ =
    (pullbackFstιToV 𝒰 f g i j ≫ (gluing 𝒰 f g).t j i) ≫ (gluing 𝒰 f g).f i j
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.op.snd
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      (pullbackSymmetry (D.f j k) (D.f j i)).hom.c.app
          (op ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).obj U)) ≫
        (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
          invApp (pullback.fst (D.f j k) (D.f j i))
              ((Opens.map (D.t' j k i).base).1
                ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 U)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
                (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
congr 1

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ invApp (pullback.snd (D.f j i) (D.f j k))
        ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
      (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom.c.app
        (op ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).obj U)) ≫
      (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
        invApp (pullback.fst (D.f j k) (D.f j i))
            ((Opens.map (D.t' j k i).base).1
              ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 U)) ≫
          (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
            ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
              (D.V (j, k)).presheaf.map (eqToHom ⋯)
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
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := ⋯
⊢ ∀ (x y : (a : ι) → R a),
    (algebraMap ((a : ι) → R a) (R i)) x = (algebraMap ((a : ι) → R a) (R i)) y ↔
      Function.update 0 i 1 * x = Function.update 0 i 1 * y

Tactic:
intro x y
      constructor
      · intro e; ext j; by_cases h : j = i <;> aesop
      · intro e; simpa using! congr_fun e i

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
i : WalkingPair
⊢ Mono ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init i))

Tactic:
rw [mono_iff_injective]

Goal state after:
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
i : WalkingPair
⊢ Function.Injective ⇑(ConcreteCategory.hom ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init i)))
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✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ (pullbackP1Iso 𝒰 f g i).hom) ≫
      Multicoequalizer.π (gluing 𝒰 f g).diagram i =
    ((((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
            pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯) ≫
          (pullbackSymmetry s.fst (𝒰.f i)).hom) ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) ≫
      Multicoequalizer.π (gluing 𝒰 f g).diagram i

Tactic:
congr 1

Goal state after:
case e_a
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ (pullbackP1Iso 𝒰 f g i).hom =
    (((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
          pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯) ≫
        (pullbackSymmetry s.fst (𝒰.f i)).hom) ≫
      pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯
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
i : 𝒰.I₀
⊢ pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i)) (pullback.fst g (𝒰.f i))
      (𝒰.f i) ⋯ ⋯ =
    (openCoverOfBase' 𝒰 f g).f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i)

Tactic:
openCoverOfBase'_f

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 : 𝒰.I₀
⊢ pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i)) (pullback.fst g (𝒰.f i))
      (𝒰.f i) ⋯ ⋯ =
    (pullbackSymmetry
          (pullback.snd f
            (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))
          (pullback.snd g
            (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))).hom ≫
      (limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv ≫
        pullback.map
            (pullback.snd f
                (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
              𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst)
            g
            (pullback.fst f
                (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
              f)
            g
            (𝟙
              (pullback f
                (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst)))
            (𝟙 Y) (𝟙 Z) ⋯ ⋯ ≫
          pullback.map
            (pullback.fst f
                (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst) ≫
              f)
            g f g
            (pullback.fst f
              (𝒰.f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i).fst))
            (𝟙 Y) (𝟙 Z) ⋯ ⋯
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ ((D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
        limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
          (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))) ≫
      (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))) =
    limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
        (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))) ≫
      (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k)))

Tactic:
congr 1

Goal state after:
case op.left.e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
      limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
        (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))) =
    limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
      (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))
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) = ⊤
⊢ Ideal.span (Set.range (mulNumerator s p)) = ⊤

Tactic:
← Ideal.radical_eq_top,

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) = ⊤
⊢ (Ideal.span (Set.range (mulNumerator s p))).radical = ⊤
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: case succ
R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : IsLocalization.Away x S
I J : Ideal R
hle : map (algebraMap R S) I ≤ map (algebraMap R S) J
hxJ : ∀ (y : R), x * y ∈ J → y ∈ J
y : R
hy : y ∈ I
n : ℕ
ih : x ^ n * y ∈ J → y ∈ J
h : x ^ (n + 1) * y ∈ J
⊢ y ∈ J

Tactic:
rw [add_comm, pow_add, pow_one, mul_assoc] at h

Goal state after:
case succ
R : Type u_2
S : Type u_3
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : IsLocalization.Away x S
I J : Ideal R
hle : map (algebraMap R S) I ≤ map (algebraMap R S) J
hxJ : ∀ (y : R), x * y ∈ J → y ∈ J
y : R
hy : y ∈ I
n : ℕ
ih : x ^ n * y ∈ J → y ∈ J
h : x * (x ^ n * y) ∈ J
⊢ y ∈ J
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Spec.map (𝟙 (of S)) = Spec.map (ofHom includeLeftRingHom ≫ ofHom ↑(lmul' R))

Tactic:
congr 1

Goal state after:
case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ 𝟙 (of S) = ofHom includeLeftRingHom ≫ ofHom ↑(lmul' R)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Spec.map (𝟙 (of S)) = Spec.map (ofHom ↑includeRight ≫ ofHom ↑(lmul' R))

Tactic:
congr 1

Goal state after:
case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ 𝟙 (of S) = ofHom ↑includeRight ≫ ofHom ↑(lmul' R)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x✝ : QuasiCompact f
h : ∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (⇑f ⁻¹' U)
⊢ Continuous ⇑f

Tactic:
by fun_prop

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
x✝¹ : HasPullback f g
x✝ : IsPreimmersion g
this : SurjectiveOnStalks (pullback.fst f g)
L : ↥(pullback f g) → ↑{x | f x.1 = g x.2} := fun x ↦ ⟨((pullback.fst f g) x, (pullback.snd f g) x), ⋯⟩
⊢ Continuous L

Tactic:
by fun_prop

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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↥Z
hU : IsOpen U
hU' : IsCompact U
⊢ Continuous ⇑g

Tactic:
by fun_prop

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

Goal state before:
pp: case mp
X : Scheme
⊢ (∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) →
    ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

pp: case mpr
X : Scheme
⊢ (∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)) →
    ∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)

Tactic:
· intro H U V; exact H U V U.1.2 U.2.isCompact V.1.2 V.2.isCompact

Goal state after:
case mpr
X : Scheme
⊢ (∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)) →
    ∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case a
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
U : Set ↥Z
hU : IsOpen U
hU' : IsCompact U
⊢ IsOpen (⇑g ⁻¹' U)

Tactic:
exact Continuous.isOpen_preimage (by fun_prop) _ hU

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

Goal state before:
pp: X : Scheme
⊢ QuasiSeparatedSpace ↥X ↔ QuasiCompact (prod.lift (𝟙 X) (𝟙 X))

Tactic:
← MorphismProperty.cancel_right_of_respectsIso @QuasiCompact _ (prodIsoPullback X X).hom,

Goal state after:
X : Scheme
⊢ QuasiSeparatedSpace ↥X ↔ QuasiCompact (prod.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case refine_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
H' :
  ∀ (i : ↑s),
    ∃ n,
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n *
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
        0
⊢ ∃ n, f ^ n * x = 0

Tactic:
choose n hn using H'

Goal state after:
case refine_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
hn :
  ∀ (i : ↑s),
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n i *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x =
      0
⊢ ∃ n, f ^ n * x = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case h
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
hn :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ (Finset.univ.sup n - n i)) *
      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n i *
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x) =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ (Finset.univ.sup n - n i)) * 0
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ Finset.univ.sup n * x) = 0

Tactic:
simp only [← map_mul, ← map_pow] at hn

Goal state after:
case h
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
n : ↑s → ℕ
this : Finite ↑s
val✝ : Fintype ↑s
i : ↑s
hn :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ (Finset.univ.sup n - n i) * (f ^ n i * x)) =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ (Finset.univ.sup n - n i)) * 0
⊢ (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) (f ^ Finset.univ.sup n * x) = 0
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
⊢ Antitone support

Tactic:
by
  intro I J h
  rw [← SetLike.coe_subset_coe, I.coe_support_eq_eq_iInter_zeroLocus,
    J.coe_support_eq_eq_iInter_zeroLocus]
  exact Set.iInter_mono fun U ↦ X.zeroLocus_mono (h U)

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsIso f ↔ IsOpenImmersion f ∧ Surjective f

Tactic:
rw [surjective_iff, ← TopCat.epi_iff_surjective, isIso_iff_isOpenImmersion_and_epi_base]

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

Goal state before:
pp: ⊢ (((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Topology.IsOpenEmbedding) ⊓
        topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) ⊓
      stalkwise fun {R S} [CommRing R] [CommRing S] x ↦ Function.Bijective ⇑x) =
    (isomorphisms TopCat).inverseImage Scheme.forgetToTop ⊓
      stalkwise fun {R S} [CommRing R] [CommRing S] f ↦ Function.Bijective ⇑f

Tactic:
congr 1

Goal state after:
case e_a
⊢ ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Topology.IsOpenEmbedding) ⊓
      topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective) =
    (isomorphisms TopCat).inverseImage Scheme.forgetToTop
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(IsAffineOpen.isoSpec ⋯).inv '' Set.range ⇑(Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))) =
    (fun a ↦ (IsAffineOpen.isoSpec ⋯).inv a) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
range_comap_of_surjective

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(IsAffineOpen.isoSpec ⋯).inv ''
      PrimeSpectrum.zeroLocus ↑(RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))) =
    (fun a ↦ (IsAffineOpen.isoSpec ⋯).inv a) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

case hf
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
⊢ (I * J).radical = I.radical ⊓ J.radical

Tactic:
by
  ext U : 2
  simp only [radical_ideal, ideal_mul, Pi.mul_apply, Ideal.radical_mul, ideal_inf, Pi.inf_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫
      Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫
        (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv ≫ X.homOfLE h

Tactic:
congr 1

Goal state after:
case e_a
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    (IsAffineOpen.isoSpec ⋯).inv ≫ X.homOfLE h
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑I.support) =
    PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑(I.ideal U))

Tactic:
congr 1

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑I.support = PrimeSpectrum.zeroLocus ↑(I.ideal U)
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ Spec.map ((U.topIso.inv ≫ (↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial) ≫ inv (Hom.stalkMap U.ι ⟨x, hxU⟩)) =
    Spec.map (X.presheaf.germ U x hxU)

Tactic:
congr 1

Goal state after:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ (U.topIso.inv ≫ (↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial) ≫ inv (Hom.stalkMap U.ι ⟨x, hxU⟩) = X.presheaf.germ U x hxU
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : X.Opens
hU : f (closedPoint ↑R) ∈ U
⊢ Hom.app f U ≫ (Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint ↑R) hU ≫ (stalkClosedPointIso R).hom =
    Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (eqToIso ⋯).op).hom ≫ (ΓSpecIso R).hom

Tactic:
congr 1

Goal state after:
case e_a
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : X.Opens
hU : f (closedPoint ↑R) ∈ U
⊢ (Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint ↑R) hU ≫ (stalkClosedPointIso R).hom =
    (Functor.mapIso (Spec R).presheaf (eqToIso ⋯).op).hom ≫ (ΓSpecIso R).hom