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

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

Tactic:
by
  ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
X Y : C
⊢ (associator X (⊥_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom = map (rightUnitor X).hom (𝟙 Y)

Tactic:
by
  ext <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝⁴ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝³ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ g₂ ≫ inv i₃ = inv i₂ ≫ f₂

pp: case refine_3
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝⁴ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝³ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ ≫ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ?refine_2 = 𝟙 (pullback f₁ f₂)

pp: case refine_4
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝⁴ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝³ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ?refine_2 ≫ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ = 𝟙 (pullback g₁ g₂)

Tactic:
· rw [IsIso.comp_inv_eq, Category.assoc, eq₂, IsIso.inv_hom_id_assoc]

Goal state after:
case refine_3
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝⁴ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝³ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ ≫ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯ = 𝟙 (pullback f₁ f₂)

case refine_4
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : W ⟶ S
f₂ : X ⟶ S
inst✝⁴ : HasPullback f₁ f₂
g₁ : Y ⟶ T
g₂ : Z ⟶ T
inst✝³ : HasPullback g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯ ≫ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ = 𝟙 (pullback g₁ g₂)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ g₂ ≫ inv i₂ = inv i₃ ≫ f₂

pp: case refine_3
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ ≫ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ?refine_2 = 𝟙 (pushout f₁ f₂)

pp: case refine_4
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ?refine_2 ≫ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ = 𝟙 (pushout g₁ g₂)

Tactic:
· rw [IsIso.comp_inv_eq, Category.assoc, eq₂, IsIso.inv_hom_id_assoc]

Goal state after:
case refine_3
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ ≫ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯ = 𝟙 (pushout f₁ f₂)

case refine_4
C : Type u
inst✝⁵ : Category.{v, u} C
W✝ X✝ Y✝ Z✝ W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝⁴ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝³ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst✝² : IsIso i₁
inst✝¹ : IsIso i₂
inst✝ : IsIso i₃
⊢ map g₁ g₂ f₁ f₂ (inv i₁) (inv i₂) (inv i₃) ⋯ ⋯ ≫ map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ = 𝟙 (pushout g₁ g₂)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g f' g' : X ⟶ Y
hf : f = f'
hg : g = g'
⊢ (parallelPair f g).map right ≫ (Iso.refl ((parallelPair f g).obj one)).hom =
    (Iso.refl ((parallelPair f g).obj zero)).hom ≫ (parallelPair f' g').map right

Tactic:
by simp [hg]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
D : Type u'
F : D → C
x✝⁵ x✝⁴ x✝³ : InducedCategory C F
x✝² : x✝⁵ ⟶ x✝⁴
x✝¹ : R
x✝ : x✝⁴ ⟶ x✝³
⊢ (x✝² ≫ (x✝¹ • x✝)).hom = (x✝¹ • x✝² ≫ x✝).hom

Tactic:
apply comp_smul

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ᵣ D
G : D ⥤ᵣ E
⊢ rightExactFunctor C E ((forget D E ⋙ (Functor.whiskeringLeft C D E).obj F.obj).obj G)

Tactic:
dsimp; exact comp_preservesFiniteColimits _ _

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : D ⥤ᵣ E
G : C ⥤ᵣ D
⊢ rightExactFunctor C E ((forget C D ⋙ (Functor.whiskeringRight C D E).obj F.obj).obj G)

Tactic:
dsimp; exact comp_preservesFiniteColimits _ _

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ₑ D
G : D ⥤ₑ E
⊢ rightExactFunctor C E ((forget D E ⋙ (Functor.whiskeringLeft C D E).obj F.obj).obj G)

Tactic:
dsimp; exact comp_preservesFiniteColimits _ _

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : D ⥤ₑ E
G : C ⥤ₑ D
⊢ rightExactFunctor C E ((forget C D ⋙ (Functor.whiskeringRight C D E).obj F.obj).obj G)

Tactic:
dsimp; exact comp_preservesFiniteColimits _ _

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 : C
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
X✝ Y✝ : BinaryBicone P Q
f : X✝ ⟶ Y✝
⊢ { pt := F.obj X✝.pt, fst := F.map X✝.fst, snd := F.map X✝.snd, inl := F.map X✝.inl, inr := F.map X✝.inr, inl_fst := ⋯,
          inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }.inr ≫
      F.map f.hom =
    { pt := F.obj Y✝.pt, fst := F.map Y✝.fst, snd := F.map Y✝.snd, inl := F.map Y✝.inl, inr := F.map Y✝.inr,
        inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }.inr

Tactic:
simp [-BinaryBiconeMorphism.winr, ← f.winr]

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

Goal state before:
pp: J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j : Subtype p
⊢ ι f ↑j ≫ toSubtype f p = ι (Subtype.restrict p f) j

Tactic:
by
  classical
  ext
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π, biproduct.ι_π]
  split_ifs with h₁ h₂ h₂
  exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

Goal state after:
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
⊢ fst ≫ inl + snd ≫ inr = 𝟙 (X ⊞ Y)

Tactic:
by
  ext <;> simp

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 ⟶ Y
g : X ⟶ Z
⊢ map f g = fst ≫ f ≫ inl + snd ≫ g ≫ inr

Tactic:
by
  ext <;> simp

Goal state after:
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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
j : Subtype pᶜ
k : Subtype p
⊢ 0 ≫ biproduct.π (Subtype.restrict pᶜ f) j = 0

pp: case hnc
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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
j : Subtype pᶜ
k : Subtype p
⊢ ¬(p ↑k)ᶜ

Tactic:
· simp only [zero_comp]

Goal state after:
case hnc
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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
j : Subtype pᶜ
k : Subtype p
⊢ ¬(p ↑k)ᶜ
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
⊢ IsZero A ∧ IsZero B → IsZero (A ⊞ B)

Tactic:
rintro ⟨hA, hB⟩
    rw [IsZero.iff_id_eq_zero]
    apply biprod.hom_ext
    · apply hA.eq_of_tgt
    · apply hB.eq_of_tgt

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : 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
j : Fin n
hab : q.succAbove j < q
⊢ j.castSucc < q

Tactic:
simpa [succAbove_lt_iff_castSucc_lt] using hab

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_2
inst✝ : (i : Fin (n + 1)) → LE (α i)
⊢ insertNthOrderIso α 0 = consOrderIso α

Tactic:
ext; simp [insertNthOrderIso]

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

Goal state before:
pp: case a.a.a
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
| f ≫ (biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr)

pp: case a.a.a
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
| inv f

pp: case a.a
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.fst

pp: case a
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

Tactic:
rw [comp_add]

Goal state after:
case a.a.a
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
| f ≫ biprod.fst ≫ biprod.inl + f ≫ biprod.snd ≫ biprod.inr

case a.a.a
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
| inv f

case a.a
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.fst

case a
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
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
⊢ f ∈
      Trunc.lift
        (fun e ↦ map { toFun := fun f i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0, inj' := ⋯ } (finAntidiagonal (#s) n))
        ⋯ (Fintype.truncEquivFinOfCardEq ⋯) ↔
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Tactic:
induction Fintype.truncEquivFinOfCardEq (Fintype.card_coe s) using Trunc.ind with | _ e
   =>  _ 

Goal state after:
case a
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : ↥s ≃ Fin #s
⊢ f ∈
      Trunc.lift
        (fun e ↦ map { toFun := fun f i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0, inj' := ⋯ } (finAntidiagonal (#s) n))
        ⋯ (Trunc.mk e) ↔
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
⊢ ↑j - c.sizeUpTo ↑(c.index j) < c.blocksFun (c.index j)

Tactic:
by
    rw [tsub_lt_iff_right, add_comm, ← sizeUpTo_succ']
    · exact lt_sizeUpTo_index_succ _ _
    · exact sizeUpTo_index_le _ _

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✝ : 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:
by rintro ⟨⟩; simp

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✝ : 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:
by rintro ⟨⟩; simp

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

Goal state before:
pp: n₁ n₂ : ℕ
c₁ : Composition n₁
c₂ : Composition n₂
i₁ : Fin c₁.length
i₂ : Fin c₂.length
hn : n₁ = n₂
hc : c₁.blocks = c₂.blocks
hi : ↑i₁ = ↑i₂
⊢ c₁.blocksFun i₁ = c₂.blocksFun i₂

Tactic:
cases hn

Goal state after:
case refl
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin c₁.length
c₂ : Composition n₁
i₂ : Fin c₂.length
hc : c₁.blocks = c₂.blocks
hi : ↑i₁ = ↑i₂
⊢ c₁.blocksFun i₁ = c₂.blocksFun i₂
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:
by rintro ⟨⟩; simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : Perm α
x y : α
hy : (swap x (f x) * f) y ≠ y
⊢ f y ≠ y ∧ y ≠ x

Tactic:
by
  simp only [swap_apply_def, mul_apply, f.injective.eq_iff] at *
  grind

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✝ : 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:
by rintro ⟨⟩; simp

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

Goal state before:
pp: α : Type u_1
p : Perm α
n : ℤ
x : α
⊢ ¬(p ^ n) x = x → ¬p x = x

Tactic:
intro hx

Goal state after:
α : Type u_1
p : Perm α
n : ℤ
x : α
hx : ¬(p ^ n) x = x
⊢ ¬p x = x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ g x ∈ c.support ↔ x ∈ c.support

Tactic:
by
  simp only [mem_support, not_iff_not, ← mul_apply]
  rw [← hgc, mul_apply, Equiv.apply_eq_iff_eq]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → tl.prod.support = List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support tl)
h : List.Pairwise Disjoint (hd :: tl)
⊢ (hd :: tl).prod.support = List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support (hd :: tl))

Tactic:
rw [List.pairwise_cons] at h
    have : Disjoint hd tl.prod := disjoint_prod_right _ h.left
    simp [this.support_mul, hl h.right]

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

Goal state before:
pp: case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
⊢ (y :: l).formPerm (y :: l)[n] ≠ x

Tactic:
intro hx

Goal state after:
case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
hx : (y :: l).formPerm (y :: l)[n] = x
⊢ False
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
⊢ (y :: l).formPerm (y :: l)[n] ≠ y

Tactic:
intro hx

Goal state after:
case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
hx : (y :: l).formPerm (y :: l)[n] = y
⊢ False
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
⊢ Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ) = ⊤

Tactic:
apply top_unique
  rw [← mclosure_isSwap, Submonoid.closure_le]
  rintro _ ⟨i, j, ne, rfl⟩
  wlog lt : i < j generalizing i j
  · rw [swap_comm]; exact this _ _ ne.symm (ne.lt_or_gt.resolve_left lt)
  induction j using Fin.induction with
  | zero => cases lt
  | succ j ih =>
    have mem : swap j.castSucc j.succ ∈ Submonoid.closure
      (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ) := Submonoid.subset_closure ⟨_, rfl⟩
    obtain rfl | lts := (Fin.le_castSucc_iff.mpr lt).eq_or_lt
    · exact mem
    rw [swap_comm, ← swap_mul_swap_mul_swap (y := Fin.castSucc j) lts.ne lt.ne]
    exact mul_mem (mul_mem mem <| ih lts.ne lts) mem

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

Goal state before:
pp: n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if f⁻¹ ⟨a, b⟩.fst ≤ f⁻¹ ⟨a, b⟩.snd then -1 else 1) =
    if f (f⁻¹.signBijAux ⟨a, b⟩).fst ≤ f (f⁻¹.signBijAux ⟨a, b⟩).snd then -1 else 1

Tactic:
by
    by_cases h : f.symm b < f.symm a
    · simp_all [signBijAux, (mem_finPairsLT.1 hab).not_ge]
    · simp_all [signBijAux, dif_neg h, (mem_finPairsLT.1 hab).le]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
g : α
hg : f g ≠ g ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle g y
a : ℤ
ha : (f ^ a) g = x
b : ℤ
hb : (f ^ b) g = y
⊢ (f ^ (b - a) * f ^ a) g = y

Tactic:
← zpow_add,

Goal state after:
α : Type u_2
f : Perm α
x y : α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
g : α
hg : f g ≠ g ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle g y
a : ℤ
ha : (f ^ a) g = x
b : ℤ
hb : (f ^ b) g = y
⊢ (f ^ (b - a + a)) g = y
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case inr.inr
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1

Tactic:
· have le : 1 ≤ a₂ := Nat.succ_le_of_lt H'
      have lt : 1 < a₁ := le.trans_lt ha₁
      have h01 : Equiv.swap (0 : Fin (n + 2)) 1 1 = 0 := by simp only [swap_apply_right]
      rcases le.eq_or_lt with (rfl | lt')
      · rw [swap_apply_of_ne_of_ne H.ne' lt.ne', h01, if_neg H.not_ge]
      · rw [swap_apply_of_ne_of_ne (ne_of_gt H) (ne_of_gt lt),
          swap_apply_of_ne_of_ne (ne_of_gt H') (ne_of_gt lt'), if_neg ha₁.not_ge]

Goal state after: