mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
e✝ : ι
f g : A
hg : g ∈ 𝒜 e✝
x : A
hx : x = f * g
a : Away 𝒜 f
e : Away 𝒜 x ≃+* ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range := RingEquiv.ofLeftInverse ⋯
⊢ (Exists.choose ⋯ ↑((Subring.inclusion ⋯) ((awayMapAux 𝒜 ⋯).rangeRestrict a))).val = (awayMapAux 𝒜 ⋯) a

Tactic:
convert_to! (e (e.symm ⟨awayMapAux 𝒜 (f := f) ⟨_, hx⟩ a,
    range_awayMapAux_subset 𝒜 hg hx ⟨_, rfl⟩⟩)).1 = _

Goal state after:
case convert_2
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
e✝ : ι
f g : A
hg : g ∈ 𝒜 e✝
x : A
hx : x = f * g
a : Away 𝒜 f
e : Away 𝒜 x ≃+* ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range := RingEquiv.ofLeftInverse ⋯
⊢ ↑(e (e.symm ⟨(awayMapAux 𝒜 ⋯) a, ⋯⟩)) = (awayMapAux 𝒜 ⋯) a
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec R).Modules
f : modulesSpecToSheaf.obj M ⟶ modulesSpecToSheaf.obj N
U : (Opens ↥(Spec R))ᵒᵖ
⊢ ∀ (m : ↑((Spec R).ringCatSheaf.obj.obj U)) (x : ↑(M.val.1 U)),
    (ModuleCat.Hom.hom (f.hom.app U)).toFun (m • x) =
      (RingHom.id ↑((Spec R).ringCatSheaf.obj.obj U)) m • (ModuleCat.Hom.hom (f.hom.app U)).toFun x

Tactic:
intro t

Goal state after:
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec R).Modules
f : modulesSpecToSheaf.obj M ⟶ modulesSpecToSheaf.obj N
U : (Opens ↥(Spec R))ᵒᵖ
t : ↑((Spec R).ringCatSheaf.obj.obj U)
⊢ ∀ (x : ↑(M.val.1 U)),
    (ModuleCat.Hom.hom (f.hom.app U)).toFun (t • x) =
      (RingHom.id ↑((Spec R).ringCatSheaf.obj.obj U)) t • (ModuleCat.Hom.hom (f.hom.app U)).toFun x
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec R).Modules
f : modulesSpecToSheaf.obj M ⟶ modulesSpecToSheaf.obj N
U : (Opens ↥(Spec R))ᵒᵖ
t : ↑((Spec R).ringCatSheaf.obj.obj U)
m : ↑(M.val.1 U)
x : ↥(Spec R)
hxU : x ∈ unop U
r : ↑R
hxr : x ∈ ↑(basicOpen r)
hrU : basicOpen r ≤ unop U
⊢ (ConcreteCategory.hom (N.val.map (homOfLE hrU).op)) ((ConcreteCategory.hom (f.hom.app (op (unop U)))) (t • m)) =
    (ConcreteCategory.hom ((Spec R).ringCatSheaf.obj.map (homOfLE hrU).op)) t •
      (ConcreteCategory.hom (N.val.map (homOfLE hrU).op)) ((ConcreteCategory.hom (f.hom.app (op (unop U)))) m)

Tactic:
have (x : _) :
        f.1.app _ (M.1.map (homOfLE hrU).op _) = N.1.map (homOfLE hrU).op (f.1.app _ x) :=
      congr($(f.1.naturality (homOfLE hrU).op).hom x)

Goal state after:
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec R).Modules
f : modulesSpecToSheaf.obj M ⟶ modulesSpecToSheaf.obj N
U : (Opens ↥(Spec R))ᵒᵖ
t : ↑((Spec R).ringCatSheaf.obj.obj U)
m : ↑(M.val.1 U)
x : ↥(Spec R)
hxU : x ∈ unop U
r : ↑R
hxr : x ∈ ↑(basicOpen r)
hrU : basicOpen r ≤ unop U
this :
  ∀ (x : ↑((modulesSpecToSheaf.obj M).obj.obj (op (unop U)))),
    (ConcreteCategory.hom (f.hom.app (op (basicOpen r)))) ((ConcreteCategory.hom (M.val.map (homOfLE hrU).op)) x) =
      (ConcreteCategory.hom (N.val.map (homOfLE hrU).op)) ((ConcreteCategory.hom (f.hom.app (op (unop U)))) x)
⊢ (ConcreteCategory.hom (N.val.map (homOfLE hrU).op)) ((ConcreteCategory.hom (f.hom.app (op (unop U)))) (t • m)) =
    (ConcreteCategory.hom ((Spec R).ringCatSheaf.obj.map (homOfLE hrU).op)) t •
      (ConcreteCategory.hom (N.val.map (homOfLE hrU).op)) ((ConcreteCategory.hom (f.hom.app (op (unop U)))) m)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
U : Opens (ProjectiveSpectrum 𝒜)
V : Opens (ProjectiveSpectrum ℬ)
hUV : V.carrier ⊆ ⇑(ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier
⊢ ⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑1, ⋯⟩ = 1

Tactic:
by ext; simp [comapStructureSheafFun]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
U : Opens (ProjectiveSpectrum 𝒜)
V : Opens (ProjectiveSpectrum ℬ)
hUV : V.carrier ⊆ ⇑(ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier
x y : ↑((structureSheaf 𝒜).obj.obj (Opposite.op U))
⊢ ⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑(x * y), ⋯⟩ =
    ⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑x, ⋯⟩ *
      ⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑y, ⋯⟩

Tactic:
by ext; simp [comapStructureSheafFun]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
U : Opens (ProjectiveSpectrum 𝒜)
V : Opens (ProjectiveSpectrum ℬ)
hUV : V.carrier ⊆ ⇑(ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier
⊢ ⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑0, ⋯⟩ = 0

Tactic:
by ext; simp [comapStructureSheafFun]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst✝¹¹ : CommRing A
inst✝¹⁰ : SetLike σ A
inst✝⁹ : AddSubgroupClass σ A
inst✝⁸ : CommRing B
inst✝⁷ : SetLike τ B
inst✝⁶ : AddSubgroupClass τ B
inst✝⁵ : CommRing C
inst✝⁴ : SetLike ψ C
inst✝³ : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
hg : 𝒞₊ ≤ HomogeneousIdeal.map g (ℬ₊)
U : Opens (ProjectiveSpectrum 𝒜)
V : Opens (ProjectiveSpectrum ℬ)
hUV : V.carrier ⊆ ⇑(ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier
x y : ↑((structureSheaf 𝒜).obj.obj (Opposite.op U))
⊢ ⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑(x + y), ⋯⟩ =
    ⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑x, ⋯⟩ +
      ⟨comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV ↑y, ⋯⟩

Tactic:
by ext; simp [comapStructureSheafFun]

Goal state after:
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
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (Scheme.ΓSpecIso (CommRingCat.of (A⁰_ f))).inv ≫
      (Spec A⁰_ f).presheaf.germ ⊤ ((ConcreteCategory.hom (toSpec 𝒜 f).base) x) ⋯ ≫
        LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x =
    awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x

Tactic:
erw [LocallyRingedSpace.stalkMap_germ (toSpec 𝒜 f) ⊤ x (by simp)]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (Scheme.ΓSpecIso (CommRingCat.of (A⁰_ f))).inv ≫
      (toSpec 𝒜 f).c.app (op ⊤) ≫ (Proj.restrict ⋯).presheaf.germ ((Opens.map (toSpec 𝒜 f).base).obj ⊤) x ⋯ =
    awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case h₁
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f :=
  { R := commSq.R, commRing := commSq.commRing, domain := ⋯, valuationRing := ⋯, K := commSq.K, field := commSq.field,
    algebra := commSq.algebra, isFractionRing := ⋯, i₁ := commSq.i₁ ≫ X'_to_X, i₂ := commSq.i₂ ≫ Y'_to_Y, commSq := ⋯ }
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
⊢ Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ commSq.i₂ = commSq.i₁ ≫ f'

Tactic:
rw [commSq.commSq.w]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Basic

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁶ : Category.{v', u'} A
inst✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
P Q : Cᵒᵖ ⥤ A
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝¹ : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst✝ : Presheaf.IsLocallyInjective J f
⊢ ∀ (X : C) (x : Φ.fiber.obj X) (p₁ p₂ : ToType (P.obj (op X))),
    (ConcreteCategory.hom (f.app (op X))) p₁ = (ConcreteCategory.hom (f.app (op X))) p₂ →
      (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₁ = (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₂

Tactic:
intro X x p₁ p₂ h

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁶ : Category.{v', u'} A
inst✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
P Q : Cᵒᵖ ⥤ A
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝¹ : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst✝ : Presheaf.IsLocallyInjective J f
X : C
x : Φ.fiber.obj X
p₁ p₂ : ToType (P.obj (op X))
h : (ConcreteCategory.hom (f.app (op X))) p₁ = (ConcreteCategory.hom (f.app (op X))) p₂
⊢ (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₁ = (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₂
Module: Mathlib.CategoryTheory.Sites.ConstantSheaf

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
T : C
hT : IsTerminal T
F : Cᵒᵖ ⥤ D
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((((evaluation Cᵒᵖ D).obj (Opposite.op T) ⋙ const Cᵒᵖ).obj F).map x✝ ≫
      match x✝¹ with
      | Opposite.op X => F.map (hT.from X).op) =
    (match x✝² with
      | Opposite.op X => F.map (hT.from X).op) ≫
      ((𝟭 (Cᵒᵖ ⥤ D)).obj F).map x✝

Tactic:
simp only [Functor.comp_obj, Functor.const_obj_obj, Functor.id_obj, Functor.const_obj_map,
          Category.id_comp, ← Functor.map_comp]
        congr
        simp

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

Goal state before:
pp: case refine_1
S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ (𝒰.restrictIndex (Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom 𝒰.forgetQc.toPreZeroHypercover).s₀)).presieve₀ ∈
    qcPrecoverage.coverings S

Tactic:
rw [Scheme.presieve₀_mem_qcPrecoverage_iff]

Goal state after:
case refine_1
S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ QuasiCompactCover
    (𝒰.restrictIndex (Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom 𝒰.forgetQc.toPreZeroHypercover).s₀))
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: case refine_1
S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ (𝒰.restrictIndex (Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom 𝒰.forgetQc.toPreZeroHypercover).s₀)).presieve₀ ∈
    qcPrecoverage.coverings S

pp: case refine_2
S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ (𝒰.restrictIndex (Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom 𝒰.forgetQc.toPreZeroHypercover).s₀)).presieve₀ ∈
    (precoverage P).coverings S

Tactic:
· rw [Scheme.presieve₀_mem_qcPrecoverage_iff]
      exact .of_hom (𝒱 := QuasiCompactCover.ulift 𝒰.1) ⟨Sum.inr, fun i ↦ 𝟙 _, by cat_disch⟩

Goal state after:
case refine_2
S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ (𝒰.restrictIndex (Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom 𝒰.forgetQc.toPreZeroHypercover).s₀)).presieve₀ ∈
    (precoverage P).coverings S
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : Y ⟶ X
Hf : EffectiveEpiStruct f
D : Type (max u v) := ObjectProperty.FullSubcategory fun T ↦ (Sieve.generateSingleton f).arrows T.hom
F : D ⥤ C := (Sieve.generateSingleton f).arrows.diagram
⊢ ∀ (s : Cocone (Sieve.generateSingleton f).arrows.diagram) (j : (Sieve.generateSingleton f).arrows.category),
    (Sieve.generateSingleton f).arrows.cocone.ι.app j ≫ Hf.desc (s.ι.app { obj := Over.mk f, property := ⋯ }) ⋯ =
      s.ι.app j

Tactic:
rintro S ⟨T, g, hT⟩
      dsimp
      generalize_proofs h₁ h₂ h₃
      simp only [← hT, Category.assoc, Hf.fac _ h₂]
      let y : D := ⟨Over.mk f, 𝟙 _, by simp⟩
      let x : D := ⟨Over.mk T.hom, g, hT⟩
      let g' : x ⟶ y := ObjectProperty.homMk (Over.homMk g)
      change F.map g' ≫ _ = _
      rw [S.w]
      rfl

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 : C(↥(Spec S), T)
h :
  ∀ {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:
refine ⟨?_, ?_, ?_⟩

Goal state after:
case refine_2.refine_1
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)
h :
  ∀ {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
⊢ (fun X ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))

case refine_2.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)
h :
  ∀ {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
⊢ (fun y ↦ (ConcreteCategory.hom ((continuousMapPresheaf T).map (Spec.map f).op)) y = x) ?refine_2.refine_1

case refine_2.refine_3
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)
h :
  ∀ {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 : (fun X ↦ X) ((continuousMapPresheaf T).obj (Opposite.op (Spec R)))),
    (fun y ↦ (ConcreteCategory.hom ((continuousMapPresheaf T).map (Spec.map f).op)) y = x) y → y = ?refine_2.refine_1
Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites

Goal state before:
pp: case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝ : P.IsStableUnderComposition
K : Precoverage C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover ((Over.forget P ⊤ S).obj X)
𝒱 : PreZeroHypercover X := ⋯
⊢ Presieve.map (Over.forget P ⊤ S) 𝒱.presieve₀ = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
Presieve.map_ofArrows

Goal state after:
case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝ : P.IsStableUnderComposition
K : Precoverage C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover ((Over.forget P ⊤ S).obj X)
𝒱 : PreZeroHypercover X :=
  { I₀ := 𝒰.I₀, X := fun i ↦ Over.mk ⊤ (𝒰.X i).hom ⋯, f := fun i ↦ Over.homMk (Over.Hom.left (𝒰.f i)) ⋯ trivial }
⊢ (Presieve.ofArrows (fun i ↦ (Over.forget P ⊤ S).obj (𝒱.X i)) fun i ↦ (Over.forget P ⊤ S).map (𝒱.f i)) =
    Presieve.ofArrows 𝒰.X 𝒰.f
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
X₁ X₂ : J ⥤ C
φ : X₁ ⟶ X₂
inst✝ : ∀ (j : J), Epi (φ.app j)
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
Z : C
g₁ g₂ : c₂.pt ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
⊢ c₂.ι.app j ≫ g₁ = c₂.ι.app j ≫ g₂

Tactic:
← cancel_epi (φ.app j),

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
X₁ X₂ : J ⥤ C
φ : X₁ ⟶ X₂
inst✝ : ∀ (j : J), Epi (φ.app j)
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
Z : C
g₁ g₂ : c₂.pt ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
⊢ φ.app j ≫ c₂.ι.app j ≫ g₁ = φ.app j ≫ c₂.ι.app j ≫ g₂
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j : J
h : IsMin ⊥
iter₁ iter₂ : Φ.Iteration ⊥
k₁ : J
h₁₂ : k₁ ≤ ⊥
h₂ : ⊥ ≤ ⊥
⊢ k₁ = ⊥

Tactic:
simpa using h₁₂

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hi : Order.IsSuccLimit i
⊢ IsColimit ((Set.principalSegIio i).cocone (Φ.iterationFunctor J))

Tactic:
by
    let e : (Set.principalSegIio i).monotone.functor ⋙
      (Φ.iterationFunctor J) ≅ restrictionLT (Φ.iter i).F (by simp) :=
      NatIso.ofComponents (fun _ ↦ eqToIso (Φ.iterationFunctor_obj _ _ _)) (by
        rintro ⟨k₁, h₁⟩ ⟨k₂, h₂⟩ f
        apply Arrow.mk_injective
        simpa using! Φ.arrowMk_iterationFunctor_map k₁ k₂ (leOfHom f) (Φ.iter i) h₂.le)
    refine (IsColimit.precomposeInvEquiv e _).1 ?_
    refine IsColimit.ofIsoColimit ((Φ.iter i).isColimit i hi (by simp)) ?_
    refine Cocone.ext (eqToIso (Φ.iterationFunctor_obj i (Φ.iter i) (by simp)).symm) ?_
    rintro ⟨k, hk⟩
    apply Arrow.mk_injective
    simp [Φ.arrowMk_iterationFunctor_map k i hk.le (Φ.iter i) (by simp), e]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ W f ↔ ofHoms (fun i ↦ (↑((equivShrink ↑W.toSet).symm i)).hom) f

Tactic:
rw [ofHoms_iff]

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ W f ↔ ∃ i, Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case isSuccLimit
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
⊢ e₁.val = e₂.val

Tactic:
have h₁ := e₁.map_limit i hi (by rfl)

Goal state after:
case isSuccLimit
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
h₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val,
        ⋯⟩
⊢ e₁.val = e₂.val
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case inr
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
i : J
e : d.Extension val₀ i
hj : ¬IsMax i
hi : i < Order.succ i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ i hj e.val) =
    d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ i hj e.val))

Tactic:
simp only [homOfLE_refl, op_id, map_id, id_apply, homOfLE_leOfHom, d.map_succ]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case inl
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op))
      (d.lift j hj
        ⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ =>
          (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
            (d.lift j hj
              ⟨fun x ↦
                match x with
                | op ⟨i, hi⟩ => (e i hi).val,
                ⋯⟩),
        ⋯⟩

Tactic:
have := (e i hij').map_limit i hi (by rfl)

Goal state after:
case inl
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
this :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e i hij').val =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e i hij').val,
        ⋯⟩
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op))
      (d.lift j hj
        ⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ =>
          (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
            (d.lift j hj
              ⟨fun x ↦
                match x with
                | op ⟨i, hi⟩ => (e i hi).val,
                ⋯⟩),
        ⋯⟩
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : A ≠ ⊤
⊢ A < largerSubobject hG A

Tactic:
by
  dsimp only [largerSubobject]
  rw [dif_neg hA]
  exact (exists_larger_subobject hG A hA).choose_spec.choose

Goal state after: