mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ unsym a * unsym b * unsym a * unsym a + unsym b * unsym a * unsym a * unsym a +
          unsym a * unsym a * unsym a * unsym b +
        unsym a * unsym a * unsym b * unsym a -
      (unsym a * unsym b * unsym a * unsym a + unsym a * unsym a * unsym a * unsym b +
          unsym b * unsym a * unsym a * unsym a +
        unsym a * unsym a * unsym b * unsym a) =
    0

Tactic:
rw [add_sub_add_right_eq_sub, add_assoc, add_assoc, add_sub_add_left_eq_sub, add_comm,
        add_sub_add_right_eq_sub, sub_eq_zero]

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
u : U
⊢ A.compHahnSeries B (r • u) = r • A.compHahnSeries B u

Tactic:
by
  ext
  simp only [compHahnSeries_coeff, map_smul, coeff_apply_apply, HahnSeries.coeff_smul]
  rw [← HahnSeries.coeff_smul]

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

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
⊢ g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf = g₂.c

Tactic:
ext V

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens ↑↑(X.restrict hf)
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
⊢ IsColimit ((forget C).mapCocone (colimitCocone F))

Tactic:
apply IsColimit.ofIsoColimit (colimit.isColimit _)

Goal state after:
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
⊢ colimit.cocone (F ⋙ forget C) ≅ (forget C).mapCocone (colimitCocone F)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ (P.and Q.toPrelocalPredicate).pred f

Tactic:
refine ⟨P.locality f ?_, Q.locality f ?_⟩ <;>
      (intro x; have ⟨V, hV, i, h⟩ := w x; use V, hV, i)

Goal state after:
case h
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
x : ↥U✝
V : Opens ↑X
hV : ↑x ∈ V
i : V ⟶ U✝
h : (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ P.pred fun x ↦ f (i x)

case h
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
x : ↥U✝
V : Opens ↑X
hV : ↑x ∈ V
i : V ⟶ U✝
h : (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ Q.pred fun x ↦ f (i x)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case inr
X : Scheme
x : ↥X
hx : IsClosed {x}
b : ↥X
a✝ : b ≤ x
h : b ≠ x
⊢ x ≤ b

Tactic:
have := IsClosed.not_specializes hx rfl h

Goal state after:
case inr
X : Scheme
x : ↥X
hx : IsClosed {x}
b : ↥X
a✝ : b ≤ x
h : b ≠ x
this : ¬x ⤳ b
⊢ x ≤ b
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₁ : U = U'
e₂ : V = V'
P : {R S : CommRingCat} → (R ⟶ S) → Prop
⊢ P (appLE f U V e) ↔ P (appLE f U' V' ⋯)

Tactic:
subst e₁

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₂ : V = V'
P : {R S : CommRingCat} → (R ⟶ S) → Prop
⊢ P (appLE f U V e) ↔ P (appLE f U V' ⋯)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
⊢ X.basicOpen (f + g) ≤ X.basicOpen f ⊔ X.basicOpen g

Tactic:
by
  intro x hx
  have hxU : x ∈ U := X.basicOpen_le _ hx
  simp_rw [← SetLike.mem_coe, Opens.coe_sup, Set.mem_union, SetLike.mem_coe] -- TODO : Opens.mem_sup
  simp only [Scheme.mem_basicOpen _ _ _ hxU, map_add] at hx ⊢
  exact IsLocalRing.isUnit_or_isUnit_of_isUnit_add hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case h
R : CommRingCat
s : Set ↑Γ(Spec R, ⊤)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv)

Tactic:
exact (ConcreteCategory.bijective_of_isIso (C := CommRingCat) _).2

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ (appIso f U).inv ≫ app f (f ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯).op = 𝟙 Γ(X, U)

Tactic:
rw [Scheme.Hom.appIso_inv_app_assoc, ← Functor.map_comp, ← X.presheaf.map_id]

Goal state after:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ X.presheaf.map ((eqToHom ⋯).op ≫ (eqToHom ⋯).op) = X.presheaf.map (𝟙 (op U))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₁ : U = U'
e₂ : V = V'
P : MorphismProperty Scheme
⊢ P (resLE f U V e) ↔ P (resLE f U' V' ⋯)

Tactic:
subst e₁

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₂ : V = V'
P : MorphismProperty Scheme
⊢ P (resLE f U V e) ↔ P (resLE f U V' ⋯)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : TopologicalSpace.Opens ↥X
x : ↥X
hU : x ∈ ↑U
S : Set ↥X
hS : S ∈ {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}
hxS : x ∈ S
hSU : S ⊆ ↑U
⊢ { carrier := S, is_open' := ⋯ } ∈ X.affineOpens

Tactic:
rcases hS with ⟨i, rfl⟩

Goal state after:
X : Scheme
U : TopologicalSpace.Opens ↥X
x : ↥X
hU : x ∈ ↑U
i : X.affineBasisCover.I₀
hxS : x ∈ Set.range ⇑(X.affineBasisCover.f i)
hSU : Set.range ⇑(X.affineBasisCover.f i) ⊆ ↑U
⊢ { carrier := Set.range ⇑(X.affineBasisCover.f i), is_open' := ⋯ } ∈ X.affineOpens
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e'_3
X : Scheme
inst✝ : IsAffine X
e_2✝ : X.instTopologicalSpaceCarrierCarrier = (Scheme.forgetToTop.obj X).str
⊢ Set.range X.basicOpen =
    {x |
      ∃ U ∈ Set.range PrimeSpectrum.basicOpen,
        { carrier := ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' ↑U, is_open' := ⋯ } = x}

Tactic:
ext V

Goal state after:
case e'_3
X : Scheme
inst✝ : IsAffine X
e_2✝ : X.instTopologicalSpaceCarrierCarrier = (Scheme.forgetToTop.obj X).str
V : Opens ↥X
⊢ V ∈ Set.range X.basicOpen ↔
    V ∈
      {x |
        ∃ U ∈ Set.range PrimeSpectrum.basicOpen,
          { carrier := ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' ↑U, is_open' := ⋯ } = x}
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
| hV.isoSpec.inv ≫ V.ι

Tactic:
← X.homOfLE_ι (V := U) f.unop.le,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
| hV.isoSpec.inv ≫ X.homOfLE ⋯ ≫ U.ι
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
this :
  CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)))
          ((structureSheafInType ↑(unop (op (Γ.obj (op X)))) ↑(unop (op (Γ.obj (op X))))).obj.obj (op (basicOpen 1)))) ≫
      X.toΓSpecSheafedSpace.hom.c.app (op (basicOpen 1)) =
    X.toToΓSpecMapBasicOpen 1
⊢ CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)))
          ((structureSheafInType ↑(unop (op (Γ.obj (op X)))) ↑(unop (op (Γ.obj (op X))))).obj.obj (op ⊤))) ≫
      X.toΓSpec.c.app (op ⊤) =
    𝟙 (Γ.obj (op X))

Tactic:
unfold toToΓSpecMapBasicOpen toΓSpecMapBasicOpen at this

Goal state after:
X : LocallyRingedSpace
this :
  CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)))
          ((structureSheafInType ↑(unop (op (Γ.obj (op X)))) ↑(unop (op (Γ.obj (op X))))).obj.obj (op (basicOpen 1)))) ≫
      X.toΓSpecSheafedSpace.hom.c.app (op (basicOpen 1)) =
    X.presheaf.map ((Opens.map X.toΓSpecBase).obj (basicOpen 1)).leTop.op
⊢ CommRingCat.ofHom
        (algebraMap (↑(Γ.obj (op X)))
          ((structureSheafInType ↑(unop (op (Γ.obj (op X)))) ↑(unop (op (Γ.obj (op X))))).obj.obj (op ⊤))) ≫
      X.toΓSpec.c.app (op ⊤) =
    𝟙 (Γ.obj (op X))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
⊢ ⊤.ι = ⋯.isoSpec.hom ≫ X.isoSpec.inv

Tactic:
simp [isoSpec_hom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
ι : Type u_1
U : ι → X.Opens
hU : IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
x : ↥X
⊢ ⋯.fromSpec (⋯.isoSpec.hom ⟨x, ⋯⟩) = x

Tactic:
simp [← Scheme.Hom.comp_apply]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) x =
    (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y

Tactic:
have : colimit.ι diagram one x = colimit.ι diagram one y := by
    dsimp only [coequalizer.π] at h
    rw [← ι_preservesColimitIso_hom, ConcreteCategory.forget_map_eq_ofHom, types_comp_apply]
    simp_all

Goal state after:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) x =
    (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
this : (ConcreteCategory.hom (colimit.ι diagram one)) x = (ConcreteCategory.hom (colimit.ι diagram one)) y
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel ⇑(ConcreteCategory.hom D.diagram.fstSigmaMap)
      ⇑(ConcreteCategory.hom D.diagram.sndSigmaMap))
    x y
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U =
    (fun x ↦
        (⇑(ConcreteCategory.hom (D.f i j)) ∘ ⇑(ConcreteCategory.hom (D.t j i)))
          ((ConcreteCategory.hom (D.t i j)) x)) ⁻¹'
      U

pp: case hf
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ Function.Bijective ⇑(ConcreteCategory.hom (D.t i j))

Tactic:
· change _ = (D.t i j ≫ D.t j i ≫ _) ⁻¹' _
    rw [𝖣.t_inv_assoc]

Goal state after:
case hf
D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ Function.Bijective ⇑(ConcreteCategory.hom (D.t i j))
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
x : ↑(of α)
i : J
hx : x ∈ (fun i ↦ ↑(U i)) i
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Tactic:
exact ⟨(ofOpenSubsets U).toGlueData.ι i ⟨x, hx⟩, ι_fromOpenSubsetsGlue_apply _ _ _⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

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

Tactic:
ext y

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: σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
h : i ≠ j
⊢ Disjoint (Scheme.Hom.opensRange (Sigma.ι g i)) (Scheme.Hom.opensRange (Sigma.ι g j))

Tactic:
intro U hU hU' x hx
  obtain ⟨x, rfl⟩ := hU hx
  obtain ⟨y, hy⟩ := hU' hx
  obtain ⟨rfl⟩ := (sigmaι_eq_iff _ _ _ _ _).mp hy
  cases h rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g✝ : σ → Scheme
inst✝ : Small.{u, v} σ
g : σ → Scheme
i j : σ
hij : i ≠ j
⊢ Nonempty (IsInitial (pullback.cone (Sigma.ι g i) (Sigma.ι g j)).pt)

Tactic:
rw [isInitial_iff_isEmpty]

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g✝ : σ → Scheme
inst✝ : Small.{u, v} σ
g : σ → Scheme
i j : σ
hij : i ≠ j
⊢ IsEmpty ↥(pullback.cone (Sigma.ι g i) (Sigma.ι g j)).pt
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case left.refine_2
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ix : ι
x y : ↥(f ix)
e : (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ⟨ix, x⟩ = (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ⟨ix, y⟩
this : (α ix) x = (α ix) y
⊢ ⟨ix, x⟩ = ⟨ix, y⟩

Tactic:
(α ix).isOpenEmbedding.injective this

Goal state after:
case left.refine_2
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ix : ι
x y : ↥(f ix)
e : (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ⟨ix, x⟩ = (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ⟨ix, y⟩
this : (α ix) x = (α ix) y
⊢ ⟨ix, y⟩ = ⟨ix, y⟩
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case right.refine_1
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
x : ↥(∐ f)
y :
  ↥((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).X
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
hy :
  ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ (Sigma.desc α)
      (((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y) =
    (α (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x).as) y

Tactic:
simp [← Scheme.Hom.comp_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h
σ : Type v
inst✝¹ : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst✝ : ∀ (i : σ), IsOpenImmersion (f i)
hcov : ⨆ i, Scheme.Hom.opensRange (f i) = ⊤
hdisj : _root_.Pairwise (Disjoint on fun x ↦ Scheme.Hom.opensRange (f x))
this✝ : IsOpenImmersion (Sigma.desc f)
i : σ
y : ↥(X i)
hx : (f i) y ∈ ⊤
this : (f i) y ∈ ⨆ i, Scheme.Hom.opensRange (f i)
⊢ (Sigma.desc f) ((Sigma.ι X i) y) = (f i) y

Tactic:
simp [← Scheme.Hom.comp_apply]

Goal state after:
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₀
⊢ (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)).ι

Tactic:
simp [Scheme.Opens.iSupOpenCover, Iso.inv_comp_eq, Subsingleton.elim k.2.1 k.2.2]

Goal state after:
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.opensImagePreimageMap i k U ≫
      (D.f k j).c.app (op ((Opens.map (D.ι k).base).obj (⋯.functor.obj U))) ≫
        (D.t j k).c.app ((Opens.map (D.f k j).base).op.obj (op ((Opens.map (D.ι k).base).obj (⋯.functor.obj U)))) ≫
          (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
rw [opensImagePreimageMap_app_assoc, (D.t j k).c.naturality_assoc,
                snd_invApp_t_app_assoc,
                ← PresheafedSpace.comp_c_app_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
⊢ (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.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
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : α z = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← cancel_mono (pullback.snd _ _), ← cancel_mono (Scheme.Opens.ι _)]

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
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : α z = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
x y : ↑↑(D.U i)
h1 : y ∈ U
h2 :
  (ConcreteCategory.hom (D.ι i).base) y =
    (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) x
⊢ x ∈ U

Tactic:
convert! h1 using 1

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
x y : ↑↑(D.U i)
h1 : y ∈ U
h2 :
  (ConcreteCategory.hom (D.ι i).base) y =
    (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) x
⊢ x = y
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h.hU
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ ↑U ⊆ Set.range ⇑(ConcreteCategory.hom (D.f i i).base)

Tactic:
· rw [Set.range_eq_univ.mpr _]
    · simp
    · rw [← TopCat.epi_iff_surjective]
      infer_instance

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

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝² : P.IsLocal
X Y UX UY : Scheme
inst✝¹ : IsAffine UY
f : X ⟶ Y
iY : UY ⟶ Y
inst✝ : IsOpenImmersion iY
iX : UX ⟶ X
f' : UX ⟶ UY
h : IsPullback iX f' f iY
hf : targetAffineLocally P f
⊢ P (pullback.snd f iY)

Tactic:
exact (P.arrow_mk_iso_iff
    (morphismRestrictOpensRange f _)).mp (hf ⟨_, isAffineOpen_opensRange iY⟩)

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
this : Q.IsLocal := isLocal_affineProperty P
⊢ P f ↔ ∀ (i : 𝒰.toPreZeroHypercover.1), Q (Scheme.Cover.pullbackHom 𝒰 f i)

Tactic:
rw [iff_of_iSup_eq_top (P := P)
    (fun i ↦ ⟨_, isAffineOpen_opensRange _⟩) 𝒰.iSup_opensRange]

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
this : Q.IsLocal := isLocal_affineProperty P
⊢ (∀ (i : 𝒰.I₀), Q (f ∣_ ↑⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩)) ↔
    ∀ (i : 𝒰.toPreZeroHypercover.1), Q (Scheme.Cover.pullbackHom 𝒰 f i)
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
inst✝ : Small.{u, w} J
s : Cocone F
j : J
| failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
enter [2]; tactic => exact Multicoequalizer.π_desc _ _ _ _ _

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝ : Q.IsLocal
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hs' : ∀ (r : ↥s), Q.diagonal (f ∣_ Y.basicOpen ↑r)
⊢ Q.diagonal f

Tactic:
refine (diagonal_iff (targetAffineLocally Q)).mpr ?_
    let 𝒰 := Y.openCoverOfIsOpenCover _
      ((isAffineOpen_top Y).iSup_basicOpen_eq_self_iff.mpr hs)
    have (i : _) : IsAffine (𝒰.X i) := (isAffineOpen_top Y).basicOpen i.1
    refine diagonal_of_openCover_diagonal (targetAffineLocally Q) f 𝒰 ?_
    intro i
    exact (Q.diagonal.arrow_mk_iso_iff
      (morphismRestrictEq _ (by simp [𝒰]) ≪≫ morphismRestrictOpensRange _ _)).mp (hs' i)

Goal state after: