mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx :
  (TopCat.Hom.hom
        (Spec.map
            (CommRingCat.ofHom
              ((IsLocalization.map (Localization.Away (f i.snd.fst)) f ⋯).comp
                (algebraMap (Away 𝒜 i.snd.fst) (Localization.Away i.snd.fst))))).base)
      ((TopCat.Hom.hom (basicOpenIsoSpecAway (f i.snd.fst)).hom.base)
        ((↑(PrimeSpectrum.basicOpen (f i.snd.fst))).restrictPreimage (⇑X.toSpecΓ)
          ((TopCat.Hom.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE ⋯))) x))) ∈
    ↑((TopologicalSpace.Opens.map (awayι 𝒜 i.snd.fst ⋯ ⋯).base).obj (basicOpen 𝒜 r))
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ X.basicOpen (f r)

Tactic:
Proj.awayι_preimage_basicOpen (𝒜 := 𝒜) i.2.2.2 i.2.2.1 hr hn,

Goal state after:
case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx :
  (TopCat.Hom.hom
        (Spec.map
            (CommRingCat.ofHom
              ((IsLocalization.map (Localization.Away (f i.snd.fst)) f ⋯).comp
                (algebraMap (Away 𝒜 i.snd.fst) (Localization.Away i.snd.fst))))).base)
      ((TopCat.Hom.hom (basicOpenIsoSpecAway (f i.snd.fst)).hom.base)
        ((↑(PrimeSpectrum.basicOpen (f i.snd.fst))).restrictPreimage (⇑X.toSpecΓ)
          ((TopCat.Hom.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE ⋯))) x))) ∈
    ↑(PrimeSpectrum.basicOpen (Away.isLocalizationElem ⋯ hr))
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ X.basicOpen (f r)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case pos.e_a.e_x
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
g : ℕ → A⁰_ f :=
  fun j ↦
    (m + m).choose j •
      if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
        else
          HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ }
j : ℕ
hj : j ∈ range (m + m + 1)
h2 : ¬m + m < j
h1 : j ≤ m
⊢ ↑(((decompose 𝒜) a) i) ^ j * ↑(((decompose 𝒜) b) i) ^ (m + m - j) =
    ↑(((decompose 𝒜) a) i) ^ j * ↑(((decompose 𝒜) b) i) ^ (m + (m - j))

Tactic:
Nat.add_sub_assoc h1

Goal state after:
case pos.e_a.e_x
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
g : ℕ → A⁰_ f :=
  fun j ↦
    (m + m).choose j •
      if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
        else
          HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ }
j : ℕ
hj : j ∈ range (m + m + 1)
h2 : ¬m + m < j
h1 : j ≤ m
⊢ ↑(((decompose 𝒜) a) i) ^ j * ↑(((decompose 𝒜) b) i) ^ (m + (m - j)) =
    ↑(((decompose 𝒜) a) i) ^ j * ↑(((decompose 𝒜) b) i) ^ (m + (m - j))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case e_y
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
g : ℕ → A⁰_ f :=
  fun j ↦
    (m + m).choose j •
      if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
        else
          HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ }
j : ℕ
hj : j ∈ range (m + m + 1)
h2 : ¬m + m < j
h1 : j ≤ m
⊢ ⟨f ^ (i + i), ⋯⟩ = ⟨f ^ i, ⋯⟩ * ⟨f ^ i, ⋯⟩

Tactic:
simp_rw [pow_add]; rfl

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

Goal state before:
pp: case e_y
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
g : ℕ → A⁰_ f :=
  fun j ↦
    (m + m).choose j •
      if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
        else
          HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ }
j : ℕ
hj : j ∈ range (m + m + 1)
h2 : ¬m + m < j
h1 : ¬j ≤ m
⊢ ⟨f ^ (i + i), ⋯⟩ = ⟨f ^ i, ⋯⟩ * ⟨f ^ i, ⋯⟩

Tactic:
simp_rw [pow_add]; rfl

