mathlib-initiative/mathlib-tactics huggingface dataset:
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 : F.obj W₀ ⟶ F.obj X₀
i : (data (F.obj X₀)).I₀
p : F.obj W₀ ⟶ F.obj ((data (F.obj X₀)).X i)
fac : p ≫ (data (F.obj X₀)).f i = a
⊢ hom data G₀ X₀ ≫ IsDenseSubsite.mapPreimage J F G₀ a =
    presheafObjπ data G₀ (F.obj X₀) i ≫ IsDenseSubsite.mapPreimage J F G₀ p

Tactic:
by
  refine Presheaf.IsSheaf.hom_ext G₀.property
      ⟨_, IsDenseSubsite.imageSieve_mem J₀ J F a⟩ _ _ ?_
  rintro ⟨T₀, b, ⟨c, hc⟩⟩
  dsimp
  simp only [assoc, IsDenseSubsite.mapPreimage_comp_map, ← hc,
    IsDenseSubsite.mapPreimage_map]
  exact hom_map data G₀ c _ (by simp only [assoc, fac, hc])

Goal state after:
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₄
sq : IsPushout t l r b
⊢ Epi (kernel.map t b l r ⋯)

Tactic:
rw [epi_iff_surjective_up_to_refinements]

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₄
sq : IsPushout t l r b
⊢ ∀ ⦃A : C⦄ (y : A ⟶ kernel b), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ kernel.map t b l r ⋯
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
F F' : Sheaf J (Type v)
f : F ⟶ F'
x : F.obj.obj (op X)
⊢ J.yonedaEquiv.symm x ≫ f = J.yonedaEquiv.symm ((ConcreteCategory.hom (f.hom.app (op X))) x)

Tactic:
by
  apply J.yonedaEquiv.injective
  simp [yonedaEquiv_comp]

Goal state after:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : ¬IsMax i
j : Fin (n + 1)
⊢ i < j ↔ lastCases (last n) succ i ≤ j

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last (by simpa using! hi)
        simp [castSucc_lt_iff_succ_le]

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

Goal state before:
pp: case refine_3
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)
m : (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).pt ⟶ s.pt
hm : ∀ (j : ι), (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).inj j ≫ m = s.inj j
Y : Cᵒᵖ
g : unop Y ⟶ c.pt
hg : (Sieve.ofArrows X c.inj).arrows g
⊢ (ConcreteCategory.hom (((Sieve.ofArrows X c.inj).functorInclusion ≫ m.hom).app Y)).toFun ⟨g, hg⟩ =
    (ConcreteCategory.hom
          ({
                app := fun Y ↦
                  ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
                naturality := ⋯ }.app
            Y)).toFun
      ⟨g, hg⟩

Tactic:
simp [← hm (Sieve.ofArrows.i hg)]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
⊢ HasColimitsOfShape α C

Tactic:
by_cases hf : Function.Surjective f

Goal state after:
case pos
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : Function.Surjective ⇑f
⊢ HasColimitsOfShape α C

case neg
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
⊢ HasColimitsOfShape α C
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
Z : C
φ φ' : X₂ ⟶ Z
h₀ : f ≫ φ = f ≫ φ'
h : ∀ (i : c.ι), c.cell i ≫ φ = c.cell i ≫ φ'
⊢ φ = φ'

Tactic:
apply c.isPushout.hom_ext h₀

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
Z : C
φ φ' : X₂ ⟶ Z
h₀ : f ≫ φ = f ≫ φ'
h : ∀ (i : c.ι), c.cell i ≫ φ = c.cell i ≫ φ'
⊢ c.g₂ ≫ φ = c.g₂ ≫ φ'
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: case inl
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
n : ℕ
F : ComposableArrows C n
j : Fin n
hj : ¬IsMax j.castSucc
hF : Arrow.mk (F.map (homOfLE ⋯)) ∈ W.toSet
eq : Arrow.mk (homOfLE ⋯) = Arrow.mk (homOfLE ⋯)
⊢ Arrow.mk ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯)) ∈ W.toSet

Tactic:
replace eq := congr_arg F.mapArrow.obj eq

Goal state after:
case inl
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
n : ℕ
F : ComposableArrows C n
j : Fin n
hj : ¬IsMax j.castSucc
hF : Arrow.mk (F.map (homOfLE ⋯)) ∈ W.toSet
eq : (Functor.mapArrow F).obj (Arrow.mk (homOfLE ⋯)) = (Functor.mapArrow F).obj (Arrow.mk (homOfLE ⋯))
⊢ Arrow.mk ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯)) ∈ W.toSet
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
ι : Type w
X Y : C
F₁ F₂ : Discrete ι ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
φ : F₁ ⟶ F₂
hφ : (ofHoms g).functorCategory (Discrete ι) φ
g₁ : c₁.pt ⟶ X₁
g₂ : { pt := c₂.pt, ι := φ ≫ c₂.ι }.pt ⟶ X₂
sq : IsPushout g₁ (h₁.desc { pt := c₂.pt, ι := φ ≫ c₂.ι }) f g₂
⊢ Nonempty (AttachCells g f)

Tactic:
let π (i : ι) : α := ((ofHoms_iff _ _).1 (hφ ⟨i⟩)).choose

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
ι : Type w
X Y : C
F₁ F₂ : Discrete ι ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
φ : F₁ ⟶ F₂
hφ : (ofHoms g).functorCategory (Discrete ι) φ
g₁ : c₁.pt ⟶ X₁
g₂ : { pt := c₂.pt, ι := φ ≫ c₂.ι }.pt ⟶ X₂
sq : IsPushout g₁ (h₁.desc { pt := c₂.pt, ι := φ ≫ c₂.ι }) f g₂
π : ι → α := fun i ↦ ⋯.choose
⊢ Nonempty (AttachCells g f)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i : J
hi : i ≤ Order.succ j
h₁ : i ≤ j
⊢ (if h₁ : i ≤ j then (objIso F X ⟨i, ⋯⟩).hom ≫ F.map (𝟙 ⟨i, ⋯⟩) ≫ (objIso F X ⟨i, h₁⟩).inv
    else
      if h₂ : i ≤ j then (objIso F X ⟨i, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv ≫ eqToHom ⋯
      else 𝟙 (obj F X ⟨i, ⋯⟩)) =
    𝟙 (obj F X ⟨i, ⋯⟩)

pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i : J
hi : i ≤ Order.succ j
h₁ : ¬i ≤ j
⊢ (if h₁ : i ≤ j then (objIso F X ⟨i, ⋯⟩).hom ≫ F.map (𝟙 ⟨i, ⋯⟩) ≫ (objIso F X ⟨i, h₁⟩).inv
    else
      if h₂ : i ≤ j then (objIso F X ⟨i, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv ≫ eqToHom ⋯
      else 𝟙 (obj F X ⟨i, ⋯⟩)) =
    𝟙 (obj F X ⟨i, ⋯⟩)

Tactic:
· rw [dif_pos h₁, CategoryTheory.Functor.map_id, id_comp, Iso.hom_inv_id]

Goal state after:
case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i : J
hi : i ≤ Order.succ j
h₁ : ¬i ≤ j
⊢ (if h₁ : i ≤ j then (objIso F X ⟨i, ⋯⟩).hom ≫ F.map (𝟙 ⟨i, ⋯⟩) ≫ (objIso F X ⟨i, h₁⟩).inv
    else
      if h₂ : i ≤ j then (objIso F X ⟨i, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv ≫ eqToHom ⋯
      else 𝟙 (obj F X ⟨i, ⋯⟩)) =
    𝟙 (obj F X ⟨i, ⋯⟩)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ < j
⊢ (ofCocone c).map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).hom = (ofCoconeObjIso c i₁ ⋯).hom ≫ F.map (homOfLE hi)

Tactic:
ofCocone_map c i₁ i₂ hi hi₂,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ < j
⊢ ((ofCoconeObjIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv) ≫ (ofCoconeObjIso c i₂ hi₂).hom =
    (ofCoconeObjIso c i₁ ⋯).hom ≫ F.map (homOfLE hi)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: 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
x✝ : J
h : x✝ < ⊥
⊢ arrowSucc ((Functor.const ↑(Set.Iic ⊥)).obj Φ.X₀) x✝ h =
    Φ.toSuccArrow (((Functor.const ↑(Set.Iic ⊥)).obj Φ.X₀).obj ⟨x✝, ⋯⟩)

Tactic:
simp at h

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
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
⊢ arrowMap (functor hj iter) k i ⋯ hij = arrowι (restrictionLT (functor hj iter) hij) hi k hk

Tactic:
· rw [arrowMap_functor_to_top _ _ _ hk, ← arrowι_def _ hi]
      congr 1
      apply Arrow.functor_ext
      rintro ⟨l₁, hl₁⟩ ⟨l₂, hl₂⟩ f
      dsimp
      generalize_proofs
      rw [← arrowMap, arrow_mk_mapObj, arrowMap_functor _ _ _ _ _ hl₂, arrow_mk_mapObj]

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

Goal state before:
pp: case succ
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 : ¬IsMax i
hi' : Subsingleton (d.Extension val₀ i)
e₁ e₂ : d.Extension val₀ (Order.succ i)
h₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val =
    d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val)
⊢ e₁.val = e₂.val

Tactic:
have h₂ := e₂.map_succ i (Order.lt_succ_of_not_isMax hi)

Goal state after:
case succ
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 : ¬IsMax i
hi' : Subsingleton (d.Extension val₀ i)
e₁ e₂ : d.Extension val₀ (Order.succ i)
h₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val =
    d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val)
h₂ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val =
    d.succ i ⋯ ((ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val)
⊢ e₁.val = e₂.val
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : 1 < p
⊢ padicValRat p ↑p = 1

Tactic:
simp [hp]

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

Goal state before:
pp: case h
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X A✝ : C
f : A✝ ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
⊢ ∃ A', ∃ (h : Subobject.mk f < A'), (generatingMonomorphisms G).pushouts ((Subobject.mk f).ofLE A' ⋯)

Tactic:
| _ f
   => 

Goal state after:
case h
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X A✝ : C
f : A✝ ⟶ X
inst✝ : Mono f
hA : Subobject.mk f ≠ ⊤
⊢ ∃ A', ∃ (h : Subobject.mk f < A'), (generatingMonomorphisms G).pushouts ((Subobject.mk f).ofLE A' ⋯)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ y : ℤ_[p]
x✝ : ↥(nonZeroDivisors ℤ_[p])
x : ℤ_[p]
hx : x ∈ nonZeroDivisors ℤ_[p]
⊢ IsUnit ↑↑⟨x, hx⟩

Tactic:
isUnit_iff_ne_zero,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ y : ℤ_[p]
x✝ : ↥(nonZeroDivisors ℤ_[p])
x : ℤ_[p]
hx : x ∈ nonZeroDivisors ℤ_[p]
⊢ ↑↑⟨x, hx⟩ ≠ 0
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
ha_norm : ‖a‖ = 1
⊢ ∃ x_1, x * (algebraMap ℤ_[p] ℚ_[p]) ↑x_1.2 = (algebraMap ℤ_[p] ℚ_[p]) x_1.1

Tactic:
use
        (⟨a, le_of_eq ha_norm⟩,
          ⟨(p ^ n : ℤ_[p]), mem_nonZeroDivisors_iff_ne_zero.mpr (NeZero.ne _)⟩)

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖x‖ ≤ 1
n : ℕ := ⋯
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := ⋯
ha : a = x * ↑p ^ n
ha_norm : ‖a‖ = 1
⊢ x * (algebraMap ℤ_[p] ℚ_[p]) ↑(⟨a, ⋯⟩, ⟨↑p ^ n, ⋯⟩).2 = (algebraMap ℤ_[p] ℚ_[p]) (⟨a, ⋯⟩, ⟨↑p ^ n, ⋯⟩).1
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y x✝ y✝ : ℤ_[p]
h : x✝ = y✝
⊢ ↑1 * x✝ = ↑1 * y✝

Tactic:
by rw [h]

Goal state after:
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
hfg : f ≈ g
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
⊢ False

Tactic:
have : padicNorm p (f i) < padicNorm p (f i) := by
    apply lt_of_lt_of_le hN'
    apply sub_le_self
    apply padicNorm.nonneg

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN : ∀ j ≥ N, padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
this : padicNorm p (↑f i) < padicNorm p (↑f i)
⊢ False
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
⊢ f.norm = g.norm

Tactic:
have hg : g ≈ 0 := Setoid.trans (Setoid.symm hfg) hf

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : f ≈ 0
hg : g ≈ 0
⊢ f.norm = g.norm
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
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
m : s.pt ⟶ ((Φ.skyscraperPresheaf M).mapCone R.arrows.cocone.op).pt
hm :
  ∀ (j : R.arrows.categoryᵒᵖ),
    (m ≫ Pi.map' ⇑(ConcreteCategory.hom (Φ.fiber.map (unop j).obj.hom)) fun x ↦ 𝟙 M) = s.π.app j
⊢ m = ⋯.choose

Tactic:
ext x

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasProducts A
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
m : s.pt ⟶ ((Φ.skyscraperPresheaf M).mapCone R.arrows.cocone.op).pt
hm :
  ∀ (j : R.arrows.categoryᵒᵖ),
    (m ≫ Pi.map' ⇑(ConcreteCategory.hom (Φ.fiber.map (unop j).obj.hom)) fun x ↦ 𝟙 M) = s.π.app j
x : unop (Φ.fiber.op.obj R.arrows.cocone.op.pt)
⊢ m ≫ Pi.π (fun t ↦ M) x = ⋯.choose ≫ Pi.π (fun t ↦ M) x
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
q r : ℚ
h : q = r
⊢ ↑q = ↑r

Tactic:
by rw [h]

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

Goal state before:
pp: ι : Type u_1
S : Scheme
Ω : ι → Type u
inst✝¹ : (i : ι) → Field (Ω i)
inst✝ : ∀ (i : ι), IsSepClosed (Ω i)
s : (i : ι) → Spec (CommRingCat.of (Ω i)) ⟶ S
hs : ⋃ i, Set.range ⇑(s i) = Set.univ
X : S.Etale
α : Type (u + 1)
T : α → S.Etale
f : (i : α) → T i ⟶ X
hR :
  ∀ (Φ : (ObjectProperty.ofObj fun i ↦ pointSmallEtale (s i)).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : (Sieve.ofArrows T f).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
⊢ ⋃ i, Set.range ⇑(f i).left = Set.univ

Tactic:
ext x

Goal state after:
ι : Type u_1
S : Scheme
Ω : ι → Type u
inst✝¹ : (i : ι) → Field (Ω i)
inst✝ : ∀ (i : ι), IsSepClosed (Ω i)
s : (i : ι) → Spec (CommRingCat.of (Ω i)) ⟶ S
hs : ⋃ i, Set.range ⇑(s i) = Set.univ
X : S.Etale
α : Type (u + 1)
T : α → S.Etale
f : (i : α) → T i ⟶ X
hR :
  ∀ (Φ : (ObjectProperty.ofObj fun i ↦ pointSmallEtale (s i)).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : (Sieve.ofArrows T f).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
x : ↥X.left
⊢ x ∈ ⋃ i, Set.range ⇑(f i).left ↔ x ∈ Set.univ
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ (((-1) ^ 0 • X.σ ⟨0, ⋯⟩) ≫ eqToHom ⋯) ≫ K[X].d 1 0 = 0

Tactic:
suffices X.σ 0 ≫ X.δ 0 + -X.σ 0 ≫ X.δ 1 = 0 by simpa

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ X.σ 0 ≫ X.δ 0 + -X.σ 0 ≫ X.δ 1 = 0
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f n ≫ PInfty.f n = PInfty.f n

Tactic:
simp only [PInfty_f, P_f_idem]

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

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
⊢ ⟦f⟧ ≠ 0 → ‖⟦f⟧‖ = ↑p ^ (-valuation ⟦f⟧)

Tactic:
| _ f
   => 

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
⊢ ⟦f⟧ ≠ 0 → ‖⟦f⟧‖ = ↑p ^ (-valuation ⟦f⟧)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: case mpr
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (unop Δ).len ≤ (unop A.fst).len → (unop A.fst).len = (unop Δ).len

Tactic:
· exact le_antisymm (len_le_of_epi A.e)

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

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h✝ : ¬Δ = Δ'
⊢ K.X Δ.len ⟶ K.X Δ'.len

Tactic:
by_cases Isδ₀ i

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h✝¹ : ¬Δ = Δ'
h✝ : Isδ₀ i
⊢ K.X Δ.len ⟶ K.X Δ'.len

case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h✝¹ : ¬Δ = Δ'
h✝ : ¬Isδ₀ i
⊢ K.X Δ.len ⟶ K.X Δ'.len
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
⊢ Φ₁.f = Φ₂.f

Tactic:
by rw [h]

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
⊢ Sigma.ι (summand K Δ) A ≫ map K θ = Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)

Tactic:
simp only [map, colimit.ι_desc, Cofan.mk_ι_app]

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
⊢ Termwise.mapMono K (image.ι (θ.unop ≫ A.e)) ≫ Sigma.ι (summand K Δ') (A.pull θ) =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)
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
⊢ ((splitting K).cofan Δ).inj A ≫ (obj K).map θ =
    Termwise.mapMono K i ≫ ((splitting K).cofan Δ').inj (Splitting.IndexSet.mk e)

Tactic:
by
  dsimp [Splitting.cofan]
  change (_ ≫ (Γ₀.obj K).map A.e.op) ≫ (Γ₀.obj K).map θ = _
  rw [assoc, ← Functor.map_comp]
  dsimp [splitting]
  rw [Γ₀.Obj.map_on_summand₀ K (Splitting.IndexSet.id A.1)
    (show e ≫ i = ((Splitting.IndexSet.e A).op ≫ θ).unop ≫ 𝟙 _ by rw [comp_id, fac]; rfl)]
  dsimp only [Splitting.IndexSet.id_fst, Splitting.IndexSet.mk, op_unop, Splitting.IndexSet.e]
  rw [Γ₀.Obj.map_on_summand₀ K (Splitting.IndexSet.id (op Δ''))
      (show e ≫ 𝟙 Δ'' = e.op.unop ≫ 𝟙 _ by simp), Termwise.mapMono_id]
  dsimp only [Splitting.IndexSet.id_fst]
  rw [id_comp]
  rfl

Goal state after: