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

Goal state before:
pp: case zero
σ : 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
sx : Away 𝒜 (x i₀)
a : ℕ
ai : ι → ℕ
hai✝ : ∑ i, ai i • d i = a • d i₀
hai : ∑ x, ai x * d x = a * d i₀
H : (∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1)) ∈ 𝒜 ((a * d i₀) • d j)
h : d j = 0
⊢ ψ i₀ ^ (a * d i₀ + d i₀ * a * (0 - 1)) = ψ i₀ ^ (d i₀ * a * 0)

Tactic:
cases (hdi j).ne' h

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
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
⊢ restriction data G₀ ((data X).f i₁ ≫ f) ≫ G₀.obj.map (b ≫ (data X).p₁ j).op =
    restriction data G₀ ((data X).f i₂ ≫ f) ≫ G₀.obj.map (b ≫ (data X).p₂ j).op

Tactic:
rw [restriction_map (p := p), restriction_map (p := p)]

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

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
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₀
⊢ restriction data G₀ ((data X).f i) = presheafObjπ data G₀ X i

Tactic:
restriction_eq_of_fac data G₀ ((data X).f i) (𝟙 _) (by simp),

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
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₀
⊢ presheafObjπ data G₀ X i ≫ IsDenseSubsite.mapPreimage J F G₀ (𝟙 (F.obj ((data X).X i))) = presheafObjπ data G₀ X i
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 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
O : Type u_2
commRing✝ : CommRing O
domain✝ : IsDomain O
valuationRing✝ : ValuationRing O
K : Type u_2
field✝ : Field K
algebra✝ : Algebra O K
isFractionRing✝ : IsFractionRing O K
i₁ : Spec (CommRingCat.of K) ⟶ Proj 𝒜
i₂ : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of ↥(𝒜 0))
w : CommSq i₁ (Spec.map (CommRingCat.ofHom (algebraMap O K))) (toSpecZero 𝒜) i₂
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
hi : i₁ (IsLocalRing.closedPoint K) ∈ basicOpen 𝒜 ↑i
this : Set.range ⇑i₁ ⊆ ↑(Hom.opensRange (awayι 𝒜 ↑i ⋯ ⋯))
φ : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of (Away 𝒜 ↑i)) := IsOpenImmersion.lift (awayι 𝒜 ↑i ⋯ ⋯) i₁ this
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers ↑i)) ≫ Spec.preimage φ
i₀ : ↥x
φ' : Away 𝒜 (↑i * ↑i₀) →+* K
hφ : φ'.comp (awayMap 𝒜 ⋯ ⋯) = CommRingCat.Hom.hom (Spec.preimage φ)
hφ' : (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
e : O ≃+* ↥(algebraMap O K).range := (AlgEquiv.ofInjective (Algebra.ofId O K) ⋯).toRingEquiv
φ'' : Away 𝒜 ↑i₀ →+* O := e.symm.toRingHom.comp ((Subring.inclusion hφ').comp (φ'.comp (awayMap 𝒜 ⋯ ⋯)).rangeRestrict)
hφ'' : (algebraMap O K).comp φ'' = φ'.comp (awayMap 𝒜 ⋯ ⋯)
| i₂

Tactic:
← Spec.map_preimage i₂

Goal state after:
σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
O : Type u_2
commRing✝ : CommRing O
domain✝ : IsDomain O
valuationRing✝ : ValuationRing O
K : Type u_2
field✝ : Field K
algebra✝ : Algebra O K
isFractionRing✝ : IsFractionRing O K
i₁ : Spec (CommRingCat.of K) ⟶ Proj 𝒜
i₂ : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of ↥(𝒜 0))
w : CommSq i₁ (Spec.map (CommRingCat.ofHom (algebraMap O K))) (toSpecZero 𝒜) i₂
x : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
hi : i₁ (IsLocalRing.closedPoint K) ∈ basicOpen 𝒜 ↑i
this : Set.range ⇑i₁ ⊆ ↑(Hom.opensRange (awayι 𝒜 ↑i ⋯ ⋯))
φ : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of (Away 𝒜 ↑i)) := IsOpenImmersion.lift (awayι 𝒜 ↑i ⋯ ⋯) i₁ this
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers ↑i)) ≫ Spec.preimage φ
i₀ : ↥x
φ' : Away 𝒜 (↑i * ↑i₀) →+* K
hφ : φ'.comp (awayMap 𝒜 ⋯ ⋯) = CommRingCat.Hom.hom (Spec.preimage φ)
hφ' : (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
e : O ≃+* ↥(algebraMap O K).range := (AlgEquiv.ofInjective (Algebra.ofId O K) ⋯).toRingEquiv
φ'' : Away 𝒜 ↑i₀ →+* O := e.symm.toRingHom.comp ((Subring.inclusion hφ').comp (φ'.comp (awayMap 𝒜 ⋯ ⋯)).rangeRestrict)
hφ'' : (algebraMap O K).comp φ'' = φ'.comp (awayMap 𝒜 ⋯ ⋯)
| Spec.map (Spec.preimage i₂)
Module: Mathlib.AlgebraicGeometry.Sites.Fpqc

Goal state before:
pp: ⊢ fppfPrecoverage = precoverage @Flat ⊓ precoverage @LocallyOfFinitePresentation

Tactic:
grind [fppfPrecoverage, precoverage, precoverage, MorphismProperty.precoverage_inf]

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

Goal state before:
pp: ⊢ etalePrecoverage ≤ proetalePrecoverage

Tactic:
rw [proetalePrecoverage, propQCPrecoverage, etalePrecoverage, le_inf_iff]

Goal state after:
⊢ precoverage @Etale ≤ qcPrecoverage ∧ precoverage @Etale ≤ precoverage @WeaklyEtale
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 : X ⟶ Y
⊢ J.yonedaEquiv (J.yoneda.map f) = f

Tactic:
rw [yonedaEquiv_apply]
  simp

Goal state after:
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 (unop X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (F.obj.map g)) (J.uliftYonedaEquiv f) = (ConcreteCategory.hom (f.hom.app Y)) { down := g.unop }

Tactic:
by
  rw [uliftYonedaEquiv_naturality', uliftYonedaEquiv_comp, uliftYonedaEquiv_uliftYoneda_map]

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ (coproducts.{w, v, u} (ofHoms g)).pushouts f → Nonempty (AttachCells g f)

Tactic:
rintro ⟨Y₁, Y₂, m, g₁, g₂, h, sq⟩

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
m : Y₁ ⟶ Y₂
g₁ : Y₁ ⟶ X₁
g₂ : Y₂ ⟶ X₂
h : coproducts.{w, v, u} (ofHoms g) m
sq : IsPushout g₁ m f g₂
⊢ Nonempty (AttachCells g f)
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
j : J
hj : ¬IsMax j
⊢ Φ.prop ((Φ.iterationFunctor J).map (homOfLE ⋯))

Tactic:
by
    have := (Φ.iter (Order.succ j)).prop_map_succ j (Order.lt_succ_of_not_isMax hj)
    rw [prop_iff] at this ⊢
    simp only [Φ.iterationFunctor_obj j (Φ.iter (Order.succ j)) (Order.le_succ j),
      Φ.arrowMk_iterationFunctor_map _ _ (Order.le_succ j) (Φ.iter (Order.succ j)) (by simp),
      this]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ ((coproducts.{t, v, u} W).pushouts.transfiniteCompositionsOfShape J).retracts ≤ W.rlp.llp

Tactic:
by
  rw [le_llp_iff_le_rlp, rlp_retracts, ← le_llp_iff_le_rlp]
  apply transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp

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 κ
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
this : PreservesColimit (relativeCellComplexιObj I κ f).F (coyoneda.obj (Opposite.op A))
g : A ⟶ obj I κ f
b : B ⟶ Y
⊢ ∀ (sq : CommSq g i (πObj I κ f) b), sq.HasLift

Tactic:
sq

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
this : PreservesColimit (relativeCellComplexιObj I κ f).F (coyoneda.obj (Opposite.op A))
g : A ⟶ obj I κ f
b : B ⟶ Y
sq : CommSq g i (πObj I κ f) b
⊢ sq.HasLift
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
⊢ padicValRat p q = ↑(multiplicity (↑p) n) - ↑(multiplicity (↑p) d)

Tactic:
let ⟨c, hc1, hc2⟩ := Rat.num_den_mk hd qdf

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * ↑q.den
⊢ padicValRat p q = ↑(multiplicity (↑p) n) - ↑(multiplicity (↑p) d)
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
this✝ : HasPushouts C
this : PreservesColimit (relativeCellComplexιObj I κ f).F (coyoneda.obj (Opposite.op A))
g : A ⟶ obj I κ f
b : B ⟶ Y
sq : CommSq g i (πObj I κ f) b
j : κ.ord.ToType
t : A ⟶ (relativeCellComplexιObj I κ f).F.obj j
ht : t ≫ (relativeCellComplexιObj I κ f).incl.app j = g
⊢ (relativeCellComplexιObj I κ f).F.map (homOfLE ⋯) ≫ (relativeCellComplexιObjFObjSuccIso I κ f j).hom =
    𝟙 ((relativeCellComplexιObj I κ f).F.obj j) ≫
      ιFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom

Tactic:
ιFunctorObj_eq,

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
this : PreservesColimit (relativeCellComplexιObj I κ f).F (coyoneda.obj (Opposite.op A))
g : A ⟶ obj I κ f
b : B ⟶ Y
sq : CommSq g i (πObj I κ f) b
j : κ.ord.ToType
t : A ⟶ (relativeCellComplexιObj I κ f).F.obj j
ht : t ≫ (relativeCellComplexιObj I κ f).incl.app j = g
⊢ (relativeCellComplexιObj I κ f).F.map (homOfLE ⋯) ≫ (relativeCellComplexιObjFObjSuccIso I κ f j).hom =
    𝟙 ((relativeCellComplexιObj I κ f).F.obj j) ≫
      (relativeCellComplexιObj I κ f).F.map (homOfLE ⋯) ≫ (relativeCellComplexιObjFObjSuccIso I κ f j).hom
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
⊢ q.num * r.num /. ↑(q.den * r.den) = q.num * r.num /. (↑q.den * ↑r.den)

Tactic:
Nat.cast_mul

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
⊢ q.num * r.num /. (↑q.den * ↑r.den) = q.num * r.num /. (↑q.den * ↑r.den)
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case hmn
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ -padicValRat p (q + r) ≤ -padicValRat p q

Tactic:
apply neg_le_neg

Goal state after:
case hmn
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p j : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
S : Finset ℕ
hn1 : ∀ (i : ℕ), 0 < F i
s : ℕ
S' : Finset ℕ
Hnot : s ∉ S'
Hne : S'.Nonempty
Hind : (∀ i ∈ S', padicValRat p (F j) < padicValRat p (F i)) → padicValRat p (F j) < padicValRat p (∑ i ∈ S', F i)
hF : ∀ i ∈ Finset.cons s S' Hnot, padicValRat p (F j) < padicValRat p (F i)
⊢ s ∈ Finset.cons s S' Hnot

Tactic:
simp [Finset.mem_insert, true_or]

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

Goal state before:
pp: case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ∈ n.divisors.erase 1

Tactic:
Finset.mem_erase,

Goal state after:
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ≠ 1 ∧ p ^ (k + 1) ∈ n.divisors
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r * ↑r.den‖ = ‖↑r.num‖
⊢ False

Tactic:
padicNormE.mul

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ padicValNat p n ! ≤ n

Tactic:
by_cases hn : n = 0
  · simp [hn]
  · exact le_of_lt (padicValNat_factorial_lt_of_ne_zero p hn)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑p ∈ nonunits ℤ_[p]

Tactic:
have : (p : ℝ)⁻¹ < 1 := inv_lt_one_of_one_lt₀ <| mod_cast hp.out.one_lt
  rwa [← norm_p, ← mem_nonunits] at this

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

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
ε : ℝ
hε : ε > 0
m : ℕ
hm : ↑p ^ (-↑m) < ε
n : ℕ
hn : n ≥ m
⊢ ‖x n - x m‖ ≤ ↑p ^ (-↑m)

Tactic:
rw [← neg_sub, norm_neg]

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℕ → ℤ_[p]
hx : ∀ {m n : ℕ}, m ≤ n → ‖x m - x n‖ ≤ ↑p ^ (-↑m)
ε : ℝ
hε : ε > 0
m : ℕ
hm : ↑p ^ (-↑m) < ε
n : ℕ
hn : n ≥ m
⊢ ‖x m - x n‖ ≤ ↑p ^ (-↑m)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : f ≈ 0
⊢ (f + g).norm = max f.norm g.norm

Tactic:
have : LimZero (f - 0) := hf
    have : f + g ≈ g := show LimZero (f + g - g) by simpa only [sub_zero, add_sub_cancel_right]
    have h1 : (f + g).norm = g.norm := norm_equiv this
    have h2 : f.norm = 0 := (norm_zero_iff _).2 hf
    rw [h1, h2, max_eq_right (norm_nonneg _)]

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))
this : Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm (𝟙 U)) ∈ J U
⊢ ∀ {U_1 : C} (s : ToType ((shrinkYoneda.{w, v, u}.obj U).obj (op U_1))), Presheaf.imageSieve f s ∈ J U_1

Tactic:
intro V g

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))
this : Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm (𝟙 U)) ∈ J U
V : C
g : ToType ((shrinkYoneda.{w, v, u}.obj U).obj (op V))
⊢ Presheaf.imageSieve f g ∈ J V
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inr.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : ¬stationaryPoint hne' ≤ N
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε

Tactic:
exact hN _ (lt_of_not_ge hle).le _ le_rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: j : ℕ
⊢ ¬c.Rel 0 j

Tactic:
intro hj
  dsimp at hj
  apply Nat.not_succ_le_zero j
  rw [Nat.succ_eq_add_one, hj]

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

Goal state before:
pp: case hbc.h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑(limSeq f j) - ↑f (max N N2)) < ε / 3 + ε / 3

pp: case h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑f (max N N2) - ↑(limSeq f (max N N2))) < ε / 3

Tactic:
· suffices padicNormE (limSeq f j - f j + (f j - f (max N N2)) : ℚ_[p]) < ε / 3 + ε / 3 by
        simpa only [sub_add_sub_cancel]
      apply lt_of_le_of_lt
      · apply padicNormE.add_le
      · apply _root_.add_lt_add
        · rw [padicNormE.map_sub]
          apply mod_cast hN j
          exact le_of_max_le_left hj
        · exact hN2 _ (le_of_max_le_right hj) _ (le_max_right _ _)

Goal state after:
case h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑f (max N N2) - ↑(limSeq f (max N N2))) < ε / 3
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑p * ↑x‖ < 1

Tactic:
padicNormE.mul

Goal state after:
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑p‖ * ‖↑x‖ < 1
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
⊢ (↑n).valuation = ↑(padicValInt p n)

Tactic:
by
  rw [← Rat.cast_intCast, valuation_ratCast, padicValRat.of_int]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition

Goal state before:
pp: case neg.e_a.e_s
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
i : ℕ
hi : i < n + 1
⊢ ⟨i, hi⟩ ∈ {i | ↑i < q + 1}.erase q' ↔ ⟨i, hi⟩ ∈ {i | ↑i < q}

Tactic:
Finset.mem_erase,

Goal state after:
case neg.e_a.e_s
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
i : ℕ
hi : i < n + 1
⊢ ⟨i, hi⟩ ≠ q' ∧ ⟨i, hi⟩ ∈ {i | ↑i < q + 1} ↔ ⟨i, hi⟩ ∈ {i | ↑i < q}