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 𝒜
B : Type u_4
τ : Type u_5
inst✝⁷ : CommRing B
inst✝⁶ : SetLike τ B
inst✝⁵ : AddSubgroupClass τ B
ℬ : ι → τ
inst✝⁴ : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst✝³ : CommRing C
inst✝² : SetLike ψ C
inst✝¹ : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst✝ : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
⊢ Quotient.map' (fun x ↦ { deg := x.deg, num := ⟨g ↑x.num, ⋯⟩, den := ⟨g ↑x.den, ⋯⟩, den_mem := ⋯ }) ⋯
      (Quotient.mk'' x + Quotient.mk'' y) =
    Quotient.map' (fun x ↦ { deg := x.deg, num := ⟨g ↑x.num, ⋯⟩, den := ⟨g ↑x.den, ⋯⟩, den_mem := ⋯ }) ⋯
        (Quotient.mk'' x) +
      Quotient.map' (fun x ↦ { deg := x.deg, num := ⟨g ↑x.num, ⋯⟩, den := ⟨g ↑x.den, ⋯⟩, den_mem := ⋯ }) ⋯
        (Quotient.mk'' y)

Tactic:
simp only [← mk_add, Quotient.map'_mk'', num_add, map_add, map_mul, den_add]

Goal state after:
ι : 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 𝒜
B : Type u_4
τ : Type u_5
inst✝⁷ : CommRing B
inst✝⁶ : SetLike τ B
inst✝⁵ : AddSubgroupClass τ B
ℬ : ι → τ
inst✝⁴ : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst✝³ : CommRing C
inst✝² : SetLike ψ C
inst✝¹ : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst✝ : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
⊢ Quotient.mk''
      { deg := (x + y).deg, num := ⟨g ↑x.den * g ↑y.num + g ↑y.den * g ↑x.num, ⋯⟩, den := ⟨g ↑x.den * g ↑y.den, ⋯⟩,
        den_mem := ⋯ } =
    mk
      ({ deg := x.deg, num := ⟨g ↑x.num, ⋯⟩, den := ⟨g ↑x.den, ⋯⟩, den_mem := ⋯ } +
        { deg := y.deg, num := ⟨g ↑y.num, ⋯⟩, den := ⟨g ↑y.den, ⋯⟩, den_mem := ⋯ })
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 𝒜
P : Submonoid A
⊢ map (GradedRingHom.id 𝒜) ⋯ = RingHom.id (HomogeneousLocalization 𝒜 P)

Tactic:
by
  ext x
  obtain ⟨c, rfl⟩ := x.mk_surjective
  simp [map_mk]

Goal state after:
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 𝒜
B : Type u_4
τ : Type u_5
inst✝⁷ : CommRing B
inst✝⁶ : SetLike τ B
inst✝⁵ : AddSubgroupClass τ B
ℬ : ι → τ
inst✝⁴ : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst✝³ : CommRing C
inst✝² : SetLike ψ C
inst✝¹ : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
P : Submonoid A
Q : Submonoid B
R : Submonoid C
hpq : P ≤ Submonoid.comap f Q
hqr : Q ≤ Submonoid.comap g R
⊢ map (g.comp f) ⋯ = (map g hqr).comp (map f hpq)

Tactic:
by
  ext x
  obtain ⟨c, rfl⟩ := x.mk_surjective
  simp [map_mk]

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 : 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
⊢ ((pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg ⋯))) ≫
      awayι 𝒜 g g_deg hm' =
    Limits.pullback.snd (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ≫ awayι 𝒜 g g_deg hm'

Tactic:
← Limits.pullback.condition,

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : 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
⊢ ((pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg ⋯))) ≫
      awayι 𝒜 g g_deg hm' =
    Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ≫ awayι 𝒜 f f_deg hm
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 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
⊢ Set.range ⇑(Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg ⋯))) =
    ↑(PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg))

Tactic:
· let := (awayMap (f := f) 𝒜 g_deg rfl).toAlgebra
    let := HomogeneousLocalization.Away.isLocalization_mul f_deg g_deg rfl hm.ne'
    exact PrimeSpectrum.localization_away_comap_range _ _

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 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
H : f t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
H' : f t' = x'
h0d' : 0 < d'
hd' : t' ∈ 𝒜 d'
s : A
hts : t * s = t'
n : ℕ
hn : d + n = d'
hs : s ∈ 𝒜 n
hx'x : PrimeSpectrum.basicOpen x' ≤ PrimeSpectrum.basicOpen x
⊢ X.basicOpen x' ≤ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen x'

Tactic:
simp [X.toSpecΓ_preimage_basicOpen]

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

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
M : Y.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
⊢ SheafOfModules.IsQuasicoherent ((restrictFunctor f).obj M)

Tactic:
let α : X.presheaf ⟶ f.opensFunctor.op ⋙ Y.presheaf := { app U := (f.appIso U.unop).inv }

Goal state after:
R : CommRingCat
M✝ : ModuleCat ↑R
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
M : Y.Modules
inst✝ : SheafOfModules.IsQuasicoherent M
α : X.presheaf ⟶ (Hom.opensFunctor f).op ⋙ Y.presheaf := { app := fun U ↦ (Hom.appIso f (unop U)).inv, naturality := ⋯ }
⊢ SheafOfModules.IsQuasicoherent ((restrictFunctor f).obj M)
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 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
hs' : ∀ i ∈ s, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n
dx : ↥s → ℕ
hdx : ∀ (x : ↥s), dx x ≠ 0
hxd : ∀ (x : ↥s), ↑x ∈ 𝒜 (dx x)
hd : d = 0
f' : Away 𝒜 f := ⋯
a : ℕ
hai : ∑ i, 0 i • dx i = a • d
hai' : ∀ (i : ↥s), 0 i ≤ d
⊢ val (Away.mk 𝒜 hf a 1 ⋯) = val (f' ^ a)

Tactic:
simp [f', Localization.mk_pow]

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

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
⊢ pullback ((affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜) ((affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜) ≅
    Spec (CommRingCat.of (Away 𝒜 ↑i.snd ⊗[↥(𝒜 0)] Away 𝒜 ↑j.snd))

Tactic:
refine pullback.congrHom ?_ ?_ ≪≫ pullbackSpecIso (𝒜 0) (Away 𝒜 (i.2 : A)) (Away 𝒜 (j.2 : A))

Goal state after:
case refine_1
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
⊢ (affineOpenCover 𝒜).f i ≫ toSpecZero 𝒜 = Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑i.snd)))

case refine_2
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
i j : (affineOpenCover 𝒜).openCover.I₀
⊢ (affineOpenCover 𝒜).f j ≫ toSpecZero 𝒜 = Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 ↑j.snd)))
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
Y X : Q.Over ⊤ S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
⊢ Presieve.pullbackArrows f (𝒰.toPresieveOverProp p) ∈
    {R | ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)), R = 𝒰.toPresieveOverProp h}

Tactic:
refine ⟨𝒰.pullbackCoverOverProp' S f.left (Q := Q) Y.prop X.prop p, inferInstance, ?_, ?_⟩

Goal state after:
case refine_1
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
Y X : Q.Over ⊤ S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
⊢ ∀ (j : (Cover.pullbackCoverOverProp' S 𝒰 f.left ⋯ ⋯ p).I₀),
    Q ((Cover.pullbackCoverOverProp' S 𝒰 f.left ⋯ ⋯ p).X j ↘ S)

case refine_2
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
Y X : Q.Over ⊤ S
f : X ⟶ Y
𝒰 : Cover (precoverage P) Y.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
⊢ Presieve.pullbackArrows f (𝒰.toPresieveOverProp p) =
    (Cover.pullbackCoverOverProp' S 𝒰 f.left ⋯ ⋯ p).toPresieveOverProp ?refine_1
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this✝ : IsClosedImmersion g
hZ : IsAffine Z
l : Spec (CommRingCat.of S.K) ⟶ Z := pullback.lift S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) ⋯
hg : l ≫ g = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))
e : Arrow.mk (CommRingCat.ofHom (algebraMap S.R S.K)) ≅
  Arrow.mk (Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)))) :=
  arrowIsoΓSpecOfIsAffine (CommRingCat.ofHom (algebraMap S.R S.K))
P : MorphismProperty CommRingCat :=
  RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ Function.Injective ⇑f).RespectsIso
⊢ P (CommRingCat.ofHom (algebraMap S.R S.K))

Tactic:
exact FaithfulSMul.algebraMap_injective S.R S.K

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
p₁ p₂ : ToType (P.obj (op X))
h : (ConcreteCategory.hom (f.app (op X))) p₁ = (ConcreteCategory.hom (f.app (op X))) p₂
Y : C
g : Y ⟶ unop (op X)
hg : (Presheaf.equalizerSieve p₁ p₂).arrows g
y : Φ.fiber.obj Y
⊢ (ConcreteCategory.hom (Φ.toPresheafFiber X ((ConcreteCategory.hom (Φ.fiber.map g)) y) P)) p₁ =
    (ConcreteCategory.hom (Φ.toPresheafFiber X ((ConcreteCategory.hom (Φ.fiber.map g)) y) P)) p₂

Tactic:
simp_all [← toPresheafFiber_w_apply]

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
inst✝ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S).arrows (F.map e ≫ (data X).f j)
⊢ 𝟙 { Y := F.obj Y₀, f := F.map e ≫ (data X).f j, hf := he }.Y ≫
      { Y := F.obj Y₀, f := F.map e ≫ (data X).f j, hf := he }.f =
    (F.map d ≫ F.map b ≫ (data a.Y).f i) ≫ a.f

Tactic:
by
              simp only [fac₁, fac₂, assoc, id_comp]

Goal state after:
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:
by
        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_2
S : Scheme
X Y : Scheme
f : X ⟶ Y
⊢ ∀ (E : PreZeroHypercover Y) [inst : ∀ (i : E.I₀), HasPullback f (E.f i)],
    qcCoverFamily.property E → qcCoverFamily.property (PreZeroHypercover.pullback₁ f E)

Tactic:
E

Goal state after:
case refine_2
S : Scheme
X Y : Scheme
f : X ⟶ Y
E : PreZeroHypercover Y
⊢ ∀ [inst : ∀ (i : E.I₀), HasPullback f (E.f i)],
    qcCoverFamily.property E → qcCoverFamily.property (PreZeroHypercover.pullback₁ f E)
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: case refine_2
S : Scheme
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst : ∀ (i : E.I₀), HasPullback f (E.f i)],
    qcCoverFamily.property E → qcCoverFamily.property (PreZeroHypercover.pullback₁ f E)

Tactic:
intro X Y f E h hE
    simp only [qcCoverFamily_property, Scheme.quasiCompactCover_iff] at hE ⊢
    infer_instance

Goal state after:
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
T : C
x₄ : T ⟶ X₄
this : Epi ⋯.shortComplex.g
T' : C
π : T' ⟶ T
w✝ : Epi π
u : T' ⟶ ⋯.shortComplex.X₂
hu : π ≫ x₄ = u ≫ ⋯.shortComplex.g
⊢ π ≫ x₄ = (u ≫ biprod.fst) ≫ r + (u ≫ biprod.snd) ≫ b

Tactic:
simp only [hu, assoc, ← Preadditive.comp_add]

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
T : C
x₄ : T ⟶ X₄
this : Epi ⋯.shortComplex.g
T' : C
π : T' ⟶ T
w✝ : Epi π
u : T' ⟶ ⋯.shortComplex.X₂
hu : π ≫ x₄ = u ≫ ⋯.shortComplex.g
⊢ u ≫ ⋯.shortComplex.g = u ≫ (biprod.fst ≫ r + biprod.snd ≫ b)
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
φ : X₁ ⟶ X₂
inst✝ : Mono φ
c₁ : Cocone X₁
hc₁ : IsColimit c₁
c₂ : Cocone X₂
hc₂ : IsColimit c₂
f : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = φ.app j ≫ c₂.ι.app j
j : J
⊢ c₁.ι.app j ≫ (hc₁.coconePointUniqueUpToIso (colimit.isColimit X₁)).hom ≫ colimMap φ =
    c₁.ι.app j ≫ f ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit X₂)).hom

Tactic:
rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
        colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
        IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]

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
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 ≫ f ≫ g₁ = φ.app j ≫ c₂.ι.app j ≫ g₂

Tactic:
h,

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
⊢ c₁.ι.app j ≫ f ≫ g₂ = φ.app j ≫ c₂.ι.app j ≫ g₂
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.obj.map g.op)) (J.uliftYonedaEquiv f) =
    J.uliftYonedaEquiv ((uliftYoneda.{v', v, u} J).map g ≫ f)

Tactic:
by
  change (f.hom.app (op X) ≫ F.obj.map g.op) ⟨𝟙 X⟩ = f.hom.app (op Y) ⟨𝟙 Y ≫ g⟩
  rw [← f.hom.naturality]
  simp [uliftYoneda]

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

Goal state before:
pp: case neg
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)
s : Cofan fun i ↦ J.yoneda.obj (X i)
Y : C
i j : ι
a : Y ⟶ X i
b : Y ⟶ X j
hab : a ≫ c.inj i = b ≫ c.inj j
h : ¬i = j
⊢ (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b

Tactic:
· obtain ⟨h⟩ := hdisj h a b hab
      have := Types.isTerminalEquivUnique _ (Sheaf.isTerminalOfBotCover s.pt _ (hempty Y h))
      exact Subsingleton.elim _ _

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

Goal state before:
pp: J : Type u
inst✝ : LinearOrder J
j : J
⊢ ∀ (j₂ : J), ∃ j₁, j₂ ≤ ↑j₁

Tactic:
intro k

Goal state after:
J : Type u
inst✝ : LinearOrder J
j k : J
⊢ ∃ j₁, k ≤ ↑j₁
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
⊢ (monomorphisms C).IsStableUnderTransfiniteComposition

Tactic:
by
  infer_instance

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

Goal state before:
pp: case neg
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
hi : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
⊢ (if h₂ : Order.succ j ≤ j then
      (objIso F X ⟨Order.succ j, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv ≫ eqToHom ⋯
    else 𝟙 (obj F X ⟨Order.succ j, ⋯⟩)) =
    𝟙 (obj F X ⟨Order.succ j, ⋯⟩)

Tactic:
dif_neg h₁

Goal state after:
case neg
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
hi : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
⊢ 𝟙 (obj F X ⟨Order.succ j, ⋯⟩) = 𝟙 (obj F X ⟨Order.succ j, ⋯⟩)
Module: Mathlib.CategoryTheory.MorphismProperty.IsSmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W✝ : MorphismProperty C
α : Type u_1
W : α → MorphismProperty C
inst✝¹ : Small.{w, u_1} α
inst✝ : ∀ (a : α), IsSmall.{w, v, u} (W a)
x✝ : (i : α) × ↑(W i).toSet
i : α
f : ↑(W i).toSet
⊢ ∃ i_1, ↑f ∈ (W i_1).toSet

Tactic:
exact ⟨i, f.prop⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
this✝¹ : LocallySmall.{w, v, u} C
this✝ : IsSmall.{w, v, u} I
this : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
⊢ (succStruct I κ).prop ≤ (propArrow I).functorCategory (Arrow C)

Tactic:
have := hasPushouts I κ

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
this✝² : LocallySmall.{w, v, u} C
this✝¹ : IsSmall.{w, v, u} I
this✝ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts C
⊢ (succStruct I κ).prop ≤ (propArrow I).functorCategory (Arrow C)
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
this : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
⊢ ∀ {f_1 : A ⟶ obj I κ f} {g : B ⟶ Y} (sq : CommSq f_1 i (πObj I κ f) g), sq.HasLift

Tactic:
have := hasPushouts I κ

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y A B : C
i : A ⟶ B
hi : I i
f : X ⟶ Y
this✝ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts C
⊢ ∀ {f_1 : A ⟶ obj I κ f} {g : B ⟶ Y} (sq : CommSq f_1 i (πObj I κ f) g), sq.HasLift
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
I : MorphismProperty C
inst✝ : I.IsCardinalForSmallObjectArgument Cardinal.aleph0
e : ℕ ≃o Cardinal.aleph0.ord.ToType := ULift.orderIso.{w, 0}.symm.trans (OrderIso.ofRelIsoLT ⋯.some)
⊢ I.rlp.llp = ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape ℕ).retracts

Tactic:
rw [SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument' _ Cardinal.aleph0,
    MorphismProperty.transfiniteCompositionsOfShape_eq_of_orderIso _ e]

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

Goal state before:
pp: case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ (↑p)⁻¹ < padicNorm p ↑m

Tactic:
h,

Goal state after:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h : padicNorm p ↑m = 1
⊢ (↑p)⁻¹ < 1
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)

Tactic:
h,

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (0 + F d)