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

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
Y Z : Cᵒᵖ ⥤ Type v₁
f : Y ⟶ Z
g : ((yoneda.op ⋙ coyoneda).obj X).obj Y
⊢ (ConcreteCategory.hom (((yoneda.op ⋙ coyoneda).obj X).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
      g =
    (ConcreteCategory.hom
          ((yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
            ((evaluation Cᵒᵖ (Type v₁) ⋙
                      (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
                  X).map
              f)).toFun
      g

Tactic:
simp [yonedaEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
φ : Arrow C → (s : C) × (t : C) × (s ⟶ t) := fun f ↦ ⟨f.left, ⟨f.right, f.hom⟩⟩
s t : C
f f' : (𝟭 C).obj s ⟶ (𝟭 C).obj t
h :
  Arrow.right { left := s, right := t, hom := f } = Arrow.right { left := s, right := t, hom := f' } ∧
    Arrow.hom { left := s, right := t, hom := f } ≍ Arrow.hom { left := s, right := t, hom := f' }
⊢ { left := s, right := t, hom := f } = { left := s, right := t, hom := f' }

Tactic:
obtain rfl : f = f' := by simpa using h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
φ : Arrow C → (s : C) × (t : C) × (s ⟶ t) := fun f ↦ ⟨f.left, ⟨f.right, f.hom⟩⟩
s t : C
f : (𝟭 C).obj s ⟶ (𝟭 C).obj t
h :
  Arrow.right { left := s, right := t, hom := f } = Arrow.right { left := s, right := t, hom := f } ∧
    Arrow.hom { left := s, right := t, hom := f } ≍ Arrow.hom { left := s, right := t, hom := f }
⊢ { left := s, right := t, hom := f } = { left := s, right := t, hom := f }
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Small.{w, u} C
inst✝³ : LocallySmall.{w, v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Small.{w, u'} D
inst✝ : LocallySmall.{w, v', u'} D
F G : C ⥤ D
h : (fun F f ↦ Arrow.mk (F.map f.hom)) F = (fun F f ↦ Arrow.mk (F.map f.hom)) G
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
have : Arrow.mk (F.map f) = Arrow.mk (G.map f) := congr_fun h (Arrow.mk f)
    rw [Arrow.mk_eq_mk_iff] at this
    tauto

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F✝ : J ⥤ C
L : (J ⥤ C) ⥤ C
adj : const J ⊣ L
F : J ⥤ C
s : Cone F
j : J
eq : L.map s.π ≫ (adj.counit.app F).app j = (adj.counit.app ((const J).obj s.pt)).app j ≫ s.π.app j
eq' : adj.unit.app s.pt ≫ (adj.counit.app ((const J).obj s.pt)).app j = 𝟙 s.pt
⊢ adj.unit.app s.pt ≫ (adj.counit.app ((const J).obj s.pt)).app j ≫ s.π.app j = s.π.app j

Tactic:
reassoc_of% eq'

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F✝ : J ⥤ C
L : (J ⥤ C) ⥤ C
adj : const J ⊣ L
F : J ⥤ C
s : Cone F
j : J
eq : L.map s.π ≫ (adj.counit.app F).app j = (adj.counit.app ((const J).obj s.pt)).app j ≫ s.π.app j
eq' : adj.unit.app s.pt ≫ (adj.counit.app ((const J).obj s.pt)).app j = 𝟙 s.pt
⊢ s.π.app j = s.π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_2
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan fun x ↦
    match x with
    | ⟨a, b⟩ => Y a b
a : α
b : β a
⊢ (mk c.pt fun x ↦
            match x with
            | ⟨a, b⟩ => π a b ≫ c.inj a).inj
        ⟨a, b⟩ ≫
      hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩)) =
    t.inj ⟨a, b⟩

Tactic:
simp only [mk_pt, cofan_mk_inj, Category.assoc]

Goal state after:
case refine_2
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan fun x ↦
    match x with
    | ⟨a, b⟩ => Y a b
a : α
b : β a
⊢ π a b ≫ c.inj a ≫ hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩)) = t.inj ⟨a, b⟩
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ prod.map f (𝟙 (⊤_ C)) ≫ (prod.rightUnitor Y).hom = (prod.rightUnitor X).hom ≫ f

Tactic:
prod.rightUnitor_hom_naturality

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ (prod.rightUnitor X).hom ≫ f = (prod.rightUnitor X).hom ≫ f
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f f' : StructuredArrow S T
g : f.right ≅ f'.right
w : f.hom ≫ T.map g.hom = f'.hom
⊢ f.left = f'.left

Tactic:
by ext

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f f' : CostructuredArrow S T
g : f.left ≅ f'.left
w : S.map g.hom ≫ f'.hom = f.hom
⊢ f.right = f'.right

Tactic:
by ext

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 × T
Y✝ Z✝ : CostructuredArrow (Functor.diag T) X
m : Y✝ ⟶ Z✝
⊢ (Over.forget X.1).map (((proj (Functor.diag T) X).toOver X.1 (fun g ↦ g.hom.1) ⋯).map m) ≫ Z✝.hom.2 = Y✝.hom.2

Tactic:
have := congrArg (·.2) m.w

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : CostructuredArrow (Functor.diag T) X
m : Y✝ ⟶ Z✝
this : ((Functor.diag T).map m.left ≫ Z✝.hom).2 = (Y✝.hom ≫ (Functor.fromPUnit X).map m.right).2
⊢ (Over.forget X.1).map (((proj (Functor.diag T) X).toOver X.1 (fun g ↦ g.hom.1) ⋯).map m) ≫ Z✝.hom.2 = Y✝.hom.2
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst✝¹ : Epi h
inst✝ : HasPushout f g
⊢ f ≫ pushout.inl f g = g ≫ pushout.inr f g

Tactic:
exact pushout.condition

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ 𝟙 (image f) ≫ g = v ≫ q ≫ g

Tactic:
← t,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ (v ≫ q) ≫ g = v ≫ q ≫ g
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X : C
f g : X ≅ 0
⊢ f = g

Tactic:
by ext

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X : C
f : 0 ⟶ X
Z✝ : C
g h : Z✝ ⟶ 0
x✝ : g ≫ f = h ≫ f
⊢ g = h

Tactic:
by ext

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X : C
f : X ⟶ 0
Z✝ : C
g h : 0 ⟶ Z✝
x✝ : f ≫ g = f ≫ h
⊢ g = h

Tactic:
by ext

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
t : IsInitial X
⊢ (zeroIsoIsInitial t).hom = 0

Tactic:
by ext

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
t : IsInitial X
⊢ (zeroIsoIsInitial t).inv = 0

Tactic:
by ext

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
t : IsTerminal X
⊢ (zeroIsoIsTerminal t).hom = 0

Tactic:
by ext

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
t : IsTerminal X
⊢ (zeroIsoIsTerminal t).inv = 0

Tactic:
by ext

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
⊢ zeroIsoInitial.hom = 0

Tactic:
by ext

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
⊢ zeroIsoInitial.inv = 0

Tactic:
by ext

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
⊢ zeroIsoTerminal.hom = 0

Tactic:
by ext

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
⊢ zeroIsoTerminal.inv = 0

Tactic:
by ext

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
f : X ⟶ 0
⊢ f = 0

Tactic:
by ext

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
f : 0 ⟶ X
⊢ f = 0

Tactic:
by ext

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f : X ⟶ Y
inst✝ : HasColimit (parallelPair f 0)
w : cokernel.π f = 0
R✝ : C
g : Y ⟶ R✝
h : f ≫ g = 0
⊢ g = 0

Tactic:
by rw [← cokernel.π_desc f g h, w, Limits.zero_comp]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
inst✝ : Mono f
this : Mono (Fork.ι c)
⊢ IsZero c.pt

Tactic:
rw [IsZero.iff_id_eq_zero, ← cancel_mono c.ι, ← cancel_mono f, Category.assoc,
    Category.assoc, c.condition, comp_zero, zero_comp]

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

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
P Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
⊢ Epi (map f g)

Tactic:
show biprod.map f g =
    (biprod.isoCoprod _ _).hom ≫ coprod.map f g ≫ (biprod.isoCoprod _ _).inv by aesop

Goal state after:
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
P Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
⊢ Epi ((isoCoprod W X).hom ≫ coprod.map f g ≫ (isoCoprod Y Z).inv)
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.toCocone.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
⊢ m = b.fst ≫ f + b.snd ≫ g

Tactic:
by
      dsimp at m
      have h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0 := by simpa using sub_eq_zero.2 h₁
      have h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0 := by simpa using sub_eq_zero.2 h₂
      obtain ⟨q : Y ⟶ T, hq : b.snd ≫ q = m - (b.fst ≫ f + b.snd ≫ g)⟩ :=
        CokernelCofork.IsColimit.desc' hb _ h₁'
      rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inr_snd, Category.assoc, hq, h₂',
        comp_zero]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ biprod.inl ≫ f ≫ inv f ≫ biprod.fst = 0

Tactic:
← Category.id_comp (inv f),

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ biprod.inl ≫ f ≫ (𝟙 (Y ⊞ Z) ≫ inv f) ≫ biprod.fst = 0
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
i : ℕ
h : i ∈ c.blocks
⊢ i ≤ n

Tactic:
rw [← c.blocks_sum]

Goal state after:
n : ℕ
c : Composition n
i : ℕ
h : i ∈ c.blocks
⊢ i ≤ c.blocks.sum
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
| n

Tactic:
rw [← c.blocks_sum]

Goal state after:
n : ℕ
c : Composition n
| c.blocks.sum
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ 0 < c.length ↔ 0 < n

Tactic:
by
  simp [pos_iff_ne_zero]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
σ τ : Type
inst✝³ : Finite τ
S : σ → C
inst✝² : HasBiproduct S
T : τ → C
inst✝¹ : HasBiproduct T
s : σ
f : ⨁ S ⟶ ⨁ T
inst✝ : IsIso f
val✝ : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
⊢ biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s = 0

Tactic:
← Category.id_comp (inv f),

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
σ τ : Type
inst✝³ : Finite τ
S : σ → C
inst✝² : HasBiproduct S
T : τ → C
inst✝¹ : HasBiproduct T
s : σ
f : ⨁ S ⟶ ⨁ T
inst✝ : IsIso f
val✝ : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
⊢ biproduct.ι S s ≫ f ≫ (𝟙 (⨁ T) ≫ inv f) ≫ biproduct.π S s = 0
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✝ : PreservesBiproduct f F
c✝ : Cone (Discrete.functor f)
hc : IsLimit c✝
val✝ : Fintype J
⊢ ∀ (j : Discrete J),
    ((Cone.postcompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapBicone (Bicone.ofLimitCone hc)).toCone).π.app
        j =
      (Iso.refl
            ((Cone.postcompose (Discrete.compNatIsoDiscrete f F).inv).obj
                (F.mapBicone (Bicone.ofLimitCone hc)).toCone).pt).hom ≫
        (F.mapCone c✝).π.app j

Tactic:
rintro ⟨⟩

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✝ : PreservesBiproduct f F
c✝ : Cone (Discrete.functor f)
hc : IsLimit c✝
val✝ : Fintype J
as✝ : J
⊢ ((Cone.postcompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapBicone (Bicone.ofLimitCone hc)).toCone).π.app
      { as := as✝ } =
    (Iso.refl
          ((Cone.postcompose (Discrete.compNatIsoDiscrete f F).inv).obj
              (F.mapBicone (Bicone.ofLimitCone hc)).toCone).pt).hom ≫
      (F.mapCone c✝).π.app { as := as✝ }
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✝ : PreservesLimit (Discrete.functor f) F
b : Bicone f
hb : b.IsBilimit
val✝ : Fintype J
⊢ ∀ (j : Discrete J),
    ((Cone.postcompose (Discrete.compNatIsoDiscrete f F).hom).obj (F.mapCone b.toCone)).π.app j =
      (Iso.refl ((Cone.postcompose (Discrete.compNatIsoDiscrete f F).hom).obj (F.mapCone b.toCone)).pt).hom ≫
        (F.mapBicone b).toCone.π.app j

Tactic:
rintro ⟨⟩

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✝ : PreservesLimit (Discrete.functor f) F
b : Bicone f
hb : b.IsBilimit
val✝ : Fintype J
as✝ : J
⊢ ((Cone.postcompose (Discrete.compNatIsoDiscrete f F).hom).obj (F.mapCone b.toCone)).π.app { as := as✝ } =
    (Iso.refl ((Cone.postcompose (Discrete.compNatIsoDiscrete f F).hom).obj (F.mapCone b.toCone)).pt).hom ≫
      (F.mapBicone b).toCone.π.app { as := as✝ }
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✝ : PreservesBiproduct f F
c : Cocone (Discrete.functor f)
hc : IsColimit c
val✝ : Fintype J
⊢ ∀ (j : Discrete J),
    ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).hom).obj
                (F.mapBicone (Bicone.ofColimitCocone hc)).toCocone).ι.app
          j ≫
        (Iso.refl
            ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).hom).obj
                (F.mapBicone (Bicone.ofColimitCocone hc)).toCocone).pt).hom =
      (F.mapCocone c).ι.app j

Tactic:
rintro ⟨⟩

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✝ : PreservesBiproduct f F
c : Cocone (Discrete.functor f)
hc : IsColimit c
val✝ : Fintype J
as✝ : J
⊢ ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).hom).obj
              (F.mapBicone (Bicone.ofColimitCocone hc)).toCocone).ι.app
        { as := as✝ } ≫
      (Iso.refl
          ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).hom).obj
              (F.mapBicone (Bicone.ofColimitCocone hc)).toCocone).pt).hom =
    (F.mapCocone c).ι.app { as := as✝ }
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✝ : PreservesColimit (Discrete.functor f) F
b : Bicone f
hb : b.IsBilimit
val✝ : Fintype J
⊢ ∀ (j : Discrete J),
    ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).ι.app j ≫
        (Iso.refl ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).pt).hom =
      (F.mapBicone b).toCocone.ι.app j

Tactic:
rintro ⟨⟩

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✝ : PreservesColimit (Discrete.functor f) F
b : Bicone f
hb : b.IsBilimit
val✝ : Fintype J
as✝ : J
⊢ ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).ι.app { as := as✝ } ≫
      (Iso.refl ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).pt).hom =
    (F.mapBicone b).toCocone.ι.app { as := as✝ }
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
ji : ¬j = i
⊢ ∑ k, c.blocksFun k ≤ c.blocksFun i

Tactic:
simp only [c.sum_blocksFun, hi]

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

Goal state before:
pp: α : Type u_1
l : List α
ns : List ℕ
i : ℕ
hi : i < (l.splitWrtCompositionAux ns).length
⊢ (l.splitWrtCompositionAux ns)[i] = drop (take i ns).sum (take (take (i + 1) ns).sum l)

Tactic:
induction ns generalizing l i with

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
hqc : sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ
⊢ Disjoint (sq \ sp) (sp ∪ sq)ᶜ

Tactic:
simp [Set.disjoint_left]; tauto

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
hqc : sqᶜ = sp \ sq ∪ (sp ∪ sq)ᶜ
epc : ↑spᶜ ≃ ↑(sq \ sp) ⊕ ↑(sp ∪ sq)ᶜ := (setCongr hpc).trans (Set.union ⋯)
⊢ Disjoint (sp \ sq) (sp ∪ sq)ᶜ

Tactic:
simp [Set.disjoint_left]; tauto

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: β : Type u_2
s t : Finset β
h : s.card = t.card
σ : Perm β
hσ : ∀ (a : ↥s), σ ↑a = ↑((Finset.equivOfCardEq h) a)
a : β
ha : a ∈ s
hb : (Equiv.toEmbedding σ) a ∈ Finset.map (Equiv.toEmbedding σ) s
⊢ (Equiv.toEmbedding σ) a ∈ t

Tactic:
exact (hσ ⟨a, ha⟩) ▸ ((s.equivOfCardEq h) ⟨a, ha⟩).2

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

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ¬b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Tactic:
simp only [not_exists, false_iff, not_and, not_true]

Goal state after:
case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ∀ (x : α), ¬g x = x → ¬f.asEmbedding x = b