mathlib-initiative/mathlib-tactics huggingface dataset:
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 X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
i : I
t : A i ⟶ π₁.left
b : B i ⟶ π₁.right
w : t ≫ π₁.hom = f i ≫ b
⊢ (t ≫ Arrow.Hom.left τ) ≫ Arrow.Hom.left τ' = t ≫ Arrow.Hom.left (τ ≫ τ')

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
hf : W f
⊢ Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm ((equivShrink ↑W.toSet) ⟨Arrow.mk f, hf⟩))).hom

Tactic:
by simp

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

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) val₀ = val₀

Tactic:
by simp

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
inst✝ : SuccOrder J
⊢ sq'.f' ≫ p = F.map (homOfLE ⋯) ≫ c.ι.app (Order.succ j) ≫ g

Tactic:
by simp

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
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g✝ : c.pt ⟶ Y
inst✝ : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ sqFunctor c p f g✝).sections
i i' : ↑(Set.Iio j)
g : i ⟶ i'
⊢ (⋯.functor ⋙ F).map g ≫ (↑s (Opposite.op i')).f' =
    (↑s (Opposite.op i)).f' ≫ ((Functor.const ↑(Set.Iio j)).obj X).map g

Tactic:
have := congr_arg SqStruct.f' (s.2 g.op)
          dsimp at this ⊢
          rw [this, comp_id]

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
⊢ (coproducts.{w, v, u} (ofHoms I.homFamily)).pushouts ≤ (coproducts.{w, v, u} I).pushouts

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ pullback.fst p f ≫ (Iso.refl X).hom =
    (Subobject.underlyingIso (pullback.snd p f)).symm.hom ≫
      (Subobject.underlyingIso (pullback.snd p f)).hom ≫ pullback.fst p f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ pullback.snd p f ≫ (Iso.refl (Opposite.unop (Opposite.op G))).hom =
    (Subobject.underlyingIso (pullback.snd p f)).symm.hom ≫ (Subobject.mk (pullback.snd p f)).arrow

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ pushout.inl (pullback.fst p f) (pullback.snd p f) ≫ (Iso.refl (pushout (pullback.fst p f) (pullback.snd p f))).hom =
    (Iso.refl X).hom ≫ pushout.inl (pullback.fst p f) (pullback.snd p f)

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ pushout.inr (pullback.fst p f) (pullback.snd p f) ≫ (Iso.refl (pushout (pullback.fst p f) (pullback.snd p f))).hom =
    (Iso.refl (Opposite.unop (Opposite.op G))).hom ≫ pushout.inr (pullback.fst p f) (pullback.snd p f)

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ pushout.inl (pullback.fst p f) (pullback.snd p f) ≫ pushout.desc p f ⋯ = p

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
inst✝ : Mono p
f : (coyoneda.obj (Opposite.op G)).obj Y
hf : ∀ (x : (coyoneda.obj (Opposite.op G)).obj X), ¬(ConcreteCategory.hom ((yoneda.map p).app (Opposite.op G))) x = f
⊢ pushout.inr (pullback.fst p f) (pullback.snd p f) ≫ pushout.desc p f ⋯ = f

Tactic:
by simp

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
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ιObj I κ f).incl.app (Order.succ j) ≫ πObj I κ f =
    (relativeCellComplexιObj I κ f).incl.app j ≫ πObj I κ f

Tactic:
by simp

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

Goal state before:
pp: p n : ℕ
⊢ 0 ≤ padicValRat p ↑n

Tactic:
by simp

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

Goal state before:
pp: p n : ℕ
⊢ ↑(padicValNat p n) = padicValRat p ↑n

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
⊢ largerSubobject hG ⊤ = ⊤

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
this : IsIso (largerSubobject hG ⊤).arrow
⊢ (asIso ⊤.arrow).hom ≫ (Arrow.mk (𝟙 X)).hom =
    (Arrow.mk (⊤.ofLE (largerSubobject hG ⊤) ⋯)).hom ≫ (asIso (largerSubobject hG ⊤).arrow).hom

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hJ : HasCardinalLT (Subobject X) (Cardinal.mk J)
⊢ largerSubobject hG ⊤ = ⊤

Tactic:
by simp

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
⊢ ∀ {f_1 : A ⟶ obj I κ f} {g : B ⟶ Y} (sq : CommSq f_1 i (πObj I κ f) g), sq.HasLift

Tactic:
have := hasColimitsOfShape_discrete I κ
  have := hasPushouts I κ
  have := preservesColimit I κ i hi _ (relativeCellComplexιObj I κ f)
  intro g b sq
  obtain ⟨j, t, ht⟩ := Types.jointly_surjective _
    (isColimitOfPreserves (coyoneda.obj (Opposite.op A))
      (relativeCellComplexιObj I κ f).isColimit) g
  dsimp at g b sq t ht
  obtain ⟨l, hl₁, hl₂⟩ := ιFunctorObj_extension' I.homFamily
    ((relativeCellComplexιObj I κ f).incl.app j ≫ πObj I κ f)
    ((relativeCellComplexιObj I κ f).F.map (homOfLE (Order.le_succ j)))
    ((relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫ πObj I κ f) (by simp) (Iso.refl _)
    (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).symm
    (relativeCellComplexιObjFObjSuccIso I κ f j)
    (by dsimp; rw [ιFunctorObj_eq, id_comp])
    (by dsimp; rw [πFunctorObj_eq, assoc, Iso.hom_inv_id_assoc])
    (i := ⟨i, hi⟩) t b (by rw [reassoc_of% ht, sq.w]; dsimp)
  dsimp at hl₁
  exact ⟨⟨{
    l := l ≫ (relativeCellComplexιObj I κ f).incl.app (Order.succ j)
    fac_left := by simp [reassoc_of% hl₁, ← ht]
    fac_right := by rw [assoc, hl₂]
  }⟩⟩

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
hf : I.rlp.llp f
⊢ ιObj I κ f ≫ πObj I κ f = f ≫ 𝟙 Y

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
⊢ padicValRat p q ≤ padicValRat p (q + r)

Tactic:
have hqrd : q.num * r.den + q.den * r.num ≠ 0 := Rat.mk_num_ne_zero_of_ne_zero hqr hqreq

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
h : padicNorm p q = 0
⊢ q = 0

Tactic:
apply by_contradiction; intro hq
  unfold padicNorm at h; rw [if_neg hq] at h
  apply absurd h
  apply zpow_ne_zero
  exact mod_cast hp.1.ne_zero

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ -padicValRat p ↑z ≤ 0

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ emultiplicity ↑p ↑q.den + emultiplicity (↑p) (q.num * ↑r.den) ≤
    emultiplicity (↑p) ((q.num * ↑r.den + ↑q.den * r.num) * ↑q.den)

Tactic:
add_mul

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ emultiplicity ↑p ↑q.den + emultiplicity (↑p) (q.num * ↑r.den) ≤
    emultiplicity (↑p) (q.num * ↑r.den * ↑q.den + ↑q.den * r.num * ↑q.den)
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
k : ℕ
hF : ∀ i ∈ {k}, padicValRat p (F j) < padicValRat p (F i)
⊢ k ∈ {k}

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ 1 ∈ {x | ‖x‖ ≤ 1}

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ 0 ∈ {x | ‖x‖ ≤ 1}

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ_[p]
⊢ ⟨↑k, ⋯⟩ = k

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ
⊢ ↑z1 = ↑z2 ↔ z1 = z2

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖↑p ^ n‖ = ↑p ^ (-↑n)

Tactic:
by simp

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

Goal state before:
pp: case neg
p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
dvd : ¬p ∣ a
⊢ padicValNat p a + p ≤ a

Tactic:
· rw [padicValNat.eq_zero_of_not_dvd dvd]
    lia

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation 0 = 0

Tactic:
by simp [valuation]

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

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

Tactic:
by simp [valuation]

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

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

Tactic:
by simp [valuation]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
hz2 : ‖z2‖ < 1
⊢ ‖z1 * z2‖ = ‖z1‖ * ‖z2‖

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (if 0 = 0 then 0 else exp (-padicValRat p 0)) = 0

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (if 1 = 0 then 0 else exp (-padicValRat p 1)) = 1

Tactic:
by simp

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

Goal state before:
pp: case coe
p : ℕ
hp : Fact (Nat.Prime p)
x : Multiplicative ℤ
⊢ ∃ a, (padicValuation p) a = ↑x

Tactic:
induction x with | ofAdd x
     =>  _ 

Goal state after:
case coe.ofAdd
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ∃ a, (padicValuation p) a = ↑(Multiplicative.ofAdd x)
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
F G : Sheaf J AddCommGrpCat
n : ℕ
f g : F ⟶ G
x : F.H n
⊢ (map (f + g) n) x = (map f n) x + (map g n) x

Tactic:
by
  simp [map, Ext.mk₀_add]

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 : PullbackCone f f
hc : IsLimit c
h : c.fst = c.snd
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
by simp

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 : PullbackCone f f
hc : IsLimit c
a✝ : IsIso c.fst
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
by simp

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
h : c.inl = c.inr
⊢ f ≫ 𝟙 Y = f ≫ 𝟙 Y

Tactic:
by simp

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
⊢ f ≫ 𝟙 Y = f ≫ 𝟙 Y

Tactic:
by simp

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
P Q : Cᵒᵖ ⥤ A
M N : A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
g : P ⟶ Φ.skyscraperPresheaf M
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : Φ.fiber.obj X),
    P.map f.op ≫ g.app (op X) ≫ Pi.π (fun t ↦ M) x =
      g.app (op Y) ≫ Pi.π (fun t ↦ M) ((ConcreteCategory.hom (Φ.fiber.map f)) x)

Tactic:
by simp

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
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
ι : Type u_1
inst✝ : Small.{w, u_1} ι
U : ι → C
f : (i : ι) → U i ⟶ X
hf : Sieve.ofArrows U f ∈ J X
Φ : P.FullSubcategory
Z Y : C
i : ι
p : Z ⟶ U i
z : Φ.obj.fiber.obj Z
⊢ (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) ((ConcreteCategory.hom (Φ.obj.fiber.map p)) z) =
    (ConcreteCategory.hom (Φ.obj.fiber.map (p ≫ f i))) z

Tactic:
by simp

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
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
unfold norm; split_ifs
  -- Porting note: originally `padic_index_simp [hfg, hf, hg]`
  rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
  apply padicNorm.nonarchimedean

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
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : Sieve.ofArrows U f ∈ J X
Φ : P.FullSubcategory
Z Y : C
i : ι
p : Z ⟶ U i
z : Φ.obj.fiber.obj Z
⊢ (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) ((ConcreteCategory.hom (Φ.obj.fiber.map p)) z) =
    (ConcreteCategory.hom (Φ.obj.fiber.map (p ≫ f i))) z

Tactic:
by simp

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
⊢ ∀ (k : ℕ), padicNorm p (↑(-a) k) = padicNorm p (↑a k)

Tactic:
by simp

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

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
Y : Scheme
f : Y ⟶ S
x✝ : Etale f
y : Spec (CommRingCat.of Ω) ⟶ Y
hy : y ≫ f = s
⊢ y default ∈ ⊤

Tactic:
by simp

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

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
Y : Scheme
f : Y ⟶ S
x✝ : Etale f
R : CommRingCat
j : Spec (CommRingCat.of ↑R) ⟶ Y
w✝ : IsOpenImmersion j
y' : Spec (CommRingCat.of Ω) ⟶ Spec (CommRingCat.of ↑R)
hy : (y' ≫ j) ≫ f = s
⊢ ⊤ j

Tactic:
by simp

Goal state after:
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✝ i j k : ι
⊢ yoneda.map (pullback₃.p₂ ⋯ (f j) (f k)) ≫ f j = yoneda.map (pullback₃.p₃ ⋯ (f j) (f k)) ≫ f k

Tactic:
by simp

Goal state after:
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✝ i j k : ι
⊢ yoneda.map (pullback₃.p₂ ⋯ (f j) (f k)) ≫ f j = yoneda.map (pullback₃.p₁ ⋯ (f j) (f k)) ≫ f i

Tactic:
by simp

Goal state after:
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✝ i j k : ι
⊢ (⋯.lift₃ (f k) (f i) (pullback₃.p₂ ⋯ (f j) (f k)) (pullback₃.p₃ ⋯ (f j) (f k)) (pullback₃.p₁ ⋯ (f j) (f k)) ⋯ ⋯ ≫
        pullback.snd (⋯.fst' (f k)) (⋯.fst' (f i))) ≫
      ⋯.fst' (f i) =
    (pullback.fst (⋯.fst' (f j)) (⋯.fst' (f k)) ≫ ⋯.symmetry ⋯) ≫ ⋯.fst' (f i)

Tactic:
by simp

Goal state after:
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✝ i j k : ι
⊢ (⋯.lift₃ (f k) (f i) (pullback₃.p₂ ⋯ (f j) (f k)) (pullback₃.p₃ ⋯ (f j) (f k)) (pullback₃.p₁ ⋯ (f j) (f k)) ⋯ ⋯ ≫
        pullback.snd (⋯.fst' (f k)) (⋯.fst' (f i))) ≫
      ⋯.snd (f i) =
    (pullback.fst (⋯.fst' (f j)) (⋯.fst' (f k)) ≫ ⋯.symmetry ⋯) ≫ ⋯.snd (f i)

Tactic:
by simp

Goal state after:
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✝ i j k : ι
⊢ (⋯.lift₃ (f k) (f i) (pullback₃.p₂ ⋯ (f j) (f k)) (pullback₃.p₃ ⋯ (f j) (f k)) (pullback₃.p₁ ⋯ (f j) (f k)) ⋯ ⋯ ≫
        ⋯.lift₃ (f i) (f j) (pullback₃.p₂ ⋯ (f k) (f i)) (pullback₃.p₃ ⋯ (f k) (f i)) (pullback₃.p₁ ⋯ (f k) (f i)) ⋯ ⋯ ≫
          ⋯.lift₃ (f j) (f k) (pullback₃.p₂ ⋯ (f i) (f j)) (pullback₃.p₃ ⋯ (f i) (f j)) (pullback₃.p₁ ⋯ (f i) (f j)) ⋯
            ⋯) ≫
      pullback₃.p₁ ⋯ (f j) (f k) =
    𝟙 (Limits.pullback (⋯.fst' (f j)) (⋯.fst' (f k))) ≫ pullback₃.p₁ ⋯ (f j) (f k)

Tactic:
by simp

Goal state after:
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✝ i j k : ι
⊢ (⋯.lift₃ (f k) (f i) (pullback₃.p₂ ⋯ (f j) (f k)) (pullback₃.p₃ ⋯ (f j) (f k)) (pullback₃.p₁ ⋯ (f j) (f k)) ⋯ ⋯ ≫
        ⋯.lift₃ (f i) (f j) (pullback₃.p₂ ⋯ (f k) (f i)) (pullback₃.p₃ ⋯ (f k) (f i)) (pullback₃.p₁ ⋯ (f k) (f i)) ⋯ ⋯ ≫
          ⋯.lift₃ (f j) (f k) (pullback₃.p₂ ⋯ (f i) (f j)) (pullback₃.p₃ ⋯ (f i) (f j)) (pullback₃.p₁ ⋯ (f i) (f j)) ⋯
            ⋯) ≫
      pullback₃.p₂ ⋯ (f j) (f k) =
    𝟙 (Limits.pullback (⋯.fst' (f j)) (⋯.fst' (f k))) ≫ pullback₃.p₂ ⋯ (f j) (f k)

Tactic:
by simp

Goal state after: