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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := this.toFinset
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

Tactic:
by_cases h1 : f.coeff p.1 = 0

Goal state after:
case pos
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := this.toFinset
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
h1 : f.coeff p.1 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

case neg
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := this.toFinset
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
h1 : ¬f.coeff p.1 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := this.toFinset
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
p : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

Tactic:
by_cases h1 : f.coeff p.1 = 0 <;> simp_all

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

Goal state before:
pp: case h
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
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
t : m.base = colimit.desc (F ⋙ forget C) ((forget C).mapCocone s)
⊢ m.c ≫ whiskerRight (eqToHom ⋯) (colimitCocone F).pt.presheaf = (desc F s).c

Tactic:
· refine NatTrans.ext (funext fun U => limit_obj_ext fun j => ?_)
      simp [desc, descCApp,
        PresheafedSpace.congr_app (w (unop j)).symm U,
        NatTrans.congr (limit.π (pushforwardDiagramToColimit F).leftOp j)
        (congr_arg op (Functor.congr_obj (congr_arg Opens.map t) (unop U)))]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ appLE g U V e₁ ≫ appLE f V W e₂ = appLE (f ≫ g) U W ⋯

Tactic:
by
  dsimp [Hom.appLE]
  rw [Category.assoc, f.naturality_assoc, ← Functor.map_comp]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : Opens ↥X
x : ↥U
f s : ↑Γ(X, U)
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s)
n : ℕ
hf : s ^ n * f = 0
hu : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (s ^ n))
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0

Tactic:
rw [← hu.mul_right_eq_zero, ← map_mul, hf, map_zero]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsOpenImmersion g
⊢ opensRange (f ≫ g) = opensRange g

Tactic:
rw [opensRange_comp, opensRange_of_isIso, image_top_eq_opensRange]

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

Goal state before:
pp: S T : Type u_1
f : S ⟶ T
hf : IsIso f
x : T
⊢ ∃ Y g, Presieve.singleton f g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)

Tactic:
by
    use S, f, ⟨⟩
    exact surjective_of_epi f x

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

Goal state before:
pp: X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
⊢ E.Small

Tactic:
choose i y hy using ofArrows_mem_jointlySurjectivePrecoverage_iff.mp E.mem₀

Goal state after:
X : Type u
E : jointlySurjectivePrecoverage.ZeroHypercover X
i : X → E.I₀
y : (x : X) → (fun X ↦ X) (E.X (i x))
hy : ∀ (x : X), (ConcreteCategory.hom (E.f (i x))) (y x) = x
⊢ E.Small
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))

Tactic:
change HasLimit (cospan ((forget).map f) ((forget).map g))

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ HasLimit (cospan (forget.map f) (forget.map g))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (pullback.fst (Scheme.forgetToTop.map g) (Scheme.forgetToTop.map f))) ''
      ⇑(ConcreteCategory.hom (pullback.snd g.base f.base)) ⁻¹' Set.univ =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)

Tactic:
erw [TopCat.pullback_fst_image_snd_preimage]

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map g)) ⁻¹'
      ⇑(ConcreteCategory.hom (Scheme.forgetToTop.map f)) '' Set.univ =
    ↑(g ⁻¹ᵁ Scheme.Hom.opensRange f)
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X Y Z : Scheme
𝒰✝ : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
𝒰 : Cover (precoverage P) X
⊢ { I₀ := ↥X, X := fun x ↦ 𝒰.X (𝒰.idx x), f := fun x ↦ 𝒰.f (𝒰.idx x) }.presieve₀ ∈ (precoverage P).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, fun i ↦ 𝒰.map_prop _⟩
    use x, (𝒰.exists_eq x).choose_spec.choose, (𝒰.exists_eq x).choose_spec.choose_spec

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
H :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
⊢ IsIso
    ((preservesColimitIso forgetToPresheafedSpace F).inv.c.app (op (H.functor.obj U)) ≫
      (colimit.ι (F ⋙ forgetToPresheafedSpace) i).c.app
        (op ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (unop (op (H.functor.obj U))))))

Tactic:
← PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝¹ : HasColimit F
i : Discrete ι
inst✝ : HasStrictTerminalObjects C
U : Opens ↑↑(F.obj i).toPresheafedSpace
h₁ :
  colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv =
    forgetToPresheafedSpace.map (colimit.ι F i)
h₂ :
  colimit.ι F i =
    { hom := colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv }
H :
  IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫ (preservesColimitIso forgetToPresheafedSpace F).inv).base)
⊢ IsIso
    ((preservesColimitIso forgetToPresheafedSpace F).inv.c.app (op (H.functor.obj U)) ≫
      (PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit (F ⋙ forgetToPresheafedSpace)
            ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj
              (unop (op (H.functor.obj U))))).hom ≫
        limit.π
          (PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
            ((Opens.map (preservesColimitIso forgetToPresheafedSpace F).inv.base).obj (unop (op (H.functor.obj U)))))
          (op i))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ Nonempty ↥↑U ↔ (↑U).Nonempty

Tactic:
simp only [toScheme_carrier, SetLike.coe_sort_coe, nonempty_subtype]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
⊢ { I₀ := s, X := fun i ↦ ↑(U i), f := fun i ↦ (U i).ι }.presieve₀ ∈ (precoverage IsOpenImmersion).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]
    refine ⟨fun x ↦ ?_, inferInstance⟩
    have hx : x ∈ ⨆ i, U i := hU.symm ▸ show x ∈ (⊤ : X.Opens) by trivial
    rw [Opens.mem_iSup] at hx
    obtain ⟨i, hi⟩ := hx
    use i
    simpa

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: case mp
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 =
      (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (F.obj.map (homOfLE e).op))
          ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) ∧
    (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 =
      (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x))

Tactic:
← TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst,

Goal state after:
case mp
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
          ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) =
      (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (F.obj.map (homOfLE e).op))
          ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) ∧
    (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 =
      (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
x : ↥↑(⨆ i, U i)
⊢ ∃ i, x ∈ Set.range ⇑({ I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.f i)

Tactic:
obtain ⟨i, hi⟩ := TopologicalSpace.Opens.mem_iSup.mp x.2

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ : Scheme
U✝ : X✝.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
x : ↥↑(⨆ i, U i)
i : J
hi : ↑x ∈ U i
⊢ ∃ i, x ∈ Set.range ⇑({ I₀ := J, X := fun i ↦ ↑(U i), f := fun j ↦ X.homOfLE ⋯ }.f i)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ (X.isoOfEq ⋯).hom ≫ U.ι = (Iso.refl ↑U).hom ≫ U.ι

Tactic:
Scheme.isoOfEq_hom_ι,

Goal state after:
X : Scheme
U : X.Opens
⊢ U.ι = (Iso.refl ↑U).hom ≫ U.ι
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
this :
  Function.Bijective
    ⇑((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
          (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
        ((ConcreteCategory.hom (toStalk R x)) f))
a : ↑((structurePresheafInModuleCat R M).stalk x)
⊢ ((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) f) a =
    ((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
          (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
        ((ConcreteCategory.hom (toStalk R x)) f))
      a

Tactic:
simp only [Module.algebraMap_end_apply]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
this :
  Function.Bijective
    ⇑((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
          (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
        ((ConcreteCategory.hom (toStalk R x)) f))
a : ↑((structurePresheafInModuleCat R M).stalk x)
⊢ f • a = (ConcreteCategory.hom (toStalk R x)) f • a
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ hU.fromSpec ⁻¹ᵁ X.basicOpen f = (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, U)).inv) f)

Tactic:
rw [Scheme.preimage_basicOpen, hU.fromSpec_app_self]
  exact Scheme.basicOpen_res_eq _ _ (eqToHom hU.fromSpec_preimage_self).op

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = pullback.fst (D.f i i) (D.f i j) ≫ D.t i i
eq₂ : pullback.fst (D.f i i) (D.f i j) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)
⊢ D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom

Tactic:
rw [D.t_id, Category.comp_id, eq₂] at eq₁

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
eq₁ : D.t' i i j ≫ pullback.snd (D.f i j) (D.f i i) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)
eq₂ : pullback.fst (D.f i i) (D.f i j) = (pullback.snd (D.f i i) (D.f i j) ≫ D.f i j) ≫ inv (D.f i i)
⊢ D.t' i i j = (pullbackSymmetry (D.f i i) (D.f i j)).hom
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
i j : D.J
⊢ Mono (D.f' i j)

Tactic:
dsimp [GlueData'.f']

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j : D.J
⊢ Mono (if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i j h)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      ((PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c.app
          (op U) ≫
        (coequalizer.π f.toHom g.toHom).c.app
          (op
            ((Opens.map
                  (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                        (Hom.toShHom g)).hom.base).obj
              (unop (op U))))))

Tactic:
← PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      ((PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c.app
          (op U) ≫
        (PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit (parallelPair f.toHom g.toHom)
              ((Opens.map
                    (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                          (Hom.toShHom g)).hom.base).obj
                (unop (op U)))).hom ≫
          limit.π
            (PresheafedSpace.componentwiseDiagram (parallelPair f.toHom g.toHom)
              ((Opens.map
                    (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                          (Hom.toShHom g)).hom.base).obj
                (unop (op U))))
            (op WalkingParallelPair.one)))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: case inst.inst
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this✝ :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
this : IsIso (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c
⊢ IsLocalHom
    (PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit (parallelPair f.toHom g.toHom)
          ((Opens.map
                (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f)
                      (Hom.toShHom g)).hom.base).obj
            (unop (op U)))).hom.hom'

Tactic:
· apply isLocalHom_of_isIso

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

Goal state before:
pp: case inst
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
this✝ :
  coequalizer.π f.toHom g.toHom ≫
      (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom =
    (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom
this : IsIso (PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c
⊢ IsLocalHom
    ((PreservesCoequalizer.iso SheafedSpace.forgetToPresheafedSpace (Hom.toShHom f) (Hom.toShHom g)).hom.c.app
        (op U)).hom'

Tactic:
· apply isLocalHom_of_isIso

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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑Y.toTopCat
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom x))

Tactic:
constructor
  rintro a ha
  rcases TopCat.Presheaf.exists_germ_eq _ a with ⟨U, hU, s, rfl⟩
  rw [PresheafedSpace.stalkMap_germ_apply (coequalizer.π f.toShHom g.toShHom).hom U _ hU] at ha
  let V := imageBasicOpen f g U s
  have hV : (coequalizer.π f.toShHom g.toShHom).hom.base ⁻¹'
      ((coequalizer.π f.toShHom g.toShHom).hom.base '' V.1) = V.1 :=
    imageBasicOpen_image_preimage f g U s
  have hV' : V = ⟨(coequalizer.π f.toShHom g.toShHom).hom.base ⁻¹'
      ((coequalizer.π f.toShHom g.toShHom).hom.base '' V.1), hV.symm ▸ V.2⟩ :=
    SetLike.ext' hV.symm
  have V_open : IsOpen ((coequalizer.π f.toShHom g.toShHom).hom.base '' V.1) :=
    imageBasicOpen_image_open f g U s
  have VleU : ⟨(coequalizer.π f.toShHom g.toShHom).hom.base '' V.1, V_open⟩ ≤ U :=
    Set.image_subset_iff.mpr (Y.toRingedSpace.basicOpen_le _)
  have hxV : x ∈ V := ⟨hU, ha⟩
  rw [← (coequalizer f.toShHom g.toShHom).presheaf.germ_res_apply (homOfLE VleU) _
      (@Set.mem_image_of_mem _ _ (coequalizer.π f.toShHom g.toShHom).hom.base x V.1 hxV) s]
  apply RingHom.isUnit_map
  rw [← isUnit_map_iff ((coequalizer.π f.toShHom g.toShHom).hom.c.app _).hom,
    ← CommRingCat.comp_apply, NatTrans.naturality, CommRingCat.comp_apply,
    ← isUnit_map_iff (Y.presheaf.map (eqToHom hV').op).hom]
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11224): change `rw` to `erw`
  erw [← CommRingCat.comp_apply, ← CommRingCat.comp_apply, ← Y.presheaf.map_comp]
  convert!
    @RingedSpace.isUnit_res_basicOpen Y.toRingedSpace (unop _)
      (((coequalizer.π f.toShHom g.toShHom).hom.c.app (op U)) s)

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 : C
Y : Over X
m : Y ⟶ mk (𝟙 X)
⊢ Hom.left m = Hom.left (homMk Y.hom ⋯)

Tactic:
by simpa using m.w

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 Y : C
f : X ⟶ Y
A B : Over Y
⊢ Hom.left (prodComparisonIso (pullback f) A B).inv ≫
      pullback.fst (pullback.fst A.hom B.hom ≫ A.hom) f ≫ pullback.fst A.hom B.hom =
    pullback.fst (pullback.snd A.hom f) (pullback.snd B.hom f) ≫ pullback.fst A.hom f

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

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
hf : P f
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
by
  use {1}
  let e : S ≃+* Localization.Away (1 : S) :=
    (IsLocalization.atUnits S (Submonoid.powers 1) (by simp)).toRingEquiv
  simp only [Set.mem_singleton_iff, forall_eq, Ideal.span_singleton_one, exists_const]
  exact hP.left f e hf

Goal state after: