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

Goal state before:
pp: case inv
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x : PreEnvelGroup R
ih_x :
  ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x⟧ =
    F ⟦x⟧
⊢ ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x.inv⟧ =
    F ⟦x.inv⟧

Tactic:
have hm : ⟦x.inv⟧ = @Inv.inv (EnvelGroup R) _ ⟦x⟧ := rfl

Goal state after:
case inv
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x : PreEnvelGroup R
ih_x :
  ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x⟧ =
    F ⟦x⟧
hm : ⟦x.inv⟧ = (⟦x⟧)⁻¹
⊢ ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x.inv⟧ =
    F ⟦x.inv⟧
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ q.lift (x * y) = q.lift x * q.lift y

Tactic:
by
  simp only [lift, Algebra.algebraMap_eq_smul_one]
  simp_rw [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one, smul_smul]
  simp only [i_mul_i, j_mul_j, i_mul_j, j_mul_i, i_mul_k, k_mul_i, k_mul_j, j_mul_k, k_mul_k]
  simp only [smul_smul, smul_neg, sub_eq_add_neg, ← add_assoc, neg_smul]
  simp only [mul_right_comm _ _ (c₁ * c₃), mul_comm _ (c₁ * c₃)]
  simp only [mul_comm _ c₁]
  simp only [mul_right_comm _ _ c₃]
  simp only [← mul_assoc]
  simp only [re_mul, sub_eq_add_neg, add_smul, neg_smul, imI_mul, ← add_assoc, imJ_mul, imK_mul]
  linear_combination (norm := module)

Goal state after:
Module: Mathlib.Algebra.SkewMonoidAlgebra.Lift

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
f : SkewMonoidAlgebra k G
| F f

Tactic:
rw [lift_unique' F]
    simp [lift_apply]

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : SkewMonoidAlgebra k G →ₐ[k] A
f : SkewMonoidAlgebra k G
| f.sum fun a b ↦ b • F (single a 1)
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → f x = f y
x : R
⊢ (lift ⟨f, w⟩) ((mkRingHom r) x) = f x

Tactic:
by
  simp_rw [lift_def, preLift_def, mkRingHom_def]
  rfl

Goal state after:
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
n : ℕ
inst✝ : Semiring R
a : R
h : n ≠ 0
⊢ (C a).coeff n = 0

Tactic:
rw [coeff_C, if_neg h]

Goal state after:
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ x + y = x ↔ x ≤ y

Tactic:
trop_add_def,

Goal state after:
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ trop (min (untrop x) (untrop y)) = x ↔ x ≤ y
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ x + y = y ↔ y ≤ x

Tactic:
trop_add_def,

Goal state after:
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ trop (min (untrop x) (untrop y)) = y ↔ y ≤ x
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
⊢ x + y = z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x

Tactic:
trop_add_def,

Goal state after:
R : Type u
inst✝ : LinearOrder R
x y z : Tropical R
⊢ trop (min (untrop x) (untrop y)) = z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case cons
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : OrderTop R
s : Tropical R
x : Multiset (Tropical R)
IH : untrop x.sum = (map untrop x).inf
⊢ untrop (s ::ₘ x).sum = (map untrop (s ::ₘ x)).inf

Tactic:
simp only [sum_cons, untrop_add, map_cons, inf_cons, ← IH]

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

Goal state before:
pp: C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
D : Type u₃
inst✝⁷ : Category.{v₃, u₃} D
G : C ⥤ D
A : Type u₁
inst✝⁶ : Category.{v₁, u₁} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁵ : G.IsContinuous J K
inst✝⁴ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasLeftKanExtension F
inst✝³ : RepresentablyFlat G
inst✝² : HasSheafify K A
inst✝¹ : HasSheafify J A
inst✝ : PreservesFiniteLimits G.op.lan
this : PreservesFiniteLimits (G.op.lan ⋙ presheafToSheaf K A)
⊢ PreservesFiniteLimits (sheafPullback G A J K)

Tactic:
apply comp_preservesFiniteLimits

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

Goal state before:
pp: case app
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
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
X : Jᵒᵖ
x : ↑((F ⋙ forget C).obj (unop X))
⊢ (ConcreteCategory.hom
        (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base)
      ((ConcreteCategory.hom (colimit.ι (F ⋙ forget C) (unop X))) x) =
    (ConcreteCategory.hom (colimit.ι F (unop X)).base) x

Tactic:
simp only [colimitCocone, colimit, ← TopCat.comp_app]

Goal state after:
case app
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
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
X : Jᵒᵖ
x : ↑((F ⋙ forget C).obj (unop X))
⊢ (ConcreteCategory.hom
        (colimit.ι (F ⋙ forget C) (unop X) ≫
          (colimit.isoColimitCocone
                  {
                    cocone :=
                      {
                        pt :=
                          { carrier := Limits.colimit (F ⋙ forget C),
                            presheaf := limit (pushforwardDiagramToColimit F).leftOp },
                        ι :=
                          {
                            app := fun j ↦
                              { base := colimit.ι (F ⋙ forget C) j,
                                c := limit.π (pushforwardDiagramToColimit F).leftOp (op j) },
                            naturality := ⋯ } },
                    isColimit := colimitCoconeIsColimit F }).symm.hom.base))
      x =
    (ConcreteCategory.hom (colimit.ι F (unop X)).base) x
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i ↦ ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).obj U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))),
    (fun s ↦ IsGluing (X.sheafToTypes T).obj U sf' s) y → y = gl
⊢ P.pred gl

Tactic:
apply P.locality
      rintro ⟨x, mem⟩
      -- Once we're at a particular point `x`, we can select some open set `x ∈ U i`.
      choose i hi using Opens.mem_iSup.mp mem
      -- We claim that the predicate holds in `U i`
      use U i, hi, Opens.leSupr U i
      -- This follows, since our original family `sf` satisfies the predicate
      convert! (sf i).property using 1
      exact gl_spec i

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

Goal state before:
pp: case a
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
U : (Opens ↑↑X)ᵒᵖ
⊢ {
      carrier :=
        ⇑(ConcreteCategory.hom (pullback.snd f.base g.base)) ''
          ↑((↑(TopCat.Hom.frameHom (pullback.fst f.base g.base))).toFunctor.obj (unop U)),
      is_open' := ⋯ } ≤
    (↑(TopCat.Hom.frameHom g.base)).toFunctor.obj
      { carrier := ⇑(ConcreteCategory.hom f.base) '' ↑(unop U), is_open' := ⋯ }

Tactic:
· rintro _ ⟨x, h₁, rfl⟩
                    exact ⟨_, h₁, CategoryTheory.congr_fun pullback.condition x⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
H : X.toLocallyRingedSpace = Y.toLocallyRingedSpace
⊢ X = Y

Tactic:
cases X

Goal state after:
case mk
Y : Scheme
toLocallyRingedSpace✝ : LocallyRingedSpace
local_affine✝ :
  ∀ (x : ↑toLocallyRingedSpace✝.toTopCat),
    ∃ U R, Nonempty (toLocallyRingedSpace✝.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
H :
  { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ }.toLocallyRingedSpace =
    Y.toLocallyRingedSpace
⊢ { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ } = Y
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : SheafedSpace C
f : X ⟶ Y
inst✝ : SheafedSpace.IsOpenImmersion f
⊢ toSheafedSpace Y f.hom = X

Tactic:
cases X

Goal state after:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
Y : SheafedSpace C
toPresheafedSpace✝ : PresheafedSpace C
IsSheaf✝ : toPresheafedSpace✝.presheaf.IsSheaf
f : { toPresheafedSpace := toPresheafedSpace✝, IsSheaf := IsSheaf✝ } ⟶ Y
inst✝ : SheafedSpace.IsOpenImmersion f
⊢ toSheafedSpace Y f.hom = { toPresheafedSpace := toPresheafedSpace✝, IsSheaf := IsSheaf✝ }
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
x✝ : ↥(unop (op (basicOpen (g' * g))))
y : ↑(PrimeSpectrum.Top R)
hy✝ : y ∈ unop (op (basicOpen (g' * g)))
hy : y ∈ unop (op (basicOpen g' ⊓ basicOpen g))
hgy : g ∉ (↑⟨y, ⋯⟩).asIdeal
H : (fun x ↦ ↑s (iVU x)) ⟨y, ⋯⟩ = LocalizedModule.mk f ⟨g, hgy⟩
⊢ (g * g') • f = (g' * g) • f

Tactic:
ring_nf

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
a : ↥(unop (op (basicOpen (g i * g j))))
⊢ (g j * g i) • f j = (g i * g j) • f j

Tactic:
ring_nf

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) (X.homOfLE hU) (X.homOfLE hV)

Tactic:
by
  refine (isPullback_morphismRestrict (X.homOfLE hV) (W.ι ⁻¹ᵁ U)).of_iso (V.ι.isoImage _ ≪≫
    X.isoOfEq ?_) (W.ι.isoImage _ ≪≫ X.isoOfEq ?_) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_ ?_
  · rw [← TopologicalSpace.Opens.map_comp_obj, ← Scheme.Hom.comp_base, Scheme.homOfLE_ι]
    exact V.functor_map_eq_inf U
  · exact (W.functor_map_eq_inf U).trans (by simpa)
  all_goals { simp [← cancel_mono (Scheme.Opens.ι _)] }

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 U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ (Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f ↑x) ≫ stalkMap V.ι x =
    (Y.presheaf.stalkCongr ⋯).hom ≫ stalkMap (V.ι ≫ f) x

Tactic:
stalkMap_comp

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ (Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f ↑x) ≫ stalkMap V.ι x =
    (Y.presheaf.stalkCongr ⋯).hom ≫ stalkMap f (V.ι x) ≫ stalkMap V.ι x
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case mp
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
loc_inst : IsLocalization.Away r ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))
⊢ ConcreteCategory.hom
        (CommRingCat.ofHom
            (algebraMap (↑(Γ.obj (op X)))
              ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))) ≫
          f) =
      (IsLocalization.Away.lift r ⋯).comp
        (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))) →
    f = X.toΓSpecCApp r

Tactic:
intro h
    ext : 1
    exact IsLocalization.ringHom_ext (Submonoid.powers r) h

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (X.toToΓSpecMapBasicOpen 1 ≫
        ((pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base).obj X.presheaf).germ (basicOpen 1)
          ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ⋯) ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x =
    X.presheaf.germ ⊤ x True.intro

Tactic:
← dsimp% stalkPushforward_germ _ _ X.presheaf ⊤

Goal state after:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (X.toToΓSpecMapBasicOpen 1 ≫
        ((pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base).obj X.presheaf).germ (basicOpen 1)
          ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ⋯) ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x =
    ((pushforward CommRingCat ?m.124).obj X.presheaf).germ ⊤ ((ConcreteCategory.hom ?m.124) x) True.intro ≫
      stalkPushforward CommRingCat ?m.124 X.presheaf x

X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ TopCat

X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ ↑X.toPresheafedSpace ⟶ ?m.123
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R S : CommRingCat
φ ψ : R ⟶ S
⊢ map φ = map ψ ↔ φ = ψ

Tactic:
rw [iff_comm, ← Quiver.Hom.op_inj.eq_iff, ← Scheme.Spec.map_injective.eq_iff]

Goal state after:
R S : CommRingCat
φ ψ : R ⟶ S
⊢ Scheme.Spec.map φ.op = Scheme.Spec.map ψ.op ↔ map φ = map ψ
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
e : cospan (F.map (D.ι i)) (F.map (D.ι j)) ≅ cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun x ↦
      Option.casesOn (motive := fun t ↦
        x = t →
          ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x))
        x (fun h ↦ ⋯ ▸ D.gluedIso F)
        (fun val h ↦ ⋯ ▸ Iso.refl ((cospan (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
    ⋯
⊢ IsLimit (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)

Tactic:
apply IsLimit.postcomposeHomEquiv e _ _

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v, u₁} C
C' : Type u₂
inst✝⁴ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝³ : HasMulticoequalizer D.diagram
inst✝² : PreservesColimit D.diagram.multispan F
inst✝¹ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst✝ : ReflectsLimit (cospan (D.ι i) (D.ι j)) F
hc : IsLimit ((D.mapGlueData F).vPullbackCone i j)
e : cospan (F.map (D.ι i)) (F.map (D.ι j)) ≅ cospan ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) := ⋯
⊢ IsLimit ((Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: ι : Type v
inst✝ : Small.{u, v} ι
F : Discrete ι ⥤ LocallyRingedSpace
i : Discrete ι
y : ↑↑((F ⋙ forgetToSheafedSpace).obj i).toPresheafedSpace
this : IsLocalRing ↑(((F ⋙ forgetToSheafedSpace).obj i).presheaf.stalk y)
⊢ IsLocalRing
    ↑((colimit (F ⋙ forgetToSheafedSpace)).presheaf.stalk
        ((ConcreteCategory.hom (colimit.ι (F ⋙ forgetToSheafedSpace) i).hom.base) y))

Tactic:
exact
      (asIso ((colimit.ι (C := SheafedSpace.{u + 1, u, u} CommRingCat.{u})
        (F ⋙ forgetToSheafedSpace) i :).hom.stalkMap y)).symm.commRingCatIsoToRingEquiv.isLocalRing

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y =
    𝟙 (pullback (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)))

Tactic:
by
  apply pullback.hom_ext <;> simp_rw [Category.id_comp, Category.assoc]
  · apply glued_cover_cocycle_fst
  · apply glued_cover_cocycle_snd

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
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
⊢ ∃ l fi fj fk α z,
    IsOpenImmersion α ∧
      α ≫ pullback.fst (V F i j).ι (V F i k).ι = (Hom.isoOpensRange (F.map fi)).hom ≫ (F.obj i).homOfLE ⋯ ∧
        α ≫ pullback.snd (V F i j).ι (V F i k).ι = (Hom.isoOpensRange (F.map fi)).hom ≫ (F.obj i).homOfLE ⋯ ∧ α z = x

Tactic:
obtain ⟨k₁, y₁, hy₁⟩ := mem_iSup.mp ((pullback.fst (C := Scheme) _ _) x).2

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
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
y₁ : ↥(F.obj k₁.fst)
hy₁ : (F.map k₁.snd.1) y₁ = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
⊢ ∃ l fi fj fk α z,
    IsOpenImmersion α ∧
      α ≫ pullback.fst (V F i j).ι (V F i k).ι = (Hom.isoOpensRange (F.map fi)).hom ≫ (F.obj i).homOfLE ⋯ ∧
        α ≫ pullback.snd (V F i j).ι (V F i k).ι = (Hom.isoOpensRange (F.map fi)).hom ≫ (F.obj i).homOfLE ⋯ ∧ α z = x
Module: Mathlib.AlgebraicGeometry.Limits

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

Tactic:
suffices Topology.IsOpenEmbedding (Sigma.desc α ∘ sigmaMk f) by
      convert! this.comp (sigmaMk f).symm.isOpenEmbedding; ext; simp

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

Goal state before:
pp: case right.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))
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
⊢ Scheme.Hom.stalkMap (Sigma.desc α)
        (((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
            (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
          y) ≫
      Scheme.Hom.stalkMap
        ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y =
    (X.presheaf.stalkCongr ⋯).hom ≫
      Scheme.Hom.stalkMap (α (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x).as) y

Tactic:
· simp [← Scheme.Hom.stalkMap_comp, Scheme.Hom.stalkMap_congr_hom _ _ (colimit.ι_desc _ _)]

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 : 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₂))
⊢ ∃ U_1,
    x ∈ U_1 ∧
      U_1.ι ≫
          pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
            (Hom.isoOpensRange (F.map k₁.snd.1)).inv ≫ F.map k₁.snd.2 =
        U_1.ι ≫
          pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
            (Hom.isoOpensRange (F.map k₂.snd.1)).inv ≫ F.map k₂.snd.2

Tactic:
obtain ⟨l, hli, hlj, y, hy₁, hy₂⟩ := (F ⋙ forget).exists_map_eq_of_isLocallyDirected k₁.2.1 k₂.2.1
    ((pullback.fst _ _ ≫ (F.map k₁.2.1).isoOpensRange.inv) x)
    ((pullback.snd _ _ ≫ (F.map k₂.2.1).isoOpensRange.inv) x) (by
      simp only [Functor.comp_obj, forget_obj, Functor.comp_map, forget_map,
        ConcreteCategory.hom_ofHom, Hom.comp_base, TopCat.hom_comp, ContinuousMap.comp_apply,
        TypeCat.Fun.coe_mk]
      simp only [← Hom.comp_apply]
      congr 5
      simpa using congr($(pullback.condition (f := (F.obj i).homOfLE h₁)
        (g := (F.obj i).homOfLE h₂)) ≫ 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
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
⊢ ∃ U_1,
    x ∈ U_1 ∧
      U_1.ι ≫
          pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
            (Hom.isoOpensRange (F.map k₁.snd.1)).inv ≫ F.map k₁.snd.2 =
        U_1.ι ≫
          pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
            (Hom.isoOpensRange (F.map k₂.snd.1)).inv ≫ F.map k₂.snd.2
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
x : ↥Y
⊢ (coprodMk X Y) (Sum.inr x) = coprod.inr x

Tactic:
by
  change ((TopCat.binaryCofan X Y).inr ≫
    (colimit.isoColimitCocone ⟨_, TopCat.binaryCofanIsColimit _ _⟩).inv ≫ _) x =
      Scheme.forgetToTop.map coprod.inr x
  congr 2
  refine (colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.binaryCofanIsColimit _ _⟩ _ _).trans ?_
  exact coprodComparison_inr Scheme.forgetToTop

Goal state after: