mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
lift : (s : PullbackCone f g) → s.pt ⟶ t.pt
fac_left : ∀ (s : PullbackCone f g), lift s ≫ t.fst = s.fst
fac_right : ∀ (s : PullbackCone f g), lift s ≫ t.snd = s.snd
s : Cone (cospan f g)
j : WalkingCospan
⊢ lift s ≫ t.π.app none = s.π.app WalkingCospan.left ≫ (cospan f g).map WalkingCospan.Hom.inl

Tactic:
← t.w WalkingCospan.Hom.inl,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
lift : (s : PullbackCone f g) → s.pt ⟶ t.pt
fac_left : ∀ (s : PullbackCone f g), lift s ≫ t.fst = s.fst
fac_right : ∀ (s : PullbackCone f g), lift s ≫ t.snd = s.snd
s : Cone (cospan f g)
j : WalkingCospan
⊢ lift s ≫ t.π.app WalkingCospan.left ≫ (cospan f g).map WalkingCospan.Hom.inl =
    s.π.app WalkingCospan.left ≫ (cospan f g).map WalkingCospan.Hom.inl
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝¹³ : Category.{v₁, u₁} A
inst✝¹² : Category.{v₂, u₂} B
inst✝¹¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝¹⁰ : Category.{v₄, u₄} A'
inst✝⁹ : Category.{v₅, u₅} B'
inst✝⁸ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝⁷ : Category.{v₇, u₇} A''
inst✝⁶ : Category.{v₈, u₈} B''
inst✝⁵ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
A''' : Type u₁₀
B''' : Type u₁₁
C''' : Type u₁₂
inst✝⁴ : Category.{v₁₀, u₁₀} A'''
inst✝³ : Category.{v₁₁, u₁₁} B'''
inst✝² : Category.{v₁₂, u₁₂} C'''
F''' : A''' ⥤ B'''
G''' : C''' ⥤ B'''
ψ✝ ψ'✝ ψ'' : CatCospanTransform F G F' G'
η✝ : ψ✝ ⟶ ψ'✝
η' : ψ'✝ ⟶ ψ''
φ✝ φ'✝ φ'' : CatCospanTransform F' G' F'' G''
θ✝ : φ✝ ⟶ φ'✝
θ' : φ'✝ ⟶ φ''
τ τ' : CatCospanTransform F'' G'' F''' G'''
γ : τ ⟶ τ'
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
inst✝¹ : IsIso η
φ φ' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
inst✝ : IsIso θ
⊢ ψ ◁ inv θ ≫ ψ ◁ θ = 𝟙 (ψ.comp φ')

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
lift : (s : PullbackCone f g) → s.pt ⟶ t.pt
fac_left : ∀ (s : PullbackCone f g), lift s ≫ t.fst = s.fst
fac_right : ∀ (s : PullbackCone f g), lift s ≫ t.snd = s.snd
s : Cone (cospan f g)
j : WalkingCospan
⊢ lift s ≫ t.π.app none = s.π.app none

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W✝ X✝ Y✝ Z✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsWeakLimit t
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ lift ht h k w ≫ t.fst = h ∧ lift ht h k w ≫ t.snd = k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁹ : Category.{v₁, u₁} A
inst✝⁸ : Category.{v₂, u₂} B
inst✝⁷ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁶ : Category.{v₄, u₄} A'
inst✝⁵ : Category.{v₅, u₅} B'
inst✝⁴ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝³ : Category.{v₇, u₇} A''
inst✝² : Category.{v₈, u₈} B''
inst✝¹ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ : CatCospanTransform F G F' G'
φ φ' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
inst✝ : IsIso θ
⊢ inv (ψ ◁ θ) = ψ ◁ inv θ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasWeakLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
⊢ (weakEqualizer.ι (prod.fst ≫ f) (prod.snd ≫ g) ≫ prod.fst) ≫ f =
    (weakEqualizer.ι (prod.fst ≫ f) (prod.snd ≫ g) ≫ prod.snd) ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝¹³ : Category.{v₁, u₁} A
inst✝¹² : Category.{v₂, u₂} B
inst✝¹¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝¹⁰ : Category.{v₄, u₄} A'
inst✝⁹ : Category.{v₅, u₅} B'
inst✝⁸ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝⁷ : Category.{v₇, u₇} A''
inst✝⁶ : Category.{v₈, u₈} B''
inst✝⁵ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
A''' : Type u₁₀
B''' : Type u₁₁
C''' : Type u₁₂
inst✝⁴ : Category.{v₁₀, u₁₀} A'''
inst✝³ : Category.{v₁₁, u₁₁} B'''
inst✝² : Category.{v₁₂, u₁₂} C'''
F''' : A''' ⥤ B'''
G''' : C''' ⥤ B'''
ψ✝ ψ'✝ ψ'' : CatCospanTransform F G F' G'
η✝ : ψ✝ ⟶ ψ'✝
η' : ψ'✝ ⟶ ψ''
φ✝ φ'✝ φ'' : CatCospanTransform F' G' F'' G''
θ✝ : φ✝ ⟶ φ'✝
θ' : φ'✝ ⟶ φ''
τ τ' : CatCospanTransform F'' G'' F''' G'''
γ : τ ⟶ τ'
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
inst✝¹ : IsIso η
φ φ' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
inst✝ : IsIso θ
⊢ η ▷ φ ≫ inv η ▷ φ = 𝟙 (ψ.comp φ)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasWeakLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
s : PullbackCone f g
⊢ prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right) ≫ prod.fst ≫ f =
    prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right) ≫ prod.snd ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝¹³ : Category.{v₁, u₁} A
inst✝¹² : Category.{v₂, u₂} B
inst✝¹¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝¹⁰ : Category.{v₄, u₄} A'
inst✝⁹ : Category.{v₅, u₅} B'
inst✝⁸ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝⁷ : Category.{v₇, u₇} A''
inst✝⁶ : Category.{v₈, u₈} B''
inst✝⁵ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
A''' : Type u₁₀
B''' : Type u₁₁
C''' : Type u₁₂
inst✝⁴ : Category.{v₁₀, u₁₀} A'''
inst✝³ : Category.{v₁₁, u₁₁} B'''
inst✝² : Category.{v₁₂, u₁₂} C'''
F''' : A''' ⥤ B'''
G''' : C''' ⥤ B'''
ψ✝ ψ'✝ ψ'' : CatCospanTransform F G F' G'
η✝ : ψ✝ ⟶ ψ'✝
η' : ψ'✝ ⟶ ψ''
φ✝ φ'✝ φ'' : CatCospanTransform F' G' F'' G''
θ✝ : φ✝ ⟶ φ'✝
θ' : φ'✝ ⟶ φ''
τ τ' : CatCospanTransform F'' G'' F''' G'''
γ : τ ⟶ τ'
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
inst✝¹ : IsIso η
φ φ' : CatCospanTransform F' G' F'' G''
θ : φ ⟶ φ'
inst✝ : IsIso θ
⊢ inv η ▷ φ ≫ η ▷ φ = 𝟙 (ψ'.comp φ)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasWeakLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
⊢ ∀ (s : PullbackCone f g),
    weakEqualizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ ≫
        weakEqualizer.ι (prod.fst ≫ f) (prod.snd ≫ g) ≫ prod.fst =
      s.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasWeakLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
⊢ ∀ (s : PullbackCone f g),
    weakEqualizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) ⋯ ≫
        weakEqualizer.ι (prod.fst ≫ f) (prod.snd ≫ g) ≫ prod.snd =
      s.snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁹ : Category.{v₁, u₁} A
inst✝⁸ : Category.{v₂, u₂} B
inst✝⁷ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁶ : Category.{v₄, u₄} A'
inst✝⁵ : Category.{v₅, u₅} B'
inst✝⁴ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝³ : Category.{v₇, u₇} A''
inst✝² : Category.{v₈, u₈} B''
inst✝¹ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
inst✝ : IsIso η
φ : CatCospanTransform F' G' F'' G''
⊢ inv (η ▷ φ) = inv η ▷ φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
hj : ¬IsMax j
hj' : hf.incl.app j ≫ g₁ = hf.incl.app j ≫ g₂
⊢ (fun g ↦ hf.F.map (homOfLE ⋯) ≫ g) (hf.incl.app (Order.succ j) ≫ g₁) =
    (fun g ↦ hf.F.map (homOfLE ⋯) ≫ g) (hf.incl.app (Order.succ j) ≫ g₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝¹ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
hj : Order.IsSuccLimit j
hj' : ∀ b < j, hf.incl.app b ≫ g₁ = hf.incl.app b ≫ g₂
x✝ : ↑(Set.Iio j)
k : J
hk : k ∈ Set.Iio j
⊢ ((Set.principalSegIio j).cocone hf.F).ι.app ⟨k, hk⟩ ≫ hf.incl.app j ≫ g₁ =
    ((Set.principalSegIio j).cocone hf.F).ι.app ⟨k, hk⟩ ≫ hf.incl.app j ≫ g₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝² : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g✝ : X ⟶ Z
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ hf.F.op ⋙ yoneda.obj Z).sections
x✝¹ x✝ : ↑(Set.Iio j)
g : x✝¹ ⟶ x✝
⊢ (⋯.functor ⋙ hf.F).map g ≫ ↑s (op x✝) = ↑s (op x✝¹) ≫ ((Functor.const ↑(Set.Iio j)).obj Z).map g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g : X ⟶ Z
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ hf.F.op ⋙ yoneda.obj Z).sections
c : Cocone (⋯.functor ⋙ hf.F) := { pt := Z, ι := { app := fun k ↦ ↑s (op k), naturality := ⋯ } }
k : J
hk : k < j
⊢ (ConcreteCategory.hom ((hf.F.op ⋙ yoneda.obj Z).map (homOfLE ⋯).op))
      ((hf.F.isColimitOfIsWellOrderContinuous j hj).desc c) =
    ↑s (op ⟨k, hk⟩)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g : X ⟶ Z
j : J
hj : Order.IsSuccLimit j
s : ↑(⋯.functor.op ⋙ hf.F.op ⋙ yoneda.obj Z).sections
⊢ ∃ y, ∀ (i : J) (hi : i < j), (ConcreteCategory.hom ((hf.F.op ⋙ yoneda.obj Z).map (homOfLE ⋯).op)) y = ↑s (op ⟨i, hi⟩)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
C : Type u'
inst✝ : Category.{v', u'} C
W : J ⥤ Type w
F : J ⥤ C
pt : C
π : ⦃j : J⦄ → W.obj j → (pt ⟶ F.obj j)
hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), π x ≫ F.map f = π ((ConcreteCategory.hom (W.map f)) x)
x₁ x₂ : W.Elements
f : x₁ ⟶ x₂
⊢ ((Functor.const W.Elements).obj pt).map f ≫ π x₂.snd = π x₁.snd ≫ (CategoryOfElements.π W ⋙ F).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
C : Type u'
inst✝ : Category.{v', u'} C
W : J ⥤ Type w
F✝ : J ⥤ C
pt : C
π : ⦃j : J⦄ → W.obj j → (pt ⟶ F✝.obj j)
hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), π x ≫ F✝.map f = π ((ConcreteCategory.hom (W.map f)) x)
F : J ⥤ C
j : J
x✝¹ x✝ : (coyoneda.obj (op j)).Elements
f : x✝¹ ⟶ x✝
⊢ ((Functor.const (coyoneda.obj (op j)).Elements).obj (F.obj j)).map f ≫ F.map x✝.snd =
    F.map x✝¹.snd ≫ (CategoryOfElements.π (coyoneda.obj (op j)) ⋙ F).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f✝ : X ⟶ Y
x✝² : P.isLocal.transfiniteCompositionsOfShape J f✝
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f✝
g : X ⟶ Z
d : (hf.F.op ⋙ yoneda.obj Z).WellOrderInductionData := Functor.WellOrderInductionData.ofExists ⋯ ⋯
σ : ↑(hf.F.op ⋙ yoneda.obj Z).sections := d.sectionsMk (hf.isoBot.hom ≫ g)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ hf.F.map f ≫ ↑σ (op x✝) = ↑σ (op x✝¹) ≫ ((Functor.const J).obj Z).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
C : Type u'
inst✝ : Category.{v', u'} C
W : J ⥤ Type w
F✝ : J ⥤ C
pt : C
π : ⦃j : J⦄ → W.obj j → (pt ⟶ F✝.obj j)
hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), π x ≫ F✝.map f = π ((ConcreteCategory.hom (W.map f)) x)
F : J ⥤ C
j : J
s : Cone (CategoryOfElements.π (coyoneda.obj (op j)) ⋙ F)
x : (coyoneda.obj (op j)).Elements
⊢ (ConcreteCategory.hom ((coyoneda.obj (op j)).map x.snd)) ((coyoneda.obj (op j)).elementsMk j (𝟙 j)).snd = x.snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
C : Type u'
inst✝ : Category.{v', u'} C
W : J ⥤ Type w
F✝ : J ⥤ C
pt : C
π : ⦃j : J⦄ → W.obj j → (pt ⟶ F✝.obj j)
hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), π x ≫ F✝.map f = π ((ConcreteCategory.hom (W.map f)) x)
F : J ⥤ C
j : J
s : Cone (CategoryOfElements.π (coyoneda.obj (op j)) ⋙ F)
x : (coyoneda.obj (op j)).Elements
⊢ WeightedCone.π s (𝟙 j) ≫ (WeightedCone.coyoneda F j).π.app x = s.π.app x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g : X ⟶ Z
d : (hf.F.op ⋙ yoneda.obj Z).WellOrderInductionData := Functor.WellOrderInductionData.ofExists ⋯ ⋯
σ : ↑(hf.F.op ⋙ yoneda.obj Z).sections := d.sectionsMk (hf.isoBot.hom ≫ g)
c : Cocone hf.F := { pt := Z, ι := { app := fun j ↦ ↑σ (op j), naturality := ⋯ } }
⊢ (fun g ↦ f ≫ g) (hf.isColimit.desc c) = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
C : Type u'
inst✝ : Category.{v', u'} C
W : J ⥤ Type w
F✝ : J ⥤ C
pt : C
π : ⦃j : J⦄ → W.obj j → (pt ⟶ F✝.obj j)
hπ : ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂), π x ≫ F✝.map f = π ((ConcreteCategory.hom (W.map f)) x)
F : J ⥤ C
j : J
s : Cone (CategoryOfElements.π (coyoneda.obj (op j)) ⋙ F)
m : s.pt ⟶ (WeightedCone.coyoneda F j).pt
hm : ∀ (j_1 : (coyoneda.obj (op j)).Elements), m ≫ (WeightedCone.coyoneda F j).π.app j_1 = s.π.app j_1
⊢ m = WeightedCone.π s (𝟙 j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝⁴ : Category.{v, u} J
C : Type u'
inst✝³ : Category.{v', u'} C
W W' W'' : J ⥤ Type w
g : W ⟶ W'
g' : W' ⟶ W''
F : J ⥤ C
inst✝² : HasWeightedLimit W F
inst✝¹ : HasWeightedLimit W' F
inst✝ : HasWeightedLimit W'' F
j₁ j₂ : J
x : W.obj j₁
f : j₁ ⟶ j₂
⊢ W.weightedLimObjObjπ F x ≫ F.map f = W.weightedLimObjObjπ F ((ConcreteCategory.hom (W.map f)) x)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
C : Type u'
inst✝¹ : Category.{v', u'} C
W : J ⥤ Type w
F : J ⥤ C
inst✝ : HasWeightedLimit W F
⊢ W.weightedLimObjMap (𝟙 F) = 𝟙 (W.weightedLimObjObj F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝⁴ : Category.{v, u} J
C : Type u'
inst✝³ : Category.{v', u'} C
W : J ⥤ Type w
F₁ F₂ F₃ : J ⥤ C
inst✝² : HasWeightedLimit W F₁
inst✝¹ : HasWeightedLimit W F₂
inst✝ : HasWeightedLimit W F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
⊢ W.weightedLimObjMap (f ≫ g) = W.weightedLimObjMap f ≫ W.weightedLimObjMap g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
⊢ Function.Bijective fun g ↦ f ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝⁴ : Category.{v, u} J
C : Type u'
inst✝³ : Category.{v', u'} C
W W' W'' : J ⥤ Type w
g : W ⟶ W'
g' : W' ⟶ W''
F : J ⥤ C
inst✝² : HasWeightedLimit W F
inst✝¹ : HasWeightedLimit W' F
inst✝ : HasWeightedLimit W'' F
⊢ ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂),
    W'.weightedLimObjObjπ F ((ConcreteCategory.hom (g.app j₁)) x) ≫ F.map f =
      W'.weightedLimObjObjπ F ((ConcreteCategory.hom (g.app j₂)) ((ConcreteCategory.hom (W.map f)) x))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
C : Type u'
inst✝¹ : Category.{v', u'} C
W : J ⥤ Type w
F : J ⥤ C
inst✝ : HasWeightedLimit W F
⊢ weightedLimFlipObjMap (𝟙 W) F = 𝟙 (W.weightedLimObjObj F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit

Goal state before:
pp: J : Type u
inst✝⁴ : Category.{v, u} J
C : Type u'
inst✝³ : Category.{v', u'} C
W W' W'' : J ⥤ Type w
g : W ⟶ W'
g' : W' ⟶ W''
F : J ⥤ C
inst✝² : HasWeightedLimit W F
inst✝¹ : HasWeightedLimit W' F
inst✝ : HasWeightedLimit W'' F
⊢ weightedLimFlipObjMap g' F ≫ weightedLimFlipObjMap g F = weightedLimFlipObjMap (g ≫ g') F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝ : W₂.HasTwoOutOfThreeProperty
⊢ W₂ ≤ W₁.inverseImage ρ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝¹ : Φ.functor.Full
inst✝ : Φ.functor.Faithful
X₁ : C₁
⊢ W₁ ((ι i).app X₁)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝¹ : Φ.functor.Full
inst✝ : Φ.functor.Faithful
X₁ : C₁
⊢ W₁ ((ι i).app X₁)

Tactic:
by
  simpa [hW₁] using hi (Φ.functor.obj X₁)

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝³ : Φ.functor.Full
inst✝² : Φ.functor.Faithful
inst✝¹ : W₂.HasTwoOutOfThreeProperty
inst✝ : W₂.IsMultiplicative
X₂ : C₂
⊢ W₁.IsMultiplicative

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝³ : Φ.functor.Full
inst✝² : Φ.functor.Faithful
inst✝¹ : W₂.HasTwoOutOfThreeProperty
inst✝ : W₂.IsMultiplicative
X₂ : C₂
⊢ IsConnected (Φ.RightResolution X₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝³ : Φ.functor.Full
inst✝² : Φ.functor.Faithful
inst✝¹ : W₂.HasTwoOutOfThreeProperty
inst✝ : W₂.IsMultiplicative
⊢ W₁.IsMultiplicative

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.FiniteProducts

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
J : Type
inst✝³ : HasProductsOfShape J C
inst✝² : W.IsStableUnderProductsOfShape J
inst✝¹ : W.ContainsIdentities
inst✝ : Finite J
⊢ (whiskeringRight (Discrete J) C D).obj L ⋙ limitFunctor L W J ≅ lim ⋙ L

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.FiniteProducts

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
J : Type
inst✝³ : HasProductsOfShape J C
inst✝² : W.IsStableUnderProductsOfShape J
inst✝¹ : W.ContainsIdentities
inst✝ : Finite J
F : Discrete J ⥤ C
⊢ (adj L W J).counit.app (F ⋙ L) =
    (const (Discrete J)).map ((compLimitFunctorIso L W J).hom.app F) ≫
      (compConstIso (Discrete J) L).hom.app (lim.obj F) ≫ whiskerRight (constLimAdj.counit.app F) L

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.FiniteProducts

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
J : Type
inst✝³ : HasProductsOfShape J C
inst✝² : W.IsStableUnderProductsOfShape J
inst✝¹ : W.ContainsIdentities
inst✝ : Finite J
F : Discrete J ⥤ C
⊢ ∀ (j : Discrete J),
    (coneOfAdj (adj L W J) (F ⋙ L)).π.app j =
      ((compLimitFunctorIso L W J).app F).hom ≫ (L.mapCone (limit.cone F)).π.app j

Tactic:
by

Goal state after: