mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
hF h₂ : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map✝ : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
⊢ { preimage := f₁, map_preimage := hf₁, preimage_map := preimage_map✝ } = h₂

Tactic:
| mk f₁ hf₁ _ =>

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : ∀ (X Y : C), Function.Bijective F.map
this✝ : F.Faithful
this : F.Full
⊢ Nonempty F.FullyFaithful

Tactic:
exact ⟨.ofFullyFaithful _⟩

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (𝟙 (e.inverse.obj Y)))

pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

pp: case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)

pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))

pp: case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))

Tactic:
map_id,

Goal state after:
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (𝟙 (e.functor.obj (e.inverse.obj Y)))

case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)

case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))

case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
⊢ G = F

Tactic:
fapply Functor.ext

Goal state after:
case h_obj
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
⊢ ∀ (X : Discrete I), G.obj X = F.obj X

case h_map
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
G F : Discrete I ⥤ C
h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }
⊢ autoParam (∀ (X Y : Discrete I) (f : X ⟶ Y), G.map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯) Functor.ext._auto_1
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ (f.inv ≫ f.hom) i = 𝟙 (Y i)

Tactic:
Iso.inv_hom_id,

Goal state after:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ 𝟙 Y i = 𝟙 (Y i)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
E : Type u_2
inst✝ : Category.{v_2, u_2} E
P : MorphismProperty C
F : C ⥤ D
G : D ⥤ E
X✝ Y✝ : E
f✝ : X✝ ⟶ Y✝
⊢ (P.strictMap F).strictMap G f✝ ↔ P.strictMap (F ⋙ G) f✝

Tactic:
exact ⟨fun ⟨⟨h⟩⟩ ↦ ⟨h⟩, fun ⟨h⟩ ↦ ⟨⟨h⟩⟩⟩

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

Goal state before:
pp: A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F₁.EssSurj
inst✝³ : F₂.EssSurj
inst✝² : F.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X : Comma L' R'
⊢ L'.map (F₁.objObjPreimageIso X.left).hom ≫ X.hom =
    L'.map (F₁.objObjPreimageIso X.left).hom ≫
      X.hom ≫ R'.map ((F₂.objObjPreimageIso X.right).inv ≫ (F₂.objObjPreimageIso X.right).hom)

Tactic:
Iso.inv_hom_id,

Goal state after:
A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F₁.EssSurj
inst✝³ : F₂.EssSurj
inst✝² : F.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X : Comma L' R'
⊢ L'.map (F₁.objObjPreimageIso X.left).hom ≫ X.hom =
    L'.map (F₁.objObjPreimageIso X.left).hom ≫ X.hom ≫ R'.map (𝟙 X.right)
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : (ConcreteCategory.hom f) g₁ = (ConcreteCategory.hom f) g₂
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
t1 : asHom g₁ = asHom g₂
⊢ g₁ = g₂

Tactic:
apply asHom_injective t1

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget CommRingCat).map f)

Goal state after:
X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
i : (forget CommRingCat).obj X ≅ (forget CommRingCat).obj Y := asIso ((forget CommRingCat).map f)
⊢ IsIso f
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: X : Type u
⊢ Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X))) = 𝟭 (Discrete X)

Tactic:
fapply Functor.ext

Goal state after:
case h_obj
X : Type u
⊢ ∀ (X_1 : Discrete X),
    (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X)))).obj X_1 = (𝟭 (Discrete X)).obj X_1

case h_map
X : Type u
⊢ autoParam
    (∀ (X_1 Y : Discrete X) (f : X_1 ⟶ Y),
      (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X)))).map f =
        eqToHom ⋯ ≫ (𝟭 (Discrete X)).map f ≫ eqToHom ⋯)
    ext._auto_1
Module: Mathlib.CategoryTheory.LiftingProperties.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Opposite.op Y ⟶ Opposite.op B
g : Opposite.op X ⟶ Opposite.op A
sq : CommSq f p.op i.op g
⊢ sq.HasLift

Tactic:
simp only [CommSq.HasLift.iff_unop, Quiver.Hom.unop_op]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Opposite.op Y ⟶ Opposite.op B
g : Opposite.op X ⟶ Opposite.op A
sq : CommSq f p.op i.op g
⊢ ⋯.HasLift
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ c.π.app j✝ ≫ α.app j✝ = lift G ((Cone.postcompose α).obj c) ≫ π G j✝

Tactic:
limit.lift_π

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ c.π.app j✝ ≫ α.app j✝ = ((Cone.postcompose α).obj c).π.app j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
j✝ : J
⊢ G.map (c.π.app j✝) = lift (F ⋙ G) (G.mapCone c) ≫ π (F ⋙ G) j✝

Tactic:
limit.lift_π

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
j✝ : J
⊢ G.map (c.π.app j✝) = (G.mapCone c).π.app j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
⊢ H.map (post F G) ≫ post (F ⋙ G) H = post F (G ⋙ H)

Tactic:
have : HasLimit (F ⋙ G ⋙ H) := h
  ext; erw [assoc, limit.post_π, ← H.map_comp, limit.post_π, limit.post_π]; rfl

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

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
⊢ H.map (post F G) ≫ post (F ⋙ G) H = post F (G ⋙ H)

Tactic:
by
  have : HasLimit (F ⋙ G ⋙ H) := h
  ext; erw [assoc, limit.post_π, ← H.map_comp, limit.post_π, limit.post_π]; rfl

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
j : WidePushoutShape J
⊢ F.obj j = (wideSpan (F.obj none) (fun j ↦ F.obj (some j)) fun j ↦ F.map (Hom.init j)).obj j

Tactic:
cases j; repeat rfl

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

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Over X
φ : f✝ ⟶ g✝
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
⊢ l ≫ f.hom = (mk (m ≫ f.hom)).hom

Tactic:
by
        dsimp; rw [← Over.w k, ← Category.assoc, congrArg (· ≫ g.hom) a, Category.assoc]

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

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ map (f ≫ g) = map g ⋙ map f

Tactic:
fapply Functor.ext

Goal state after:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (X_1 : Under Z), (map (f ≫ g)).obj X_1 = (map g ⋙ map f).obj X_1

case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ autoParam
    (∀ (X_1 Y_1 : Under Z) (f_1 : X_1 ⟶ Y_1), (map (f ≫ g)).map f_1 = eqToHom ⋯ ≫ (map g ⋙ map f).map f_1 ≫ eqToHom ⋯)
    Functor.ext._auto_1
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ factorThruImage (f ≫ g) ≫ preComp f g = f ≫ factorThruImage g

Tactic:
by simp [image.preComp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : PreservesLimit (Functor.empty C) G
F : Discrete PEmpty.{1} ⥤ D
⊢ HasLimit F

Tactic:
by
  have := HasLimit.mk ⟨_, isLimitOfHasTerminalOfPreservesLimit G⟩
  apply hasLimit_of_iso F.uniqueFromEmpty.symm

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

Goal state before:
pp: case h₀
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g✝ f g : X ⟶ Y
Z : C
h✝ : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h✝
hc : IsLimit c
s' : Fork (h✝ ≫ f) (h✝ ≫ g)
m : s'.pt ⟶ (precompFork h✝ s c).pt
h : m ≫ (precompFork h✝ s c).ι = s'.ι
⊢ ∀ (j : WalkingParallelPair), (m ≫ c.fst) ≫ s.π.app j = hs.lift (Fork.ofι (s'.ι ≫ h✝) ⋯) ≫ s.π.app j

Tactic:
apply Fork.equalizer_ext

Goal state after:
case h₀
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g✝ f g : X ⟶ Y
Z : C
h✝ : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h✝
hc : IsLimit c
s' : Fork (h✝ ≫ f) (h✝ ≫ g)
m : s'.pt ⟶ (precompFork h✝ s c).pt
h : m ≫ (precompFork h✝ s c).ι = s'.ι
⊢ (m ≫ c.fst) ≫ s.ι = hs.lift (Fork.ofι (s'.ι ≫ h✝) ⋯) ≫ s.ι
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
hX : IsTerminal X
⊢ IsZero X

Tactic:
IsZero.iff_id_eq_zero

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
hX : IsTerminal X
⊢ 𝟙 X = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
hX : IsInitial X
⊢ IsZero X

Tactic:
IsZero.iff_id_eq_zero

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
hX : IsInitial X
⊢ 𝟙 X = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ (iso G X Y).inv ≫ G.map prod.fst = prod.fst

Tactic:
rw [← Iso.cancel_iso_hom_left (PreservesLimitPair.iso G X Y), ← Category.assoc, Iso.hom_inv_id]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ 𝟙 (G.obj (X ⨯ Y)) ≫ G.map prod.fst = (iso G X Y).hom ≫ prod.fst
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ (iso G X Y).inv ≫ G.map prod.snd = prod.snd

Tactic:
rw [← Iso.cancel_iso_hom_left (PreservesLimitPair.iso G X Y), ← Category.assoc, Iso.hom_inv_id]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ 𝟙 (G.obj (X ⨯ Y)) ≫ G.map prod.snd = (iso G X Y).hom ≫ prod.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
⊢ (c.whisker g).IsBilimit ≃ c.IsBilimit

Tactic:
by
  refine equivOfSubsingletonOfSubsingleton (fun hc => ⟨?_, ?_⟩) fun hc => ⟨?_, ?_⟩
  · let := IsLimit.ofIsoLimit hc.isLimit (Bicone.whiskerToCone c g)
    let := (IsLimit.postcomposeHomEquiv (Discrete.functorComp f g).symm _) this
    exact IsLimit.ofWhiskerEquivalence (Discrete.equivalence g) this
  · let := IsColimit.ofIsoColimit hc.isColimit (Bicone.whiskerToCocone c g)
    let := (IsColimit.precomposeHomEquiv (Discrete.functorComp f g) _) this
    exact IsColimit.ofWhiskerEquivalence (Discrete.equivalence g) this
  · apply IsLimit.ofIsoLimit _ (Bicone.whiskerToCone c g).symm
    apply (IsLimit.postcomposeHomEquiv (Discrete.functorComp f g).symm _).symm _
    exact IsLimit.whiskerEquivalence hc.isLimit (Discrete.equivalence g)
  · apply IsColimit.ofIsoColimit _ (Bicone.whiskerToCocone c g).symm
    apply (IsColimit.precomposeHomEquiv (Discrete.functorComp f g) _).symm _
    exact IsColimit.whiskerEquivalence hc.isColimit (Discrete.equivalence g)

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

Goal state before:
pp: case neg
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
j : J
h : ¬k = e j
⊢ ι f j ≫ (desc fun j ↦ (w j).inv ≫ ι g (e j)) ≫ π g k =
    ι f j ≫ (lift fun k ↦ π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯) ≫ π g k

Tactic:
· simp only [ι_desc_assoc, Category.assoc, lift_π]
    rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
    · simp
    · rintro rfl
      simp at h
    · exact Ne.symm h

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

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✝¹ : Preadditive C
inst✝ : Preadditive D
F : C ⥤ D
hF : IsZero F
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ IsZero (F.obj x✝²)

Tactic:
IsZero.iff_id_eq_zero

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✝¹ : Preadditive C
inst✝ : Preadditive D
F : C ⥤ D
hF : IsZero F
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ 𝟙 (F.obj x✝²) = 0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ t.fst = BinaryCofan.IsColimit.desc ht (𝟙 X) 0

Tactic:
apply ht.uniq (BinaryCofan.mk (𝟙 X) 0)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ ∀ (j : Discrete WalkingPair), t.toCocone.ι.app j ≫ t.fst = (BinaryCofan.mk (𝟙 X) 0).ι.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
h : 𝟙 (A ⊞ B) = 0
⊢ 𝟙 A = 0 ∧ 𝟙 B = 0

Tactic:
simp only [show 𝟙 A = biprod.inl ≫ 𝟙 (A ⊞ B) ≫ biprod.fst by simp,
      show 𝟙 B = biprod.inr ≫ 𝟙 (A ⊞ B) ≫ biprod.snd by simp, h, zero_comp, comp_zero,
      and_self]

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

Goal state before:
pp: case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
hA : IsZero A
hB : IsZero B
⊢ IsZero (A ⊞ B)

Tactic:
IsZero.iff_id_eq_zero

Goal state after:
case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
hA : IsZero A
hB : IsZero B
⊢ 𝟙 (A ⊞ B) = 0
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_4.x.x
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
hab : q < q
⊢ q.insertNth x f q < q.insertNth x f q

Tactic:
simp at hab

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
⊢ f ∈ (antidiagonal n).disjiUnion (fun ab ↦ map { toFun := Fin.cons ab.1, inj' := ⋯ } ↑(aux d ab.2)) ⋯ ↔ ∑ i, f i = n

Tactic:
mem_disjiUnion,

Goal state after:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
⊢ (∃ a ∈ antidiagonal n, f ∈ map { toFun := Fin.cons a.1, inj' := ⋯ } ↑(aux d a.2)) ↔ ∑ i, f i = n
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
⊢ Function.Injective fun p ↦
    { support := p.parts.toFinset, toFun := fun m ↦ count m p.parts * m, mem_support_toFun := ⋯ }

Tactic:
intro p

Goal state after:
n : ℕ
p : n.Partition
⊢ ∀ ⦃a₂ : n.Partition⦄,
    (fun p ↦ { support := p.parts.toFinset, toFun := fun m ↦ count m p.parts * m, mem_support_toFun := ⋯ }) p =
        (fun p ↦ { support := p.parts.toFinset, toFun := fun m ↦ count m p.parts * m, mem_support_toFun := ⋯ }) a₂ →
      p = a₂
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
i₁ : ℕ := (↑i).pred
i₁_lt_i : i₁ < ↑i
i₁_succ : i₁ + 1 = ↑i
⊢ False

Tactic:
have := Nat.find_min (c.index_exists j.2) i₁_lt_i

Goal state after:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length := c.index j
H : ↑j < c.sizeUpTo ↑i
i_pos : 0 < ↑i
i₁ : ℕ := (↑i).pred
i₁_lt_i : i₁ < ↑i
i₁_succ : i₁ + 1 = ↑i
this : ¬(↑j < c.sizeUpTo (i₁ + 1) ∧ i₁ < c.length)
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : j ∈ Set.range ⇑(c.embedding i)
k : Fin (c.blocksFun i)
hk : c.sizeUpTo ↑i + ↑k = ↑j
⊢ c.sizeUpTo ↑i ≤ c.sizeUpTo ↑i + ↑k ∧ c.sizeUpTo ↑i + ↑k < c.sizeUpTo (↑i).succ

Tactic:
simp [sizeUpTo_succ', k.is_lt]

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type u_1
inst✝³ : Finite J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Mono (F.biproductComparison f)
⊢ HasProduct fun b ↦ F.obj (f b)

Tactic:
change HasProduct (F.obj ∘ f)

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type u_1
inst✝³ : Finite J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Mono (F.biproductComparison f)
⊢ HasProduct (F.obj ∘ f)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x y : Subtype p
⊢ ofSubtype (swap x y) = swap ↑x ↑y

Tactic:
grind [ofSubtype_apply_of_mem, ofSubtype_apply_of_not_mem]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : ↑((c.boundaries.orderIsoOfFin ⋯) i) = ↑⟨j, hj⟩
⊢ (take (↑i) c.blocks).sum = ↑j

Tactic:
dsimp at hi

Goal state after:
case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : (c.boundaries.orderEmbOfFin ⋯) i = j
⊢ (take (↑i) c.blocks).sum = ↑j
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
x : α
hx : x ∈ l.formPerm.support
hx' : x ∈ {x | l.formPerm x ≠ x}
⊢ x ∈ l.toFinset

Tactic:
simpa using support_formPerm_le' _ hx'

Goal state after:
Module: Mathlib.Data.Set.Pairwise.List

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List α
inst✝ : Std.Symm r
hl : l.Nodup
⊢ {a | a ∈ l}.Pairwise r ↔ Pairwise r l

Tactic:
induction l with | nil => simp | cons a l ih => ?_

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
l✝ : List α
inst✝ : Std.Symm r
a : α
l : List α
ih : l.Nodup → ({a | a ∈ l}.Pairwise r ↔ Pairwise r l)
hl : (a :: l).Nodup
⊢ {a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
hffx : f (f x) ≠ x
i : ℤ
hy : (swap x (f x) * f) ((f ^ i) x) ≠ (f ^ i) x
⊢ (f ^ (i - 1)) (f x) = (f ^ i) x

Tactic:
simp [← mul_apply, -coe_mul, ← zpow_add_one]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
⊢ sign (f.subtypePerm h₁) = sign f

Tactic:
let l := (truncSwapFactors (subtypePerm f h₁)).out

Goal state after:
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
l : { l // l.prod = f.subtypePerm h₁ ∧ ∀ g ∈ l, g.IsSwap } := (f.subtypePerm h₁).truncSwapFactors.out
⊢ sign (f.subtypePerm h₁) = sign f