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

Goal state before:
pp: case add
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ω : Type u_6
ι : Type u_7
F : Type u_8
G : Type u_9
inst✝¹³ : Semiring A
inst✝¹² : Semiring B
inst✝¹¹ : Semiring C
inst✝¹⁰ : SetLike σ A
inst✝⁹ : SetLike τ B
inst✝⁸ : SetLike ω C
inst✝⁷ : AddSubmonoidClass σ A
inst✝⁶ : AddSubmonoidClass τ B
inst✝⁵ : AddSubmonoidClass ω C
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ω
inst✝² : GradedRing 𝒜
inst✝¹ : GradedRing ℬ
inst✝ : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
I : HomogeneousIdeal 𝒜
b x✝ y✝ : B
hx✝ : x✝ ∈ Submodule.span B (⇑f '' ↑I.toIdeal)
hy✝ : y✝ ∈ Submodule.span B (⇑f '' ↑I.toIdeal)
a✝¹ : ∀ (i : ι), ↑(((DirectSum.decompose ℬ) x✝) i) ∈ Ideal.map f I.toIdeal
a✝ : ∀ (i : ι), ↑(((DirectSum.decompose ℬ) y✝) i) ∈ Ideal.map f I.toIdeal
i : ι
⊢ ↑(((DirectSum.decompose ℬ) (x✝ + y✝)) i) ∈ Ideal.map f I.toIdeal

Tactic:
| add =>

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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
⊢ (proj 𝒜 (i - n)) x ^ m ∈ 𝒜 ?m.177

Tactic:
by mem_tac

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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
a : A
ha : a ∈ asIdeal f_deg hm q
j : ℕ
h : ¬i = j
⊢ HomogeneousLocalization.mk
      { deg := m * j, num := ⟨(proj 𝒜 j) ↑(((decompose 𝒜) a) i) ^ m, ⋯⟩, den := ⟨f ^ j, ⋯⟩, den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
by
    simpa only [proj_apply, decompose_of_mem_ne 𝒜 (SetLike.coe_mem (decompose 𝒜 a i)) h,
      zero_pow hm.ne', map_zero] using carrier.zero_mem f_deg hm q j

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

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
⊢ IsIntegral (↥R.toSubring) x⁻¹

Tactic:
let := invertibleOfNonzero hx0

Goal state after:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
x : K
hx : x ∉ R.toSubring
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
⊢ IsIntegral (↥R.toSubring) x⁻¹
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: case inr
K : Type u_3
inst✝¹ : Field K
x : K
R : Subring K
hxR : x ∉ R
inst✝ : IsIntegrallyClosedIn (↥R) K
hx0 : x ≠ 0
⊢ ∃ V, R ≤ V.toSubring ∧ x ∉ V

Tactic:
let := invertibleOfNonzero hx0

Goal state after:
case inr
K : Type u_3
inst✝¹ : Field K
x : K
R : Subring K
hxR : x ∉ R
inst✝ : IsIntegrallyClosedIn (↥R) K
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
⊢ ∃ V, R ≤ V.toSubring ∧ x ∉ V
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: case inr
K : Type u_3
inst✝¹ : Field K
x : K
R : LocalSubring K
hxR : x ∉ R.toSubring
inst✝ : IsIntegrallyClosedIn (↥R.toSubring) K
hx0 : x ≠ 0
⊢ ∃ V, R ≤ V.toLocalSubring ∧ x ∉ V

Tactic:
let := invertibleOfNonzero hx0

Goal state after:
case inr
K : Type u_3
inst✝¹ : Field K
x : K
R : LocalSubring K
hxR : x ∉ R.toSubring
inst✝ : IsIntegrallyClosedIn (↥R.toSubring) K
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
⊢ ∃ V, R ≤ V.toLocalSubring ∧ x ∉ V
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: 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
⊢ Function.Injective (Subtype.val ∘ ⇑(g.rangeRestrict.comp f))

Tactic:
by convert! (IsFractionRing.injective R K); rw [← h]; rfl

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

Goal state before:
pp: 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' := ⋯ }
this : LocalSubring.range g ≤ V.toLocalSubring
x : S
y : R
hy : (algebraMap R K) y = g x
⊢ ∃ a, (g.rangeRestrict.comp f) a = ⟨g x, ⋯⟩

Tactic:
exact ⟨y, Subtype.ext (by simpa [← h] using hy)⟩

Goal state after:
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
X : Q.Over ⊤ S
R : Sieve X
Y : ↥X.left → Q.Over ⊤ S
f : (x : ↥X.left) → Y x ⟶ X
y : (x : ↥X.left) → ↥(Y x).left
hf : ∀ (x : ↥X.left), R.arrows (f x)
hP : ∀ (x : ↥X.left), P (f x).left
hy : ∀ (x : ↥X.left), (f x).left (y x) = x
⊢ { I₀ := ↥X.left, X := fun i ↦ (Y i).left, f := fun i ↦ (f i).left }.presieve₀ ∈ (precoverage P).coverings X.left

Tactic:
rw [presieve₀_mem_precoverage_iff]

Goal state after:
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
X : Q.Over ⊤ S
R : Sieve X
Y : ↥X.left → Q.Over ⊤ S
f : (x : ↥X.left) → Y x ⟶ X
y : (x : ↥X.left) → ↥(Y x).left
hf : ∀ (x : ↥X.left), R.arrows (f x)
hP : ∀ (x : ↥X.left), P (f x).left
hy : ∀ (x : ↥X.left), (f x).left (y x) = x
⊢ (∀ (x : ↥X.left), ∃ i, x ∈ Set.range ⇑({ I₀ := ↥X.left, X := fun i ↦ (Y i).left, f := fun i ↦ (f i).left }.f i)) ∧
    ∀ (i : { I₀ := ↥X.left, X := fun i ↦ (Y i).left, f := fun i ↦ (f i).left }.I₀),
      P ({ I₀ := ↥X.left, X := fun i ↦ (Y i).left, f := fun i ↦ (f i).left }.f i)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case intro
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
⊢ ∃ j₀ φ', φ'.comp (awayMap 𝒜 ⋯ ⋯) = φ ∧ (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range

Tactic:
have ⟨i₀, hi1⟩ : ∃ a, ψ a = Kmax := by simpa using Finset.max'_mem (Finset.univ.image ψ)

Goal state after:
case intro
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
⊢ ∃ j₀ φ', φ'.comp (awayMap 𝒜 ⋯ ⋯) = φ ∧ (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case intro
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := IsLocalization.Away.lift (Away.isLocalizationElem ⋯ ⋯) hunit
⊢ ∃ j₀ φ', φ'.comp (awayMap 𝒜 ⋯ ⋯) = φ ∧ (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range

Tactic:
have hφ'1 (s) : φ' (awayMap 𝒜 (hxdi i₀) rfl s) = φ s := IsLocalization.Away.lift_eq _ hunit s

Goal state after:
case intro
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := IsLocalization.Away.lift (Away.isLocalizationElem ⋯ ⋯) hunit
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
⊢ ∃ j₀ φ', φ'.comp (awayMap 𝒜 ⋯ ⋯) = φ ∧ (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_3
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : Aux M ⊤
f : ↑R
⊢ ∀ (x : ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f)))),
    ∃ n y, f ^ n • x = (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)) y

Tactic:
intro x
    obtain ⟨n, t, ht⟩ := h.existence _ _ x
    use n, t, ht.symm

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

Goal state before:
pp: S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
⊢ (𝒰.ulift.sum (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover)).presieve₀ ∈ (precoverage P).coverings S

Tactic:
rw [presieve₀_mem_precoverage_iff]

Goal state after:
S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
⊢ (∀ (x : ↥S), ∃ i, x ∈ Set.range ⇑((𝒰.ulift.sum (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover)).f i)) ∧
    ∀ (i : (𝒰.ulift.sum (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover)).I₀),
      P ((𝒰.ulift.sum (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover)).f i)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case fac
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 Y✝ : C
f : X ⟶ Y✝
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y✝
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y✝).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y✝).toPreOneHypercover.X i
fac : p ≫ (data Y✝).f i = F.map b ≫ a
⊢ p ≫ (data Y✝).f i = F.map (b ≫ (data X).p₂ j) ≫ (data X).f i₂ ≫ f

Tactic:
simp_all

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

Goal state before:
pp: case fac
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 Y✝ : C
f : X ⟶ Y✝
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y✝
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y✝).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y✝).toPreOneHypercover.X i
fac : p ≫ (data Y✝).f i = F.map b ≫ a
⊢ p ≫ (data Y✝).f i = F.map (b ≫ (data X).p₁ j) ≫ (data X).f i₁ ≫ f

Tactic:
simp_all

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
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
this : F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd)) ∈ J₀ U₀
V₀ : C₀
a : V₀ ⟶ U₀
x₁ : V₀ ⟶ (data Y).X (Sieve.ofArrows.i hc)
fac₁ : F.map x₁ = F.map a ≫ Sieve.ofArrows.h hc
x₂ : V₀ ⟶ (data X).X (Sieve.ofArrows.i hd)
fac₂ : F.map x₂ = F.map (a ≫ c) ≫ Sieve.ofArrows.h hd
⊢ F.map x₁ ≫ (data Y).f (Sieve.ofArrows.i hc) = F.map x₂ ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g

Tactic:
simp_all

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

Goal state before:
pp: 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)
⊢ ∃ T, Presieve.map (Over.forget P ⊤ S) T = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
let 𝒱 : PreZeroHypercover X :=
    ⟨𝒰.I₀, fun i ↦ Over.mk _ (𝒰.X i).hom ?_, fun i ↦ Over.homMk (𝒰.f i).left (by simp) trivial⟩

Goal state after:
case refine_2
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 }
⊢ ∃ T, Presieve.map (Over.forget P ⊤ S) T = Presieve.ofArrows 𝒰.X 𝒰.f

case refine_1
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)
i : 𝒰.I₀
⊢ P (𝒰.X i).hom
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: case refine_2
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₄
sq : IsPushout t l r b
A₀ : C
z : A₀ ⟶ kernel b
A₁ : C
π₁ : A₁ ⟶ A₀
w✝ : Epi π₁
x₁ :
  A₁ ⟶
    { X₁ := X₁, X₂ := X₂ ⊞ X₃, X₃ := ⋯.cokernelCofork.pt, f := biprod.lift t (-l), g := Cofork.π ⋯.cokernelCofork,
        zero := ⋯ }.X₁
hx₁ :
  π₁ ≫ z ≫ kernel.ι b ≫ biprod.inr =
    x₁ ≫
      { X₁ := X₁, X₂ := X₂ ⊞ X₃, X₃ := ⋯.cokernelCofork.pt, f := biprod.lift t (-l), g := Cofork.π ⋯.cokernelCofork,
          zero := ⋯ }.f
⊢ π₁ ≫ z = (-kernel.lift t x₁ ⋯) ≫ kernel.map t b l r ⋯

Tactic:
· ext
    simpa using hx₁ =≫ biprod.snd

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f✝ : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f✝ = (F.obj j).obj.hom
this : Mono f✝
A✝ : C
g : A✝ ⟶ X
inst✝ : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk g
j j' : J
f : j ⟶ j'
⊢ (F ⋙ MonoOver.forget X ⋙ Over.forget X).map f ≫ Subobject.ofMkLEMk (F.obj j').obj.hom g ⋯ =
    Subobject.ofMkLEMk (F.obj j).obj.hom g ⋯ ≫ ((Functor.const J).obj A✝).map f

Tactic:
dsimp
          simpa only [← cancel_mono g, Category.assoc, Subobject.ofMkLEMk_comp,
            Category.comp_id] using MonoOver.w (F.map f)

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

Goal state before:
pp: case pos
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 : ι
a b : Y ⟶ X i
hab : a ≫ c.inj i = b ≫ c.inj i
⊢ (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) b

Tactic:
rw [(cancel_mono _).mp hab]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃

Tactic:
by
  obtain hi₁₂ | rfl := hi.lt_or_eq
  · obtain hi₂₃ | rfl := hi'.lt_or_eq
    · dsimp [map]
      obtain hi₃' | rfl := hi₃.lt_or_eq
      · rw [dif_pos hi₃', dif_pos (hi₂₃.trans hi₃'), dif_pos hi₃', assoc, assoc,
          Iso.inv_hom_id_assoc, ← Functor.map_comp_assoc, homOfLE_comp]
      · rw [dif_neg (by simp), dif_pos (hi₁₂.trans hi₂₃), dif_pos hi₂₃, dif_neg (by simp),
          dif_pos hi₂₃, eqToHom_refl, comp_id, assoc, assoc, Iso.inv_hom_id_assoc,
          Cocone.w_assoc]
    · rw [map_id, comp_id]
  · rw [map_id, id_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
ι : Type t
inst✝ : Small.{w, t} ι
A B : ι → C
f : (i : ι) → A i ⟶ B i
⊢ IsSmall.{w, v, u} (ofHoms f)

Tactic:
let φ (i : ι) : (ofHoms f).toSet := ⟨Arrow.mk (f i), ⟨i⟩⟩
  have hφ : Function.Surjective φ := by
    rintro ⟨⟨_, _, f⟩, ⟨i⟩⟩
    exact ⟨i, rfl⟩
  exact ⟨small_of_surjective hφ⟩

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

Goal state before:
pp: p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ padicValRat p ↑z = ↑(multiplicity (↑p) z)

Tactic:
of_int,

Goal state after:
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ ↑(padicValInt p z) = ↑(multiplicity (↑p) z)
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p ↑m = 1 ↔ ¬p ∣ m

Tactic:
by
  rw [← Int.natCast_dvd_natCast, ← int_eq_one_iff, Int.cast_natCast]

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

Goal state before:
pp: p n : ℕ
hp : 1 ≤ 0
h : ¬p ∣ n
⊢ False

Tactic:
exact lt_irrefl 0 (lt_of_lt_of_le zero_lt_one hp)

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
h1 : 2 ^ padicValNat 2 (n + 1) < n + 1
h2 : n < 2 ^ (padicValNat 2 (n + 1) + 1)
⊢ False

Tactic:
← mul_one (2 ^ _)

Goal state after:
n : ℕ
hn : n ≠ 0
h1 : 2 ^ padicValNat 2 (n + 1) * 1 < n + 1
h2 : n < 2 ^ (padicValNat 2 (n + 1) + 1)
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
this : ‖z‖ * ‖w‖ ≤ ‖z‖
⊢ 1 ≤ ‖z‖

Tactic:
← norm_mul,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
this : ‖z * w‖ ≤ ‖z‖
⊢ 1 ≤ ‖z‖
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ¬IsUnit z ↔ ‖z‖ < 1

Tactic:
by
  simpa using mem_nonunits

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

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ -↑(padicValInt p x) ≤ log 1

Tactic:
simp_all

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

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ 1 ≠ 0

Tactic:
simp_all

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
⊢ (padicValuation p) x ≤ 1

Tactic:
by
  simp only [← Rat.padicValuation_cast, Rat.padicValuation, Valuation.coe_mk,
    MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, Rat.intCast_eq_zero_iff, padicValRat.of_int]
  split_ifs
  · simp
  · rw [← le_log_iff_exp_le] <;>
    simp_all

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

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : x = 0
⊢ 0 = 1 ↔ ¬↑p ∣ x

Tactic:
simp_all

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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : ¬n = 0
⊢ padicValNat p n ! ≤ n

Tactic:
exact le_of_lt (padicValNat_factorial_lt_of_ne_zero p hn)

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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx✝ : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := ⟨x, ⋯⟩
n : ℕ
this✝ : 0 < ↑p ^ (-↑n)
i : ℕ
hx : ‖x n - x i‖ ≤ ↑p ^ (-↑n)
hi : ‖↑x' i - ↑(const norm x'.lim) i‖ < ↑p ^ (-↑n)
hin : n < i
this : ‖x n - x i + (x i - x'.lim)‖ ≤ max ‖x n - x i‖ ‖x i - x'.lim‖
⊢ ‖x n - x'.lim‖ ≤ ↑p ^ (-↑n)

Tactic:
sub_add_sub_cancel

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx✝ : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
x' : CauSeq ℤ_[p] norm := ⟨x, ⋯⟩
n : ℕ
this✝ : 0 < ↑p ^ (-↑n)
i : ℕ
hx : ‖x n - x i‖ ≤ ↑p ^ (-↑n)
hi : ‖↑x' i - ↑(const norm x'.lim) i‖ < ↑p ^ (-↑n)
hin : n < i
this : ‖x n - x'.lim‖ ≤ max ‖x n - x i‖ ‖x i - x'.lim‖
⊢ ‖x n - x'.lim‖ ≤ ↑p ^ (-↑n)