mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P✝ Q P : MorphismProperty C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ P.precoverage.coverings X
this : S.HasPullbacks f
Z : C
⊢ ∀ ⦃f_1 : Z ⟶ Y⦄, Presieve.pullbackArrows f S f_1 → P f_1

Tactic:
g

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P✝ Q P : MorphismProperty C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ P.precoverage.coverings X
this : S.HasPullbacks f
Z : C
g : Z ⟶ Y
⊢ Presieve.pullbackArrows f S g → P g
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P✝ Q P : MorphismProperty C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ P.precoverage.coverings X
this : S.HasPullbacks f
⊢ Presieve.pullbackArrows f S ∈ P.precoverage.coverings Y

Tactic:
intro Z g ⟨W, a, h⟩

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
P✝ Q P : MorphismProperty C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ P.precoverage.coverings X
this : S.HasPullbacks f
Z : C
g : Z ⟶ Y
W : C
a : W ⟶ X
h : S a
⊢ P (pullback.snd a f)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ ∀ (j : WalkingCospan),
    (limit.cone (cospan f.base g.base)).π.app j =
      𝟙 (((Functor.const WalkingCospan).obj (limit.cone (cospan f.base g.base)).pt).obj j) ≫
        ((forget C).mapCone (pullbackConeOfLeft f g)).π.app j ≫ (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app j

Tactic:
Category.id_comp

Goal state after:
case w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ ∀ (j : WalkingCospan),
    (limit.cone (cospan f.base g.base)).π.app j =
      ((forget C).mapCone (pullbackConeOfLeft f g)).π.app j ≫ (diagramIsoCospan (cospan f g ⋙ forget C)).hom.app j
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom g.base)
⊢ lift f g ⋯ ≫ lift g f ⋯ = 𝟙 Y

Tactic:
← cancel_mono g

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
inst✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom g.base)
⊢ (lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ g
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
e : Set.range ⇑f = Set.range ⇑g
⊢ lift f g ⋯ ≫ lift g f ⋯ = 𝟙 Y

Tactic:
← cancel_mono g

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst✝ : IsOpenImmersion g
e : Set.range ⇑f = Set.range ⇑g
⊢ (lift f g ⋯ ≫ lift g f ⋯) ≫ g = 𝟙 Y ≫ g
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
⊢ ∀ (g : Y ⟶ Z) [inst : HasPullback f g], IsOpenImmersion g → IsOpenImmersion (pullback.fst f g)

Tactic:
g

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
⊢ ∀ [inst : HasPullback f g], IsOpenImmersion g → IsOpenImmersion (pullback.fst f g)
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
x : ↥X
h :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op ≫ (IsOpenImmersion.ΓIso (𝒰.f (Cover.idx 𝒰 x)) U).inv)) f =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op ≫ (IsOpenImmersion.ΓIso (𝒰.f (Cover.idx 𝒰 x)) U).inv)) g
⊢ (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) f = (ConcreteCategory.hom (X.sheaf.obj.map (homOfLE ⋯).op)) g

Tactic:
exact (IsOpenImmersion.ΓIso (𝒰.f (𝒰.idx x)) U).commRingCatIsoToRingEquiv.symm.injective h

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
fn : 𝒰.I₀ → ℕ
hfn : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s ^ fn i = 0
this : Fintype 𝒰.I₀
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.I₀), fn i ≤ N
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s ^ N = 0

Tactic:
exact pow_eq_zero_of_le (hfnleN i) (hfn i)

Goal state after:
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: X Y : TopCommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget₂ TopCommRingCat TopCat).map f)
i_Top : (forget₂ TopCommRingCat TopCat).obj X ≅ (forget₂ TopCommRingCat TopCat).obj Y :=
  asIso ((forget₂ TopCommRingCat TopCat).map f)
e_Ring : X.α ≃+* Y.α :=
  let __src := ↑f;
  let __src_1 := ((forget TopCat).mapIso i_Top).toEquiv;
  { toFun := (↑↑__src).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
x : X.α
⊢ ↑(ConcreteCategory.hom (f ≫ ⟨↑e_Ring.symm, ⋯⟩)) x = ↑(ConcreteCategory.hom (𝟙 X)) x

Tactic:
exact e_Ring.left_inv x

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ U.ι = 𝟙 ↑U ≫ U.ι

Tactic:
Category.id_comp

Goal state after:
X : Scheme
U : X.Opens
⊢ U.ι = U.ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ (𝟙 X ⁻¹ᵁ U).ι = 𝟙 ↑(𝟙 X ⁻¹ᵁ U) ≫ U.ι

Tactic:
Category.id_comp

Goal state after:
X : Scheme
U : X.Opens
⊢ (𝟙 X ⁻¹ᵁ U).ι = U.ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
⊢ f = 𝟙 X ≫ f

Tactic:
Category.id_comp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
⊢ f = f
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ ((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ (Arrow.mk (f ∣_ Scheme.Hom.opensRange g)).hom) ≫ e.inv =
    (Arrow.mk (pullback.snd f g)).hom

Tactic:
← cancel_mono g

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ (((t ≫ (pullbackRestrictIsoRestrict f V).hom) ≫ (Arrow.mk (f ∣_ Scheme.Hom.opensRange g)).hom) ≫ e.inv) ≫ g =
    (Arrow.mk (pullback.snd f g)).hom ≫ g
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : V' ≤ V
⊢ resLE (𝟙 X ≫ f) U V' ⋯ = resLE f U V' ⋯

Tactic:
Category.id_comp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ U.topIso.hom ≫ (Arrow.mk (Scheme.Hom.appLE f U V e)).hom =
    (Arrow.mk (Scheme.Hom.appTop (Scheme.Hom.resLE f U V e))).hom ≫ V.topIso.hom

Tactic:
simp only [Scheme.Opens.topIso_hom, eqToHom_op, Arrow.mk_hom, Scheme.Hom.map_appLE]
  rw [Scheme.Hom.appTop, ← Scheme.Hom.appLE_eq_app, Scheme.Hom.resLE_appLE, Scheme.Hom.appLE_map]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U ≤ V
⊢ U.toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE h).op) = X.homOfLE h ≫ V.toSpecΓ

Tactic:
delta Scheme.Opens.toSpecΓ
  simp [← Spec.map_comp, ← X.presheaf.map_comp, toSpecΓ_naturality_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) (hU.primeIdealOf ⟨x, hx⟩).asIdeal

Tactic:
set y := hU.primeIdealOf ⟨x, hx⟩ with hy

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
y : PrimeSpectrum ↑Γ(X, U) := hU.primeIdealOf ⟨x, hx⟩
hy : y = hU.primeIdealOf ⟨x, hx⟩
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) y.asIdeal
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
hU : (ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x ∈ U
s : ToType ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
ha :
  IsUnit
    ((ConcreteCategory.hom
        (Y.presheaf.germ ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).obj U) x hU))
      ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s))
V : Opens ↑Y.toTopCat := imageBasicOpen f g U s
hV :
  ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ⁻¹'
      ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier =
    V.carrier
hV' :
  V =
    {
      carrier :=
        ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ⁻¹'
          ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier,
      is_open' := ⋯ }
V_open : IsOpen (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier)
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ U
          ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x) hU))
      s)

Tactic:
have VleU : ⟨(coequalizer.π f.toShHom g.toShHom).hom.base '' V.1, V_open⟩ ≤ U :=
    Set.image_subset_iff.mpr (Y.toRingedSpace.basicOpen_le _)

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
hU : (ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x ∈ U
s : ToType ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
ha :
  IsUnit
    ((ConcreteCategory.hom
        (Y.presheaf.germ ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).obj U) x hU))
      ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s))
V : Opens ↑Y.toTopCat := imageBasicOpen f g U s
hV :
  ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ⁻¹'
      ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier =
    V.carrier
hV' :
  V =
    {
      carrier :=
        ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) ⁻¹'
          ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier,
      is_open' := ⋯ }
V_open : IsOpen (⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier)
VleU :
  { carrier := ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier,
      is_open' := V_open } ≤
    U
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.germ U
          ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) x) hU))
      s)
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 j k)) ⟨↑((ConcreteCategory.hom (h.t i j)) ⟨x, hx⟩), ⋯⟩), ⋯⟩ =
    ↑((ConcreteCategory.hom (h.t i k)) ⟨x, hx'⟩)

Tactic:
exact h.cocycle i j k ⟨x, hx⟩ hx'

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X A B Y : C
f : X ⟶ Y
gA : A ⟶ Y
gB : B ⟶ Y
⊢ Hom.left (prodComparisonIso (pullback f) (mk gA) (mk gB)).inv ≫ pullback.snd (pullback.fst gA gB ≫ gA) f =
    pullback.snd ((pullback f).obj (mk gA)).hom ((pullback f).obj (mk gB)).hom ≫ pullback.snd (mk gB).hom f

Tactic:
by
  rw [← cancel_epi (prodComparisonIso (Over.pullback f) _ _).hom.left,
    Over.hom_left_inv_left_assoc]
  simp [CartesianMonoidalCategory.prodComparison]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inl ≫ (coprodZeroIso X).hom = 𝟙 X

Tactic:
by
  dsimp [coprodZeroIso, binaryCofanZeroRight]
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_2
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this✝ : HasPullback (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ g = 𝟙 Y ≫ g

Tactic:
Category.id_comp

Goal state after:
case refine_2
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j : 𝒰.I₀
this✝ : HasPullback (pullback.snd (𝒰.f j) (𝒰.f i) ≫ 𝒰.f i ≫ f) g
this : HasPullback (pullback.snd (𝒰.f i) (𝒰.f j) ≫ 𝒰.f j ≫ f) g
⊢ g = g
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.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
    𝟙 (v 𝒰 f g i i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)

Tactic:
Category.id_comp

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.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
    pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)
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) =
    𝟙 (v 𝒰 f g i i) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)

Tactic:
Category.id_comp

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) =
    pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_2
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ 𝒰.f k = 𝟙 (𝒰.X k) ≫ 𝒰.f k

Tactic:
Category.id_comp

Goal state after:
case refine_2
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ 𝒰.f k = 𝒰.f k
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.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) =
    𝟙 (pullback (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)

Tactic:
Category.id_comp

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

Tactic:
Category.id_comp

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 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)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ (D.f i j).c.app (op U) ≫
      (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
        (pullback.fst (D.f j i) (D.f j k)).c.app
            (op ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (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)).base).1
                ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              ((TopCat.Presheaf.pushforward C (D.f j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯).op =
    (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 ?w)

Tactic:
← (D.V (j, k)).presheaf.map_comp

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
⊢ (D.f i j).c.app (op U) ≫
      (D.t j i).c.app ((Opens.map (D.f i j).base).op.obj (op U)) ≫
        (pullback.fst (D.f j i) (D.f j k)).c.app
            (op ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (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)).base).1
                ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ (Opens.map (D.f j k).base).op.map (eqToHom ⋯).op) =
    (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 ?w)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
⊢ IsOpenImmersion coprod.inl

Tactic:
← ι_left_coprodIsoSigma_inv

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: case convert_1
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
i : WalkingPair
⊢ IsOpenImmersion (fi i)

Tactic:
cases i <;> (simp [fi]; infer_instance)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: 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
i j : WalkingPair
hij : WalkingPair.left ≠ WalkingPair.right
⊢ Function.onFun Disjoint (fun x ↦ Scheme.Hom.opensRange (fi x)) WalkingPair.left WalkingPair.right

Tactic:
| =>

Goal state after:
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
i j : WalkingPair
hij : WalkingPair.left ≠ WalkingPair.right
⊢ Function.onFun Disjoint (fun x ↦ Scheme.Hom.opensRange (fi x)) WalkingPair.left WalkingPair.right
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: 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
i j : WalkingPair
hij : WalkingPair.right ≠ WalkingPair.left
⊢ Function.onFun Disjoint (fun x ↦ Scheme.Hom.opensRange (fi x)) WalkingPair.right WalkingPair.left

Tactic:
| =>

Goal state after:
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
i j : WalkingPair
hij : WalkingPair.right ≠ WalkingPair.left
⊢ Function.onFun Disjoint (fun x ↦ Scheme.Hom.opensRange (fi x)) WalkingPair.right WalkingPair.left
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
k : (Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).I₀
⊢ (Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).f k ≫ t F i i =
    (Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).f k ≫ 𝟙 ↑(V F i i)

Tactic:
simp only [Category.comp_id, ← cancel_mono (Scheme.Opens.ι _), Category.assoc,
    IsOpenImmersion.lift_fac, Scheme.Cover.ι_glueMorphisms, t, tAux, V]

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
k : (Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).I₀
⊢ (Hom.isoOpensRange (F.map k.snd.1)).inv ≫ F.map k.snd.2 =
    (Opens.iSupOpenCover fun i_1 ↦ Hom.opensRange (F.map i_1.snd.1)).f k ≫ (⨆ k, Hom.opensRange (F.map k.snd.1)).ι