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

Goal state before:
pp: case coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a b : WithZero α
a✝ : α
⊢ (a + b) * ↑a✝ = a * ↑a✝ + b * ↑a✝

Tactic:
cases a

Goal state after:
case coe.zero
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
b : WithZero α
a✝ : α
⊢ (0 + b) * ↑a✝ = 0 * ↑a✝ + b * ↑a✝

case coe.coe
α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
b : WithZero α
a✝¹ a✝ : α
⊢ (↑a✝ + b) * ↑a✝¹ = ↑a✝ * ↑a✝¹ + b * ↑a✝¹
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁴ : Semiring R
S : Type uS
inst✝³ : CommSemiring S
T : Type uT
A : Type uA
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
inst✝ : Algebra S R
r : R → R → Prop
⊢ ∀ (x y : S),
    { toQuot := Quot.mk (Rel r) ((algebraMap S R) (x + y)) } =
      { toQuot := Quot.mk (Rel r) ((algebraMap S R) x) } + { toQuot := Quot.mk (Rel r) ((algebraMap S R) y) }

Tactic:
simp [add_quot]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
⊢ ∀ (x y : R), { toQuot := Quot.mk (Rel r) (x + y) } = { toQuot := Quot.mk (Rel r) x } + { toQuot := Quot.mk (Rel r) y }

Tactic:
simp [add_quot]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
⊢ p.sum f = ∑ n ∈ p.support, f n (p.coeff n)

Tactic:
simp only [sum_def', SkewMonoidAlgebra.sum_def, Finsupp.sum]
  apply Finset.sum_of_injOn (toAdd) (Injective.injOn fun ⦃a₁ a₂⦄ a ↦ a) (fun _ ↦ ?_) <;>
  simp +contextual [coeff]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : n ≠ 1
⊢ X.coeff n = 0

Tactic:
rw [coeff_X, if_neg hn.symm]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p q : SkewPolynomial R
n : ℕ
⊢ (p + q).coeff n = p.coeff n + q.coeff n

Tactic:
simp [coeff]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
a b : R
n : ℕ
⊢ (monomial n) (a - b) = (monomial n) a - (monomial n) b

Tactic:
rw [sub_eq_add_neg, monomial_add, monomial_neg, sub_eq_add_neg]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddGroup k
a : SkewMonoidAlgebra k G
⊢ -a + a = 0

Tactic:
cases a

Goal state after:
case ofCoeff
k : Type u_1
G : Type u_2
inst✝ : AddGroup k
coeff✝ : G →₀ k
⊢ -{ coeff := coeff✝ } + { coeff := coeff✝ } = 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
⊢ 1 * f = f

Tactic:
induction f with
    | single g a => rw [one_def, mul_def, sum_single_index] <;> simp
    | add f g _ _ => simp_all [mul_add]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
α β : X.Hom Y
w : α.base = β.base
h : α.c ≍ β.c
⊢ α = β

Tactic:
cases α
  cases β
  congr

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ X.basicOpen f ≤ U

Tactic:
rintro x ⟨h, _⟩

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
h : x ∈ U
h✝ : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x h)) f)
⊢ x ∈ U
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ m = desc F s

Tactic:
have t :
      m.base =
        colimit.desc (F ⋙ PresheafedSpace.forget C) ((PresheafedSpace.forget C).mapCocone s) := by
      dsimp
      -- `colimit.hom_ext` used to be automatically applied by `ext` before https://github.com/leanprover-community/mathlib4/pull/21302
      apply colimit.hom_ext fun j => ?_
      ext
      rw [colimit.ι_desc, mapCocone_ι_app, ← w j]
      simp
    ext : 1
    · exact t
    · 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.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ X.toRestrictTop ≫ X.ofRestrict ⋯ = 𝟙 X

Tactic:
ext
    · rfl
    · erw [comp_c, ofRestrict_top_c, toRestrictTop_c, eqToHom_map, whiskerRight_id', comp_id,
        eqToHom_trans, eqToHom_refl]
      rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case w
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
⊢ α.hom.base = β.hom.base

pp: case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
⊢ α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = β.hom.c

Tactic:
· exact w

Goal state after:
case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
⊢ α.hom.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = β.hom.c
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: U V X Y : Scheme
g : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
f : X ⟶ Y
inst✝¹ : IsOpenImmersion iU
inst✝ : IsOpenImmersion iV
H : iU ≫ f = g ≫ iV
H' : f ⁻¹ᵁ Scheme.Hom.opensRange iV = Scheme.Hom.opensRange iU
e : pullback iV f ≅ U := isoOfRangeEq (pullback.snd iV f) iU ⋯
⊢ IsPullback g iU iV f

Tactic:
convert!
    (IsPullback.of_horiz_isIso
          (show CommSq e.inv iU (pullback.snd iV f) (𝟙 X) from ⟨by simp [e]⟩)).paste_horiz
      (IsPullback.of_hasPullback iV f)

Goal state after:
case e'_7
U V X Y : Scheme
g : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
f : X ⟶ Y
inst✝¹ : IsOpenImmersion iU
inst✝ : IsOpenImmersion iV
H : iU ≫ f = g ≫ iV
H' : f ⁻¹ᵁ Scheme.Hom.opensRange iV = Scheme.Hom.opensRange iU
e : pullback iV f ≅ U := isoOfRangeEq (pullback.snd iV f) iU ⋯
⊢ g = e.inv ≫ pullback.fst iV f
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
U : (Opens ↑X)ᵒᵖ
m : Submonoid ↑(F.presheaf.obj U) := ⋯
s : ↑(F.presheaf.obj U)
hs : s ∈ m
t : ↑(F.presheaf.obj U)
e : t * s = 0
x : ↑X
hx : x ∈ unop U
⊢ (ConcreteCategory.hom (F.presheaf.germ (unop U) x hx)) t *
      (CommRingCat.Hom.hom (F.presheaf.germ (unop U) ↑⟨x, hx⟩ ⋯)) s =
    0

Tactic:
rw [← map_mul, e, map_zero]

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) ≫ (V.stalkIso x).inv =
    (U.stalkIso ((resLE f U V e) x)).inv ≫ stalkMap (resLE f U V e) x

Tactic:
Opens.stalkIso_inv,

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 =
    (U.stalkIso ((resLE f U V e) x)).inv ≫ stalkMap (resLE f U V e) x
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 =
    (U.stalkIso ((resLE f U V e) x)).inv ≫ stalkMap (resLE f U V e) x

Tactic:
Opens.stalkIso_inv,

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 =
    stalkMap U.ι ((resLE f U V e) x) ≫ stalkMap (resLE f U V e) x
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f

Tactic:
rw [Iso.eq_inv_comp, isoSpec, asIso_hom, ← Scheme.toSpecΓ_naturality_assoc, isoSpec,
    asIso_inv, IsIso.hom_inv_id, Category.comp_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: case w
X Y : LocallyRingedSpace
f : X ⟶ Y
⊢ ((𝟭 LocallyRingedSpace).obj X).toΓSpec.base ≫ (Spec.locallyRingedSpaceMap (Γ.rightOp.map f).unop).base =
    ((𝟭 LocallyRingedSpace).map f ≫ Y.toΓSpec).base

Tactic:
ext1 x

Goal state after:
case w
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑↑((𝟭 LocallyRingedSpace).obj X).toPresheafedSpace
⊢ (ConcreteCategory.hom
        (((𝟭 LocallyRingedSpace).obj X).toΓSpec.base ≫ (Spec.locallyRingedSpaceMap (Γ.rightOp.map f).unop).base))
      x =
    (ConcreteCategory.hom ((𝟭 LocallyRingedSpace).map f ≫ Y.toΓSpec).base) x
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : ↑x ∈ U
this : IsAffine ↑U
r : ↑Γ(↑U, ⊤)
h₁ : ⟨↑x, h⟩ ∈ ↑((↑U).basicOpen r)
h₂ : (↑U).basicOpen r ≤ U.ι ⁻¹ᵁ V
⊢ ↑x ∈ X.basicOpen r

Tactic:
simpa [U.mem_basicOpen_toScheme] using! h₁

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : Scheme
B : CommRingCat
φ : B ⟶ Γ(X, ⊤)
⊢ Scheme.Hom.appTop ((ΓSpec.adjunction.homEquiv X (op B)) φ.op) = (Scheme.ΓSpecIso B).hom ≫ φ

Tactic:
rw [← Iso.inv_comp_eq, ΓSpecIso_inv_ΓSpec_adjunction_homEquiv]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
g : ↑Γ(X, X.basicOpen f)
⊢ ∃ f', X.basicOpen f' = X.basicOpen g

Tactic:
by
  have := isLocalization_basicOpen hU f
  obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.surj'' (Submonoid.powers f) g
  use f * x
  rw [Algebra.smul_def, Scheme.basicOpen_mul, Scheme.basicOpen_mul, RingHom.algebraMap_toAlgebra,
    Scheme.basicOpen_res]
  refine (inf_eq_left.mpr (inf_le_left.trans_eq (Scheme.basicOpen_of_isUnit _ ?_).symm)).symm
  exact
    Submonoid.leftInv_le_isUnit _
      (IsLocalization.toInvSubmonoid (Submonoid.powers f) (Γ(X, X.basicOpen f))
        _).prop

Goal state after:
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
y : ↑(PrimeSpectrum.Top S)
this✝² : Module R N := Module.compHom N σ
this✝¹ : Algebra R S := σ.toAlgebra
this✝ : IsScalarTower R S N
f' : M →ₗ[R] N :=
  let __spread.0 := f;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
x : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this : Function.Bijective ⇑((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N))) ↑⟨σ ↑x, ⋯⟩)
⊢ ⇑((algebraMap R (Module.End R (LocalizedModule y.asIdeal.primeCompl N))) ↑x) =
    ⇑((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N))) ↑⟨σ ↑x, ⋯⟩)

Tactic:
exact (IsScalarTower.algebraMap_smul ..).symm

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
z : ↑(pullback (D.f j i) (D.f j k)) :=
  (ConcreteCategory.hom (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv)
    ⟨((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x, y), ⋯⟩
⊢ D.Rel ⟨i, a⟩ ⟨k, c⟩

Tactic:
have eq₁ : (D.t j i) ((pullback.fst _ _ : _ /-(D.f j k)-/ ⟶ D.V (j, i)) z) = x := by
      dsimp only [coe_of, z]
      rw [pullbackIsoProdSubtype_inv_fst_apply, D.t_inv_apply]

Goal state after:
D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
z : ↑(pullback (D.f j i) (D.f j k)) :=
  (ConcreteCategory.hom (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv)
    ⟨((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x, y), ⋯⟩
eq₁ : (ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z) = x
⊢ D.Rel ⟨i, a⟩ ⟨k, c⟩
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e'_2
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
e_1✝ : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum ↑Γ(X, U))
⊢ (fun i ↦ ⇑hU.fromSpec ⁻¹' ↑(X.basicOpen ↑i)) = fun i ↦ (PrimeSpectrum.basicOpen ↑i).carrier

Tactic:
ext1 x

Goal state after:
case e'_2
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
e_1✝ : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum ↑Γ(X, U))
x : ↑s
⊢ ⇑hU.fromSpec ⁻¹' ↑(X.basicOpen ↑x) = (PrimeSpectrum.basicOpen ↑x).carrier
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i j : D.J
x : ↑D.glued
x₁ : ↑(D.U i)
eq₁ : (ConcreteCategory.hom (D.ι i)) x₁ = x
x₂ : ↑(D.U j)
eq₂ : (ConcreteCategory.hom (D.ι j)) x₂ = x
y : ↑(D.V (⟨i, x₁⟩.fst, ⟨j, x₂⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, x₁⟩.fst ⟨j, x₂⟩.fst)) y = ⟨i, x₁⟩.snd
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (D.f i j ≫ D.ι i))

Tactic:
· subst eq₁
      exact ⟨y, by simp [e₁]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : BinaryFan 0 X
m : s.pt ⟶ X
x✝ : m ≫ 0 = s.fst
h₂ : m ≫ 𝟙 X = s.snd
⊢ m = s.snd

Tactic:
simpa using h₂

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ (prodZeroIso X).inv ≫ prod.fst = 𝟙 X

Tactic:
by
  dsimp [prodZeroIso, binaryFanZeroRight]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : BinaryCofan 0 X
m : X ⟶ s.pt
x✝ : 0 ≫ m = s.inl
h₂ : 𝟙 X ≫ m = s.inr
⊢ m = s.inr

Tactic:
simpa using h₂

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : (𝒰.f i) x = (𝒰.f j) y
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt ≅
  (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j))) (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j)))
      ⋯).pt :=
  (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).conePointUniqueUpToIso
    (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.f i) (𝒰.f j))
⊢ ((gluedCover 𝒰).ι i) x = ((gluedCover 𝒰).ι j) y

Tactic:
𝒰.gluedCover.ι_eq_iff

Goal state after:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : (𝒰.f i) x = (𝒰.f j) y
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt ≅
  (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j))) (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j)))
      ⋯).pt :=
  (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).conePointUniqueUpToIso
    (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.f i) (𝒰.f j))
⊢ (gluedCover 𝒰).Rel ⟨i, x⟩ ⟨j, y⟩
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.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ pullback.snd (𝒰.f i ≫ f) g =
    pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ pullback.snd (𝒰.f i ≫ f) g

Tactic:
· simp only [Category.assoc, t_fst_snd]

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

Goal state before:
pp: case op.op.snd
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ D.opensImagePreimageMap i j U ≫
      (D.f j k).c.app (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    D.opensImagePreimageMap i k U ≫
      ((D.f k j).c.app (op ((Opens.map (D.ι k).base).obj (⋯.functor.obj U))) ≫
          (D.t j k).c.app ((Opens.map (D.f k j).base).op.obj (op ((Opens.map (D.ι k).base).obj (⋯.functor.obj U))))) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
rw [opensImagePreimageMap_app_assoc]

Goal state after:
case op.op.snd
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          (unop (op ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 (unop (op U))))) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    D.opensImagePreimageMap i k U ≫
      ((D.f k j).c.app (op ((Opens.map (D.ι k).base).obj (⋯.functor.obj U))) ≫
          (D.t j k).c.app ((Opens.map (D.f k j).base).op.obj (op ((Opens.map (D.ι k).base).obj (⋯.functor.obj U))))) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_1.refine_1
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥(X' ⨿ Y')
⊢ x ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) ↔ x ∈ ↑(Scheme.Hom.opensRange coprod.inl)

Tactic:
obtain ⟨x | x, rfl⟩ := (coprodMk _ _).surjective x

Goal state after:
case refine_1.refine_1.inl
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥X'
⊢ (coprodMk X' Y') (Sum.inl x) ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) ↔
    (coprodMk X' Y') (Sum.inl x) ∈ ↑(Scheme.Hom.opensRange coprod.inl)

case refine_1.refine_1.inr
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥Y'
⊢ (coprodMk X' Y') (Sum.inr x) ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) ↔
    (coprodMk X' Y') (Sum.inr x) ∈ ↑(Scheme.Hom.opensRange coprod.inl)