mathlib-initiative/mathlib-tactics huggingface dataset:
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
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
⊢ LocallyOfFiniteType ((basicOpenIsoSpec 𝒜 ↑i ⋯ ⋯).inv ≫ (basicOpen 𝒜 ↑i).ι ≫ toSpecZero 𝒜)

Tactic:
← Category.assoc,

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
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
⊢ LocallyOfFiniteType (((basicOpenIsoSpec 𝒜 ↑i ⋯ ⋯).inv ≫ (basicOpen 𝒜 ↑i).ι) ≫ toSpecZero 𝒜)
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
inst✝³ : IsDenseSubsite J₀ J F
inst✝² : HasPullbacks C
inst✝¹ : F.Full
inst✝ : F.Faithful
S : C
ι : C → Type w
U : (S : C) → ι S → C₀
f : (S : C) → (i : ι S) → F.obj (U S i) ⟶ S
hf : ∀ (S : C), Sieve.ofArrows (fun i ↦ F.obj (U S i)) (f S) ∈ J S
i j : ι S
W₀ : C₀
p₁ : W₀ ⟶ U S i
p₂ : W₀ ⟶ U S j
hp : F.map p₁ ≫ f S i = F.map p₂ ≫ f S j
this : F.IsCoverDense J
T : C
Z : C₀
q : Z ⟶ W₀
r : T ⟶ F.obj Z
Y : C
k : ι (pullback (f S i) (f S j))
s : F.obj Z ⟶ F.obj (U (pullback (f S i) (f S j)) k)
fac : s ≫ f (pullback (f S i) (f S j)) k = F.map q ≫ pullback.lift (F.map p₁) (F.map p₂) hp
fac₁ : s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j) = F.map q ≫ F.map p₁
fac₂ : s ≫ f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j) = F.map q ≫ F.map p₂
⊢ F.map (q ≫ p₂) =
    F.map
      (F.preimage s ≫
        { I₀ := ι S, X := U S, f := f S, I₁ := fun i j ↦ ι (pullback (f S i) (f S j)),
              Y := fun i j ↦ U (pullback (f S i) (f S j)),
              p₁ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.fst (f S i) (f S j)),
              p₂ := fun i j k ↦ F.preimage (f (pullback (f S i) (f S j)) k ≫ pullback.snd (f S i) (f S j)), w := ⋯ }.p₂
          k)

Tactic:
by simp [fac₂]

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

Goal state before:
pp: Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
S : Scheme
R : Sieve S
x : ↥S
a : S.residueField x ⟶ CommRingCat.of Ω
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
⊢ ∃ Y f,
    ∃ (_ : R.arrows f),
      ∃ y,
        (ConcreteCategory.hom ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).map f)) y =
          (SpecToEquivOfField Ω S).symm ⟨x, a⟩

Tactic:
obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq x

Goal state after:
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
S : Scheme
R : Sieve S
𝒰 : Cover (precoverage @Etale) S
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ R.arrows
i : 𝒰.I₀
y : ↥(𝒰.X i)
a : S.residueField ((𝒰.f i) y) ⟶ CommRingCat.of Ω
⊢ ∃ Y f,
    ∃ (_ : R.arrows f),
      ∃ y_1,
        (ConcreteCategory.hom ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).map f)) y_1 =
          (SpecToEquivOfField Ω S).symm ⟨(𝒰.f i) y, a⟩
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
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
⊢ restriction.res data G₀ h₁ ≫ G₀.obj.map p₁.op = restriction.res data G₀ h₂ ≫ G₀.obj.map p₂.op

Tactic:
refine Presheaf.IsSheaf.hom_ext G₀.property
        ⟨_, J₀.intersection_covering
          (IsDenseSubsite.imageSieve_mem J₀ J F (F.map p₁ ≫ h₁.q))
          (IsDenseSubsite.imageSieve_mem J₀ J F (F.map p₂ ≫ h₂.q))⟩ _ _ ?_

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
X₀ : C₀
f : F.obj X₀ ⟶ X
Z₁ : C₀
g₁ : Z₁ ⟶ X₀
h₁ : (data X).SieveStruct f g₁
Z₂ : C₀
g₂ : Z₂ ⟶ X₀
h₂ : (data X).SieveStruct f g₂
T₀ : C₀
p₁ : T₀ ⟶ Z₁
p₂ : T₀ ⟶ Z₂
w : p₁ ≫ g₁ = p₂ ≫ g₂
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨F.imageSieve (F.map p₁ ≫ h₁.q) ⊓ F.imageSieve (F.map p₂ ≫ h₂.q), ⋯⟩),
    (restriction.res data G₀ h₁ ≫ G₀.obj.map p₁.op) ≫ G₀.obj.map I.f.op =
      (restriction.res data G₀ h₂ ≫ G₀.obj.map p₂.op) ≫ G₀.obj.map I.f.op
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: S : Scheme
E : PreZeroHypercover S
⊢ E.presieve₀ ∈ qcPrecoverage.coverings S ↔ QuasiCompactCover E

Tactic:
← PreZeroHypercover.presieve₀_shrink,

Goal state after:
S : Scheme
E : PreZeroHypercover S
⊢ E.shrink.presieve₀ ∈ qcPrecoverage.coverings S ↔ QuasiCompactCover E
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ propQCPrecoverage P ≤ propQCPrecoverage Q

Tactic:
rw [propQCPrecoverage, propQCPrecoverage]

Goal state after:
P Q : MorphismProperty Scheme
h : P ≤ Q
⊢ qcPrecoverage ⊓ precoverage P ≤ qcPrecoverage ⊓ precoverage Q
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
⊢ presheafMap data G₀ g ≫
      presheafObjπ data G₀ X (Sieve.ofArrows.i hd) ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd) =
    presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc)

Tactic:
presheafMap_π_assoc

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 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
⊢ restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd) =
    presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc)
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: T : Type v
inst✝ : TopologicalSpace T
⊢ Presheaf.IsSheaf Scheme.fpqcTopology (continuousMapPresheaf T)

Tactic:
by
  rw [isSheaf_iff_isSheaf_of_type, Scheme.fpqcTopology_eq_propQCTopology,
    isSheaf_type_propQCTopology_iff]
  refine ⟨?_, fun {R S} f hf₁ hf₂ ↦ ?_⟩
  · rw [← isSheaf_iff_isSheaf_of_type]
    exact isSheaf_zariskiTopology_continuousMapPresheaf _
  · rw [Presieve.isSheafFor_singleton]
    have : Topology.IsQuotientMap (Spec.map f) := Flat.isQuotientMap_of_surjective _
    intro (x : C(Spec S, T)) h
    refine ⟨?_, ?_, ?_⟩
    · refine Topology.IsQuotientMap.lift this x fun a b hfab ↦ ?_
      obtain ⟨c, rfl, rfl⟩ := Scheme.Pullback.exists_preimage_pullback a b hfab
      exact congr($(h (pullback.fst (Spec.map f) (Spec.map f))
        (pullback.snd _ _) pullback.condition).1 c)
    · apply Topology.IsQuotientMap.lift_comp
    · intro y hy
      rwa [← ContinuousMap.cancel_right (Spec.map f).surjective, Topology.IsQuotientMap.lift_comp]

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

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
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
inst✝ : IsFiltered J
j : Under j₀
⊢ (colimit.cocone
              { X₁ := kernel (g y), X₂ := (Functor.const (Under j₀)).obj X, X₃ := Under.forget j₀ ⋙ Y,
                  f := kernel.ι (g y), g := g y, zero := ⋯ }.X₁).ι.app
        j ≫
      f y =
    { X₁ := kernel (g y), X₂ := (Functor.const (Under j₀)).obj X, X₃ := Under.forget j₀ ⋙ Y, f := kernel.ι (g y),
              g := g y, zero := ⋯ }.f.app
        j ≫
      (constCocone (Under j₀) X).ι.app j

Tactic:
simpa using! hf y j

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

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
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
this : IsFiltered J
j : Under j₀
⊢ (colimit.cocone (kernel (g y))).ι.app j ≫ f y = ((F y).obj j).obj.hom

Tactic:
simpa using! hf y j

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
inst✝¹ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝ : HasPushout (functorObjTop f πY) (functorObjLeft f πY)
⊢ functorMap f τ ≫ πFunctorObj f πY = πFunctorObj f πX ≫ Arrow.Hom.right τ

Tactic:
by
  ext ⟨i, t, b, w⟩
  · simp [functorMap]
  · simp [functorMap, ι_functorMapTgt_assoc f τ i t b w _ rfl]

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

Goal state before:
pp: case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
i : J
hj : ¬IsMax i
iter : Φ.Iteration i
hi₁✝ : i < Order.succ i
hi₁ : i ≤ i
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨i, ⋯⟩))) i hi₁✝ =
    Φ.toSuccArrow ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨i, ⋯⟩))).obj ⟨i, ⋯⟩)

Tactic:
rw [arrowSucc_extendToSucc, toSuccArrow,
        extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i]

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 : C
f : X ⟶ Y
this : HasIterationOfShape κ.ord.ToType C
h : (succStruct I κ).prop.TransfiniteCompositionOfShape κ.ord.ToType (ιIteration I κ) :=
  transfiniteCompositionOfShapeSuccStructPropιIteration I κ
⊢ RelativeCellComplex (fun x ↦ I.homFamily) (ιObj I κ f)

Tactic:
exact
  { toTransfiniteCompositionOfShape :=
      h.toTransfiniteCompositionOfShape.map ((evaluation _ _).obj f ⋙ Arrow.leftFunc)
    attachCells j hj :=
      attachCellsOfSuccStructProp I κ (h.map_mem j hj) f }

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

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

Tactic:
conv_rhs =>
    rw [← q.num_divInt_den, padicValRat.defn p hq', ← r.num_divInt_den, padicValRat.defn p hr']

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ ↑(multiplicity (↑p) (q.num * r.num)) - ↑(multiplicity (↑p) (↑q.den * ↑r.den)) =
    ↑(multiplicity (↑p) q.num) - ↑(multiplicity ↑p ↑q.den) + (↑(multiplicity (↑p) r.num) - ↑(multiplicity ↑p ↑r.den))
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
⊢ padicValRat p q⁻¹ + padicValRat p q = 0

Tactic:
← padicValRat.mul (inv_ne_zero hq) hq,

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
⊢ padicValRat p (q⁻¹ * q) = 0
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ : ℚ
hx : x✝ = 0
⊢ padicNorm p x✝ = 0

Tactic:
simp [hx]

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

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

Tactic:
· rw [← exp_zero, exp_injective.eq_iff]
    simp_all [Nat.Prime.ne_one Fact.out]

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

Goal state before:
pp: case inr.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
h : p ∣ x.den
h' : ↑p ∣ x.num
⊢ False

Tactic:
rw [Int.natCast_dvd] at h'

Goal state after:
case inr.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
h : p ∣ x.den
h' : p ∣ x.num.natAbs
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (f * g).norm = f.norm * g.norm

Tactic:
unfold norm

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (if hf : f * g ≈ 0 then 0 else padicNorm p (↑(f * g) (stationaryPoint hf))) =
    (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) *
      if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf))
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ IsIso c.fst → c.fst = c.snd

Tactic:
intro
    obtain ⟨φ, hφ₁, hφ₂⟩ := PullbackCone.IsLimit.lift' hc (𝟙 X) (𝟙 X) (by simp)
    have : IsSplitEpi φ := IsSplitEpi.mk ⟨SplitEpi.mk c.fst (by
      rw [← cancel_mono c.fst, assoc, id_comp, hφ₁, comp_id])⟩
    rw [← cancel_epi φ, hφ₁, hφ₂]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PushoutCocone f f
hc : IsColimit c
a✝ : IsIso c.inl
φ : c.pt ⟶ Y
hφ₁ : c.inl ≫ φ = 𝟙 Y
hφ₂ : c.inr ≫ φ = 𝟙 Y
⊢ φ ≫ c.inl = 𝟙 c.pt

Tactic:
rw [← cancel_epi c.inl, reassoc_of% hφ₁, comp_id]

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
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝⁸ : Category.{v', u'} A
inst✝⁷ : LocallySmall.{w, v, u} C
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
inst✝³ : (forget A).ReflectsIsomorphisms
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
hJ : J.HasSheafCompose (forget A)
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝¹ : HasWeakSheafify J A
inst✝ : HasProducts A
⊢ J.W f ↔ ∀ (Φ : P.FullSubcategory), IsIso (Φ.obj.presheafFiber.map f)

Tactic:
rw [GrothendieckTopology.W_iff, (hP.jointlyReflectIsomorphisms A).isIso_iff]

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝⁸ : Category.{v', u'} A
inst✝⁷ : LocallySmall.{w, v, u} C
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
inst✝³ : (forget A).ReflectsIsomorphisms
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
hJ : J.HasSheafCompose (forget A)
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝¹ : HasWeakSheafify J A
inst✝ : HasProducts A
⊢ (∀ (i : P.FullSubcategory), IsIso (i.obj.sheafFiber.map ((presheafToSheaf J A).map f))) ↔
    ∀ (Φ : P.FullSubcategory), IsIso (Φ.obj.presheafFiber.map f)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
unfold norm

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) =
    if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf))
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
unfold norm

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (if hf : f + g ≈ 0 then 0 else padicNorm p (↑(f + g) (stationaryPoint hf))) ≤
    max (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf)))
      (if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf)))
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
P : Cᵒᵖ ⥤ A
M N : A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
f : Φ.presheafFiber.obj P ⟶ M
g : M ⟶ N
⊢ Φ.skyscraperPresheafHomEquiv (f ≫ g) = Φ.skyscraperPresheafHomEquiv f ≫ Φ.skyscraperPresheafFunctor.map g

Tactic:
by
  ext
  dsimp
  ext
  dsimp
  rw [skyscraperPresheafHomEquiv_app_π]
  dsimp
  rw [Category.assoc, Pi.map_π, skyscraperPresheafHomEquiv_app_π_assoc]

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

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

Tactic:
exact max_eq_left (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₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
this :
  ∀ {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) [Mono f],
    (∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
      (∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U) → Presheaf.IsLocallySurjective J f
hF₂ : ¬∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
U : C
s : ToType (F₂.obj (op U))
f' : pullback f (shrinkYonedaEquiv.symm s) ⟶ shrinkYoneda.{w, v, u}.obj U := pullback.snd f (shrinkYonedaEquiv.symm s)
Φ : P.FullSubcategory
hf : Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f'))

Tactic:
← CategoryTheory.epi_iff_surjective

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₁ F₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
inst✝ : Mono f
this :
  ∀ {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) [Mono f],
    (∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))) →
      (∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U) → Presheaf.IsLocallySurjective J f
hF₂ : ¬∃ U, F₂ = shrinkYoneda.{w, v, u}.obj U
U : C
s : ToType (F₂.obj (op U))
f' : pullback f (shrinkYonedaEquiv.symm s) ⟶ shrinkYoneda.{w, v, u}.obj U := pullback.snd f (shrinkYonedaEquiv.symm s)
Φ : P.FullSubcategory
hf : Epi (Φ.obj.presheafFiber.map f)
⊢ Epi (Φ.obj.presheafFiber.map f')
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
inst✝ : HasSheafify J (Type w)
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
x✝² x✝¹ : Sheaf J (Type w)
f : x✝² ⟶ x✝¹
x✝ : Mono f
hf : ∀ (i : P.FullSubcategory), IsIso (i.obj.sheafFiber.map f)
⊢ Sheaf.IsLocallySurjective f

Tactic:
exact mk'.isLocallySurjective hP _
            (fun Φ ↦ ((isIso_iff_bijective _).1 (hf Φ)).2)

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
q r : ℚ
heq : q = r
⊢ const (padicNorm p) q ≈ const (padicNorm p) r

Tactic:
by
    rw [heq]

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

Goal state before:
pp: case hbc.h₁.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 (↑f j - ↑(limSeq f j)) < ε / 3

Tactic:
apply mod_cast hN j

Goal state after:
case hbc.h₁.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
⊢ j ≥ N
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
⊢ ∃ N, ∀ i ≥ N, padicNormE (↑f i - x) < ε

Tactic:
obtain ⟨N, hN⟩ := hx ε hε

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (x - ↑f i) < ε
⊢ ∃ N, ∀ i ≥ N, padicNormE (↑f i - x) < ε
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
⊢ (x ^ Int.negSucc n).valuation = Int.negSucc n * x.valuation

Tactic:
simp [← neg_mul]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
⊢ -1 + -↑n = Int.negSucc n ∨ x.valuation = 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ (if 1 = 0 then ⊤ else ↑(valuation 1)) = 0

Tactic:
if_neg one_ne_zero,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑(valuation 1) = 0