Goal state after:
Module: Mathlib.RingTheory.LocalRing.LocalSubring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
K : Type u_3
inst✝² : Field K
inst✝¹ : IsLocalRing R
inst✝ : Nontrivial S
f : R →+* S
x : S
⊢ x ∈ ↑f.range ↔ x ∈ ↑(map f { toSubring := ⊤, isLocalRing := ⋯ }).toSubring

Tactic:
exact congr(x ∈ $(Set.image_univ.symm))

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

Goal state before:
pp: R : CommRingCat
M : ModuleCat ↑R
s : Set ↑M
hs : Submodule.span (↑R) s = ⊤
t : Set (↑s →₀ ↑R)
ht : Submodule.span (↑R) t = (Finsupp.linearCombination (↑R) Subtype.val).ker
H₁ :
  Function.Exact ⇑(ConcreteCategory.hom (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)))
    ⇑(ConcreteCategory.hom (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)))
h₁ : IsColimit (CokernelCofork.ofπ (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)) ⋯) :=
  ModuleCat.isColimitCokernelCofork (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val))
    (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)) H₁ ⋯
⊢ IsColimit
    (CokernelCofork.ofπ
      ((tildeFinsupp ↑s).inv ≫ tilde.map (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val))) ⋯)

Tactic:
refine IsCokernel.ofIso _ (CokernelCofork.mapIsColimit _ h₁ (tilde.functor R)) _ (tildeFinsupp t)
    (tildeFinsupp s) (.refl _) (by simp) (by simp)

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

Goal state before:
pp: X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
I : Type u
W : I → TopologicalSpace.Opens ↥X
cov : (Opens.grothendieckTopology ↥X).CoversTop W
pres : (i : I) → (SheafOfModules.over M (W i)).Presentation
κ : I → Set (TopologicalSpace.Opens ↥X)
hsub : ∀ (i : I), κ i ⊆ X.affineOpens
heq : ∀ (i : I), W i = sSup (κ i)
⊢ ∃ ι U x, IsOpenCover U ∧ ∀ (i : ι), IsAffineOpen (U i)

Tactic:
refine ⟨Σ (i : I), κ i, fun j ↦ j.2, fun i ↦ ?_, ?_, ?_⟩

Goal state after:
case refine_1
X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
I : Type u
W : I → TopologicalSpace.Opens ↥X
cov : (Opens.grothendieckTopology ↥X).CoversTop W
pres : (i : I) → (SheafOfModules.over M (W i)).Presentation
κ : I → Set (TopologicalSpace.Opens ↥X)
hsub : ∀ (i : I), κ i ⊆ X.affineOpens
heq : ∀ (i : I), W i = sSup (κ i)
i : (i : I) × ↑(κ i)
⊢ SheafOfModules.Presentation (M.restrict (Opens.ι ((fun j ↦ ↑j.snd) i)))

case refine_2
X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
I : Type u
W : I → TopologicalSpace.Opens ↥X
cov : (Opens.grothendieckTopology ↥X).CoversTop W
pres : (i : I) → (SheafOfModules.over M (W i)).Presentation
κ : I → Set (TopologicalSpace.Opens ↥X)
hsub : ∀ (i : I), κ i ⊆ X.affineOpens
heq : ∀ (i : I), W i = sSup (κ i)
⊢ IsOpenCover fun j ↦ ↑j.snd

case refine_3
X : Scheme
M : X.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
I : Type u
W : I → TopologicalSpace.Opens ↥X
cov : (Opens.grothendieckTopology ↥X).CoversTop W
pres : (i : I) → (SheafOfModules.over M (W i)).Presentation
κ : I → Set (TopologicalSpace.Opens ↥X)
hsub : ∀ (i : I), κ i ⊆ X.affineOpens
heq : ∀ (i : I), W i = sSup (κ i)
⊢ ∀ (i : (i : I) × ↑(κ i)), IsAffineOpen ((fun j ↦ ↑j.snd) i)
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
⊢ ⇑A.subtype '' ↑I ⊆ Subtype.val '' ↑(map (Subring.inclusion ⋯) (maximalIdeal ↥(LocalSubring.ofPrime A M).toSubring))

Tactic:
rw [← IsLocalization.AtPrime.map_eq_maximalIdeal M, map_map]

Goal state after:
K : Type u_3
inst✝ : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
⊢ ⇑A.subtype '' ↑I ⊆
    Subtype.val '' ↑(map ((Subring.inclusion ⋯).comp (algebraMap ↥A ↥(LocalSubring.ofPrime A M).toSubring)) M)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
i : ι
⊢ basicOpen (g i) ≤ V

Tactic:
rw [hg]; exact le_iSup_of_le _ le_rfl

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

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
i : ι
⊢ basicOpen (g i) ≤ V

Tactic:
rw [hg]; exact le_iSup_of_le _ le_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
A : Type u'
inst✝ : Category.{v', u'} A
X : C
data : F.PreOneHypercoverDenseData X
i₁ i₂ : data.I₀
W₀ : C₀
p₁ : W₀ ⟶ data.X i₁
p₂ : W₀ ⟶ data.X i₂
Z Z' : C₀
g : Z ⟶ W₀
j : data.I₁ i₁ i₂
h : Z ⟶ data.Y j
fac₁ : g ≫ p₁ = h ≫ data.p₁ j
fac₂ : g ≫ p₂ = h ≫ data.p₂ j
φ : Z' ⟶ Z
⊢ ∃ j h, (φ ≫ g) ≫ p₁ = h ≫ data.p₁ j ∧ (φ ≫ g) ≫ p₂ = h ≫ data.p₂ j

Tactic:
exact ⟨j, φ ≫ h, by simpa using φ ≫= fac₁, by simpa using φ ≫= fac₂⟩

Goal state after:
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⟩

Goal state after:
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
T : Over X
g : T.left ⟶ Y
hT : g ≫ f = T.hom
⊢ (Sieve.generateSingleton f).arrows.cocone.ι.app { obj := T, property := ⋯ } ≫
      Hf.desc (S.ι.app { obj := Over.mk f, property := ⋯ }) ⋯ =
    S.ι.app { obj := T, property := ⋯ }
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
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i : (data X).I₀
⊢ presheafMap data G₀ (𝟙 X) ≫ presheafObjπ data G₀ X i = 𝟙 (presheafObj data G₀ X) ≫ presheafObjπ data G₀ X i

Tactic:
rw [presheafMap_π, comp_id, id_comp,
    restriction_eq_of_fac data G₀ ((data X).f i) (𝟙 _) (by simp),
    IsDenseSubsite.mapPreimage_id, comp_id]

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

Goal state before:
pp: ⊢ etalePrecoverage ≤ proetalePrecoverage

Tactic:
rw [proetalePrecoverage, propQCPrecoverage, etalePrecoverage, le_inf_iff]
  refine ⟨precoverage_le_qcPrecoverage_of_isOpenMap fun X Y f hf ↦ f.isOpenMap, ?_⟩
  apply precoverage_mono
  intro X Y f hf
  infer_instance

Goal state after:
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✝ : colim.PreservesMonomorphisms
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : (monomorphisms C).functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
this✝ : ∀ (j : J), Mono (f.app j)
this : Mono f
⊢ monomorphisms C φ

Tactic:
apply colim.map_mono' f hc₁ hc₂ φ (by simp [hφ])

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
⊢ (if h₁ : Order.succ j ≤ j then (objIso F X ⟨j, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ (objIso F X ⟨Order.succ j, h₁⟩).inv
    else
      if h₂ : j ≤ j then
        (objIso F X ⟨j, h₂⟩).hom ≫ F.map (𝟙 ⟨j, h₂⟩) ≫ τ ≫ (objSuccIso hj F X).inv ≫ 𝟙 (obj F X ⟨Order.succ j, ⋯⟩)
      else eqToHom ⋯) =
    (objIso F X ⟨j, ⋯⟩).hom ≫ τ ≫ (objSuccIso hj F X).inv

Tactic:
rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj),
    dif_pos (by rfl), Functor.map_id, comp_id, id_comp]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : LinearOrder J
inst✝¹ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝ : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ sqFunctor c p f g).sections
⊢ ⊥ ≠ j

Tactic:
rintro rfl
      exact Order.not_isSuccLimit_bot hj

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
sq : CommSq f (c.ι.app ⊥) p g
s : ↑(sqFunctor c p f g).sections
hs : (↑s (Opposite.op ⊥)).f' = f
t : Cocone F := { pt := X, ι := { app := fun j ↦ (↑s (Opposite.op j)).f', naturality := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
hl : ∀ (j : J), c.ι.app j ≫ l = (↑s (Opposite.op j)).f'
⊢ c.ι.app ⊥ ≫ l = f

Tactic:
hl,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
sq : CommSq f (c.ι.app ⊥) p g
s : ↑(sqFunctor c p f g).sections
hs : (↑s (Opposite.op ⊥)).f' = f
t : Cocone F := { pt := X, ι := { app := fun j ↦ (↑s (Opposite.op j)).f', naturality := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
hl : ∀ (j : J), c.ι.app j ≫ l = (↑s (Opposite.op j)).f'
⊢ (↑s (Opposite.op ⊥)).f' = f
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case inl
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ padicValRat p (0 ^ k) = ↑k * padicValRat p 0

Tactic:
cases k <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts).retracts ≤
    monomorphisms C

Tactic:
trans (transfiniteCompositions.{w} (coproducts.{w} (monomorphisms C)).pushouts).retracts

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (generatingMonomorphisms G)).pushouts).retracts ≤
    (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (monomorphisms C)).pushouts).retracts

C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
⊢ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} (monomorphisms C)).pushouts).retracts ≤ monomorphisms C
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
⊢ padicValRat p q ≤ padicValRat p (q + r)

Tactic:
exact le_padicValRat_add_of_le hqr h

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case succ
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n < p → padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
⊢ padicValNat p (p * m + (n + 1))! = padicValNat p (p * m)!

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ‖x‖ < 1 ↔ ↑p ∣ x

Tactic:
have := norm_le_pow_iff_mem_span_pow x 1

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ x ∈ Ideal.span {↑p ^ 1}
⊢ ‖x‖ < 1 ↔ ↑p ∣ x
Module: Mathlib.CategoryTheory.Types.Epimorphisms

Goal state before:
pp: x✝³ x✝² x✝¹ x✝ : Type u
b : x✝³ ⟶ x✝
r : x✝² ⟶ x✝
t : x✝¹ ⟶ x✝²
l : x✝¹ ⟶ x✝³
sq : IsPullback t l r b
hr : Function.Surjective ⇑(ConcreteCategory.hom r)
x : x✝³
y : x✝²
hy : (ConcreteCategory.hom r) y = (ConcreteCategory.hom b) x
z : x✝¹
left✝ : (ConcreteCategory.hom t) z = y
hz : (ConcreteCategory.hom l) z = x
⊢ ∃ a, (ConcreteCategory.hom l) a = x

Tactic:
exact ⟨z, hz⟩

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

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✝¹ : HasProducts A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
⊢ J.W.IsInvertedBy Φ.presheafFiber

Tactic:
by
  intro P₁ P₂ f hf
  rw [isIso_iff_coyoneda_map_bijective]
  intro M
  rw [← Function.Bijective.of_comp_iff' Φ.skyscraperPresheafHomEquiv.bijective]
  convert! (hf _ (Φ.isSheaf_skyscraperPresheaf M)).comp Φ.skyscraperPresheafHomEquiv.bijective
  ext g : 1
  simp [skyscraperPresheafHomEquiv_naturality_left]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
⊢ Presheaf.IsLocallySurjective J f

Tactic:
suffices Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm (𝟙 U)) ∈ J U from ⟨by
    intro V g
    obtain ⟨g, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective g
    replace this := J.pullback_stable g this
    rw [Presheaf.pullback_imageSieve] at this
    have hg := shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm g.op (𝟙 _)
    simp only [Quiver.Hom.unop_op, Category.comp_id] at hg
    simpa [← hg]⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
⊢ Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm (𝟙 U)) ∈ J U
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
c : C
i : c ⟶ b
h : c ⟶ a
hi : F.map i ≫ f' = F.map h ≫ g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ F.map (hf'.lift' i h hi ≫ hf'.fst' g) = F.map i

Tactic:
simp [lift']

Goal state after: