mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case refine_2
X✝ Y Z T : Scheme
M N K : X✝.Modules
φ : M ⟶ N
U✝ V✝ : X✝.Opens
X : Scheme
U V : X.Opens
f : V ⟶ U
this✝⁴ :
  (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥↑V) (Opens.grothendieckTopology ↑U.carrier)
this✝³ :
  Functor.IsDenseSubsite (Opens.grothendieckTopology ↥U) ((Opens.grothendieckTopology ↥X).over U)
    (Opens.overEquivalence U).inverse
this✝² : (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥V) (Opens.grothendieckTopology ↥↑U)
this✝¹ :
  ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
this✝ :
  (Opens.overEquivalence U).symm.functor.IsContinuous (Opens.grothendieckTopology ↥↑U)
    ((Opens.grothendieckTopology ↥X).over U)
this :
  (Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
⊢ (((Opens.overPullbackSheafEquivOver V).app X.ringCatSheaf).inv ≫
        ((Opens.overEquivalence V).symm.functor.sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥V)
              ((Opens.grothendieckTopology ↥X).over V)).map
          (Sheaf.pushforwardOverMapIso X.ringCatSheaf f).inv) ≫
      (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun W ↦ Over.isoMk (eqToIso ⋯) ⋯) ⋯).hom RingCat
            (Opens.grothendieckTopology ↥V) ((Opens.grothendieckTopology ↥X).over U)).app
        (Sheaf.over X.ringCatSheaf U) =
    {
        hom :=
          Functor.whiskerRight { app := fun U_1 ↦ (Hom.appIso (X.homOfLE ⋯) (Opposite.unop U_1)).inv, naturality := ⋯ }
            (forget₂ CommRingCat RingCat) } ≫
      ((Hom.opensFunctor (X.homOfLE ⋯)).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥↑V)
            (Opens.grothendieckTopology ↥U)).map
        ((Opens.overPullbackSheafEquivOver U).app X.ringCatSheaf).inv

Tactic:
· ext W x
    suffices X.presheaf.map _ x = ((X.homOfLE <| leOfHom f).appIso _).inv x by simpa
    rw [Scheme.Hom.appIso_homOfLE_inv]
    rfl

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

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g✝ : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (Scheme.Hom.opensRange (awayι 𝒜 f f_deg hm) ⊓ Scheme.Hom.opensRange (awayι 𝒜 g g_deg hm')).carrier =
    (Scheme.Hom.opensRange (awayι 𝒜 x ⋯ ⋯)).carrier

Tactic:
opensRange_awayι,

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g✝ : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (basicOpen 𝒜 f ⊓ Scheme.Hom.opensRange (awayι 𝒜 g g_deg hm')).carrier =
    (Scheme.Hom.opensRange (awayι 𝒜 x ⋯ ⋯)).carrier
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g✝ : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (basicOpen 𝒜 f ⊓ Scheme.Hom.opensRange (awayι 𝒜 g g_deg hm')).carrier =
    (Scheme.Hom.opensRange (awayι 𝒜 x ⋯ ⋯)).carrier

Tactic:
opensRange_awayι,

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g✝ : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g).carrier = (Scheme.Hom.opensRange (awayι 𝒜 x ⋯ ⋯)).carrier
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g✝ : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g).carrier = (Scheme.Hom.opensRange (awayι 𝒜 x ⋯ ⋯)).carrier

Tactic:
opensRange_awayι,

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g✝ : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g).carrier = (basicOpen 𝒜 x).carrier
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x✝ x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x y : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
e : pullback ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≅
  ↑(X.basicOpen (f (x.snd.fst * y.snd.fst))) := ⋯
⊢ e.inv ≫
      pullback.fst ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≫
        toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫ (basicOpen 𝒜 x.snd.fst).ι =
    toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫ (basicOpen 𝒜 (x.snd.fst * y.snd.fst)).ι

Tactic:
simpa [e, openCoverOfMapIrrelevantEqTop, Scheme.isoOfEq_inv] using
      homOfLE_toBasicOpenOfGlobalSections_ι _ _ rfl rfl y.2.2.2

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M N : ModuleCat ↑R
f : M ⟶ N
U : Opens (PrimeSpectrum ↑R)
⊢ toOpen M U ≫ (modulesSpecToSheaf.map (tilde.map f)).hom.app (op U) = f ≫ toOpen N U

Tactic:
by
  ext x; exact Subtype.ext (funext fun y ↦ IsLocalizedModule.map_apply y.1.asIdeal.primeCompl
    (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl M)
     (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl N) _ x)

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
s : Finset ι' := {x | 0 < dv x}
⊢ ∀ (i : ↥s), 0 < (dv ∘ Subtype.val) i

Tactic:
simp [s]

Goal state after:
Module: Mathlib.RingTheory.Valuation.Integral

Goal state before:
pp: case neg
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf : v (∑ i ∈ Finset.range f.natDegree, (algebraMap O R) (f.coeff i) * x ^ i) = v (-x ^ f.natDegree)
⊢ v x ≤ 1

Tactic:
simp only [map_neg, map_pow] at hf

Goal state after:
case neg
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hn : ¬f.natDegree = 0
hf : v (∑ i ∈ Finset.range f.natDegree, (algebraMap O R) (f.coeff i) * x ^ i) = v x ^ f.natDegree
⊢ v x ≤ 1
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  { toFun := FromSpec.toFun f_deg hm, invFun := ToSpec.toFun f, left_inv := ⋯, right_inv := ⋯ }
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
change IsOpen <| e ⁻¹' _

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  { toFun := FromSpec.toFun f_deg hm, invFun := ToSpec.toFun f, left_inv := ⋯, right_inv := ⋯ }
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
V : ValuationSubring K := ⋯
⊢ V.toLocalSubring ≤ LocalSubring.range g

Tactic:
have H : (algebraMap R K).range ≤ g.range := fun x ⟨a, ha⟩ ↦ ⟨f a, by simp [← ha, ← h]⟩

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
V : ValuationSubring K := { toSubring := (algebraMap R K).range, mem_or_inv_mem' := ⋯ }
H : (algebraMap R K).range ≤ g.range
⊢ V.toLocalSubring ≤ LocalSubring.range g
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal 𝒜).pred fun x ↦ (fun x ↦ (HomogeneousLocalization.mapId 𝒜 ⋯) s) (i x)

Tactic:
obtain ⟨s, rfl⟩ := HomogeneousLocalization.mk_surjective s
        obtain ⟨n, hn : f ^ n = s.den.1⟩ := s.den_mem
        exact ⟨_, x.2, 𝟙 _, s.1, s.2, s.3,
          fun x hsx ↦ x.2 (Ideal.IsPrime.mem_of_pow_mem inferInstance n (hn ▸ hsx)), fun _ ↦ rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
this : F.IsCoverDense J
S : Sieve W :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
Z : C
g : Z ⟶ W
hg : S.arrows g
⊢ Sieve Z

Tactic:
letI str := Presieve.getFunctorPushforwardStructure hg.bindStruct.hg

Goal state after:
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
this : F.IsCoverDense J
S : Sieve W :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
Z : C
g : Z ⟶ W
hg : S.arrows g
str : Presieve.FunctorPushforwardStructure F
  (F.imageSieve ((Nonempty.some ⋯).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some ⋯).map ≫ p₂)).arrows
  ((Presieve.bind.bindStruct hg).g ≫ (Nonempty.some ⋯).lift) :=
  Presieve.getFunctorPushforwardStructure ⋯
⊢ Sieve Z
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝³ : Category.{v₀, u₀} C₀
inst✝² : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : IsDenseSubsite J₀ J F
X✝ : C
data✝ : F.OneHypercoverDenseData J₀ J X✝
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ Z₀ : C₀
g : Y₀ ⟶ X₀
h : data.SieveStruct f g
p : Z₀ ⟶ Y₀
⊢ (F.map p ≫ h.q) ≫ data.f h.i₀ = F.map (p ≫ g) ≫ f

Tactic:
rw [assoc, h.fac, map_comp_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Etale

Goal state before:
pp: X : Scheme
W : X.Etale
ι : Type u_1
Z : ι → X.Etale
f : (i : ι) → Z i ⟶ W
hf : Sieve.ofArrows Z f ∈ X.smallEtaleTopology W
U : Cover (precoverage @Etale) W.left
w✝¹ : Cover.Over X U
w✝ : ∀ (j : U.I₀), Etale (U.X j ↘ X)
hU : U.toPresieveOverProp w✝ ≤ (Sieve.ofArrows Z f).arrows
i : U.I₀
u : ↥(U.X i)
Y : X.Etale
j : ι
b : (U.X i).asOverProp X ⋯ ⟶ Z j
fac : b.left ≫ (f j).left = U.f i
⊢ (f j).left (b.left u) = (U.f i) u

Tactic:
by simp [← fac]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
⊢ zariskiPrecoverage ≤ qcPrecoverage ∧ zariskiPrecoverage ≤ precoverage P

Tactic:
refine ⟨zariskiPrecoverage_le_qcPrecoverage, precoverage_mono fun X Y f hf ↦ ?_⟩

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
hf : IsOpenImmersion f
⊢ P f
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
⊢ generate (Presieve.ofArrows X π) = generateFamily X π

Tactic:
ext Y g
  constructor
  · rintro ⟨W, g, f, ⟨a⟩, rfl⟩
    exact ⟨a, g, rfl⟩
  · rintro ⟨a, g, rfl⟩
    exact ⟨_, g, π a, ⟨a⟩, rfl⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
H : IsColimit (Sieve.generateFamily X π).arrows.cocone
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
⊢ ∀ ⦃X_1 Y : (Sieve.generateFamily X π).arrows.category⦄ (f : X_1 ⟶ Y),
    ((Sieve.generateFamily X π).arrows.diagram.map f ≫
        match Y with
        | { obj := obj, property := hT } => ⋯.choose ≫ e (Exists.choose hT)) =
      (match X_1 with
        | { obj := obj, property := hT } => ⋯.choose ≫ e (Exists.choose hT)) ≫
        ((Functor.const (Sieve.generateFamily X π).arrows.category).obj W).map f

Tactic:
by
          rintro ⟨A, a, (g₁ : A.left ⟶ _), ha⟩ ⟨B, b, (g₂ : B.left ⟶ _), hb⟩ ⟨q : A ⟶ B⟩
          dsimp; rw [Category.comp_id, ← Category.assoc]
          apply h; rw [Category.assoc]
          generalize_proofs h1 h2 h3 h4
          rw [h2.choose_spec, h4.choose_spec, Over.w]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: case refine_2
T : Type v
inst✝ : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap ⇑(Spec.map f)
⊢ ∀ (x : (continuousMapPresheaf T).obj (Opposite.op (Spec S))),
    (∀ {Z : Scheme} (p₁ p₂ : Z ⟶ Spec S),
        p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
          (ConcreteCategory.hom ((continuousMapPresheaf T).map p₁.op)) x =
            (ConcreteCategory.hom ((continuousMapPresheaf T).map p₂.op)) x) →
      ∃! y, (ConcreteCategory.hom ((continuousMapPresheaf T).map (Spec.map f).op)) y = x

Tactic:
intro (x : C(Spec S, T))

Goal state after:
case refine_2
T : Type v
inst✝ : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap ⇑(Spec.map f)
x : C(↥(Spec S), T)
⊢ (∀ {Z : Scheme} (p₁ p₂ : Z ⟶ Spec S),
      p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
        (ConcreteCategory.hom ((continuousMapPresheaf T).map p₁.op)) x =
          (ConcreteCategory.hom ((continuousMapPresheaf T).map p₂.op)) x) →
    ∃! y, (ConcreteCategory.hom ((continuousMapPresheaf T).map (Spec.map f).op)) y = x
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
hx₄ : π ≫ x₄ ≫ k = π ≫ 0
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
x₂' : T₁ ⟶ X₂
hx₂' : π ≫ x₄ = x₂' ≫ r
⊢ x₄ = 0

Tactic:
comp_zero,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
hx₄ : π ≫ x₄ ≫ k = 0
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
x₂' : T₁ ⟶ X₂
hx₂' : π ≫ x₄ = x₂' ≫ r
⊢ x₄ = 0
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
hx₄ : 0 ≫ r' = 0
hx₂' : π ≫ x₄ = 0 ≫ r
⊢ x₄ = 0

Tactic:
rw [zero_comp] at hx₂'

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
hx₄ : 0 ≫ r' = 0
hx₂' : π ≫ x₄ = 0
⊢ x₄ = 0
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ S.f.app j ≫ S.g.app j ≫ c₃.ι.app j = c₁.ι.app j ≫ 0

Tactic:
comp_zero,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ S.f.app j ≫ S.g.app j ≫ c₃.ι.app j = 0
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (f.hom.app (op X) ≫ F.obj.map g.op)) { down := 𝟙 X } =
    (ConcreteCategory.hom (f.hom.app (op Y))) { down := 𝟙 Y ≫ g }

Tactic:
← f.hom.naturality

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (((uliftYoneda.{v', v, u} J).obj X).obj.map g.op ≫ f.hom.app (op Y))) { down := 𝟙 X } =
    (ConcreteCategory.hom (f.hom.app (op Y))) { down := 𝟙 Y ≫ g }
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
j : ι
⊢ (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).inj j ≫
      {
        hom :=
          ⋯.extend
            {
              app := fun Y ↦
                ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
              naturality := ⋯ } } =
    s.inj j

Tactic:
ext : 1
    let u (j : ι) : CategoryTheory.yoneda.obj (X j) ⟶ (Sieve.ofArrows _ c.inj).functor :=
      (Sieve.ofArrows _ c.inj).toFunctor (c.inj j) (Sieve.ofArrows_mk _ _ j)
    have (j : ι) : u j ≫ (Sieve.ofArrows _ c.inj).functorInclusion =
      CategoryTheory.yoneda.map (c.inj j) := rfl
    dsimp
    simp only [← this, Category.assoc, Presieve.IsSheafFor.functorInclusion_comp_extend]
    ext Z (g : Z.unop ⟶ X j)
    have h : Sieve.ofArrows X c.inj (g ≫ c.inj j) :=
      Sieve.downward_closed _ (Sieve.ofArrows_mk _ _ j) _
    exact heq s (Sieve.ofArrows.h h) g (by simp)

Goal state after:
Module: Mathlib.Order.Interval.Set.Limit

Goal state before:
pp: J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
⊢ ¬b ⋖ ↑m

Tactic:
simp only [CovBy, not_lt, not_and, not_forall, not_le]

Goal state after:
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
⊢ b < ↑m → ∃ x, ∃ (_ : b < x), x < ↑m
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ Order.pred i = ⟨Order.pred ↑i, ⋯⟩

Tactic:
by
  ext
  simp only [coe_pred_of_not_isMin hi]

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
Z : C
φ φ' : X₂ ⟶ Z
h₀ : f ≫ φ = f ≫ φ'
h : ∀ (i : c.ι), c.cell i ≫ φ = c.cell i ≫ φ'
⊢ φ = φ'

Tactic:
by
  apply c.isPushout.hom_ext h₀
  apply Cofan.IsColimit.hom_ext c.isColimit₂
  simpa [cell_def] using h

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hj : ¬IsMax i
iter : Φ.Iteration i
hi₁✝ : i < Order.succ i
hi₁ : i ≤ i
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨i, ⋯⟩))) i hi₁✝ =
    Φ.toSuccArrow ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨i, ⋯⟩))).obj ⟨i, ⋯⟩)

Tactic:
arrowSucc_extendToSucc,

Goal state after:
case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hj : ¬IsMax i
iter : Φ.Iteration i
hi₁✝ : i < Order.succ i
hi₁ : i ≤ i
⊢ Arrow.mk (Φ.toSucc (iter.F.obj ⟨i, ⋯⟩)) =
    Φ.toSuccArrow ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨i, ⋯⟩))).obj ⟨i, ⋯⟩)