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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
⊢ (X Y : Discrete PEmpty.{?u.10 + 1}) → Zero (X ⟶ Y)

Tactic:
by cat_disch

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

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

Tactic:
← id_comp f,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ 𝟙 X ≫ f = default
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X✝ : C
inst✝¹ : PreservesLimit (Functor.empty C) G
inst✝ : ReflectsLimit (Functor.empty C) G
X : C
⊢ Function.LeftInverse (isTerminalOfObj G X) (isTerminalObj G X)

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X✝ : C
inst✝¹ : PreservesLimit (Functor.empty C) G
inst✝ : ReflectsLimit (Functor.empty C) G
X : C
⊢ Function.RightInverse (isTerminalOfObj G X) (isTerminalObj G X)

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
i : IsIso (terminalComparison G)
⊢ IsLimit (G.mapCone (asEmptyCone (⊤_ C)))

Tactic:
apply (isLimitMapConeEmptyConeEquiv _ _).symm _

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
i : IsIso (terminalComparison G)
⊢ IsTerminal (G.obj (⊤_ C))
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X✝ : C
inst✝¹ : PreservesColimit (Functor.empty C) G
inst✝ : ReflectsColimit (Functor.empty C) G
X : C
⊢ Function.LeftInverse (isInitialOfObj G X) (isInitialObj G X)

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X✝ : C
inst✝¹ : PreservesColimit (Functor.empty C) G
inst✝ : ReflectsColimit (Functor.empty C) G
X : C
⊢ Function.RightInverse (isInitialOfObj G X) (isInitialObj G X)

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ Function.LeftInverse ⋯ fun h ↦ { hom := 0, inv := 0, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ Function.RightInverse ⋯ fun h ↦ { hom := 0, inv := 0, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
X Y : C
inst✝² : Category.{v, u} C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
X' Y' Z : C
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : X ⟶ X'
q : Y ⟶ Y'
wf : f ≫ q = p ≫ f'
wg : g ≫ q = p ≫ g'
h : Y' ⟶ Z
wh : f' ≫ h = g' ≫ h
⊢ π f g ≫ colimMap (parallelPairHom f g f' g' p q wf wg) ≫ desc h wh = q ≫ h

Tactic:
ι_colimMap_assoc,

Goal state after:
C : Type u
X Y : C
inst✝² : Category.{v, u} C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
X' Y' Z : C
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : X ⟶ X'
q : Y ⟶ Y'
wf : f ≫ q = p ≫ f'
wg : g ≫ q = p ≫ g'
h : Y' ⟶ Z
wh : f' ≫ h = g' ≫ h
⊢ (parallelPairHom f g f' g' p q wf wg).app one ≫ colimit.ι (parallelPair f' g') one ≫ desc h wh = q ≫ h
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X Y : C
h : 𝟙 X = 0 ∧ 𝟙 Y = 0
⊢ 0 ≫ 0 = 𝟙 X ∧ 0 ≫ 0 = 𝟙 Y

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X Y : C
⊢ Function.LeftInverse ⋯ ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms C
X Y : C
⊢ Function.RightInverse ⋯ ⋯

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
⊢ ∀ (a : ⊥_ C ⟶ X), a = default

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
⊢ ∀ (a : X ⟶ ⊤_ C), a = default

Tactic:
by cat_disch

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

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
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F G : C ⥤ D
H : D ⥤ E
inst✝ : H.PreservesZeroMorphisms
⊢ whiskerRight 0 H = 0

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
this : IsIso ((Cocone.functoriality F G).map ((colimit.isColimit F).descCoconeMorphism c))
⊢ IsIso ((colimit.isColimit F).descCoconeMorphism c)

Tactic:
by
        apply isIso_of_reflects_iso _ (Cocone.functoriality F G)

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 Y : InducedCategory C F
⊢ ∀ (m : R) (x : X ⟶ Y),
    InducedCategory.homAddEquiv.toFun (m • x) = (RingHom.id R) m • InducedCategory.homAddEquiv.toFun x

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : HMul.hMul = HMul.hMul
h_inv : Inv.inv = Inv.inv
⊢ m₁ = m₂

Tactic:
have h_mon := Monoid.ext h_mul
  have h₁ : m₁.one = m₂.one := congr_arg (·.one) h_mon
  let f : @MonoidHom M M m₁.toMulOne m₂.toMulOne :=
    @MonoidHom.mk _ _ (_) _ (@OneHom.mk _ _ (_) _ id h₁)
      (fun x y => congr_fun (congr_fun h_mul x) y)
  have : m₁.zpow = m₂.zpow := by
    ext m x
    exact @MonoidHom.map_zpow' M M m₁ m₂ f (congr_fun h_inv) x m
  have : m₁.div = m₂.div := by
    ext a b
    exact (@div_eq_mul_inv _ m₁ a b).trans
      (((congr_fun (congr_fun h_mul a) _).trans
        (congr_arg _ (congr_fun h_inv b))).trans (@div_eq_mul_inv _ m₂ a b).symm)
  rcases m₁ with @⟨_, ⟨_⟩, ⟨_⟩, ⟨_⟩⟩
  congr

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
inst✝³ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝² : HasKernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
inst✝¹ : IsIso p
inst✝ : Mono q
⊢ kernel.map f f' p q w ≫ kernel.lift f (kernel.ι f' ≫ inv p) ⋯ = 𝟙 (kernel f)

Tactic:
by cat_disch

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
inst✝³ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝² : HasKernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
inst✝¹ : IsIso p
inst✝ : Mono q
⊢ kernel.lift f (kernel.ι f' ≫ inv p) ⋯ ≫ kernel.map f f' p q w = 𝟙 (kernel f')

Tactic:
by cat_disch

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
inst✝³ : HasCokernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝² : HasCokernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
inst✝¹ : Epi p
inst✝ : IsIso q
⊢ cokernel.map f f' p q w ≫ cokernel.desc f' (inv q ≫ cokernel.π f) ⋯ = 𝟙 (cokernel f)

Tactic:
by cat_disch

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
inst✝³ : HasCokernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝² : HasCokernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
inst✝¹ : Epi p
inst✝ : IsIso q
⊢ cokernel.desc f' (inv q ≫ cokernel.π f) ⋯ ≫ cokernel.map f f' p q w = 𝟙 (cokernel f')

Tactic:
by cat_disch

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
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : G.Full
inst✝ : G.Faithful
X✝ Y✝ : Bicone F
t : (functoriality F G).obj X✝ ⟶ (functoriality F G).obj Y✝
⊢ (functoriality F G).map { hom := G.preimage t.hom, wπ := ⋯, wι := ⋯ } = t

Tactic:
by cat_disch

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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
k k' : K
⊢ c.ι (g k) ≫ c.π (g k') = if h : k = k' then eqToHom ⋯ else 0

Tactic:
by
    simp only [c.ι_π]
    split_ifs with h h' h' <;> simp [Equiv.apply_eq_iff_eq g] at h h' <;> tauto

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasKernels C
⊢ ι C ≫ Arrow.leftToRight = 0

Tactic:
by cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasCokernels C
⊢ Arrow.leftToRight ≫ π C = 0

Tactic:
by cat_disch

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
inst✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ : BinaryBicone P Q
t : (functoriality P Q F).obj X✝ ⟶ (functoriality P Q F).obj Y✝
⊢ (functoriality P Q F).map { hom := F.preimage t.hom, wfst := ⋯, wsnd := ⋯, winl := ⋯, winr := ⋯ } = t

Tactic:
by cat_disch

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

Goal state before:
pp: 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
⊢ map f g = map' f g

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

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
T : C
f : T ⟶ X
g : T ⟶ Y
⊢ lift f g = f ≫ inl + g ≫ inr

Tactic:
ext <;> simp [add_comp]

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
⊢ ∀ {W' : C} (g' : W' ⟶ ⨁ f),
    g' ≫ biproduct.toSubtype f p = 0 →
      ∀ (m : W' ⟶ ⨁ Subtype.restrict pᶜ f), m ≫ biproduct.fromSubtype f pᶜ = g' → m = g' ≫ biproduct.toSubtype f pᶜ

Tactic:
by cat_disch

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
⊢ ∀ {Z' : C} (g' : ⨁ f ⟶ Z'),
    biproduct.fromSubtype f p ≫ g' = 0 →
      ∀ (m : ⨁ Subtype.restrict pᶜ f ⟶ Z'), biproduct.toSubtype f pᶜ ≫ m = g' → m = biproduct.fromSubtype f pᶜ ≫ g'

Tactic:
by cat_disch

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
⊢ { app := fun M ↦ M.smul 1, naturality := ⋯ } = 1

Tactic:
by cat_disch

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
x✝¹ x✝ : R
⊢ { app := fun M ↦ M.smul (x✝¹ * x✝), naturality := ⋯ } =
    { app := fun M ↦ M.smul x✝¹, naturality := ⋯ } * { app := fun M ↦ M.smul x✝, naturality := ⋯ }

Tactic:
by cat_disch

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
⊢ { app := fun M ↦ M.smul 0, naturality := ⋯ } = 0

Tactic:
by cat_disch

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N : ModuleCat R
x✝¹ x✝ : R
⊢ { app := fun M ↦ M.smul (x✝¹ + x✝), naturality := ⋯ } =
    { app := fun M ↦ M.smul x✝¹, naturality := ⋯ } + { app := fun M ↦ M.smul x✝, naturality := ⋯ }

Tactic:
by cat_disch

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

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

Tactic:
refine ⟨fun h ↦ funext fun i ↦ ?_, fun h ↦ by simp [h, strictMono_id]⟩
  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)
  simpa using congrFun (key _ h) i.succ

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
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
g₁₁ : Y₁ ⟶ Z₁
g₁₂ : Y₁ ⟶ Z₂
g₂₁ : Y₂ ⟶ Z₁
g₂₂ : Y₂ ⟶ Z₂
⊢ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ ofComponents g₁₁ g₁₂ g₂₁ g₂₂ =
    ofComponents (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂)

Tactic:
dsimp [Biprod.ofComponents]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
g₁₁ : Y₁ ⟶ Z₁
g₁₂ : Y₁ ⟶ Z₂
g₂₁ : Y₂ ⟶ Z₁
g₂₂ : Y₂ ⟶ Z₂
⊢ (biprod.fst ≫ f₁₁ ≫ biprod.inl + biprod.fst ≫ f₁₂ ≫ biprod.inr + biprod.snd ≫ f₂₁ ≫ biprod.inl +
        biprod.snd ≫ f₂₂ ≫ biprod.inr) ≫
      (biprod.fst ≫ g₁₁ ≫ biprod.inl + biprod.fst ≫ g₁₂ ≫ biprod.inr + biprod.snd ≫ g₂₁ ≫ biprod.inl +
        biprod.snd ≫ g₂₂ ≫ biprod.inr) =
    biprod.fst ≫ (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) ≫ biprod.inl + biprod.fst ≫ (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) ≫ biprod.inr +
        biprod.snd ≫ (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) ≫ biprod.inl +
      biprod.snd ≫ (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) ≫ biprod.inr
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
c : Composition n
⊢ c = ones n → ∀ i ∈ c.blocks, i = 1

Tactic:
rintro rfl
    exact fun i => eq_of_mem_replicate

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

Goal state before:
pp: case mpr
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ n < n

Tactic:
calc
      n = ∑ i : Fin c.length, 1 := by simp [length_n]
      _ < ∑ i : Fin c.length, c.blocksFun i := by
        {
        obtain ⟨i, hi, i_blocks⟩ : ∃ i ∈ c.blocks, 1 < i := ne_ones_iff.1 H
        rw [← ofFn_blocksFun, mem_ofFn' c.blocksFun, Set.mem_range] at hi
        obtain ⟨j : Fin c.length, hj : c.blocksFun j = i⟩ := hi
        rw [← hj] at i_blocks
        exact Finset.sum_lt_sum (fun i _ => one_le_blocksFun c i) ⟨j, Finset.mem_univ _, i_blocks⟩
        }
      _ = n := c.sum_blocksFun

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f g : α → β
hf : Function.Injective f
hg : Function.Injective g
⊢ ∃ σ, ∀ (a : α), σ (f a) = g a

Tactic:
by
  classical
  have : Finite {x | x ∈ Set.range f} := .of_surjective _ (Set.codRestrict_range_surjective f)
  refine ⟨((Equiv.ofInjective f hf).symm.trans (Equiv.ofInjective g hg)).extendSubtype, ?_⟩
  simp [Equiv.extendSubtype_apply_of_mem]

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

Goal state before:
pp: case insert
α : 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
⊢ (k i).Disjoint (k j)

Tactic:
apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
      simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

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

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

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

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
x : α
hx : x ∈ f.support
⊢ x ∈ l.prod.support

Tactic:
rwa [mem_support, ← eq_on_support_mem_disjoint h hl _ hx, ← mem_support]

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

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle ((Equiv.symm f) x) y ↔ f.SameCycle x y

Tactic:
← sameCycle_apply_left,

Goal state after:
α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle (f ((Equiv.symm f) x)) y ↔ f.SameCycle x y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
n : ℤ
⊢ (∃ b, (f ^ (Equiv.symm (Equiv.addRight n)) b) ((f ^ n) x) = y) ↔ f.SameCycle x y

Tactic:
by simp [SameCycle, zpow_add]

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

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

Tactic:
swap_apply_of_ne_of_ne (ne_of_gt H) (ne_of_gt lt),

Goal state after:
case inr.inr.inr
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : (swap 0 1) 1 = 0
lt' : 1 < a₂
⊢ (if a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
⊢ 2 ≤ n + 2

Tactic:
exact le_add_self

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), f x ≠ x → x ∈ []
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f

Tactic:
by
    have : f = 1 := Equiv.ext fun y => Classical.not_not.1 (mt (h y) List.not_mem_nil)
    rw [this, one_def, Equiv.trans_refl, Equiv.symm_trans_self, ← one_def, signAux_one, signAux2]

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

Goal state before:
pp: case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a : Perm α
⊢ ∀ (y : Perm α),
    a ∈ closure S →
      y ∈ closure S →
        ↑a.support ⊆ ⋃ b ∈ S, ↑b.support → ↑y.support ⊆ ⋃ b ∈ S, ↑b.support → ↑(a * y).support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
b

Goal state after:
case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
⊢ a ∈ closure S →
    b ∈ closure S →
      ↑a.support ⊆ ⋃ b ∈ S, ↑b.support → ↑b.support ⊆ ⋃ b ∈ S, ↑b.support → ↑(a * b).support ⊆ ⋃ b ∈ S, ↑b.support
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : a ∈ closure S
⊢ ∀ b ∈ closure T, _root_.Disjoint a.support b.support

Tactic:
b

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : a ∈ closure S
b : Perm α
⊢ b ∈ closure T → _root_.Disjoint a.support b.support
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
⊢ sign (prodCongrLeft σ) = ∏ k, sign (σ k)

Tactic:
refine (sign_eq_sign_of_equiv _ _ (prodComm β α) ?_).trans (sign_prodCongrRight σ)
  rintro ⟨b, α⟩
  rfl

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ σ ∈ (ofSign 1).disjUnion (ofSign (-1)) ⋯ ↔ σ ∈ univ

Tactic:
simp_rw [mem_disjUnion, mem_ofSign, Int.units_eq_one_or, mem_univ]

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

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

Tactic:
apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
      simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
⊢ (g * f⁻¹).cycleType + f.cycleType = g.cycleType - f.cycleType + f.cycleType

Tactic:
← (disjoint_mul_inv_of_mem_cycleFactorsFinset hf).cycleType_mul,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
hf : f ∈ g.cycleFactorsFinset
⊢ (g * f⁻¹ * f).cycleType = g.cycleType - f.cycleType + f.cycleType