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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).toOneHypercover.multicospanShape.L
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).toPreOneHypercover.I₀
c : F.obj X₀ ⟶ (data X).toPreOneHypercover.X j
fac₁ : c ≫ (data X).toPreOneHypercover.f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
⊢ (((lift hG₀ hG s ≫ G.map a.f.op) ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫
        (F.op ⋙ G).map { Y := X₀, f := b, hf := ⋯ }.f.op) ≫
      (F.op ⋙ G).map { Y := Y₀, f := d, hf := ⋯ }.f.op =
    ((s.ι a ≫ ((data a.Y).toOneHypercover.multifork G).ι i) ≫ (F.op ⋙ G).map { Y := X₀, f := b, hf := ⋯ }.f.op) ≫
      (F.op ⋙ G).map { Y := Y₀, f := d, hf := ⋯ }.f.op

Tactic:
dsimp at i j c 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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
⊢ (((lift hG₀ hG s ≫ G.map a.f.op) ≫ G.map ((data a.Y).f i).op) ≫ G.map (F.map b).op) ≫ G.map (F.map d).op =
    ((s.ι a ≫ G.map ((data a.Y).f i).op) ≫ G.map (F.map b).op) ≫ G.map (F.map d).op
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (precoverage P) S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
i : (𝒰.ulift.sum (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover)).I₀
⊢ P ((𝒰.ulift.sum (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover)).f i)

Tactic:
induction i <;> exact 𝒰.map_prop _

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (EffectiveEpiFamilyStruct X π)
⊢ Nonempty (IsColimit (generate (Presieve.ofArrows X π)).arrows.cocone)

Tactic:
rw [Sieve.generateFamily_eq]

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (EffectiveEpiFamilyStruct X π)
⊢ Nonempty (IsColimit (generateFamily X π).arrows.cocone)
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
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
t₁ t₂ : Under j₀
f : t₁ ⟶ t₂
⊢ ((Functor.const (Under j₀)).obj X).map f ≫ y ≫ Y.map t₂.hom = (y ≫ Y.map t₁.hom) ≫ (Under.forget j₀ ⋙ Y).map f

Tactic:
by
    dsimp
    simp only [Category.id_comp, Category.assoc, ← Functor.map_comp, Under.w]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
inst✝¹ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
z : X ⟶ c.pt
this✝¹ : IsFiltered J
this✝ : ∀ (j₀ : J) [inst : HasColimitsOfShape (Under j₀) C] [colim.PreservesMonomorphisms], Mono (c.ι.app j₀)
this : Mono c.ι
j : J
h✝ : IsIso ((F z).obj j).obj.hom
⊢ (pullback.snd c.ι ((Functor.const J).map z)).app j ≫ z =
    (pullback.fst c.ι ((Functor.const J).map z)).app j ≫ c.ι.app j

Tactic:
← NatTrans.comp_app,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
inst✝¹ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
z : X ⟶ c.pt
this✝¹ : IsFiltered J
this✝ : ∀ (j₀ : J) [inst : HasColimitsOfShape (Under j₀) C] [colim.PreservesMonomorphisms], Mono (c.ι.app j₀)
this : Mono c.ι
j : J
h✝ : IsIso ((F z).obj j).obj.hom
⊢ (pullback.snd c.ι ((Functor.const J).map z)).app j ≫ z = (pullback.fst c.ι ((Functor.const J).map z) ≫ c.ι).app j
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 α
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
b : α
⊢ s.toRelEmbedding b ≤ s.toRelEmbedding a

Tactic:
exact Order.le_of_lt_succ (by simpa only [hi₀] using s.lt_top b)

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type w
inst✝² : PartialOrder J✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : ↑(Set.Iio m) → ↑(Set.Iio ↑m) :=
  fun x ↦
    match x with
    | ⟨⟨a, ha⟩, ha'⟩ => ⟨a, ha'⟩
hf : Monotone f
j' : J
hj'✝ : j' ∈ Set.Iio ↑m
hj' : j' < ↑m
h : j < j'
⊢ ⟨j', hj'✝⟩ ≤ ⟨↑⟨⟨j', ⋯⟩, hj'⟩.1, ⋯⟩

Tactic:
by rfl

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

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
⊢ W.transfiniteCompositionsOfShape J ≤ transfiniteCompositions.{w, v, u} W

Tactic:
intro A B f hf

Goal state after:
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
A B : C
f : A ⟶ B
hf : W.transfiniteCompositionsOfShape J f
⊢ transfiniteCompositions.{w, v, u} W f
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 : J
hi : i ≤ j
⊢ i ≤ i

Tactic:
by rfl

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

Goal state before:
pp: case inl.inl.inl
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₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
hi₃' : i₃ < j
⊢ (objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ hi₃').inv =
    (objIso c i₁ ⋯).hom ≫ F.map (homOfLE hi ≫ homOfLE hi') ≫ (objIso c i₃ hi₃').inv

Tactic:
homOfLE_comp

Goal state after:
case inl.inl.inl
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₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
hi₃' : i₃ < j
⊢ (objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ hi₃').inv =
    (objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ hi₃').inv
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: 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
⊢ Order.succ j ≤ Order.succ j

Tactic:
by rfl

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

Goal state before:
pp: 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
⊢ j ≤ j

Tactic:
by rfl

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

Goal state before:
pp: 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
⊢ i ≤ i

Tactic:
by rfl

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₃ : k₂ ≤ j
h₄ : k₂ < j
this : restrictionLE iter₁.F ⋯ = restrictionLE iter₂.F ⋯
⊢ ?m.491 ≤ k₂

Tactic:
by rfl

Goal state after:
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₁ i₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
h₁ : i₃ ≤ j
⊢ (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ (objIso F X ⟨i₃, h₁⟩).inv =
    (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE h₁₂ ≫ homOfLE h₂₃) ≫ (objIso F X ⟨i₃, h₁⟩).inv

Tactic:
homOfLE_comp

Goal state after:
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₁ i₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
h₁ : i₃ ≤ j
⊢ (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ (objIso F X ⟨i₃, h₁⟩).inv =
    (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ (objIso F X ⟨i₃, h₁⟩).inv
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
iter : Φ.Iteration j
k l : J
h : k ≤ l
h' : l ≤ j
⊢ j ≤ j

Tactic:
by rfl

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

Goal state before:
pp: case neg.inl
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₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
⊢ (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ τ ≫ (objSuccIso hj F X).inv =
    (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE h₁₂ ≫ homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv

Tactic:
homOfLE_comp

Goal state after:
case neg.inl
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₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
⊢ (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ τ ≫ (objSuccIso hj F X).inv =
    (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ τ ≫ (objSuccIso hj F X).inv
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
⊢ ⊥ ≤ ⊥

Tactic:
by rfl

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
⊢ i ≤ i

Tactic:
by rfl

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 ⊥)
inst✝ : WellFoundedLT J
i : J
hi : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
⊢ i ≤ i

Tactic:
by rfl

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 ⊥)
inst✝ : WellFoundedLT J
i : J
hi : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
h₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val,
        ⋯⟩
⊢ i ≤ i

Tactic:
by rfl

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

Goal state before:
pp: case inl
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (F.map (homOfLE hij' ≫ homOfLE ⋯).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val,
        ⋯⟩
⊢ (ConcreteCategory.hom (F.map (homOfLE hij✝).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val),
        ⋯⟩

Tactic:
homOfLE_comp

Goal state after:
case inl
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val,
        ⋯⟩
⊢ (ConcreteCategory.hom (F.map (homOfLE hij✝).op)) (d.succ j hj e.val) =
    d.lift i hi
      ⟨fun x ↦
        match x with
        | op ⟨k, hk⟩ => (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val),
        ⋯⟩
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 := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
⊢ sq.HasLift

Tactic:
have hl (j : J) : c.ι.app j ≫ l = (s.1 ⟨j⟩).f' := hc.fac t j

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
hl : ∀ (j : J), c.ι.app j ≫ l = (↑s (Opposite.op j)).f'
⊢ sq.HasLift
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case e'_2
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
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
      (d.lift j hj
        ⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e (Order.succ i) ⋯).val

Tactic:
dsimp
      rw [map_id, id_apply, d.map_lift _ _ _ _ ((Order.IsSuccLimit.succ_lt_iff hj).mpr hi)]

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 ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
⊢ i ≤ i

Tactic:
by rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Additive

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.Additive
Y : D
X✝ Y✝ : Cᵒᵖ
g : X✝ ⟶ Y✝
⊢ ((G ⋙ preadditiveYoneda ⋙ (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj Y).map
        g ≫
      (AddEquiv.ulift.trans ((adj.homAddEquiv (unop Y✝) Y).symm.trans AddEquiv.ulift.symm)).toAddCommGrpIso.hom =
    (AddEquiv.ulift.trans ((adj.homAddEquiv (unop X✝) Y).symm.trans AddEquiv.ulift.symm)).toAddCommGrpIso.hom ≫
      ((preadditiveYoneda ⋙
                (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat).obj F.op ⋙
                  (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).obj
            Y).map
        g

Tactic:
ext ⟨y⟩
        exact AddEquiv.ulift.injective (adj.homEquiv_naturality_left_symm g.unop y)

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

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

Tactic:
padicValRat,

Goal state after:
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ ↑(padicValInt p q.num) - ↑(padicValNat p q.den) = ↑(multiplicity (↑p) q.num) - ↑(multiplicity p q.den)
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖↑n‖ = 1 ↔ p.Coprime n

Tactic:
Padic.norm_natCast_eq_one_iff

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ p.Coprime n ↔ p.Coprime n
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case succ
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n < p → padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
⊢ padicValNat p (p * m + n).succ ! = padicValNat p (p * m)!

Tactic:
factorial_succ,

Goal state after:
case succ
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n < p → padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
⊢ padicValNat p ((p * m + n + 1) * (p * m + n)!) = padicValNat p (p * m)!
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case neg
p : ℕ
a : ℤ
hp : ¬p = 1
⊢ ↑p ^ padicValInt p a ∣ a

Tactic:
padicValInt_dvd_iff_of_ne_one hp

Goal state after:
case neg
p : ℕ
a : ℤ
hp : ¬p = 1
⊢ a = 0 ∨ padicValInt p a ≤ padicValInt p a
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case ha₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ↑p ≠ 1

Tactic:
exact mod_cast (Fact.out : p.Prime).ne_one

Goal state after:
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ c.fst = c.snd → IsIso c.fst

Tactic:
intro h
    obtain ⟨φ, hφ₁, hφ₂⟩ := PullbackCone.IsLimit.lift' hc (𝟙 X) (𝟙 X) (by simp)
    refine ⟨φ, PullbackCone.IsLimit.hom_ext hc ?_ ?_, hφ₁⟩
    · simp only [assoc, hφ₁, id_comp, comp_id]
    · simp only [assoc, hφ₂, id_comp, comp_id, h]

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 : A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
f : P ⟶ Q
g : Φ.presheafFiber.obj Q ⟶ M
⊢ Φ.skyscraperPresheafHomEquiv.symm (Φ.skyscraperPresheafHomEquiv (Φ.presheafFiber.map f ≫ g)) =
    Φ.skyscraperPresheafHomEquiv.symm (f ≫ Φ.skyscraperPresheafHomEquiv g)

Tactic:
simp [Φ.skyscraperPresheafHomEquiv_naturality_left_symm]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this✝ : (f + g - 0).LimZero
this : f ≈ -g
⊢ f.norm = g.norm

Tactic:
have : f.norm = (-g).norm := norm_equiv this

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this✝¹ : (f + g - 0).LimZero
this✝ : f ≈ -g
this : f.norm = (-g).norm
⊢ f.norm = g.norm
Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility

Goal state before:
pp: A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} A'
inst✝¹ : Category.{v_3, u_3} B
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ eB.inverse.map (F.map (eA.unitIso.hom.app (G.obj Y))) ≫
      eB.inverse.map (F.map (eA.inverse.map (hG.inv.app Y))) ≫
        eB.inverse.map (hF.inv.app (eA.inverse.obj (e'.inverse.obj (eB.functor.obj Y)))) ≫
          eB.inverse.map (e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y)))) ≫
            eB.inverse.map (e'.counitIso.hom.app (eB.functor.obj Y)) ≫ eB.unitIso.inv.app Y =
    eB.inverse.map (η.hom.app Y) ≫ eB.unitIso.inv.app Y

Tactic:
simp only [equivalence₂_inverse, comp_obj, ← τ₀_hom_app, hη, τ₁_hom_app, ←
    eB.inverse.map_comp_assoc]

Goal state after:
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} A'
inst✝¹ : Category.{v_3, u_3} B
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ eB.inverse.map
        (F.map (eA.unitIso.hom.app (G.obj Y)) ≫
          F.map (eA.inverse.map (hG.inv.app Y)) ≫
            hF.inv.app (eA.inverse.obj (e'.inverse.obj (eB.functor.obj Y))) ≫
              e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y))) ≫
                e'.functor.map (hG.hom.app Y) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y) ≫
      eB.unitIso.inv.app Y =
    eB.inverse.map (η.hom.app Y) ≫ eB.unitIso.inv.app Y
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ (Hσ q).f 0 = 0

Tactic:
unfold Hσ

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ (nullHomotopicMap' (hσ' q)).f 0 = 0