mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S : ShortComplex C
h : S.LeftHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
⊢ (S.map F).f = F.map h.f' ≫ (h.map F).i

Tactic:
map_f,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S : ShortComplex C
h : S.LeftHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
⊢ F.map S.f = F.map h.f' ≫ (h.map F).i
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ π ≫ (isoImage S hkf hcc fac).hom ≫ S.homologyIsoImageICyclesCompPOpcycles.inv =
    (S.isoCyclesOfIsLimit hkf).hom ≫ S.homologyπ

Tactic:
simp [← cancel_mono (S.homologyIsoImageICyclesCompPOpcycles.hom),
    ← cancel_mono (image.ι (S.iCycles ≫ S.pOpcycles)),
    ← reassoc_of% fac]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: S : ShortComplex Ab
x : ↑S.X₁
⊢ (ConcreteCategory.hom 0) x = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: S : ShortComplex Ab
x : ↑S.X₁
⊢ (AddCommGrpCat.Hom.hom ((AddCommGrpCat.kernelIsLimit S.g).lift (Limits.KernelFork.ofι S.f ⋯))) x ∈ S.abToCycles.range

Tactic:
AddMonoidHom.mem_range

Goal state after:
S : ShortComplex Ab
x : ↑S.X₁
⊢ ∃ x_1,
    S.abToCycles x_1 = (AddCommGrpCat.Hom.hom ((AddCommGrpCat.kernelIsLimit S.g).lift (Limits.KernelFork.ofι S.f ⋯))) x
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: S : ShortComplex Ab
x : ↥(AddCommGrpCat.Hom.hom S.g).ker
⊢ (ConcreteCategory.hom S.abLeftHomologyData.i) x = ↑x

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: S : ShortComplex Ab
⊢ Function.Surjective ⇑(ConcreteCategory.hom (AddCommGrpCat.ofHom S.abToCycles)) ↔ Function.Surjective ⇑S.abToCycles

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: S : ShortComplex Ab
⊢ S.Exact ↔ Function.Surjective ⇑S.abToCycles

Tactic:
rw [S.abLeftHomologyData.exact_iff_epi_f', abLeftHomologyData_f',
    AddCommGrpCat.epi_iff_surjective]
  rfl

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: case mp
S : ShortComplex Ab
h : (AddCommGrpCat.Hom.hom S.g).ker ≤ (AddCommGrpCat.Hom.hom S.f).range
x₁ : ↑S.X₁
⊢ (ConcreteCategory.hom 0) x₁ = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: S : ShortComplex Ab
hS : S.Exact
inst✝¹ : Finite ↑S.X₁
inst✝ : Finite ↑S.X₃
this✝ : Finite ↥(AddCommGrpCat.Hom.hom S.f).range
this : Finite (↑S.X₂ ⧸ (AddCommGrpCat.Hom.hom S.f).range)
⊢ Finite ↑S.X₂

Tactic:
exact .of_addSubgroup_quotient (H := S.f.hom.range)

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ S.f = 0 ∧ S.g = 0 → IsZero S.X₂

Tactic:
rintro ⟨hf, hg⟩
    exact hS.isZero_X₂ hf hg

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
⊢ x₂ ≫ S₁.g = 0

Tactic:
by simp only [← cancel_mono φ.τ₃, assoc, zero_comp, ← φ.comm₂₃, reassoc_of% hx₂]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Mono (kernelSequence f).f

Tactic:
by
  dsimp
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Epi (cokernelSequence f).g

Tactic:
by
  dsimp
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: case g.refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.fst ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom k ≫ ((MonoOver.forget Y).obj a).hom ≫ h =
    pullback.fst ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom k ≫
      ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ (((forget A).prod (forget A)).obj (f, g)).1.hom = f.arrow

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ (((forget A).prod (forget A)).obj (f, g)).2.hom = g.arrow

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f₁ a✝ : MonoOver A
⊢ (inf.obj (Quotient.mk'' f₁)).obj (Quotient.mk'' a✝) = (map f₁.arrow).obj ((pullback f₁.arrow).obj (Quotient.mk'' a✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (pullback g).obj (Quotient.mk'' f₁ ⊓ f₂) = (pullback g).obj (Quotient.mk'' f₁) ⊓ (pullback g).obj f₂

Tactic:
erw [inf_def, inf_def, inf_eq_map_pullback', inf_eq_map_pullback', ← pullback_comp, ←
    map_pullback pullback.condition (pullbackIsPullback f₁.arrow g), ← pullback_comp,
    pullback.condition]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map (pullback.snd f₁.arrow g)).obj ((pullback (pullback.snd f₁.arrow g ≫ g)).obj f₂) =
    (map ((MonoOver.pullback g).obj f₁).arrow).obj ((pullback (((MonoOver.pullback g).obj f₁).arrow ≫ g)).obj f₂)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map (pullback.snd f₁.arrow g)).obj ((pullback (pullback.snd f₁.arrow g ≫ g)).obj f₂) =
    (map ((MonoOver.pullback g).obj f₁).arrow).obj ((pullback (((MonoOver.pullback g).obj f₁).arrow ≫ g)).obj f₂)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.FunctorCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (coimage.π α ≫ coimageImageComparison α ≫ image.ι α).app X =
    ((evaluation C D).obj X).map (cokernel.π (kernel.ι α)) ≫
      (coimageImageComparison α).app X ≫ ((evaluation C D).obj X).map (kernel.ι (cokernel.π α))

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
x✝ : Discrete α
⊢ (Discrete.functor (((Discrete.opposite α).inverse ⋙ (Discrete.functor Z).op).obj ∘ Discrete.mk)).obj x✝ ≅
    (Discrete.functor fun x ↦ op (Z x)).obj x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (c.inj j).op = (c.ι.app { as := j }).op

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan Z
f : Fan fun x ↦ op (Z x)
hc : IsColimit c
hf : IsLimit f
c' : Cofan Z
x✝ : Discrete α
j : α
⊢ (c'.ι.app { as := j }).op = (Fan.mk (op c'.pt) fun a ↦ (c'.inj a).op).π.app { as := j }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
x✝ : Discrete α
⊢ (Discrete.functor (((Discrete.opposite α).inverse ⋙ (Discrete.functor Z).op).obj ∘ Discrete.mk)).obj x✝ ≅
    (Discrete.functor fun x ↦ op (Z x)).obj x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f f' : Fan Z
c : Cofan fun x ↦ op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
j : α
⊢ (f'.proj j).op = (f'.π.app { as := j }).op

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f : Fan Z
c : Cofan fun x ↦ op (Z x)
hf : IsLimit f
hc : IsColimit c
f' : Fan Z
x✝ : Discrete α
j : α
⊢ (f'.π.app { as := j }).op = (Cofan.mk (op f'.pt) fun a ↦ (f'.proj a).op).ι.app { as := j }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
this : HasProduct fun x ↦ WalkingPair.casesOn x A B
⊢ WalkingPair.rec (op A) (op B) WalkingPair.left = op (WalkingPair.rec A B WalkingPair.left)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
this : HasProduct fun x ↦ WalkingPair.casesOn x A B
⊢ WalkingPair.rec (op A) (op B) WalkingPair.right = op (WalkingPair.rec A B WalkingPair.right)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: case e'_2
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasColimitsOfShape (Finset (Discrete α)) C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinsetObj F),
        ι := Discrete.natTrans fun j ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    { pt := colimit (liftToFinsetObj F),
                ι :=
                  Discrete.natTrans fun j ↦
                    Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) {j} }.ι.app
          j ≫
        m =
      s.ι.app j
t : Finset (Discrete α)
j : Discrete α
hj : j ∈ t
e_1✝ : ((Discrete.functor fun x ↦ F.obj ↑x).obj { as := ⟨j, hj⟩ } ⟶ s.pt) = (F.obj j ⟶ s.pt)
⊢ colimit.ι (Discrete.functor fun x ↦ F.obj ↑x) { as := ⟨j, hj⟩ } ≫
      colimit.ι
          { obj := fun s ↦ ∐ fun x ↦ F.obj ↑x,
            map := fun {x Y} h ↦ Sigma.desc fun y ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩, map_id := ⋯, map_comp := ⋯ }
          t ≫
        m =
    Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) t ≫ m

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: case e'_2
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
F : Discrete α ⥤ C
s : Cone F
m :
  s.pt ⟶
    { pt := limit (liftToFinsetObj F),
        π := Discrete.natTrans fun j ↦ limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.pt
h :
  ∀ (j : Discrete α),
    m ≫
        { pt := limit (liftToFinsetObj F),
                π :=
                  Discrete.natTrans fun j ↦
                    limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.π.app
          j =
      s.π.app j
t : (Finset (Discrete α))ᵒᵖ
j : Discrete α
hj : j ∈ unop t
e_1✝ : (s.pt ⟶ (Discrete.functor fun x ↦ F.obj ↑x).obj { as := ⟨j, hj⟩ }) = (s.pt ⟶ F.obj j)
⊢ m ≫
      limit.π
          { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
            map_id := ⋯, map_comp := ⋯ }
          t ≫
        limit.π (Discrete.functor fun x ↦ F.obj ↑x) { as := ⟨j, hj⟩ } =
    m ≫ limit.π (liftToFinsetObj F) t ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
Y : C
η : yoneda.obj Y ⟶ A
X : C
s : yoneda.obj X ⟶ A
p : OverArrows η s
⊢ (ConcreteCategory.hom (η.app (op (unop (op X))))) (yonedaEquiv (yoneda.map p.val)) = yonedaEquiv s

Tactic:
yonedaEquiv_yoneda_map

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
Y : C
η : yoneda.obj Y ⟶ A
X : C
s : yoneda.obj X ⟶ A
p : OverArrows η s
⊢ (ConcreteCategory.hom (η.app (op (unop (op X))))) p.val = yonedaEquiv s
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
⊢ t = op (CostructuredArrow.mk (unop t).hom)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Transfer

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive D
F : C ⥤ D
hF : F.FullyFaithful
P Q R : C
f f' : P ⟶ Q
g : Q ⟶ R
⊢ F.map ((f + f') ≫ g) = F.map (f ≫ g + f' ≫ g)

Tactic:
simp [Equiv.add_def]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Transfer

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive D
F : C ⥤ D
hF : F.FullyFaithful
P Q R : C
f : P ⟶ Q
g g' : Q ⟶ R
⊢ F.map (f ≫ (g + g')) = F.map (f ≫ g + f ≫ g')

Tactic:
simp [Equiv.add_def]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Transfer

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive D
F : C ⥤ D
hF : F.FullyFaithful
this : Preadditive C := Preadditive.ofFullyFaithful hF
⊢ ∀ {X Y : C} {f g : X ⟶ Y}, F.map (f + g) = F.map f + F.map g

Tactic:
simp [Equiv.add_def]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E E' : ℰ
g : E ⟶ E'
f : P ⟶ (restrictedULiftYoneda A).obj E
⊢ (restrictedULiftYonedaHomEquiv' A P E').symm (f ≫ (restrictedULiftYoneda A).map g) =
    (restrictedULiftYonedaHomEquiv' A P E).symm f ≫
      (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).map g

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
t : zero = one
⊢ False

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
t : one = zero
⊢ False

Tactic:
grind

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case zero.id
J : Type w
⊢ (fun x ↦
        match x with
        | none => Arrow.mk (𝟙 zero)
        | some none => Arrow.mk (𝟙 one)
        | some (some t) => Arrow.mk (line t))
      ((fun f ↦
          match f.left, f.right, f.hom with
          | zero, .(zero), Hom.id .(zero) => none
          | one, .(one), Hom.id .(one) => some none
          | zero, one, line t => some (some t))
        { left := zero, right := zero, hom := Hom.id ((𝟭 (WalkingParallelFamily J)).obj zero) }) =
    { left := zero, right := zero, hom := Hom.id ((𝟭 (WalkingParallelFamily J)).obj zero) }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case zero.line
J : Type w
a✝ : J
⊢ (fun x ↦
        match x with
        | none => Arrow.mk (𝟙 zero)
        | some none => Arrow.mk (𝟙 one)
        | some (some t) => Arrow.mk (line t))
      ((fun f ↦
          match f.left, f.right, f.hom with
          | zero, .(zero), Hom.id .(zero) => none
          | one, .(one), Hom.id .(one) => some none
          | zero, one, line t => some (some t))
        { left := zero, right := one, hom := line a✝ }) =
    { left := zero, right := one, hom := line a✝ }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case one.id
J : Type w
⊢ (fun x ↦
        match x with
        | none => Arrow.mk (𝟙 zero)
        | some none => Arrow.mk (𝟙 one)
        | some (some t) => Arrow.mk (line t))
      ((fun f ↦
          match f.left, f.right, f.hom with
          | zero, .(zero), Hom.id .(zero) => none
          | one, .(one), Hom.id .(one) => some none
          | zero, one, line t => some (some t))
        { left := one, right := one, hom := Hom.id ((𝟭 (WalkingParallelFamily J)).obj one) }) =
    { left := one, right := one, hom := Hom.id ((𝟭 (WalkingParallelFamily J)).obj one) }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case none
J : Type w
⊢ (fun f ↦
        match f.left, f.right, f.hom with
        | zero, .(zero), Hom.id .(zero) => none
        | one, .(one), Hom.id .(one) => some none
        | zero, one, line t => some (some t))
      ((fun x ↦
          match x with
          | none => Arrow.mk (𝟙 zero)
          | some none => Arrow.mk (𝟙 one)
          | some (some t) => Arrow.mk (line t))
        none) =
    none

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case some.none
J : Type w
⊢ (fun f ↦
        match f.left, f.right, f.hom with
        | zero, .(zero), Hom.id .(zero) => none
        | one, .(one), Hom.id .(one) => some none
        | zero, one, line t => some (some t))
      ((fun x ↦
          match x with
          | none => Arrow.mk (𝟙 zero)
          | some none => Arrow.mk (𝟙 one)
          | some (some t) => Arrow.mk (line t))
        (some none)) =
    some none

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case some.some
J : Type w
val✝ : J
⊢ (fun f ↦
        match f.left, f.right, f.hom with
        | zero, .(zero), Hom.id .(zero) => none
        | one, .(one), Hom.id .(one) => some none
        | zero, one, line t => some (some t))
      ((fun x ↦
          match x with
          | none => Arrow.mk (𝟙 zero)
          | some none => Arrow.mk (𝟙 one)
          | some (some t) => Arrow.mk (line t))
        (some (some val✝))) =
    some (some val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).obj zero =
    ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
          parallelPair (line { down := true }) (line { down := false })).obj
      zero

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).obj one =
    ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
          parallelPair (line { down := true }) (line { down := false })).obj
      one

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
          parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
      WalkingParallelPair.zero =
    (𝟭 WalkingParallelPair).obj WalkingParallelPair.zero

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
          parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
      WalkingParallelPair.one =
    (𝟭 WalkingParallelPair).obj WalkingParallelPair.one

Tactic:
rfl

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : C
x : P.obj (op X)
⊢ uliftYonedaEquiv
      (uliftYonedaEquiv.symm
        ((hom ((G.map (uliftYonedaEquiv.symm x)).app (F.op.obj (op X))))
          ((hom ((φ.app X).app (F.op.obj (op X)))) { down := 𝟙 (unop (F.op.obj (op X))) }))) =
    (hom ((G.map (uliftYonedaEquiv.symm x)).app (op (F.obj X))))
      ((hom ((φ.app X).app (op (F.obj X)))) { down := 𝟙 (F.obj X) })

Tactic:
apply Equiv.apply_symm_apply

Goal state after:
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
x : ↑(S.map colim).X₂
hx : (AddCommGrpCat.Hom.hom (S.map colim).g) x = 0
⊢ x ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range

Tactic:
dsimp at hx

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
x : ↑(S.map colim).X₂
hx : (AddCommGrpCat.Hom.hom (colimMap S.g)) x = 0
⊢ x ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsSeparator G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
hH : ObjectProperty.singleton G G
h : G ⟶ X
⊢ h ≫ f = h ≫ g

Tactic:
exact hfg h

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsCoseparator G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
hH : ObjectProperty.singleton G G
h : Y ⟶ G
⊢ f ≫ h = g ≫ h

Tactic:
exact hfg h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
i : C
f : { as := i } ⟶ { as := i }
⊢ (fun x ↦
        match { as := i }, x with
        | { as := i }, x => ⟨i, x⟩) ∘
      ⇑(ConcreteCategory.hom ((Discrete.functor F).map f)) =
    fun x ↦
    match { as := i }, x with
    | { as := i }, x => ⟨i, x⟩

Tactic:
rfl

Goal state after: