mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝³ : HasWeakSheafify J D
inst✝² : (constantSheaf J D).Faithful
inst✝¹ : (constantSheaf J D).Full
F : Sheaf J D
inst✝ : IsConstant J F
T : C
hT : IsTerminal T
⊢ IsIso ((constantSheafAdj J D hT).counit.app F)

Tactic:
isIso_counit_app_iff_mem_essImage

Goal state after:
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
inst✝³ : HasWeakSheafify J D
inst✝² : (constantSheaf J D).Faithful
inst✝¹ : (constantSheaf J D).Full
F : Sheaf J D
inst✝ : IsConstant J F
T : C
hT : IsTerminal T
⊢ (constantSheaf J D).essImage F
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
right✝ : Finite 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc.sigma
this : IsAffine (𝒰.forgetQc.sigma.X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  (𝒰.forgetQc.sigma.X default).isoSpec.inv ≫ 𝒰.forgetQc.sigma.f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
⊢ Presieve.IsSheafFor F (Presieve.singleton (Spec.map φ))

Tactic:
refine hff _ ?_ ?_

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
right✝ : Finite 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc.sigma
this : IsAffine (𝒰.forgetQc.sigma.X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  (𝒰.forgetQc.sigma.X default).isoSpec.inv ≫ 𝒰.forgetQc.sigma.f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
⊢ P (Spec.map φ)

case refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
R : CommRingCat
𝒰 : Cover (propQCPrecoverage P) (Spec R)
left✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
right✝ : Finite 𝒰.I₀
𝒰' : Cover (precoverage P) (Spec R) := 𝒰.forgetQc.sigma
this : IsAffine (𝒰.forgetQc.sigma.X default)
f : Spec Γ(𝒰.forgetQc.sigma.X default, ⊤) ⟶ Spec R :=
  (𝒰.forgetQc.sigma.X default).isoSpec.inv ≫ 𝒰.forgetQc.sigma.f default
φ : R ⟶ Γ(𝒰.forgetQc.sigma.X default, ⊤)
hφ : Spec.map φ = f
⊢ Surjective (Spec.map φ)
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 ≫ g₁ = c₂.ι.app j ≫ g₂

Tactic:
rw [← cancel_epi (φ.app j), ← reassoc_of% hf, h, reassoc_of% hf]

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

Goal state before:
pp: case refine_1
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)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
Y Z : C
g : Z ⟶ Y
⊢ ((Sieve.ofArrows X c.inj).functor.map (op g) ≫
      ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app (op Z))) (Sieve.ofArrows.h ⋯)) =
    (↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app (op Y))) (Sieve.ofArrows.h ⋯)) ≫
      s.pt.obj.map (op g)

Tactic:
ext u

Goal state after:
case refine_1
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)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
Y Z : C
g : Z ⟶ Y
u : (Sieve.ofArrows X c.inj).functor.obj (op Y)
⊢ (ConcreteCategory.hom
          ((Sieve.ofArrows X c.inj).functor.map (op g) ≫
            ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app (op Z))) (Sieve.ofArrows.h ⋯))).toFun
      u =
    (ConcreteCategory.hom
          ((↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app (op Y))) (Sieve.ofArrows.h ⋯)) ≫
            s.pt.obj.map (op g))).toFun
      u
Module: Mathlib.CategoryTheory.Sites.SubcanonicalOver

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
⊢ (J.over X).Subcanonical

Tactic:
refine .of_isSheaf_yoneda_obj _ fun E Z R hR t ht ↦ ?_
  obtain ⟨ι, T, g, rfl⟩ := R.exists_eq_ofArrows
  let hg : Presieve.Arrows.Compatible (CategoryTheory.yoneda.obj E.left)
      (fun i ↦ (g i).left) (fun i ↦ (t (g i) (Sieve.ofArrows_mk T g i)).left) :=
    fun i j Z gi gj hgij ↦ congr($(ht (Over.homMk (U := Over.mk (gi ≫ (T i).hom)) gi rfl)
      (Over.homMk (U := Over.mk (gi ≫ (T i).hom)) gj
      (by dsimp; rw [← Over.w (g i), reassoc_of% hgij, ← Over.w (g j)]))
      (Sieve.ofArrows_mk _ _ i) (Sieve.ofArrows_mk _ _ j) (by ext; exact hgij)).left)
  rw [J.mem_over_iff, Sieve.ofArrows, Sieve.overEquiv_generate,
    ← Sieve.arrows_generate_map_eq_functorPushforward, Sieve.generate_sieve,
    Presieve.map_ofArrows] at hR
  obtain ⟨a, ha, huniq⟩ := Subcanonical.isSheaf_of_isRepresentable
    (CategoryTheory.yoneda.obj E.left) _ hR _ hg.familyOfElements_compatible.sieveExtend
  refine ⟨?_, ?_, fun y hty ↦ ?_⟩
  · refine Over.homMk a ?_
    refine (Subcanonical.isSheaf_of_isRepresentable <| CategoryTheory.yoneda.obj X)
      (.ofArrows _ <| fun i ↦ (g i).left) hR |>.isSeparatedFor.ext ?_
    rintro W u ⟨V, v, _, ⟨i⟩, rfl⟩
    have := ha _ (Sieve.ofArrows_mk _ _ i)
    dsimp at this
    simp [reassoc_of% this, Presieve.extend_agrees hg.familyOfElements_compatible (.mk i)]
  · rintro W p ⟨V, v, _, ⟨i⟩, rfl⟩
    refine Over.OverMorphism.ext ?_
    have := ha (g i).left (Sieve.ofArrows_mk _ _ i)
    dsimp at this
    simp [Category.assoc, this, Presieve.extend_agrees hg.familyOfElements_compatible (.mk i),
      Presieve.FamilyOfElements.comp_of_compatible _ ht (Sieve.ofArrows_mk _ _ i)]
  · refine Over.OverMorphism.ext (huniq _ ?_)
    rintro W p ⟨V, v, _, ⟨i⟩, rfl⟩
    have := congr($(hty _ (Sieve.ofArrows_mk _ _ i)).left)
    dsimp at this
    simp [Presieve.FamilyOfElements.comp_of_compatible _
      hg.familyOfElements_compatible.sieveExtend (Sieve.ofArrows_mk _ _ i),
      Presieve.extend_agrees hg.familyOfElements_compatible (.mk i), this]

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
inst✝¹ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
z : X ⟶ c.pt
this✝¹ : IsFiltered J
this✝ : ∀ (j₀ : J) [inst : HasColimitsOfShape (Under j₀) C] [colim.PreservesMonomorphisms], Mono (c.ι.app j₀)
this : Mono c.ι
⊢ ∃ j₀ y, z = y ≫ c.ι.app j₀

Tactic:
obtain ⟨j, _⟩ := exists_isIso_of_functor_from_monoOver (F z) hXκ _
    (colimit.isColimit _) (f z) (hf z) (epi_f hc z)

Goal state after:
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
inst✝¹ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
z : X ⟶ c.pt
this✝¹ : IsFiltered J
this✝ : ∀ (j₀ : J) [inst : HasColimitsOfShape (Under j₀) C] [colim.PreservesMonomorphisms], Mono (c.ι.app j₀)
this : Mono c.ι
j : J
h✝ : IsIso ((F z).obj j).obj.hom
⊢ ∃ j₀ y, z = y ≫ c.ι.app j₀
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: case he
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
Y : C
h : Presieve.IsSheaf J (CategoryTheory.uliftYoneda.{v', v, u}.obj Y)
⊢ ∀ ⦃X Y_1 : C⦄ (f : X ⟶ Y_1) (x : (CategoryTheory.yoneda.obj Y).obj (op Y_1)),
    Equiv.ulift.symm ((ConcreteCategory.hom ((CategoryTheory.yoneda.obj Y).map f.op)) x) =
      (ConcreteCategory.hom ((CategoryTheory.uliftYoneda.{v', v, u}.obj Y).map f.op)) (Equiv.ulift.symm x)

Tactic:
· intros
      rfl

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

Goal state before:
pp: case pos
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
⊢ ∃ x, ∃ (_ : b < x), x < ↑m

Tactic:
have := hm.2 ⟨b, hb'⟩

Goal state after:
case pos
J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
this : ¬⟨b, hb'⟩ ⋖ m
⊢ ∃ x, ∃ (_ : b < x), x < ↑m
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : PartialOrder J
j : J
F : ↑(Set.Iic j) ⥤ C
i : J
hi : i ≤ j
k₁ k₂ : ↑(Set.Iio i)
φ : k₁ ⟶ k₂
⊢ ⋯.functor.obj k₁ ≤ ⋯.functor.obj k₂

Tactic:
by simpa using leOfHom φ

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : PartialOrder J
j : J
F : ↑(Set.Iic j) ⥤ C
i : J
hi : i ≤ j
k₁ k₂ : ↑(Set.Iic i)
φ : k₁ ⟶ k₂
⊢ ⋯.functor.obj k₁ ≤ ⋯.functor.obj k₂

Tactic:
by simpa using leOfHom φ

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : i < j
⊢ Φ.prop (iter.F.map (homOfLE ⋯))

Tactic:
prop_iff,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : i < j
⊢ Arrow.mk (iter.F.map (homOfLE ⋯)) = Φ.toSuccArrow (iter.F.obj ⟨i, ⋯⟩)
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
i : J
hi : Order.IsSuccLimit i
⊢ IsColimit ((Set.principalSegIio i).cocone (Φ.iterationFunctor J))

Tactic:
let e : (Set.principalSegIio i).monotone.functor ⋙
      (Φ.iterationFunctor J) ≅ restrictionLT (Φ.iter i).F (by simp) :=
      NatIso.ofComponents (fun _ ↦ eqToIso (Φ.iterationFunctor_obj _ _ _)) (by
        rintro ⟨k₁, h₁⟩ ⟨k₂, h₂⟩ f
        apply Arrow.mk_injective
        simpa using! Φ.arrowMk_iterationFunctor_map k₁ k₂ (leOfHom f) (Φ.iter i) h₂.le)
    refine (IsColimit.precomposeInvEquiv e _).1 ?_
    refine IsColimit.ofIsoColimit ((Φ.iter i).isColimit i hi (by simp)) ?_
    refine Cocone.ext (eqToIso (Φ.iterationFunctor_obj i (Φ.iter i) (by simp)).symm) ?_
    rintro ⟨k, hk⟩
    apply Arrow.mk_injective
    simp [Φ.arrowMk_iterationFunctor_map k i hk.le (Φ.iter i) (by simp), e]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : LinearOrder J
inst✝ : OrderBot J
F : J ⥤ C
c : Cocone F
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
j : J
sq' : SqStruct c p f g j
⊢ f ≫ p = c.ι.app ⊥ ≫ g

Tactic:
rw [← sq'.w₁, assoc, sq'.w₂, Cocone.w_assoc]

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

Goal state before:
pp: case isMin
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi : IsMin i
⊢ Nonempty (d.Extension val₀ i)

Tactic:
obtain rfl : i = ⊥ := by simpa using hi
    exact ⟨zero d val₀⟩

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
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r

Tactic:
have hr' : r.num /. r.den ≠ 0 := by rwa [Rat.num_divInt_den]

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
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ padicNorm p ↑z ≤ 1

Tactic:
· rw [padicNorm, if_neg (mod_cast hz)]
    exact zpow_le_one_of_nonpos₀ (mod_cast hp.1.one_le) (by simp)

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

Goal state before:
pp: 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
⊢ padicNorm p (q + r) ≤ padicNorm p q

Tactic:
by simpa [hqr] using hnqp

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

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ↑p ^ (-↑k) < ε

Tactic:
rw [← inv_lt_inv₀ hε (zpow_pos _ _)]

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ε⁻¹ < (↑p ^ (-↑k))⁻¹

p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ 0 < ↑p
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ (Int.padicValuation p) x.num / (Int.padicValuation p) ↑x.den ≤ 1 ↔ (Int.padicValuation p) ↑x.den = 1

Tactic:
div_le_one₀

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ (Int.padicValuation p) x.num ≤ (Int.padicValuation p) ↑x.den ↔ (Int.padicValuation p) ↑x.den = 1

p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ 0 < (Int.padicValuation p) ↑x.den
Module: Mathlib.NumberTheory.Padics.PadicIntegers

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

Tactic:
norm_le_pow_iff_norm_lt_pow_add_one

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ ↑p ∣ x
⊢ ‖x‖ < 1 ↔ ‖x‖ < ↑p ^ (-↑1 + 1)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
a : ℤ
⊢ ↑p ^ padicValInt p a ∣ a

Tactic:
by_cases hp : p = 1
  · rw [hp, Nat.cast_one, one_pow]; exact one_dvd _
  rw [padicValInt_dvd_iff_of_ne_one hp]
  exact Or.inr le_rfl

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
⊢ padicNorm p (↑(f + g) (max (stationaryPoint hfg) (max ?v2✝ ?v3✝))) ≤
    max (padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3))))
      (padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg)))))

pp: case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ

pp: case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ

pp: case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ

pp: case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ

pp: case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ

pp: case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ

Tactic:
apply padicNorm.nonarchimedean

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝³ : Category.{v', u'} A
inst✝² : HasProducts A
inst✝¹ : HasColimitsOfSize.{w, w, v', u'} A
inst✝ : HasWeakSheafify J A
⊢ ∀ {X Y : Cᵒᵖ ⥤ A} (f : X ⟶ Y),
    Φ.presheafFiber.map f ≫ (asIso (Φ.presheafFiber.map (CategoryTheory.toSheafify J Y))).hom =
      (asIso (Φ.presheafFiber.map (CategoryTheory.toSheafify J X))).hom ≫ (presheafToSheaf J A ⋙ Φ.sheafFiber).map f

Tactic:
simp [sheafFiber, ← Functor.map_comp]

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

Goal state before:
pp: 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
⊢ ∃ i, ∀ j ≥ i, padicNorm p (limSeq f j - limSeq f i) < ε

Tactic:
let ⟨N2, hN2⟩ := f.cauchy₂ hε3

Goal state after:
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
⊢ ∃ i, ∀ j ≥ i, padicNorm p (limSeq f j - limSeq f i) < ε
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : ⟦f⟧ ≠ 0
this : ¬f ≈ 0
n : ℤ
hn : PadicSeq.norm f = ↑p ^ (-n)
⊢ ‖⟦f⟧‖ = ↑(↑p ^ (-n))

Tactic:
rw [← hn]; rfl

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

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ (P q).f (n + 1) ≫ (P q).f (n + 1) = (P q).f (n + 1)

Tactic:
exact (HigherFacesVanish.of_P q n).comp_P_eq_self

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ G.map (𝟙 (X _⦋n⦌)) = (P q).f n + (Q q).f n

Tactic:
P_add_Q_f

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ G.map (𝟙 (X _⦋n⦌)) = 𝟙 (((whiskering C D).obj G).obj X _⦋n⦌)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : x = 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation

Tactic:
· simpa only [hx, zero_add] using min_le_right _ _

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation
Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom = Γ₂N₁.hom

Tactic:
rw [← cancel_epi Γ₂N₁.inv, Iso.inv_hom_id]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Γ₂N₁.inv ≫ (Compatibility.υ toKaroubiCompN₂IsoN₁).hom = 𝟙 (N₁ ⋙ Γ₂)
Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₂ToKaroubiIso.inv.app X ≫
      Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X) ≫
        Γ₂N₂.hom.app ((toKaroubi (SimplicialObject C)).obj X) ≫ Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app X) =
    𝟙 (Γ₂.obj (N₁.obj X))

Tactic:
rw [← NatTrans.comp_app_assoc, ← Γ₂N₂_inv, Iso.inv_hom_id, NatTrans.id_app, id_comp,
    Γ₂N₂ToKaroubiIso_inv_app, ← Γ₂.map_comp, Iso.inv_hom_id_app, Γ₂.map_id]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.ReflQuiver

Goal state before:
pp: V : Type u
inst✝¹ : ReflQuiver V
W : Type u₂
inst✝ : ReflQuiver W
F G : ReflPrefunctor V W
h_obj : ∀ (X : V), F.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Eq.recOn ⋯ (Eq.recOn ⋯ (G.map f))
⊢ F = G

Tactic:
obtain ⟨⟨F_obj⟩⟩ := F
  obtain ⟨⟨G_obj⟩⟩ := G
  obtain rfl : F_obj = G_obj := (Set.eqOn_univ F_obj G_obj).mp fun _ _ ↦ h_obj _
  congr
  funext X Y f
  simpa using h_map X Y f

Goal state after: