mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((Cocone.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (F.mapBicone b.toBicone).toCocone).ι.app
        j ≫
      (Iso.refl
          ((Cocone.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (F.mapBicone b.toBicone).toCocone).pt).hom =
    (F.mapBinaryBicone b).toCocone.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
case left
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cocone.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (F.mapBicone b.toBicone).toCocone).ι.app
        { as := WalkingPair.left } ≫
      (Iso.refl
          ((Cocone.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (F.mapBicone b.toBicone).toCocone).pt).hom =
    (F.mapBinaryBicone b).toCocone.ι.app { as := WalkingPair.left }

case right
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cocone.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (F.mapBicone b.toBicone).toCocone).ι.app
        { as := WalkingPair.right } ≫
      (Iso.refl
          ((Cocone.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (F.mapBicone b.toBicone).toCocone).pt).hom =
    (F.mapBinaryBicone b).toCocone.ι.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : HasBinaryBiproducts C
F : C ⥤ D
h : leftExactFunctor C D F
⊢ additiveFunctor C D F

Tactic:
simp only [leftExactFunctor_iff] at h

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : HasBinaryBiproducts C
F : C ⥤ D
h : PreservesFiniteLimits F
⊢ additiveFunctor C D F
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
X Y : C
b : Bicone (pairFunction X Y)
j : Discrete WalkingPair
⊢ b.toBinaryBicone.toCone.π.app j = (Iso.refl b.toBinaryBicone.toCone.pt).hom ≫ b.toCone.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
case left
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
X Y : C
b : Bicone (pairFunction X Y)
⊢ b.toBinaryBicone.toCone.π.app { as := WalkingPair.left } =
    (Iso.refl b.toBinaryBicone.toCone.pt).hom ≫ b.toCone.π.app { as := WalkingPair.left }

case right
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
X Y : C
b : Bicone (pairFunction X Y)
⊢ b.toBinaryBicone.toCone.π.app { as := WalkingPair.right } =
    (Iso.refl b.toBinaryBicone.toCone.pt).hom ≫ b.toCone.π.app { as := WalkingPair.right }
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
X Y : C
b : Bicone (pairFunction X Y)
j : Discrete WalkingPair
⊢ b.toBinaryBicone.toCocone.ι.app j ≫ (Iso.refl b.toBinaryBicone.toCocone.pt).hom = b.toCocone.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
case left
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
X Y : C
b : Bicone (pairFunction X Y)
⊢ b.toBinaryBicone.toCocone.ι.app { as := WalkingPair.left } ≫ (Iso.refl b.toBinaryBicone.toCocone.pt).hom =
    b.toCocone.ι.app { as := WalkingPair.left }

case right
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
X Y : C
b : Bicone (pairFunction X Y)
⊢ b.toBinaryBicone.toCocone.ι.app { as := WalkingPair.right } ≫ (Iso.refl b.toBinaryBicone.toCocone.pt).hom =
    b.toCocone.ι.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone (pair X Y)
j : Discrete WalkingPair
⊢ (BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app j = s.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone (pair X Y)
⊢ (BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.left } =
    s.π.app { as := WalkingPair.left }

case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone (pair X Y)
⊢ (BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.right } =
    s.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone (pair X Y)
j : Discrete WalkingPair
⊢ b.toCocone.ι.app j ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s) = s.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone (pair X Y)
⊢ b.toCocone.ι.app { as := WalkingPair.left } ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s) =
    s.ι.app { as := WalkingPair.left }

case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone (pair X Y)
⊢ b.toCocone.ι.app { as := WalkingPair.right } ≫ (b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s) =
    s.ι.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
i : b.IsBilimit
j : Discrete WalkingPair
⊢ (b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app j = 𝟙 b.pt ≫ b.toCone.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
i : b.IsBilimit
⊢ (b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.left } =
    𝟙 b.pt ≫ b.toCone.π.app { as := WalkingPair.left }

case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
i : b.IsBilimit
⊢ (b.fst ≫ b.inl + b.snd ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.right } =
    𝟙 b.pt ≫ b.toCone.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inl ≫ map f g) ≫ snd = (inl ≫ map' f g) ≫ snd

Tactic:
simp only [mapPair_left, IsColimit.ι_map, IsLimit.map_π,
      Category.assoc, ← BinaryBicone.toCone_π_app_right, ←
      BinaryBicone.toCocone_ι_app_left]
    simp

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

Goal state before:
pp: case refine_1
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ inl ≫ (BinaryBiproduct.bicone X Y).toCone.π.app j = inl ≫ desc b.inl b.inr ≫ b.toCone.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
case refine_1.left
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inl ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.left } =
    inl ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }

case refine_1.right
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inl ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.right } =
    inl ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case refine_2
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app j = inr ≫ desc b.inl b.inr ≫ b.toCone.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
case refine_2.left
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.left } =
    inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.left }

case refine_2.right
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ inr ≫ (BinaryBiproduct.bicone X Y).toCone.π.app { as := WalkingPair.right } =
    inr ≫ desc b.inl b.inr ≫ b.toCone.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : Cocone (pair X Y)
ht : IsColimit t
j : Discrete WalkingPair
⊢ t.ι.app j ≫ (Iso.refl t.pt).hom = (BinaryBicone.ofColimitCocone ht).toCocone.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : Cocone (pair X Y)
ht : IsColimit t
⊢ t.ι.app { as := WalkingPair.left } ≫ (Iso.refl t.pt).hom =
    (BinaryBicone.ofColimitCocone ht).toCocone.ι.app { as := WalkingPair.left }

case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : Cocone (pair X Y)
ht : IsColimit t
⊢ t.ι.app { as := WalkingPair.right } ≫ (Iso.refl t.pt).hom =
    (BinaryBicone.ofColimitCocone ht).toCocone.ι.app { as := WalkingPair.right }
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✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasFiniteBiproducts C
⊢ HasZeroObject C

Tactic:
refine ⟨⟨biproduct Empty.elim, fun X => ⟨⟨⟨0⟩, ?_⟩⟩, fun X => ⟨⟨⟨0⟩, ?_⟩⟩⟩⟩

Goal state after:
case refine_1
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✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasFiniteBiproducts C
X : C
⊢ ∀ (a : ⨁ Empty.elim ⟶ X), a = default

case refine_2
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✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasFiniteBiproducts C
X : C
⊢ ∀ (a : X ⟶ ⨁ Empty.elim), a = default
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
f : Fin n → Fin (n + 1)
h : StrictMono (cons 0 f)
i : Fin n
⊢ f i = i.succ

Tactic:
have key (g : Fin (n + 1) → Fin (n + 1)) (hg : StrictMono g) : g = id := by
    -- Import restrictions prevent us using `StrictMono.eq_id`: hence this manual proof.
    refine funext fun x ↦ le_antisymm ?_ (hg.id_le x)
    simpa using ((Fin.rev_strictAnti.comp_strictMono hg).comp Fin.rev_strictAnti).id_le (Fin.rev x)

Goal state after:
n : ℕ
f : Fin n → Fin (n + 1)
h : StrictMono (cons 0 f)
i : Fin n
key : ∀ (g : Fin (n + 1) → Fin (n + 1)), StrictMono g → g = id
⊢ f i = i.succ
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case a.mp
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : ↥s ≃ Fin #s
⊢ (∃ a, ∑ i, a i = n ∧ (fun i ↦ if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f) → s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

pp: case a.mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : ↥s ≃ Fin #s
⊢ (s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s) → ∃ a, ∑ i, a i = n ∧ (fun i ↦ if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f

Tactic:
· rintro ⟨f, ⟨hf, rfl⟩, rfl⟩
    rw [sum_dite_of_true fun _ ↦ id]
    exact ⟨Fintype.sum_equiv e _ _ (by simp), by simp +contextual⟩

Goal state after:
case a.mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : ↥s ≃ Fin #s
⊢ (s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s) → ∃ a, ∑ i, a i = n ∧ (fun i ↦ if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f
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
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cone (pair X Y)
hc : IsLimit c
j : Discrete WalkingPair
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)).toCone).π.app
      j =
    (id (Iso.refl (F.obj c.pt))).hom ≫ (F.mapCone c).π.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
case left
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
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cone (pair X Y)
hc : IsLimit c
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)).toCone).π.app
      { as := WalkingPair.left } =
    (id (Iso.refl (F.obj c.pt))).hom ≫ (F.mapCone c).π.app { as := WalkingPair.left }

case right
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
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cone (pair X Y)
hc : IsLimit c
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)).toCone).π.app
      { as := WalkingPair.right } =
    (id (Iso.refl (F.obj c.pt))).hom ≫ (F.mapCone c).π.app { as := WalkingPair.right }
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
X Y : C
inst✝ : PreservesLimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app j =
    (id (Iso.refl (F.obj b.pt))).hom ≫ (F.mapBinaryBicone b).toCone.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
case left
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
X Y : C
inst✝ : PreservesLimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app { as := WalkingPair.left } =
    (id (Iso.refl (F.obj b.pt))).hom ≫ (F.mapBinaryBicone b).toCone.π.app { as := WalkingPair.left }

case right
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
X Y : C
inst✝ : PreservesLimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app { as := WalkingPair.right } =
    (id (Iso.refl (F.obj b.pt))).hom ≫ (F.mapBinaryBicone b).toCone.π.app { as := WalkingPair.right }
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
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cocone (pair X Y)
hc : IsColimit c
j : Discrete WalkingPair
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
              (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)).toCocone).ι.app
        j ≫
      (id (Iso.refl (F.obj c.pt))).hom =
    (F.mapCocone c).ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
case left
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
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cocone (pair X Y)
hc : IsColimit c
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
              (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)).toCocone).ι.app
        { as := WalkingPair.left } ≫
      (id (Iso.refl (F.obj c.pt))).hom =
    (F.mapCocone c).ι.app { as := WalkingPair.left }

case right
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
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cocone (pair X Y)
hc : IsColimit c
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
              (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)).toCocone).ι.app
        { as := WalkingPair.right } ≫
      (id (Iso.refl (F.obj c.pt))).hom =
    (F.mapCocone c).ι.app { as := WalkingPair.right }
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
X Y : C
inst✝ : PreservesColimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
j : Discrete WalkingPair
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).ι.app j ≫
      (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).pt).hom =
    (F.mapBinaryBicone b).toCocone.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩

Goal state after:
case left
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
X Y : C
inst✝ : PreservesColimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).ι.app
        { as := WalkingPair.left } ≫
      (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).pt).hom =
    (F.mapBinaryBicone b).toCocone.ι.app { as := WalkingPair.left }

case right
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
X Y : C
inst✝ : PreservesColimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).ι.app
        { as := WalkingPair.right } ≫
      (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).pt).hom =
    (F.mapBinaryBicone b).toCocone.ι.app { as := WalkingPair.right }
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
⊢ IsConj σ τ

Tactic:
refine isConj_iff.2 ⟨Equiv.extendSubtype f, ?_⟩

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
⊢ f.extendSubtype * σ * f.extendSubtype⁻¹ = τ
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = σ x
⊢ σ ∈ (sumCongrHom m n).range

Tactic:
let σ₁' := subtypePermOfFintype σ h1

Goal state after:
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := σ.subtypePermOfFintype h1
⊢ σ ∈ (sumCongrHom m n).range
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ (σ * τ * σ⁻¹).support = map (Equiv.toEmbedding σ) τ.support

Tactic:
by
  ext
  simp only [mem_map_equiv, Perm.coe_mul, Function.comp_apply, Ne, Perm.mem_support,
    Equiv.eq_symm_apply, inv_def]

Goal state after: