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

Goal state before:
pp: α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ sym (⅟2 * (unsym a * unsym c + unsym b * unsym c + unsym c * (unsym a + unsym b))) =
    sym (⅟2 * (unsym a * unsym c + unsym c * unsym a + (unsym b * unsym c + unsym c * unsym b)))

Tactic:
congr 2

Goal state after:
case e_6.e_a
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a b c : αˢʸᵐ
⊢ unsym a * unsym c + unsym b * unsym c + unsym c * (unsym a + unsym b) =
    unsym a * unsym c + unsym c * unsym a + (unsym b * unsym c + unsym c * unsym b)
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i, f i) = ⨅ i, untrop (f i)

Tactic:
rw [iInf, ← Set.image_univ, ← coe_univ, untrop_sum_eq_sInf_image, Function.comp_def]

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_4
V : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommGroup V
inst✝² : StarAddMonoid V
inst✝¹ : Module R V
inst✝ : StarModule R V
f : WithConv (End R V)
α : R
x : V
⊢ x ∈ (star f).ofConv.eigenspace α ↔ star x ∈ f.ofConv.eigenspace (star α)

Tactic:
simp_rw [mem_eigenspace_iff, intrinsicStar_apply, star_eq_iff_star_eq, star_smul, eq_comm]

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
⊢ y ∈ {x | ∃ (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)}

Tactic:
use i.le hy

Goal state after:
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)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case app.op.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
carrier✝ : Set ↑↑(Y.restrict ⋯)
is_open'✝ : IsOpen carrier✝
⊢ op
      {
        carrier :=
          ⇑(ConcreteCategory.hom f.base) ⁻¹' ↑((opensFunctor f).obj { carrier := carrier✝, is_open' := is_open'✝ }),
        is_open' := ⋯ } =
    op { carrier := carrier✝, is_open' := is_open'✝ }

Tactic:
congr 2

Goal state after:
case app.op.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
carrier✝ : Set ↑↑(Y.restrict ⋯)
is_open'✝ : IsOpen carrier✝
⊢ ⇑(ConcreteCategory.hom f.base) ⁻¹' ↑((opensFunctor f).obj { carrier := carrier✝, is_open' := is_open'✝ }) = carrier✝
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
⊢ op { carrier := ⇑(ConcreteCategory.hom s.snd.base) ⁻¹' ↑(⋯.functor.obj (unop U)), is_open' := ⋯ } =
    op { carrier := ⇑(ConcreteCategory.hom (pullback.lift s.fst.base s.snd.base ⋯)) ⁻¹' ↑(unop U), is_open' := ⋯ }

Tactic:
congr 2

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
⊢ ⇑(ConcreteCategory.hom s.snd.base) ⁻¹' ↑(⋯.functor.obj (unop U)) =
    ⇑(ConcreteCategory.hom (pullback.lift s.fst.base s.snd.base ⋯)) ⁻¹' ↑(unop U)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : LocallyRingedSpace
h : ∀ (x : ↑X.toTopCat), ∃ R f, x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ IsOpenImmersion f
x : ↑X.toTopCat
⊢ ∃ U R, Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))

Tactic:
obtain ⟨R, f, h₁, h₂⟩ := h x

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : LocallyRingedSpace
h : ∀ (x : ↑X.toTopCat), ∃ R f, x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ IsOpenImmersion f
x : ↑X.toTopCat
R : CommRingCat
f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X
h₁ : x ∈ Set.range ⇑(ConcreteCategory.hom f.base)
h₂ : IsOpenImmersion f
⊢ ∃ U R, Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case φ
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ (limit.cone (cospan f.base g.base)).pt ≅
    ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
        ((forget C).mapCone (pullbackConeOfLeft f g))).pt

Tactic:
exact Iso.refl _

Goal state after:
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
⊢ IsOpenImmersion (pullback.fst g f)

Tactic:
rw [SheafedSpace.isOpenImmersion_iff_hom]
  have : _ = (pullback.fst g f).hom := preservesLimitIso_hom_π forget (cospan g f) left
  rw [← this]
  have := HasLimit.isoOfNatIso_hom_π (diagramIsoCospan (cospan g f ⋙ forget)) left
  dsimp at this
  rw [Category.comp_id] at this
  rw [← this]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

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

Tactic:
by
  simp [← cancel_mono W.ι]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

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

Tactic:
by
  simp_rw [← resLE_id, resLE_comp_resLE, Category.id_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ
f : r ⟶ s
⊢ ((inducedFunctor basicOpen).op ⋙ (structureSheaf ↑(Γ.obj (op X))).obj).map f ≫ X.toΓSpecCApp (unop s) =
    X.toΓSpecCApp (unop r) ≫
      ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).obj).map f

Tactic:
apply (StructureSheaf.to_basicOpen_epi (Γ.obj (op X)) r.unop).1

Goal state after:
X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ
f : r ⟶ s
⊢ CommRingCat.ofHom (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen (unop r))))) ≫
      ((inducedFunctor basicOpen).op ⋙ (structureSheaf ↑(Γ.obj (op X))).obj).map f ≫ X.toΓSpecCApp (unop s) =
    CommRingCat.ofHom
        (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen (unop r))))) ≫
      X.toΓSpecCApp (unop r) ≫
        ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).obj).map f
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⋂ i ∈ s, ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ

Tactic:
simp_rw [← Set.preimage_iInter₂, Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl,
    compl_compl]

Goal state after:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ⋂ i ∈ s, zeroLocus {i}
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝ : Category.{v_1, u_1} J
F : Discrete J ⥤ Type u_2
⊢ F.IsLocallyDirected

Tactic:
by
  constructor
  rintro ⟨i⟩ ⟨j⟩ ⟨k⟩ ⟨⟨⟨⟩⟩⟩ ⟨⟨⟨⟩⟩⟩
  simpa using fun x ↦ ⟨i, 𝟙 _, 𝟙 _, x, by simp⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case w
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ PrimeSpectrum.comap ((CommRingCat.Hom.hom (X.presheaf.Γgerm x)).comp (CommRingCat.Hom.hom (f.c.app (op ⊤))))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)) =
    PrimeSpectrum.comap (CommRingCat.Hom.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x)))
      (PrimeSpectrum.comap (CommRingCat.Hom.hom (Hom.stalkMap f x)) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)))

Tactic:
← PrimeSpectrum.comap_comp_apply,

Goal state after:
case w
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ PrimeSpectrum.comap ((CommRingCat.Hom.hom (X.presheaf.Γgerm x)).comp (CommRingCat.Hom.hom (f.c.app (op ⊤))))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)) =
    PrimeSpectrum.comap
      ((CommRingCat.Hom.hom (Hom.stalkMap f x)).comp
        (CommRingCat.Hom.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x))))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case w
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ PrimeSpectrum.comap (CommRingCat.Hom.hom (f.c.app (op ⊤) ≫ X.presheaf.Γgerm x))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)) =
    PrimeSpectrum.comap (CommRingCat.Hom.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x) ≫ Hom.stalkMap f x))
      (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))

Tactic:
congr 2

Goal state after:
case w.e_f
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ f.c.app (op ⊤) ≫ X.presheaf.Γgerm x = Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x) ≫ Hom.stalkMap f x
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)ᵒᵖ
⊢ (locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R))).unop ≫
      Γ.map ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f).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

Tactic:
← Γ.rightOp_map_unop,

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)ᵒᵖ
⊢ (locallyRingedSpaceAdjunction.counit.app (op (CommRingCat.of R))).unop ≫
      (Γ.rightOp.map ((locallyRingedSpaceAdjunction.homEquiv X (op (CommRingCat.of R))) f)).unop ≫
        ((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.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
s t : (structureSheafInType R M).obj.obj (op U)
x✝ : ↥(unop (op V))
⊢ ↑⟨comapFun f U V hUV ↑(s + t), ⋯⟩ x✝ = ↑(⟨comapFun f U V hUV ↑s, ⋯⟩ + ⟨comapFun f U V hUV ↑t, ⋯⟩) x✝

Tactic:
by dsimp [comapFun]; rw [map_add]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ IsOpenImmersion.lift U.ι f ⋯ ≫ U.ι = g

Tactic:
← IsOpenImmersion.lift_fac U.ι g (by simpa [Set.range_subset_iff] using fun x hx ↦ hUg.ge hx)

Goal state after:
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ IsOpenImmersion.lift U.ι f ⋯ ≫ U.ι = IsOpenImmersion.lift U.ι g ⋯ ≫ U.ι
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom ((f.toHom ≫ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom).c.app (op U))) s) =
    X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom ((g.toHom ≫ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom).c.app (op U))) s)

Tactic:
erw [SheafedSpace.congr_hom_app (coequalizer.condition f.toShHom g.toShHom),
      CommRingCat.comp_apply, X.toRingedSpace.basicOpen_res]

Goal state after:
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ unop ((Opens.map (Hom.toShHom f ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).op.obj (op U)) ⊓
      X.toRingedSpace.basicOpen
        ((ConcreteCategory.hom ((Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s) =
    X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom ((g.toHom ≫ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom).c.app (op U))) s)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
h : MkCore
i j k : h.J
⊢ ((pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom ≫
        ofHom
            {
              toFun := fun x ↦
                ⟨(⟨↑((ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩,
              continuous_toFun := ⋯ } ≫
          (pullbackIsoProdSubtype (h.V j k).inclusion' (h.V j i).inclusion').inv) ≫
      pullback.snd (h.V j k).inclusion' (h.V j i).inclusion' =
    pullback.fst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j

Tactic:
rw [Category.assoc, Category.assoc, pullbackIsoProdSubtype_inv_snd, ← Iso.eq_inv_comp,
      pullbackIsoProdSubtype_inv_fst_assoc]

Goal state after:
D : GlueData
h : MkCore
i j k : h.J
⊢ ofHom
        {
          toFun := fun x ↦
            ⟨(⟨↑((ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩, (ConcreteCategory.hom (h.t i j)) (↑x).1), ⋯⟩,
          continuous_toFun := ⋯ } ≫
      pullbackSnd (h.V j k).inclusion' (h.V j i).inclusion' =
    pullbackFst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ op
      {
        carrier :=
          ⇑(ConcreteCategory.hom (D.t k i).base) ⁻¹'
            ⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) '' ↑U,
        is_open' := ⋯ } =
    op
      {
        carrier :=
          ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) ''
            ⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑U,
        is_open' := ⋯ }

Tactic:
congr 2

Goal state after:
case w
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
⊢ ⇑(ConcreteCategory.hom (D.t k i).base) ⁻¹' ⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) '' ↑U =
    ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) '' ⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑U
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
    pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)

Tactic:
rw [← cancel_mono (𝒰.f i)]; simp only [pullback.condition, t_snd, Category.assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
i : ι
x : ↥(f i)
⊢ (ConcreteCategory.hom
        ((TopCat.sigmaCofan fun x ↦ (f x).toTopCat).inj i ≫
          (colimit.isoColimitCocone
                { cocone := TopCat.sigmaCofan fun x ↦ (f x).toTopCat,
                  isColimit := TopCat.sigmaCofanIsColimit fun x ↦ (f x).toTopCat }).inv ≫
            (PreservesCoproduct.iso Scheme.forgetToTop f).symm.hom))
      x =
    (ConcreteCategory.hom (Scheme.forgetToTop.map (Sigma.ι f i))) x

Tactic:
congr 2

Goal state after:
ι : Type u
f : ι → Scheme
i : ι
x : ↥(f i)
⊢ (TopCat.sigmaCofan fun x ↦ (f x).toTopCat).inj i ≫
      (colimit.isoColimitCocone
            { cocone := TopCat.sigmaCofan fun x ↦ (f x).toTopCat,
              isColimit := TopCat.sigmaCofanIsColimit fun x ↦ (f x).toTopCat }).inv ≫
        (PreservesCoproduct.iso Scheme.forgetToTop f).symm.hom =
    Scheme.forgetToTop.map (Sigma.ι f i)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x✝ : WalkingPair
⊢ WalkingPair.casesOn (Equiv.ulift.symm x✝).down X Y ≅ WalkingPair.casesOn x✝ X Y

Tactic:
exact Iso.refl _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
x : ↥X
⊢ (ConcreteCategory.hom
        (((↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace).inl ≫
          (colimit.isoColimitCocone
                { cocone := (↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace,
                  isColimit := (↑X.toPresheafedSpace).binaryCofanIsColimit ↑Y.toPresheafedSpace }).inv ≫
            (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom))
      x =
    (ConcreteCategory.hom (Scheme.forgetToTop.map coprod.inl)) x

Tactic:
congr 2

Goal state after:
X Y : Scheme
x : ↥X
⊢ ((↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace).inl ≫
      (colimit.isoColimitCocone
            { cocone := (↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace,
              isColimit := (↑X.toPresheafedSpace).binaryCofanIsColimit ↑Y.toPresheafedSpace }).inv ≫
        (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom =
    Scheme.forgetToTop.map coprod.inl
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X Y : Scheme
x : ↥Y
⊢ (ConcreteCategory.hom
        (((↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace).inr ≫
          (colimit.isoColimitCocone
                { cocone := (↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace,
                  isColimit := (↑X.toPresheafedSpace).binaryCofanIsColimit ↑Y.toPresheafedSpace }).inv ≫
            (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom))
      x =
    (ConcreteCategory.hom (Scheme.forgetToTop.map coprod.inr)) x

Tactic:
congr 2

Goal state after:
X Y : Scheme
x : ↥Y
⊢ ((↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace).inr ≫
      (colimit.isoColimitCocone
            { cocone := (↑X.toPresheafedSpace).binaryCofan ↑Y.toPresheafedSpace,
              isColimit := (↑X.toPresheafedSpace).binaryCofanIsColimit ↑Y.toPresheafedSpace }).inv ≫
        (PreservesColimitPair.iso Scheme.forgetToTop X Y).hom =
    Scheme.forgetToTop.map coprod.inr
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_2
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
Z : Scheme
f : Z ⟶ X ⨿ Y
⊢ IsCompl (Scheme.Hom.opensRange (pullback.fst f coprod.inl)) (Scheme.Hom.opensRange (pullback.fst f coprod.inr))

Tactic:
Scheme.Hom.opensRange_pullbackFst,

Goal state after:
case refine_2
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
Z : Scheme
f : Z ⟶ X ⨿ Y
⊢ IsCompl (f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange (pullback.fst f coprod.inr))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        (D.f i i).c.app (op U) ≫
          (D.V (i, i)).presheaf.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U))) ≫
            (D.V (i, i)).presheaf.map (eqToHom ⋯) ≫
              invApp (D.f i i) ((Opens.map (D.t i i).base).1 (unop ((Opens.map (D.f i i).base).op.obj (op U)))) ≫
                (D.U i).presheaf.map (eqToHom ⋯).op ≫
                  (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫
                    (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))

Tactic:
rw [← Functor.map_comp_assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        (D.f i i).c.app (op U) ≫
          (D.V (i, i)).presheaf.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯) ≫
            invApp (D.f i i) ((Opens.map (D.t i i).base).1 (unop ((Opens.map (D.f i i).base).op.obj (op U)))) ≫
              (D.U i).presheaf.map (eqToHom ⋯).op ≫
                (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫
                  (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        (D.U i).presheaf.map (homOfLE ⋯).op ≫
          (D.U i).presheaf.map
              ((opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫
            (D.U i).presheaf.map (eqToHom ⋯).op ≫
              (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫
                (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))

Tactic:
rw [← Functor.map_comp_assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      (D.U i).presheaf.map ((eqToIso ⋯).inv ≫ (homOfLE ⋯).op) ≫
        (D.U i).presheaf.map
            ((opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫
          (D.U i).presheaf.map (eqToHom ⋯).op ≫
            (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫
              (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))