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

Goal state before:
pp: case h₀.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
⊢ (biprod.inl ≫
        ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
          (biprod.inr ≫ f ≫ biprod.snd)) ≫
      biprod.fst =
    (biprod.inl ≫ f) ≫ biprod.fst

pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
⊢ (biprod.inl ≫
        ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
          (biprod.inr ≫ f ≫ biprod.snd)) ≫
      biprod.snd =
    (biprod.inl ≫ f) ≫ biprod.snd

pp: case h₁.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
⊢ (biprod.inr ≫
        ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
          (biprod.inr ≫ f ≫ biprod.snd)) ≫
      biprod.fst =
    (biprod.inr ≫ f) ≫ biprod.fst

pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
⊢ (biprod.inr ≫
        ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
          (biprod.inr ≫ f ≫ biprod.snd)) ≫
      biprod.snd =
    (biprod.inr ≫ f) ≫ biprod.snd

Tactic:
<;>

Goal state after:
case h₀.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
⊢ (biprod.inl ≫
        ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
          (biprod.inr ≫ f ≫ biprod.snd)) ≫
      biprod.fst =
    (biprod.inl ≫ f) ≫ biprod.fst

case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
⊢ (biprod.inl ≫
        ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
          (biprod.inr ≫ f ≫ biprod.snd)) ≫
      biprod.snd =
    (biprod.inl ≫ f) ≫ biprod.snd

case h₁.h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
⊢ (biprod.inr ≫
        ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
          (biprod.inr ≫ f ≫ biprod.snd)) ≫
      biprod.fst =
    (biprod.inr ≫ f) ≫ biprod.fst

case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
⊢ (biprod.inr ≫
        ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
          (biprod.inr ≫ f ≫ biprod.snd)) ≫
      biprod.snd =
    (biprod.inr ≫ f) ≫ biprod.snd
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst✝¹ : IsIso f₁₁
inst✝ : IsIso (ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂
R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂
g : X₂ ⟶ Y₂
w : L.hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = biprod.map f₁₁ g
⊢ IsIso (biprod.map f₁₁ g)

Tactic:
by
    rw [← w]
    infer_instance

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case zero.zero
⊢ (antidiagonalTuple 0 0).Nodup

pp: case zero.succ
n✝ : ℕ
⊢ (antidiagonalTuple 0 (n✝ + 1)).Nodup

Tactic:
<;>

Goal state after:
case zero.zero
⊢ (antidiagonalTuple 0 0).Nodup

case zero.succ
n✝ : ℕ
⊢ (antidiagonalTuple 0 (n✝ + 1)).Nodup
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case pos
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
hn : n = 0
⊢ ∅.finsuppAntidiag n = {0}

pp: case neg
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
hn : ¬n = 0
⊢ ∅.finsuppAntidiag n = ∅

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
hn : n = 0
⊢ ∅.finsuppAntidiag n = {0}

case neg
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
hn : ¬n = 0
⊢ ∅.finsuppAntidiag n = ∅
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case pos
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
hn : n = 0
⊢ ∅.piAntidiag n = {0}

pp: case neg
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
hn : ¬n = 0
⊢ ∅.piAntidiag n = ∅

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
hn : n = 0
⊢ ∅.piAntidiag n = {0}

case neg
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
hn : ¬n = 0
⊢ ∅.piAntidiag n = ∅
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ.right.succ
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
⊢ Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal (n + 1))

Tactic:
| succ n n_ih =>

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ ↦
      ∀ a ∈ antidiagonalTuple k a₁.2,
        ∀ a_2 ∈ antidiagonalTuple k a₂.2,
          a₁.1 < a₂.1 ∨ a₁.1 = a₂.1 ∧ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun i x1 x2 ↦ x1 < x2) a a_2)
    (antidiagonal n)
⊢ Pairwise
    (fun a₁ a₂ ↦
      ∀ a ∈ antidiagonalTuple k a₁.2,
        ∀ a_2 ∈ antidiagonalTuple k a₂.2,
          a₁.1 < a₂.1 ∨ a₁.1 = a₂.1 ∧ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun i x1 x2 ↦ x1 < x2) a a_2)
    (antidiagonal (n + 1))

Tactic:
| succ n n_ih =>

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
this : ∑ m ∈ Finset.Icc 1 n, count m p.parts * m = n
⊢ p.toFinsuppAntidiag ∈ (Finset.Icc 1 n).finsuppAntidiag n

Tactic:
by simpa [toFinsuppAntidiag, hp]

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

Goal state before:
pp: α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
hg : g x = x
hf : f (f x) = f x
⊢ (f * g) x = (g * f) x

Tactic:
simp [mul_apply, f.injective hf, hg]

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

Goal state before:
pp: case inl
α : Type u_1
f : Perm α
h : f.Disjoint f
x : α
hx : f x = x
⊢ f x = 1 x

pp: case inr
α : Type u_1
f : Perm α
h : f.Disjoint f
x : α
hx : f x = x
⊢ f x = 1 x

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
f : Perm α
h : f.Disjoint f
x : α
hx : f x = x
⊢ f x = 1 x

case inr
α : Type u_1
f : Perm α
h : f.Disjoint f
x : α
hx : f x = x
⊢ f x = 1 x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case inl
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝ : f x = x
⊢ (f * g) x = x ∨ h x = x

pp: case inr
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝ : h x = x
⊢ (f * g) x = x ∨ h x = x

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝ : f x = x
⊢ (f * g) x = x ∨ h x = x

case inr
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝ : h x = x
⊢ (f * g) x = x ∨ h x = x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case inl.inl
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝¹ : f x = x
h✝ : g x = x
⊢ (f * g) x = x ∨ h x = x

pp: case inl.inr
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝¹ : f x = x
h✝ : h x = x
⊢ (f * g) x = x ∨ h x = x

pp: case inr.inl
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝¹ : h x = x
h✝ : g x = x
⊢ (f * g) x = x ∨ h x = x

pp: case inr.inr
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝¹ h✝ : h x = x
⊢ (f * g) x = x ∨ h x = x

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝¹ : f x = x
h✝ : g x = x
⊢ (f * g) x = x ∨ h x = x

case inl.inr
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝¹ : f x = x
h✝ : h x = x
⊢ (f * g) x = x ∨ h x = x

case inr.inl
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝¹ : h x = x
h✝ : g x = x
⊢ (f * g) x = x ∨ h x = x

case inr.inr
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝¹ h✝ : h x = x
⊢ (f * g) x = x ∨ h x = x
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ (∃ m ∈ antidiagonal n, ∃ g, f = g.update a m.1 ∧ g ∈ s.finsuppAntidiag m.2) ↔
    f ∈
      (antidiagonal n).biUnion fun p ↦
        map { toFun := fun f ↦ (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach

Tactic:
mem_biUnion

Goal state after:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ (∃ m ∈ antidiagonal n, ∃ g, f = g.update a m.1 ∧ g ∈ s.finsuppAntidiag m.2) ↔
    ∃ a_1 ∈ antidiagonal n, f ∈ map { toFun := fun f ↦ (↑f).update a a_1.1, inj' := ⋯ } (s.finsuppAntidiag a_1.2).attach
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: 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 }

pp: 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 }

Tactic:
<;>

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: 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 }

pp: 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 }

Tactic:
<;>

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: case h₁
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✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Mono (F.biprodComparison X Y)
⊢ prodComparison F X Y ≫ prod.fst =
    ((F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom) ≫ prod.fst

pp: case h₂
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✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Mono (F.biprodComparison X Y)
⊢ prodComparison F X Y ≫ prod.snd =
    ((F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom) ≫ prod.snd

Tactic:
<;>

Goal state after:
case h₁
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✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Mono (F.biprodComparison X Y)
⊢ prodComparison F X Y ≫ prod.fst =
    ((F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom) ≫ prod.fst

case h₂
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✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Mono (F.biprodComparison X Y)
⊢ prodComparison F X Y ≫ prod.snd =
    ((F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom) ≫ prod.snd
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: 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 }

pp: 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 }

Tactic:
<;>

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: 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 }

pp: 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 }

Tactic:
<;>

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.Data.Fintype.Inv

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α ↪ β
inst✝ : Nonempty α
b : β
h : b ∈ Set.range ⇑f
⊢ (Set.range ⇑f).domRestrict (invFun ⇑f) ⟨b, h⟩ = f.invOfMemRange ⟨b, h⟩

Tactic:
apply f.injective

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq β
f : α ↪ β
inst✝ : Nonempty α
b : β
h : b ∈ Set.range ⇑f
⊢ f ((Set.range ⇑f).domRestrict (invFun ⇑f) ⟨b, h⟩) = f (f.invOfMemRange ⟨b, h⟩)
Module: Mathlib.Data.Fintype.Inv

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Fintype α✝
p✝ : α✝ → Prop
inst✝² : DecidablePred p✝
α : Type u_4
p : α → Prop
inst✝¹ : Fintype { a // p a }
inst✝ : DecidableEq α
x y : { a // p a }
hy : (fun a ↦ ↑a = ↑x) y
⊢ y = x

Tactic:
simpa [Subtype.ext_iff] using hy

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

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
⊢ c.length < c.boundaries.card

Tactic:
rw [c.card_boundaries_eq_succ_length]
  exact Nat.lt_add_one _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i ↦ (k i).support
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ i ∈ ↑(insert i s)

pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i ↦ (k i).support
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ j ∈ ↑(insert i s)

Tactic:
<;>

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i ↦ (k i).support
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ i ∈ ↑(insert i s)

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i ↦ (k i).support
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ j ∈ ↑(insert i s)