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

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ (t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ 𝒰.f i =
    pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ 𝒰.f i

Tactic:
;

Goal state after:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ (t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ 𝒰.f i =
    pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ 𝒰.f i
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
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))
⊢ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map
        ((eqToHom ⋯).op ≫
          (opensFunctor (pullback.fst (D.f k i) (D.f k j))).op.map (eqToHom ⋯) ≫
            (opensFunctor (pullback.fst (D.f k i) (D.f k j))).op.map
              ((Opens.map (D.t' k i j).base).map (eqToHom ⋯).unop).op)

Tactic:
;

Goal state after:
case h
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))
⊢ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map
        ((eqToHom ⋯).op ≫
          (opensFunctor (pullback.fst (D.f k i) (D.f k j))).op.map (eqToHom ⋯) ≫
            (opensFunctor (pullback.fst (D.f k i) (D.f k j))).op.map
              ((Opens.map (D.t' k i j).base).map (eqToHom ⋯).unop).op)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
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 ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.snd (𝒰.f i ≫ f) g =
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.snd (𝒰.f i ≫ f) g

Tactic:
· simp_rw [Category.assoc, cocycle_snd_fst_snd 𝒰 f g i j k]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
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 ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)

Tactic:
· apply pullback.hom_ext
    · apply pullback.hom_ext
      · simp_rw [Category.assoc, cocycle_snd_fst_fst 𝒰 f g i j k]
      · simp_rw [Category.assoc, cocycle_snd_fst_snd 𝒰 f g i j k]
    · simp_rw [Category.assoc, cocycle_snd_snd 𝒰 f g i j k]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inst
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥X
i : ↥X
⊢ IsIso (Scheme.Hom.stalkMap f i)

Tactic:
;

Goal state after:
case inst
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥X
i : ↥X
⊢ IsIso (Scheme.Hom.stalkMap f i)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inst
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥X
i : ↥X
⊢ IsIso (Scheme.Hom.stalkMap f i)

Tactic:
exact isEmptyElim i

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥Y
this : IsEmpty ↥X
⊢ Function.Surjective ⇑f

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsEmpty ↥Y
this : IsEmpty ↥X
⊢ Function.Surjective ⇑f
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X : Scheme
inst✝ : IsEmpty ↥X
⊢ Subsingleton ↑Γ(X, ⊥)

Tactic:
;

Goal state after:
X : Scheme
inst✝ : IsEmpty ↥X
⊢ Subsingleton ↑Γ(X, ⊥)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X : Scheme
inst✝ : Subsingleton ↥X
x : ↥X
U : Opens ↥X
hU : IsAffine ↑U
hxU : x ∈ ↑U
y : ↥X
⊢ y ∈ ↑U ↔ y ∈ ↑⊤

Tactic:
;

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

Goal state before:
pp: case refine_1
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
k : Discrete σ
x : ↥((Discrete.functor g).obj k)
⊢ ⟨k.1, ((Discrete.functor g).map { down := { down := ⋯ } }) x⟩ =
    ⟨k.1, ((Discrete.functor g).map { down := { down := ⋯ } }) x⟩

Tactic:
;

Goal state after:
case refine_1
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
k : Discrete σ
x : ↥((Discrete.functor g).obj k)
⊢ ⟨k.1, ((Discrete.functor g).map { down := { down := ⋯ } }) x⟩ =
    ⟨k.1, ((Discrete.functor g).map { down := { down := ⋯ } }) x⟩
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
this : Topology.IsOpenEmbedding (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))
⊢ ⇑(Sigma.desc α) = (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ∘ ⇑(sigmaMk f).symm

Tactic:
;

Goal state after:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
this : Topology.IsOpenEmbedding (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))
⊢ ⇑(Sigma.desc α) = (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ∘ ⇑(sigmaMk f).symm
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
this : Topology.IsOpenEmbedding (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))
x✝ : ↥(∐ f)
⊢ (Sigma.desc α) x✝ = ((⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ∘ ⇑(sigmaMk f).symm) x✝

Tactic:
;

Goal state after:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
this : Topology.IsOpenEmbedding (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f))
x✝ : ↥(∐ f)
⊢ (Sigma.desc α) x✝ = ((⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ∘ ⇑(sigmaMk f).symm) x✝
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ IsOpenImmersion
    (Sigma.ι (fun i ↦ WalkingPair.casesOn i.down X Y) { down := WalkingPair.left } ≫ (coprodIsoSigma X Y).inv)

Tactic:
;

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ IsOpenImmersion
    (Sigma.ι (fun i ↦ WalkingPair.casesOn i.down X Y) { down := WalkingPair.left } ≫ (coprodIsoSigma X Y).inv)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ IsOpenImmersion
    (Sigma.ι (fun i ↦ WalkingPair.casesOn i.down X Y) { down := WalkingPair.right } ≫ (coprodIsoSigma X Y).inv)

Tactic:
;

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ IsOpenImmersion
    (Sigma.ι (fun i ↦ WalkingPair.casesOn i.down X Y) { down := WalkingPair.right } ≫ (coprodIsoSigma X Y).inv)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst
hlj : l ⟶ k₂.fst
y : (F ⋙ forget).obj l
hy₁ :
  (ConcreteCategory.hom ((F ⋙ forget).map hli)) y =
    (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).inv) x
hy₂ :
  (ConcreteCategory.hom ((F ⋙ forget).map hlj)) y =
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) x
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom)
    (F.map hlj ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).hom) ⋯
⊢ IsOpenImmersion (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom)

Tactic:
;

Goal state after:
J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst
hlj : l ⟶ k₂.fst
y : (F ⋙ forget).obj l
hy₁ :
  (ConcreteCategory.hom ((F ⋙ forget).map hli)) y =
    (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).inv) x
hy₂ :
  (ConcreteCategory.hom ((F ⋙ forget).map hlj)) y =
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) x
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom)
    (F.map hlj ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).hom) ⋯
⊢ IsOpenImmersion (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case 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
⊢ (Opens.map (D.f j k).base).obj (unop (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U)))) =
    (Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.left (j, k))))).base).obj (⋯.functor.obj U)

Tactic:
;

Goal state after:
case 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
⊢ (Opens.map (D.f j k).base).obj (unop (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U)))) =
    (Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.left (j, k))))).base).obj (⋯.functor.obj U)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case convert_1.left
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := fun j ↦ WalkingPair.casesOn j f g
⊢ IsOpenImmersion f

Tactic:
;

Goal state after:
case convert_1.left
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := fun j ↦ WalkingPair.casesOn j f g
⊢ IsOpenImmersion f
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
X Y : WalkingMultispan (MultispanShape.prod D.J)
f' : op X ⟶ op Y
f : Y ⟶ X := f'.unop
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop (op Y)) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map f'

Tactic:
;

Goal state after:
case op.op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
X Y : WalkingMultispan (MultispanShape.prod D.J)
f' : op X ⟶ op Y
f : Y ⟶ X := f'.unop
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop (op Y)) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map f'
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case convert_1.right
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := fun j ↦ WalkingPair.casesOn j f g
⊢ IsOpenImmersion g

Tactic:
;

Goal state after:
case convert_1.right
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := fun j ↦ WalkingPair.casesOn j f g
⊢ IsOpenImmersion g
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
X Y : WalkingMultispan (MultispanShape.prod D.J)
f' : op X ⟶ op Y
f : Y ⟶ X := f'.unop
this : f' = f.op
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop (op Y)) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map f'

Tactic:
;

Goal state after:
case op.op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
X Y : WalkingMultispan (MultispanShape.prod D.J)
f' : op X ⟶ op Y
f : Y ⟶ X := f'.unop
this : f' = f.op
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop (op Y)) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map f'
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
X Y : WalkingMultispan (MultispanShape.prod D.J)
f' : op X ⟶ op Y
f : Y ⟶ X
this : f' = f.op
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop (op Y)) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map f'

Tactic:
;

Goal state after:
case op.op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
X Y : WalkingMultispan (MultispanShape.prod D.J)
f' : op X ⟶ op Y
f : Y ⟶ X
this : f' = f.op
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop (op Y)) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map f'
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case a.inl
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
y : ↥X'
x : ↥X
hxy : coprod.inl y = (coprod.map f g) ((coprodMk X Y) (Sum.inl x))
⊢ (coprodMk X Y) (Sum.inl x) ∈ ↑(Scheme.Hom.opensRange coprod.inl)

Tactic:
;

Goal state after:
case a.inl
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
y : ↥X'
x : ↥X
hxy : coprod.inl y = (coprod.map f g) ((coprodMk X Y) (Sum.inl x))
⊢ (coprodMk X Y) (Sum.inl x) ∈ ↑(Scheme.Hom.opensRange coprod.inl)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case a.inr
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
y : ↥X'
x : ↥Y
hxy : coprod.inl y = (coprod.map f g) ((coprodMk X Y) (Sum.inr x))
⊢ (coprodMk X Y) (Sum.inr x) ∈ Scheme.Hom.opensRange coprod.inl

Tactic:
· simp only [coprodMk_inr, ← Scheme.Hom.comp_apply, coprod.inr_map] at hxy
      cases Set.disjoint_iff_forall_ne.mp (isCompl_range_inl_inr _ _).1 ⟨y, rfl⟩ ⟨_, rfl⟩ hxy

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
x✝ : ↑(CommRingCat.of R) × S
⊢ x✝ ∈ Ideal.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.fst R S))) x.asIdeal ↔ x✝ ∈ x.asIdeal.prod ⊤

Tactic:
;

Goal state after:
case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
x✝ : ↑(CommRingCat.of R) × S
⊢ x✝ ∈ Ideal.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.fst R S))) x.asIdeal ↔ x✝ ∈ x.asIdeal.prod ⊤
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
x✝ : R × ↑(CommRingCat.of S)
⊢ x✝ ∈ Ideal.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.snd R S))) x.asIdeal ↔ x✝ ∈ ⊤.prod x.asIdeal

Tactic:
;

Goal state after:
case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
x✝ : R × ↑(CommRingCat.of S)
⊢ x✝ ∈ Ideal.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (RingHom.snd R S))) x.asIdeal ↔ x✝ ∈ ⊤.prod x.asIdeal
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
⊢ ((Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inr x)).asIdeal

Tactic:
change Ideal.comap _ _ = Ideal.prod ⊤ x.asIdeal
    ext; simp [Ideal.prod, CommRingCat.ofHom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))
⊢ (coprodSpec R S) x =
    (ConcreteCategory.hom
        (TopCat.isoOfHomeo
            (PrimeSpectrum.primeSpectrumProdHomeo.trans
              (coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))))).inv)
      x

Tactic:
;

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S))
⊢ (coprodSpec R S) x =
    (ConcreteCategory.hom
        (TopCat.isoOfHomeo
            (PrimeSpectrum.primeSpectrumProdHomeo.trans
              (coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))))).inv)
      x
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
S : CommRingCatᵒᵖ
R : CommRingCat
⊢ IsIso (coprodComparison Scheme.Spec (op R) S)

Tactic:
;

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
S : CommRingCatᵒᵖ
R : CommRingCat
⊢ IsIso (coprodComparison Scheme.Spec (op R) S)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case he
ι : 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) := (Pi.evalRingHom R i).toAlgebra
j : ι
⊢ (Function.update 0 i 1 * Function.update 0 i 1) j = Function.update 0 i 1 j

Tactic:
;

Goal state after:
case he
ι : 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) := (Pi.evalRingHom R i).toAlgebra
j : ι
⊢ (Function.update 0 i 1 * Function.update 0 i 1) j = Function.update 0 i 1 j
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case H.mp
ι : 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) := (Pi.evalRingHom R i).toAlgebra
x y : (a : ι) → R a
e : (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:
;

Goal state after:
case H.mp
ι : 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) := (Pi.evalRingHom R i).toAlgebra
x y : (a : ι) → R a
e : (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
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case H.mp
ι : 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) := (Pi.evalRingHom R i).toAlgebra
x y : (a : ι) → R a
e : (algebraMap ((a : ι) → R a) (R i)) x = (algebraMap ((a : ι) → R a) (R i)) y
j : ι
⊢ (Function.update 0 i 1 * x) j = (Function.update 0 i 1 * y) j

Tactic:
;

Goal state after:
case H.mp
ι : 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) := (Pi.evalRingHom R i).toAlgebra
x y : (a : ι) → R a
e : (algebraMap ((a : ι) → R a) (R i)) x = (algebraMap ((a : ι) → R a) (R i)) y
j : ι
⊢ (Function.update 0 i 1 * x) j = (Function.update 0 i 1 * y) j
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case H.mpr
ι : 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) := (Pi.evalRingHom R i).toAlgebra
x y : (a : ι) → R a
e : Function.update 0 i 1 * x = Function.update 0 i 1 * y
⊢ (algebraMap ((a : ι) → R a) (R i)) x = (algebraMap ((a : ι) → R a) (R i)) y

Tactic:
;

Goal state after:
case H.mpr
ι : 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) := (Pi.evalRingHom R i).toAlgebra
x y : (a : ι) → R a
e : Function.update 0 i 1 * x = Function.update 0 i 1 * y
⊢ (algebraMap ((a : ι) → R a) (R i)) x = (algebraMap ((a : ι) → R a) (R i)) y
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
inst✝ : Finite ι
R : ι → CommRingCat
b✝ : ι
⊢ Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i ↦ ↑(R i)) b✝)) = Spec.map ((CommRingCat.piFan R).proj b✝)

Tactic:
;

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
inst✝ : Finite ι
R : ι → CommRingCat
b✝ : ι
⊢ Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i ↦ ↑(R i)) b✝)) = Spec.map ((CommRingCat.piFan R).proj b✝)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι✝ : Type u
f : ι✝ → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Finite σ
inst✝ : ∀ (i : σ), IsAffine (g i)
ι : Type u
e : σ ≃ ι
this : Finite ι
i : ι
⊢ IsAffine (g (e.symm i))

Tactic:
;

Goal state after:
ι✝ : Type u
f : ι✝ → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Finite σ
inst✝ : ∀ (i : σ), IsAffine (g i)
ι : Type u
e : σ ≃ ι
this : Finite ι
i : ι
⊢ IsAffine (g (e.symm i))