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

Goal state before:
pp: R✝ : Type u
inst✝³ : Semiring R✝
r✝ : R✝ → R✝ → Prop
inst✝² : StarRing R✝
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (star a) (star b)
⊢ ∀ (r_1 s : RingQuot r), star' r hr (r_1 * s) = star' r hr s * star' r hr r_1

Tactic:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp [star'_quot, mul_quot, star_mul]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : AddCommMonoid S
f g : SkewMonoidAlgebra k G
h : G → k → S
hf : ∀ (i : G), h i 0 = 0
h_add : ∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ { coeff := f.coeff + g.coeff }.sum h = f.sum h + g.sum h

Tactic:
exact Finsupp.sum_add_index' hf h_add

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Mul G
inst✝¹ : NonUnitalNonAssocSemiring k
inst✝ : DistribSMul G k
f g h : SkewMonoidAlgebra k G
⊢ ((f + g).sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) =
    (f.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) +
      g.sum fun a₁ b₁ ↦ h.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)

Tactic:
refine Eq.trans (sum_add_index ?_ ?_) ?_ <;>
      simp only [add_mul, zero_mul, single_zero, single_add, forall_true_iff, sum_zero, sum_add]

Goal state after:
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ sym 1 = 1

Tactic:
sym_one

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : AddMonoidWithOne α
inst✝¹ : Invertible 2
a : α
inst✝ : Invertible a
⊢ 1 = 1
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ min (untrop x) (untrop y) = untrop x ↔ untrop x ≤ untrop y

Tactic:
min_eq_left_iff

Goal state after:
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ untrop x ≤ untrop y ↔ untrop x ≤ untrop y
Module: Mathlib.Algebra.Tropical.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
⊢ ∀ (s : Set (Tropical R)), ¬BddBelow s → sInf s = sInf ∅

Tactic:
by
      intro s hs
      have : Set.range untrop = (Set.univ : Set R) := Equiv.range_eq_univ tropEquiv.symm
      simp only [sInf, Set.image_empty, trop_inj_iff]
      apply csInf_of_not_bddBelow
      contrapose hs
      change BddBelow (tropOrderIso.symm '' s) at hs
      exact tropOrderIso.symm.bddBelow_image.1 hs

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ (𝟙 X).c.app U = X.presheaf.map (𝟙 U)

Tactic:
rw [id_c, map_id]
  rfl

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

Goal state before:
pp: case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : x ∈ V
hf : IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ U y ⋯)) f)

Tactic:
convert! RingHom.isUnit_map (X.presheaf.germ _ y hy).hom hf

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ U
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hxU)) f)
V : Opens ↑↑X.toPresheafedSpace
i : V ⟶ U
hxV : x ∈ V
hf : IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)
y : ↑↑X.toPresheafedSpace
hy : y ∈ V.carrier
⊢ (ConcreteCategory.hom (X.presheaf.germ U y ⋯)) f =
    (CommRingCat.Hom.hom (X.presheaf.germ V y hy)) ((ConcreteCategory.hom (X.presheaf.map i.op)) f)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
⊢ IsIso (Y.presheaf.map (⋯.adjunction.counit.app (hf.functor.obj U)).op)

Tactic:
convert_to IsIso (Y.presheaf.map (𝟙 _))

Goal state after:
case e'_4
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
⊢ Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))

case e'_5
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4✝ :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
⊢ Y.presheaf.map (⋯.adjunction.counit.app (hf.functor.obj U)).op ≍ Y.presheaf.map (𝟙 (op (hf.functor.obj U)))

case convert_2
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
⊢ IsIso (Y.presheaf.map (𝟙 (op (hf.functor.obj U))))
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
⊢ IsOpenImmersion (limit.π (cospan f g) one)

Tactic:
by
  rw [← limit.w (cospan f g) WalkingCospan.Hom.inl]
  change IsOpenImmersion (_ ≫ f)
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ Scheme.Hom.app f U ≫ (ΓIso f U).hom = Y.presheaf.map (homOfLE ⋯).op

Tactic:
by
  rw [← map_ΓIso_inv]
  simp [-ΓIso_inv]

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

Goal state before:
pp: case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝ : ι
this✝ :
  colimit.ι (F ⋙ forget C) { as := as✝ } =
    (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := { as := as✝ }.as } =
    TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (((Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
              colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫
          (preservesColimitIso (forget C) F).inv))

Tactic:
rw [this, ← Category.assoc]

Goal state after:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
as✝ : ι
this✝ :
  colimit.ι (F ⋙ forget C) { as := as✝ } =
    (Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as✝ }) ≫
      (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv
this :
  colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := { as := as✝ }.as } =
    TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        ((((Discrete.natIsoFunctor.hom.app { as := as✝ } ≫
                TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as✝ }.as) ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv) ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).inv) ≫
          (preservesColimitIso (forget C) F).inv))
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case e'_2.e'_7
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀
e_1✝ :
  (pullback (pullback.fst (𝒰.f i.fst) f) ((𝒰.X i.fst).affineCover.f i.snd) ⟶ 𝒰.affineRefinement.openCover.X i) =
    (pullback (pullback.fst (𝒰.f i.fst) f) ((𝒰.X i.fst).affineCover.f i.snd) ⟶ (𝒰.X i.fst).affineCover.X i.snd)
e_5✝ : 𝒰.affineRefinement.openCover.X i = (𝒰.X i.fst).affineCover.X i.snd
⊢ (pullbackRightPullbackFstIso (𝒰.f i.fst) f ((𝒰.X i.fst).affineCover.f i.snd)).hom ≫
      pullback.fst (𝒰.affineRefinement.openCover.f i) f =
    pullback.fst ((𝒰.X i.fst).affineCover.f i.snd) (pullback.fst (𝒰.f i.fst) f)

Tactic:
exact pullbackRightPullbackFstIso_hom_fst _ _ _

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

Goal state before:
pp: case mpr.refine_3
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))))))
y : ↑(F.obj.obj (op W))
e₁ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
⊢ (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)) y

Tactic:
rw [← e₂, ← TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd]

Goal state after:
case mpr.refine_3
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))))))
y : ↑(F.obj.obj (op W))
e₁ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
⊢ (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))
      ((ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_3
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ∣_ W.ι ⁻¹ᵁ U ≫ (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom =
    (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

Tactic:
{

Goal state after:
case refine_3
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ∣_ W.ι ⁻¹ᵁ U ≫ (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom =
    (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_4
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U).ι ≫ (Iso.refl ↑V).hom =
    (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯

Tactic:
{

Goal state after:
case refine_4
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U).ι ≫ (Iso.refl ↑V).hom =
    (Scheme.Hom.isoImage V.ι (X.homOfLE hV ⁻¹ᵁ W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE ⋯
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_5
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (W.ι ⁻¹ᵁ U).ι ≫ (Iso.refl ↑W).hom = (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE hU

Tactic:
{

Goal state after:
case refine_5
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ (W.ι ⁻¹ᵁ U).ι ≫ (Iso.refl ↑W).hom = (Scheme.Hom.isoImage W.ι (W.ι ⁻¹ᵁ U) ≪≫ X.isoOfEq ⋯).hom ≫ X.homOfLE hU
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_6
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ≫ (Iso.refl ↑W).hom = (Iso.refl ↑V).hom ≫ X.homOfLE hV

Tactic:
{

Goal state after:
case refine_6
X : Scheme
U V W : X.Opens
hU : U ≤ W
hV : V ≤ W
⊢ X.homOfLE hV ≫ (Iso.refl ↑W).hom = (Iso.refl ↑V).hom ≫ X.homOfLE hV
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
⊢ Arrow.mk (f ∣_ Scheme.Hom.opensRange g) ≅ Arrow.mk (pullback.snd f g)

Tactic:
let e :=
    IsOpenImmersion.isoOfRangeEq g V.ι Subtype.range_coe.symm

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.ι ⋯
⊢ Arrow.mk (f ∣_ Scheme.Hom.opensRange g) ≅ Arrow.mk (pullback.snd f g)
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
⊢ (U.stalkIso ((resLE f U V e) x) ≪≫ Y.presheaf.stalkCongr ⋯).hom ≫ (Arrow.mk (stalkMap f ↑x)).hom =
    (Arrow.mk (stalkMap (resLE f U V e) x)).hom ≫ (V.stalkIso x).hom

Tactic:
dsimp
    rw [Category.assoc, ← Iso.eq_inv_comp, ← Category.assoc, ← Iso.comp_inv_eq,
      Opens.stalkIso_inv, Opens.stalkIso_inv, ← stalkMap_comp,
      stalkMap_congr_hom _ _ (resLE_comp_ι f e), stalkMap_comp]
    simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
⊢ IsTopologicalBasis (Set.range fun i ↦ ↑↑i)

Tactic:
← Set.image_eq_range

Goal state after:
X : Scheme
⊢ IsTopologicalBasis (SetLike.coe '' X.affineOpens)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ CommRingCat.ofHom
        (algebraMap (↑(unop (op (CommRingCat.of R))))
          ((structureSheafInType ↑(unop (op (CommRingCat.of R))) ↑(unop (op (CommRingCat.of R)))).obj.obj (op ⊤))) ≫
      (structureSheaf ↑(unop (op (CommRingCat.of R)))).obj.map (homOfLE ⋯).op ≫
        ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).c.app U =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
NatTrans.naturality _ (homOfLE (le_top (a := U.unop))).op,

Goal state after:
X : LocallyRingedSpace
R : Type u
inst✝ : CommRing R
f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)
U : (Opens ↑↑(Spec.toLocallyRingedSpace.obj (op (CommRingCat.of R))).toPresheafedSpace)ᵒᵖ
⊢ CommRingCat.ofHom
        (algebraMap (↑(unop (op (CommRingCat.of R))))
          ((structureSheafInType ↑(unop (op (CommRingCat.of R))) ↑(unop (op (CommRingCat.of R)))).obj.obj (op ⊤))) ≫
      ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).c.app (op ⊤) ≫
        ((pushforward CommRingCat ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).base).obj
              X.presheaf).map
          (homOfLE ⋯).op =
    f.unop ≫ X.presheaf.map (homOfLE ⋯).op
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)
VleU :
  { carrier := ⇑(ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) '' V.carrier,
      is_open' := V_open } ≤
    U
hxV : x ∈ V
⊢ IsUnit
    ((ConcreteCategory.hom
        ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U) ≫
          Y.presheaf.map
            ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).op.map (homOfLE VleU).op ≫
              (eqToHom hV').op)))
      s)

Tactic:
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 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:
by
  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.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ IsOpenMap ⇑(fromGlued 𝒰)

Tactic:
by
  intro U hU
  rw [isOpen_iff_forall_mem_open]
  intro x hx
  rw [𝒰.gluedCover.isOpen_iff] at hU
  use 𝒰.fromGlued '' U ∩ Set.range (𝒰.f (𝒰.idx x))
  use Set.inter_subset_left
  constructor
  · rw [← Set.image_preimage_eq_inter_range]
    apply (𝒰.f (𝒰.idx x)).isOpenEmbedding.isOpenMap
    convert! hU (𝒰.idx x) using 1
    simp only [← ι_fromGlued, gluedCover_U, Hom.comp_base, TopCat.hom_comp, ContinuousMap.coe_comp,
      Set.preimage_comp]
    congr! 1
    exact Set.preimage_image_eq _ 𝒰.fromGlued_injective
  · exact ⟨hx, 𝒰.covers x⟩

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
⊢ P (pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))

Tactic:
let e : pullback (pullback.fst f g) ((S.affineCover.pullback₁ f).f i) ≅
          _ := by
        refine pullbackSymmetry _ _ ≪≫ pullbackRightPullbackFstIso f g _ ≪≫ ?_ ≪≫
          (pullbackRightPullbackFstIso (S.affineCover.f i) g
            (pullback.snd f (S.affineCover.f i))).symm
        exact asIso
          (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simpa using! pullback.condition) (by simp))

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
e : pullback (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅
  pullback (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
    pullbackRightPullbackFstIso f g ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
      asIso
          (pullback.map ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g
            (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g
            (𝟙 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        (pullbackRightPullbackFstIso (S.affineCover.f i) g (pullback.snd f (S.affineCover.f i))).symm
⊢ P (pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.left.e_a
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
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        D.ιInvApp U ≫
          limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
            (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))) =
    limit.π (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U))
      (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))

Tactic:
apply π_ιInvApp_π

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

Goal state before:
pp: case op.right
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j : (MultispanShape.prod D.J).R
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j))

Tactic:
apply π_ιInvApp_π

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : P.RespectsIso
H : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
this : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤
⊢ P f

Tactic:
have : f = X.topIso.inv ≫ (X.isoOfEq this).inv ≫ (f ≫ g) ∣_ g.opensRange ≫
        (IsOpenImmersion.isoOfRangeEq g.opensRange.ι g (by simp)).hom := by
      simp [← cancel_mono g]

Goal state after:
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
H : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hg : IsOpenImmersion g
hfg : P (f ≫ g)
this✝ : (f ≫ g) ⁻¹ᵁ Scheme.Hom.opensRange g = ⊤
this :
  f =
    X.topIso.inv ≫
      (X.isoOfEq this✝).inv ≫
        (f ≫ g) ∣_ Scheme.Hom.opensRange g ≫ (IsOpenImmersion.isoOfRangeEq (Scheme.Hom.opensRange g).ι g ⋯).hom
⊢ P f
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
⊢ lift (D.f i j) s.fst ⋯ ≫ (D.vPullbackCone i j).snd = s.snd

pp: case refine_4
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
⊢ ∀ {m : s.pt ⟶ (D.vPullbackCone i j).pt},
    m ≫ (D.vPullbackCone i j).fst = s.fst → m ≫ (D.vPullbackCone i j).snd = s.snd → m = lift (D.f i j) s.fst ⋯

Tactic:
· rw [← cancel_mono (𝖣.ι j), Category.assoc, ← (𝖣.vPullbackCone i j).condition]
      conv_rhs => rw [← s.condition]
      erw [IsOpenImmersion.lift_fac_assoc]

Goal state after:
case refine_4
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
⊢ ∀ {m : s.pt ⟶ (D.vPullbackCone i j).pt},
    m ≫ (D.vPullbackCone i j).fst = s.fst → m ≫ (D.vPullbackCone i j).snd = s.snd → m = lift (D.f i j) s.fst ⋯