mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Sites.Etale

Goal state before:
pp: Ω : 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 Ω
k : CommRingCat := (𝒰.X i).residueField y
m : S.residueField ((𝒰.f i) y) ⟶ (𝒰.X i).residueField y := Hom.residueFieldMap (𝒰.f i) y
algInst✝¹ : Algebra ↑(S.residueField ((𝒰.f i) y)) ↑((𝒰.X i).residueField y) :=
  (CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y)).toAlgebra
algInst✝ : Algebra ↑(S.residueField ((𝒰.f i) y)) ↑(CommRingCat.of Ω) := (CommRingCat.Hom.hom a).toAlgebra
⊢ ∃ y_1,
    (ConcreteCategory.hom ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).map (𝒰.f i))) y_1 =
      (SpecToEquivOfField Ω S).symm ⟨(𝒰.f i) y, a⟩

Tactic:
let b : (𝒰.X i).residueField y →ₐ[S.residueField (𝒰.f i y)] Ω :=
      IsSepClosed.lift

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 Ω
k : CommRingCat := (𝒰.X i).residueField y
m : S.residueField ((𝒰.f i) y) ⟶ (𝒰.X i).residueField y := Hom.residueFieldMap (𝒰.f i) y
algInst✝¹ : Algebra ↑(S.residueField ((𝒰.f i) y)) ↑((𝒰.X i).residueField y) :=
  (CommRingCat.Hom.hom (Hom.residueFieldMap (𝒰.f i) y)).toAlgebra
algInst✝ : Algebra ↑(S.residueField ((𝒰.f i) y)) ↑(CommRingCat.of Ω) := (CommRingCat.Hom.hom a).toAlgebra
b : ↑((𝒰.X i).residueField y) →ₐ[↑(S.residueField ((𝒰.f i) y))] Ω := IsSepClosed.lift
⊢ ∃ y_1,
    (ConcreteCategory.hom ((coyoneda.obj (Opposite.op (Spec (CommRingCat.of Ω)))).map (𝒰.f i))) y_1 =
      (SpecToEquivOfField Ω S).symm ⟨(𝒰.f i) y, a⟩
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) [IsIso f], P.property (PreZeroHypercover.singleton f)
S T : C
f : S ⟶ T
hf : IsIso f
⊢ (PreZeroHypercover.singleton f).presieve₀ ∈ P.precoverage.coverings T

Tactic:
refine .mk _ (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
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
⊢ restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫ G₀.obj.map x₂.op =
    presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫
      IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc) ≫ G₀.obj.map a.op

Tactic:
IsDenseSubsite.mapPreimage_map_of_fac J F G₀ _ _ x₁ fac₁.symm

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
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
⊢ restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫ G₀.obj.map x₂.op =
    presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ G₀.obj.map x₁.op
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₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ (F.map p₂ ≫ Sieve.ofArrows.h hb) ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map (p₁ ≫ a)

Tactic:
by rw [assoc, hb', fac, map_comp]

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

Goal state before:
pp: case refine_2.refine_3
T : Type v
inst✝ : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap ⇑(Spec.map f)
x : C(↥(Spec S), T)
h :
  ∀ {Z : Scheme} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      (ConcreteCategory.hom ((continuousMapPresheaf T).map p₁.op)) x =
        (ConcreteCategory.hom ((continuousMapPresheaf T).map p₂.op)) x
y : (continuousMapPresheaf T).obj (Opposite.op (Spec R))
⊢ (fun y ↦ (ConcreteCategory.hom ((continuousMapPresheaf T).map (Spec.map f).op)) y = x) y → y = this.lift x ⋯

Tactic:
hy

Goal state after:
case refine_2.refine_3
T : Type v
inst✝ : TopologicalSpace T
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
this : Topology.IsQuotientMap ⇑(Spec.map f)
x : C(↥(Spec S), T)
h :
  ∀ {Z : Scheme} (p₁ p₂ : Z ⟶ Spec S),
    p₁ ≫ Spec.map f = p₂ ≫ Spec.map f →
      (ConcreteCategory.hom ((continuousMapPresheaf T).map p₁.op)) x =
        (ConcreteCategory.hom ((continuousMapPresheaf T).map p₂.op)) x
y : (continuousMapPresheaf T).obj (Opposite.op (Spec R))
hy : (ConcreteCategory.hom ((continuousMapPresheaf T).map (Spec.map f).op)) y = x
⊢ y = this.lift x ⋯
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
⊢ x₂ ≫ r' + x₃ ≫ b ≫ k = 0

Tactic:
← fac₁,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
⊢ x₂ ≫ r ≫ k + x₃ ≫ b ≫ k = 0
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ ∃ x₂', π ≫ x₄ = x₂' ≫ r

Tactic:
refine ⟨x₂ + h₂.lift (-x₂) x₃ fac₃ ≫ t, ?_⟩
      rw [eq, Preadditive.add_comp, assoc, h₁.w, IsPullback.lift_snd_assoc, add_comm]

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₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
⊢ y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀

Tactic:
hy

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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
j₀ : J
y₁ y₂ : X ⟶ Y.obj j₀
hy : y₁ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
⊢ y₂ ≫ c.ι.app j₀ = y₂ ≫ c.ι.app j₀
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
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
sq : CommSq f (c.ι.app ⊥) p g
s : ↑(sqFunctor c p f g).sections
hs : (↑s (Opposite.op ⊥)).f' = f
t : Cocone F := { pt := X, ι := { app := fun j ↦ (↑s (Opposite.op j)).f', naturality := ⋯ } }
⊢ sq.HasLift

Tactic:
let l := hc.desc t

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
sq : CommSq f (c.ι.app ⊥) p g
s : ↑(sqFunctor c p f g).sections
hs : (↑s (Opposite.op ⊥)).f' = f
t : Cocone F := { pt := X, ι := { app := fun j ↦ (↑s (Opposite.op j)).f', naturality := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
⊢ sq.HasLift
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
X Y : C
f : X ⟶ Y
h : W.llp.TransfiniteCompositionOfShape J f
this : W.llp (h.incl.app ⊥)
⊢ W.llp f

Tactic:
exact (MorphismProperty.arrow_mk_iso_iff _
    (Arrow.isoMk h.isoBot.symm (Iso.refl _))).2 this

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

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

Tactic:
apply Int.multiplicity_natAbs

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

Goal state before:
pp: p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ ↑(multiplicity (↑p) q.num) - ↑(padicValNat p q.den) = ↑(multiplicity (↑p) q.num) - ↑(multiplicity p q.den)

Tactic:
padicValNat_def' hp q.den_ne_zero

Goal state after:
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ ↑(multiplicity (↑p) q.num) - ↑(multiplicity p q.den) = ↑(multiplicity (↑p) q.num) - ↑(multiplicity p q.den)
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 κ
⊢ I.rlp.llp = (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts

Tactic:
by
  refine le_antisymm ?_
    (retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp I)
  rw [llp_rlp_of_isCardinalForSmallObjectArgument' I κ]
  apply retracts_monotone
  apply transfiniteCompositionsOfShape_le_transfiniteCompositions

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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ ↑(p ^ n) ∣ z ↔ ↑n ≤ ↑(multiplicity (↑p) z)

pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ z ≠ 0

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ 1 < ↑p

Tactic:
· norm_cast
      rw [← FiniteMultiplicity.pow_dvd_iff_le_multiplicity]
      · norm_cast
      · apply Int.finiteMultiplicity_iff.2 ⟨by simp [hp.out.ne_one], mod_cast hz⟩

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ z ≠ 0

case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
hz : ¬↑z = 0
⊢ 1 < ↑p
Module: Mathlib.NumberTheory.Padics.PadicNorm

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

Tactic:
inv_lt_one₀

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

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

Goal state before:
pp: p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ (p - 1) * padicValNat p (n + k)! - (p - 1) * padicValNat p (k ! * (n + k - k)!) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
padicValNat.mul (factorial_ne_zero _) (factorial_ne_zero _),

Goal state after:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ (p - 1) * padicValNat p (n + k)! - (p - 1) * (padicValNat p k ! + padicValNat p (n + k - k)!) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p k n : ℕ
hp : Fact (Nat.Prime p)
⊢ (p - 1) * padicValNat p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
by
  have h : k ≤ n + k := by exact Nat.le_add_left k n
  simp only [Nat.choose_eq_factorial_div_factorial h]
  rw [padicValNat.div_of_dvd <| factorial_mul_factorial_dvd_factorial h, Nat.mul_sub_left_distrib,
      padicValNat.mul (factorial_ne_zero _) (factorial_ne_zero _), Nat.mul_add]
  simp only [sub_one_mul_padicValNat_factorial]
  rw [← Nat.sub_add_comm <| digit_sum_le p k, Nat.add_sub_cancel n k, ← Nat.add_sub_assoc <|
      digit_sum_le p n, Nat.sub_sub (k + n), ← Nat.sub_right_comm, Nat.sub_sub, sub_add_eq,
      add_comm, tsub_tsub_assoc (Nat.le_refl (k + n)) <| (add_comm k n) ▸ (Nat.add_le_add
      (digit_sum_le p n) (digit_sum_le p k)), Nat.sub_self (k + n), zero_add, add_comm]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
a : ℤ
⊢ ↑p ^ n ∣ ↑a ↔ ↑p ^ n ∣ a

Tactic:
rw [← Nat.cast_pow, ← norm_int_le_pow_iff_dvd, norm_le_pow_iff_mem_span_pow,
    Ideal.mem_span_singleton, Nat.cast_pow]

Goal state after:
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
hf : c.fst = c.snd
Z : C
g g' : Z ⟶ X
h : g ≫ f = g' ≫ f
⊢ g = g'

Tactic:
obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' hc g g' h

Goal state after:
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
hf : c.fst = c.snd
Z : C
φ : Z ⟶ c.pt
h : (φ ≫ c.fst) ≫ f = (φ ≫ c.snd) ≫ f
⊢ φ ≫ c.fst = φ ≫ c.snd
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
⊢ IsIso ((presheafToSheaf J A).map f) ↔ ∀ (Φ : P.FullSubcategory), IsIso (Φ.obj.presheafFiber.map f)

Tactic:
(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.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j✝ k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
mem :
  Sieve.ofArrows (glueData hf).openCover.X (glueData hf).openCover.f ∈
    (grothendieckTopology IsOpenImmersion) (glueData hf).glued
V : Scheme
γ : V ⟶ U
Y✝ : Scheme
i : (glueData hf).openCover.I₀
a : V ⟶ (glueData hf).openCover.X i
fac₁ : a ≫ (glueData hf).openCover.f i = γ ≫ α
Y : Scheme
j : (glueData hf).openCover.I₀
b : V ⟶ (glueData hf).openCover.X j
fac₂ : b ≫ (glueData hf).openCover.f j = γ ≫ β
h :
  (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (γ ≫ α) =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (γ ≫ β)
⊢ γ ≫ α = γ ≫ β

Tactic:
← fac₁,

Goal state after:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j✝ k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
mem :
  Sieve.ofArrows (glueData hf).openCover.X (glueData hf).openCover.f ∈
    (grothendieckTopology IsOpenImmersion) (glueData hf).glued
V : Scheme
γ : V ⟶ U
Y✝ : Scheme
i : (glueData hf).openCover.I₀
a : V ⟶ (glueData hf).openCover.X i
fac₁ : a ≫ (glueData hf).openCover.f i = γ ≫ α
Y : Scheme
j : (glueData hf).openCover.I₀
b : V ⟶ (glueData hf).openCover.X j
fac₂ : b ≫ (glueData hf).openCover.f j = γ ≫ β
h :
  (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (a ≫ (glueData hf).openCover.f i) =
    (ConcreteCategory.hom ((yonedaGluedToSheaf hf).hom.app (op V))) (γ ≫ β)
⊢ a ≫ (glueData hf).openCover.f i = γ ≫ β
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ ‖x - y‖ = ‖y - x‖

Tactic:
have : y - x = (-1) * (x - y) := by ring

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ℚ_[p]
this : y - x = -1 * (x - y)
⊢ ‖x - y‖ = ‖y - x‖
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : n = 0
⊢ ‖↑{ num := n, den := d, den_nz := hn, reduced := hd }‖ ≤ 1

Tactic:
by
      have : (⟨n, d, hn, hd⟩ : ℚ) = 0 := Rat.zero_iff_num_zero.mpr hnz
      norm_num [this]

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 x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
q : ℕ
hq : (alternatingFaceMapComplex C).map f ≫ P q = P q ≫ (alternatingFaceMapComplex C).map f
⊢ P q ≫ (alternatingFaceMapComplex C).map f + P q ≫ (alternatingFaceMapComplex C).map f ≫ Hσ q =
    P q ≫ (alternatingFaceMapComplex C).map f + P q ≫ Hσ q ≫ (alternatingFaceMapComplex C).map f

Tactic:
erw [(natTransHσ q).naturality f]

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
q : ℕ
hq : (alternatingFaceMapComplex C).map f ≫ P q = P q ≫ (alternatingFaceMapComplex C).map f
⊢ P q ≫ (alternatingFaceMapComplex C).map f + P q ≫ (natTransHσ q).app x✝¹ ≫ (alternatingFaceMapComplex C).map f =
    P q ≫ (alternatingFaceMapComplex C).map f + P q ≫ Hσ q ≫ (alternatingFaceMapComplex C).map f
Module: Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ 𝟙 K[X] + P q ≫ 0 = 𝟙 K[X]

Tactic:
simp only [add_zero, comp_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
n : ι
⊢ P.p.f n ≫ P.p.f n = P.p.f n

Tactic:
simpa only [HomologicalComplex.comp_f] using HomologicalComplex.congr_hom P.idem n

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ e ≫ i = (A.e.op ≫ θ).unop ≫ 𝟙 (unop (op (unop A.fst)))

Tactic:
rw [comp_id, fac]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ θ.unop ≫ A.e = (A.e.op ≫ θ).unop
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ N₁Γ₀.inv.app K =
    (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫ (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom

Tactic:
change (N₁Γ₀.app K).inv = _
  simp only [N₁Γ₀_app]
  rfl

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
inst✝ : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
⊢ ((splitting K).cofan Δ).inj A ≫ (obj K).map θ =
    Termwise.mapMono K (image.ι (θ.unop ≫ A.e)) ≫ ((splitting K).cofan Δ').inj (A.pull θ)

Tactic:
apply Obj.map_on_summand
  apply image.fac

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
hx : ↑x ≤ 2⁻¹
⊢ p ⟨if ↑x ≤ 1 / 2 then ↑1 * 2 * ↑x else ↑1 * (2 - 2 * ↑x), ⋯⟩ =
    { toFun := (fun t ↦ if t ≤ 1 / 2 then p.extend (2 * t) else p.symm.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯ }
      x

Tactic:
simp [hx, ← extend_apply]

Goal state after: