mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case hR
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
this : F.IsCoverDense J
S : Sieve W := ⋯
T : Sieve W := ⋯
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ W⦄ (H : (Sieve.coverByImage F W).arrows f),
    Sieve.pullback (Nonempty.some H).lift
        (Sieve.functorPushforward F
          (F.imageSieve ((Nonempty.some H).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some H).map ≫ p₂))) ∈
      J Y

Tactic:
intro Y f hf

Goal state after:
case hR
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
i₁ i₂ : data.I₀
W : C
p₁ : W ⟶ F.obj (data.X i₁)
p₂ : W ⟶ F.obj (data.X i₂)
w : p₁ ≫ data.f i₁ = p₂ ≫ data.f i₂
this : F.IsCoverDense J
S : Sieve W :=
  Sieve.bind (Sieve.coverByImage F W).arrows fun Y f hf ↦
    Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂)))
T : Sieve W :=
  Sieve.bind S.arrows fun Z g hg ↦
    Sieve.pullback (Presieve.getFunctorPushforwardStructure ⋯).lift
      (Sieve.functorPushforward F (data.sieve₁₀ (Exists.choose ⋯) (Exists.choose ⋯)))
Y : C
f : Y ⟶ W
hf : (Sieve.coverByImage F W).arrows f
⊢ Sieve.pullback (Nonempty.some hf).lift
      (Sieve.functorPushforward F
        (F.imageSieve ((Nonempty.some hf).map ≫ p₁) ⊓ F.imageSieve ((Nonempty.some hf).map ≫ p₂))) ∈
    J Y
Module: Mathlib.CategoryTheory.Sites.Point.Basic

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
B : Type u''
inst✝⁴ : Category.{v'', u''} B
inst✝³ : HasColimitsOfSize.{w, w, v', u'} A
inst✝² : HasColimitsOfSize.{w, w, v'', u''} B
F : A ⥤ B
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F
X : C
x : Φ.fiber.obj X
P : Cᵒᵖ ⥤ A
⊢ Φ.toPresheafFiber X x (P ⋙ F) ≫ (Φ.presheafFiberCompIso F).hom.app P = F.map (Φ.toPresheafFiber X x P)

Tactic:
have := Functor.Final.preservesColimitsOfShape_of_final
    (FinallySmall.fromFilteredFinalModel.{w} (Φ.fiber.Elementsᵒᵖ)) F
  simp only [presheafFiberCompIso]
  exact ι_preservesColimitIso_inv F ((CategoryOfElements.π Φ.fiber).op ⋙ P) _

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

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
inst✝ : IsEmpty ↥X
⊢ ⊥ ∈ (propQCTopology P) X

Tactic:
rw [← Sieve.generate_bot]
  exact Precoverage.generate_mem_toGrothendieck (bot_mem_propQCPrecoverage X)

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

Goal state before:
pp: case refine_2
X : Scheme
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
⊢ Surjective (Spec.map f) → Presieve.IsSheafFor (yoneda.obj X) (Presieve.singleton (Spec.map f))

Tactic:
hf₂

Goal state after:
case refine_2
X : Scheme
R S : CommRingCat
f : R ⟶ S
hf₁ : Flat (Spec.map f)
hf₂ : Surjective (Spec.map f)
⊢ Presieve.IsSheafFor (yoneda.obj X) (Presieve.singleton (Spec.map f))
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ : C₀
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨Sieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀, ⋯⟩),
    (presheafObjObjIso.inv data G₀ X₀ ≫ presheafObjObjIso.hom data G₀ X₀) ≫ G₀.obj.map I.f.op =
      𝟙 (G₀.obj.obj (op X₀)) ≫ G₀.obj.map I.f.op

Tactic:
rintro ⟨Y₀, a, X, b, c, ⟨i⟩, fac⟩

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₀
a : Y₀ ⟶ X₀
Y : C
i : (data (F.obj X₀)).toPreOneHypercover.I₀
b : F.obj Y₀ ⟶ (data (F.obj X₀)).toPreOneHypercover.X i
fac : b ≫ (data (F.obj X₀)).toPreOneHypercover.f i = F.map a
⊢ (presheafObjObjIso.inv data G₀ X₀ ≫ presheafObjObjIso.hom data G₀ X₀) ≫ G₀.obj.map { Y := Y₀, f := a, hf := ⋯ }.f.op =
    𝟙 (G₀.obj.obj (op X₀)) ≫ G₀.obj.map { Y := Y₀, f := a, hf := ⋯ }.f.op
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₂ ≫ r + x₃ ≫ b = x₂ ≫ r + h₂.lift (-x₂) x₃ fac₃ ≫ t ≫ r

Tactic:
h₁.w,

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
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + h₂.lift (-x₂) x₃ fac₃ ≫ l ≫ b
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

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
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
⊢ Mono f

Tactic:
let α : F ⋙ MonoOver.forget _ ⋙ Over.forget _ ⟶ (Functor.const _).obj X :=
    { app j := (F.obj j).obj.hom }

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
F : J ⥤ MonoOver X
inst✝ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f = (F.obj j).obj.hom
α : F ⋙ MonoOver.forget X ⋙ Over.forget X ⟶ (Functor.const J).obj X :=
  { app := fun j ↦ (F.obj j).obj.hom, naturality := ⋯ }
⊢ Mono f
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

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
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst✝ : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ j, Subobject.mk (F.obj j).obj.hom
⊢ IsColimit ((Over.forget X).mapCocone c)

Tactic:
let f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
    colimit.desc _ (Cocone.mk X
      { app j := (F.obj j).obj.hom
        naturality {j j'} g := by simp [MonoOver.forget] })
  haveI := mono_of_isColimit_monoOver F (colimit.isColimit _) f (by simp [f])
  have := subobjectMk_of_isColimit_eq_iSup F (colimit.isColimit _) f (by simp [f])
  rw [← h] at this
  refine IsColimit.ofIsoColimit (colimit.isColimit _)
    (Cocone.ext (Subobject.isoOfMkEqMk _ _ this) (fun j ↦ ?_))
  rw [← cancel_mono (c.pt.hom)]
  dsimp
  rw [Category.assoc, Subobject.ofMkLEMk_comp, Over.w]
  apply colimit.ι_desc

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

Goal state before:
pp: case neg.succ
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
s : α <i J := f.toPrincipalSeg hf
a : α
hi : ¬IsMax (s.toRelEmbedding a)
a✝ : s.toRelEmbedding a = s.top → HasColimitsOfShape α C
hi₀ : Order.succ (s.toRelEmbedding a) = s.top
⊢ HasColimitsOfShape α C

Tactic:
have : OrderTop α :=
        { top := a
          le_top b := by
            rw [← s.le_iff_le]
            exact Order.le_of_lt_succ (by simpa only [hi₀] using s.lt_top b) }

Goal state after:
case neg.succ
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
s : α <i J := f.toPrincipalSeg hf
a : α
hi : ¬IsMax (s.toRelEmbedding a)
a✝ : s.toRelEmbedding a = s.top → HasColimitsOfShape α C
hi₀ : Order.succ (s.toRelEmbedding a) = s.top
this : OrderTop α
⊢ 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
⊢ (coproducts.{w, v, u} (ofHoms g)).pushouts f

Tactic:
by
  refine ⟨_, _, _, _, _, ?_, c.isPushout⟩
  have : c.m = c.isColimit₁.desc
      (Cocone.mk _ (Discrete.natTrans (fun ⟨i⟩ ↦ by exact g (c.π i)) ≫ c.cofan₂.ι)) :=
    c.isColimit₁.hom_ext (fun ⟨i⟩ ↦ by rw [IsColimit.fac]; exact c.hm i)
  rw [this, coproducts_iff]
  exact ⟨c.ι, ⟨_, _, _, _, c.isColimit₁, c.isColimit₂, _, fun i ↦ ⟨_⟩⟩⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
hf : Φ.prop f
⊢ f = Φ.toSucc X ≫ eqToHom ⋯

Tactic:
by
  cases hf
  simp

Goal state after:
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
⊢ (if h₂ : i₂ < j then (ofCocone.objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (ofCocone.objIso c i₂ h₂).inv
    else
      if h₁ : i₁ < j then (ofCocone.objIso c i₁ h₁).hom ≫ c.ι.app ⟨i₁, h₁⟩ ≫ (ofCocone.objIsoPt c).inv ≫ eqToHom ⋯
      else eqToHom ⋯) =
    (ofCocone.objIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (ofCocone.objIso c i₂ hi₂).inv

Tactic:
rw [dif_pos hi₂]

Goal state after:
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
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (functor hj iter).obj ⟨i, ⋯⟩ = iter'.F.obj ⟨i, hk⟩

Tactic:
dsimp only [functor]
  rw [ofCocone_obj_eq _ _ hi]
  apply congr_obj

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
p : X ⟶ Y
this✝ : LocallySmall.{w, v, u} C
this : IsSmall.{w, v, u} I
⊢ HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C

Tactic:
have := hasCoproducts I κ

Goal state after:
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
p : X ⟶ Y
this✝¹ : LocallySmall.{w, v, u} C
this✝ : IsSmall.{w, v, u} I
this : HasCoproducts C
⊢ HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
⊢ FiniteMultiplicity (↑p) a ↔ a ≠ 0

Tactic:
by
  simp [Int.finiteMultiplicity_iff, hp.1.ne_one]

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

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n : ℕ
ne : p ≠ q
⊢ padicValNat p (q ^ n) = 0

Tactic:
by
  rw [padicValNat.pow _, padicValNat_primes ne, mul_zero]

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

Goal state before:
pp: p n : ℕ
hn : n ≠ 0
t : ℕ
ht : ∃ a < padicValNat p n + 1, p ^ a = t
⊢ t ∈ n.divisors

Tactic:
obtain ⟨k, hk, rfl⟩ := ht

Goal state after:
p n : ℕ
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n + 1
⊢ p ^ k ∈ n.divisors
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
ht : ∃ a < padicValNat p n, p ^ (a + 1) = t
⊢ t ∈ n.divisors.erase 1

Tactic:
obtain ⟨k, hk, rfl⟩ := ht

Goal state after:
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
k : ℕ
hk : k < padicValNat p n
⊢ p ^ (k + 1) ∈ n.divisors.erase 1
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
· exact le_rfl

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

Goal state before:
pp: case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
· exact le_rfl

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

Goal state before:
pp: case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
· exact le_rfl

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

Goal state before:
pp: case refine_2
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 : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
Φ : P.FullSubcategory
x : Φ.obj.fiber.obj X
⊢ ∃ a,
    (ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.desc fun i ↦ shrinkYoneda.{w, v, u}.map (f i)))) a =
      (Φ.obj.shrinkYonedaCompPresheafFiberIso.app X).toEquiv.symm x

Tactic:
obtain ⟨i, y, rfl⟩ := hf Φ x

Goal state after:
case refine_2
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 : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
Φ : P.FullSubcategory
i : ι
y : Φ.obj.fiber.obj (U i)
⊢ ∃ a,
    (ConcreteCategory.hom (Φ.obj.presheafFiber.map (Sigma.desc fun i ↦ shrinkYoneda.{w, v, u}.map (f i)))) a =
      (Φ.obj.shrinkYonedaCompPresheafFiberIso.app X).toEquiv.symm ((ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := ⋯
⊢ stationaryPoint hf ≤ stationaryPoint hf

Tactic:
· exact le_rfl

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

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := ⋯
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ stationaryPoint hg ≤ stationaryPoint hg

Tactic:
· exact le_rfl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : f ≈ 0
this✝ : (f - 0).LimZero
this : f + g ≈ g
h1 : (f + g).norm = g.norm
h2 : f.norm = 0
⊢ (f + g).norm = max f.norm g.norm

Tactic:
rw [h1, h2, max_eq_right (norm_nonneg _)]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ : D
P : MorphismProperty C
inst✝³ : F.Faithful
inst✝² : F.Full
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : D
Y : C
g : F.obj Y ⟶ X
⊢ IsPullback g (F.map (𝟙 Y)) (𝟙 X) g

Tactic:
by simpa using IsPullback.of_id_snd

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁵ : HasBinaryProducts C
inst✝⁴ : HasPullbacks D
inst✝³ : HasBinaryProducts D
inst✝² : HasTerminal D
inst✝¹ : F.Full
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
h : F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
a : C
g : F.obj a ⟶ X
⊢ F.relativelyRepresentable g

Tactic:
intro a'

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁵ : HasBinaryProducts C
inst✝⁴ : HasPullbacks D
inst✝³ : HasBinaryProducts D
inst✝² : HasTerminal D
inst✝¹ : F.Full
inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
h : F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
a : C
g : F.obj a ⟶ X
a' : C
⊢ ∀ (g_1 : F.obj a' ⟶ X), ∃ b snd fst, IsPullback fst (F.map snd) g g_1
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case hbc.h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑(limSeq f j) - ↑f (max N N2)) < ε / 3 + ε / 3

Tactic:
suffices padicNormE (limSeq f j - f j + (f j - f (max N N2)) : ℚ_[p]) < ε / 3 + ε / 3 by
        simpa only [sub_add_sub_cancel]

Goal state after:
case hbc.h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNormE (↑(limSeq f j) - ↑f j + (↑f j - ↑f (max N N2))) < ε / 3 + ε / 3
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case hf
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∀ (j : Fin q),
    ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.natAdd (a + 2) j))) •
        (φ ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 2) j))) ≫ X.σ ⟨a, ⋯⟩ =
      0

Tactic:
rintro ⟨k, hk⟩
    suffices φ ≫ X.δ (⟨a + 2 + k, by lia⟩ : Fin (n + 2)) = 0 by
      simp only [this, Fin.natAdd_mk, Fin.cast_mk, zero_comp, smul_zero]
    convert! v ⟨a + k + 1, by lia⟩ (by rw [Fin.val_mk]; lia)
    dsimp
    lia

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
⊢ φ ≫
      ((AlternatingFaceMapComplex.obj X).d (n + 1) n ≫ hσ' q n (n + 1) ⋯ +
        hσ' q (n + 1) (n + 2) ⋯ ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1)) =
    0

Tactic:
rw [hσ'_eq_zero hqn (c_mk (n + 1) n rfl), comp_zero, zero_add]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
⊢ φ ≫ hσ' q (n + 1) (n + 2) ⋯ ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1) = 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
⊢ PadicSeq.valuation f = PadicSeq.valuation g

Tactic:
by
    by_cases hf : f ≈ 0
    · have hg : g ≈ 0 := Setoid.trans (Setoid.symm h) hf
      simp [hf, hg, PadicSeq.valuation]
    · have hg : ¬g ≈ 0 := fun hg ↦ hf (Setoid.trans h hg)
      rw [PadicSeq.val_eq_iff_norm_eq hf hg]
      exact PadicSeq.norm_equiv h

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: Δ : SimplexCategoryᵒᵖ
A₁ A₂ : IndexSet Δ
h₁ : A₁.fst = A₂.fst
h₂ : A₁.e ≫ eqToHom ⋯ = A₂.e
⊢ A₁ = A₂

Tactic:
rcases A₁ with ⟨Δ₁, ⟨α₁, hα₁⟩⟩

Goal state after:
Δ : SimplexCategoryᵒᵖ
A₂ : IndexSet Δ
Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
h₁ : ⟨Δ₁, ⟨α₁, hα₁⟩⟩.fst = A₂.fst
h₂ : e ⟨Δ₁, ⟨α₁, hα₁⟩⟩ ≫ eqToHom ⋯ = A₂.e
⊢ ⟨Δ₁, ⟨α₁, hα₁⟩⟩ = A₂
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ (({ app := fun X ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ }, naturality := ⋯ } ≫
            { app := fun X ↦ { f := inclusionOfMooreComplexMap X, comm := ⋯ }, naturality := ⋯ }).app
        X).f =
    ((𝟙 N₁).app X).f

Tactic:
simp only [PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap,
      NatTrans.comp_app, Karoubi.comp_f, N₁_obj_p, NatTrans.id_app, Karoubi.id_f]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Δ : SimplexCategoryᵒᵖ
⊢ 𝟙 (X.obj Δ) = ∑ A, s.πSummand A ≫ (s.cofan Δ).inj A

Tactic:
apply s.hom_ext'
  intro A
  dsimp
  erw [comp_id, comp_sum, Finset.sum_eq_single A, cofan_inj_πSummand_eq_id_assoc]
  · intro B _ h₂
    rw [s.cofan_inj_πSummand_eq_zero_assoc _ _ h₂, zero_comp]
  · simp

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

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : ¬j₁ = 0
⊢ PInfty.f (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0

Tactic:
· simp only [op_comp, X.map_comp, assoc, PInfty_f]
      erw [(HigherFacesVanish.of_P _ _).comp_δ_eq_zero_assoc _ hj₁, zero_comp]
      by_contra
      exact hj₁ (by simp only [Fin.ext_iff, Fin.val_zero]; lia)

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x t : ↑I
ht : t ∈ {1}
⊢ {
        toFun := fun x_1 ↦
          if ↑(x, x_1).2 ≤ 1 / 2 then (F.eval (x, x_1).1).extend (2 * ↑(x, x_1).2)
          else (G.eval (x, x_1).1).extend (2 * ↑(x, x_1).2 - 1),
        continuous_toFun := ⋯ }
      t =
    (p₀.trans p₁).toContinuousMap t

Tactic:
Set.mem_singleton_iff

Goal state after:
case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x t : ↑I
ht : t = 1
⊢ {
        toFun := fun x_1 ↦
          if ↑(x, x_1).2 ≤ 1 / 2 then (F.eval (x, x_1).1).extend (2 * ↑(x, x_1).2)
          else (G.eval (x, x_1).1).extend (2 * ↑(x, x_1).2 - 1),
        continuous_toFun := ⋯ }
      t =
    (p₀.trans p₁).toContinuousMap t