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

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

Tactic:
← image.fac f,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
w : image.ι f = 0
⊢ factorThruImage f ≫ image.ι f = 0
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
P✝ : IsIsomorphic X 0
P : X ≅ 0
⊢ 0 ≫ 0 = 𝟙 X

Tactic:
rw [← P.hom_inv_id, ← Category.id_comp P.inv]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P✝ : IsIsomorphic X 0
P : X ≅ 0
⊢ 0 ≫ 0 = P.hom ≫ 𝟙 0 ≫ P.inv
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
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
X Y : C
f : X ⟶ Y
⊢ f = 0 → F.map f = 0

Tactic:
rintro rfl

Goal state after:
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
inst✝ : F.Faithful
X Y : C
⊢ F.map 0 = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Goal state before:
pp: case calc_2
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 C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F : C ⥤ D
inst✝ : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y) =
    F.map 0 ≫ F.map (F.rightAdjoint.map 0) ≫ adj.counit.app (F.obj Y)

pp: case calc_3
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 C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F : C ⥤ D
inst✝ : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ F.map 0 ≫ F.map (F.rightAdjoint.map 0) ≫ adj.counit.app (F.obj Y) = 0

Tactic:
· simp only [← Category.assoc, ← F.map_comp, zero_comp]

Goal state after:
case calc_3
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 C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F : C ⥤ D
inst✝ : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ F.map 0 ≫ F.map (F.rightAdjoint.map 0) ≫ adj.counit.app (F.obj Y) = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : HasEqualizers C
X Y : C
f : X ⟶ Y
h : f = 0
inst✝ : HasImage f
⊢ ι f = 0

Tactic:
rw [image.eq_fac h]
  simp

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
K✝ K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : ReflectsLimit K F), a = b

Tactic:
rintro ⟨a⟩ ⟨b⟩

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
a b : ∀ {c : Cone K} (hc : IsLimit (F.mapCone c)), Nonempty (IsLimit c)
⊢ ⋯ = ⋯
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
K✝ K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : ReflectsColimit K F), a = b

Tactic:
rintro ⟨a⟩ ⟨b⟩

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
a b : ∀ {c : Cocone K} (hc : IsColimit (F.mapCocone c)), Nonempty (IsColimit c)
⊢ ⋯ = ⋯
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✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ ∀ (a b : ReflectsLimitsOfShape J F), a = b

Tactic:
rintro ⟨a⟩ ⟨b⟩

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
a b : ∀ {K : J ⥤ C}, ReflectsLimit K F
⊢ ⋯ = ⋯
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
inst✝ : HasBinaryCoproduct X Y
Z✝ : C
x✝¹ x✝ : Y ⟶ Z✝
e : coprod.snd X Y ≫ x✝¹ = coprod.snd X Y ≫ x✝
⊢ x✝¹ = x✝

Tactic:
by simpa using congrArg (coprod.inr ≫ ·) e

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✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ ∀ (a b : ReflectsColimitsOfShape J F), a = b

Tactic:
rintro ⟨a⟩ ⟨b⟩

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J✝ : Type w
inst✝¹ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
inst✝ : Category.{w', w} J
F : C ⥤ D
a b : ∀ {K : J ⥤ C}, ReflectsColimit K F
⊢ ⋯ = ⋯
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
K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b

Tactic:
rintro ⟨a⟩ ⟨b⟩

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : ∀ {J : Type w} [inst : Category.{w', w} J], ReflectsLimitsOfShape J F
⊢ ⋯ = ⋯
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
K : J ⥤ C
F : C ⥤ D
⊢ ∀ (a b : ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b

Tactic:
rintro ⟨a⟩ ⟨b⟩

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
a b : ∀ {J : Type w} [inst : Category.{w', w} J], ReflectsColimitsOfShape J F
⊢ ⋯ = ⋯
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
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Cofork (𝟙 X) f
i : IsColimit c
this : Epi c.π := epi_of_isColimit_cofork i
⊢ i.desc (Cofork.ofπ f ⋯) ≫ c.π = 𝟙 c.pt

Tactic:
rw [← cancel_epi_id c.π, ← Category.assoc, Cofork.IsColimit.π_desc, Cofork.π_ofπ, ←
      c.condition]

Goal state after:
C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f✝ g : X✝ ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Cofork (𝟙 X) f
i : IsColimit c
this : Epi c.π := epi_of_isColimit_cofork i
⊢ 𝟙 X ≫ c.π = c.π
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)
⊢ IsIso ((Cocone.forget F).map ((colimit.isColimit F).descCoconeMorphism c))

Tactic:
suffices IsIso (IsColimit.descCoconeMorphism (colimit.isColimit F) c) from by
      apply (Cocone.forget F).map_isIso _

Goal state after:
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)
⊢ IsIso ((colimit.isColimit F).descCoconeMorphism c)
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case none.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : J
⊢ Finset (none ⟶ some j')

Tactic:
· exact {Hom.init j'}

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

Goal state before:
pp: 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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
hc : (c.whisker g).IsBilimit
this✝ : IsColimit
  ((Cocone.precompose (Discrete.functorComp f ⇑g).hom).obj
    (Cocone.whisker (Discrete.functor (Discrete.mk ∘ ⇑g)) c.toCocone)) :=
  hc.isColimit.ofIsoColimit (c.whiskerToCocone g)
this : IsColimit (Cocone.whisker (Discrete.functor (Discrete.mk ∘ ⇑g)) c.toCocone) :=
  (IsColimit.precomposeHomEquiv (Discrete.functorComp f ⇑g)
      (Cocone.whisker (Discrete.functor (Discrete.mk ∘ ⇑g)) c.toCocone))
    this✝
⊢ IsColimit c.toCocone

Tactic:
exact IsColimit.ofWhiskerEquivalence (Discrete.equivalence g) this

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

Goal state before:
pp: case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
j : J
h : ¬k = e j
⊢ j ≠ e.symm k

Tactic:
rintro rfl

Goal state after:
case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
h : ¬k = e (e.symm k)
⊢ False
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ e.symm k ≠ j

Tactic:
rintro rfl

Goal state after:
case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
h : ¬k = e (e.symm k)
⊢ False
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:
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.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⟩

Goal state after:
case mpr
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
A B : C
inst✝ : HasBinaryBiproduct A B
hA : IsZero A
hB : IsZero B
⊢ IsZero (A ⊞ B)
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

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

Tactic:
obtain ⟨q : X ⟶ T, hq : b.fst ≫ q = m - (b.fst ≫ f + b.snd ≫ g)⟩ :=
        CokernelCofork.IsColimit.desc' hb _ h₂'

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
q : X ⟶ T
hq : b.fst ≫ q = m - (b.fst ≫ f + b.snd ≫ g)
⊢ m = b.fst ≫ f + b.snd ≫ g
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
⊢ f ∈ (antidiagonal n).disjiUnion (fun ab ↦ map { toFun := Fin.cons ab.1, inj' := ⋯ } ↑(aux d ab.2)) ⋯ ↔ ∑ i, f i = n

Tactic:
simp_rw [mem_disjiUnion, mem_antidiagonal, mem_map, Embedding.coeFn_mk, Prod.exists,
          (aux d _).prop, Fin.sum_univ_succ]

Goal state after:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
⊢ (∃ a b, a + b = n ∧ ∃ a_1, ∑ i, a_1 i = b ∧ Fin.cons a a_1 = f) ↔ f 0 + ∑ i, f i.succ = n
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n : ℕ
c : Composition n
⊢ n = 0 → c.blocks = []

Tactic:
rintro rfl

Goal state after:
case mpr
c : Composition 0
⊢ c.blocks = []
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr.refine_1
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
⊢ ↑j - c.sizeUpTo ↑i < c.blocksFun i

Tactic:
rw [tsub_lt_iff_left, ← sizeUpTo_succ']
      · exact h.2
      · exact h.1

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

Tactic:
rintro ⟨⟩; 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✝ : PreservesColimit (Discrete.functor f) F
b : Bicone f
hb : b.IsBilimit
val✝ : Fintype J
⊢ ∀ (j : Discrete J),
    ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).ι.app j ≫
        (Iso.refl ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).pt).hom =
      (F.mapBicone b).toCocone.ι.app j

Tactic:
rintro ⟨⟩; simp

Goal state after:
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

Goal state after:
case mp
n : ℕ
⊢ ∀ i ∈ (ones n).blocks, i = 1
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
c : Composition n
⊢ c = ones n → c.length = n

Tactic:
rintro rfl

Goal state after:
case mp
n : ℕ
⊢ (ones n).length = n
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
hn : 0 < n
c : Composition n
⊢ c = single n hn → ∃ i, n ≤ c.blocksFun i

Tactic:
rintro rfl

Goal state after:
case mp
n : ℕ
hn : 0 < n
⊢ ∃ i, n ≤ (single n hn).blocksFun i
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)
⊢ ((insert i s).noncommProd k ⋯).support = (insert i s).biUnion fun i ↦ (k i).support

Tactic:
have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
      hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.biUnion_insert]
    rw [Equiv.Perm.Disjoint.support_mul, hrec hs']
    apply disjoint_noncommProd_right
    intro j hj
    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.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
b : α
l' : List α
x : α
hx : (zipWith Equiv.swap (a :: l) (b :: l')).prod x ≠ x
h : (zipWith Equiv.swap l l').prod x = x
⊢ x = a → x ∈ a :: l

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
b : α
l' : List α
x : α
h : (zipWith Equiv.swap l l').prod x = x
hx : (zipWith Equiv.swap (x :: l) (b :: l')).prod x ≠ x
⊢ x ∈ x :: l
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mp
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
⊢ x ∈ Set.range Sum.inr → σ x ∈ Set.range Sum.inr

Tactic:
rcases hx : σ x with l | r

Goal state after:
case mp.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
l : m
hx : σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inr → Sum.inl l ∈ Set.range Sum.inr

case mp.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inr → Sum.inr r ∈ Set.range Sum.inr
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
b : α
l' : List α
x : α
hx : (zipWith Equiv.swap (a :: l) (b :: l')).prod x ≠ x
h : (zipWith Equiv.swap l l').prod x = x
⊢ x = b → x ∈ b :: l'

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
l l' : List α
x : α
h : (zipWith Equiv.swap l l').prod x = x
hx : (zipWith Equiv.swap (a :: l) (x :: l')).prod x ≠ x
⊢ x ∈ x :: l'
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : (swap x y).support = {x, y}
⊢ x ≠ y

Tactic:
rintro rfl

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : α
h : (swap x x).support = {x, x}
⊢ False
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mpr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
⊢ x ∈ Set.range Sum.inl → σ x ∈ Set.range Sum.inl

Tactic:
rcases hx : σ x with l | r

Goal state after:
case mpr.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inl → Sum.inl l ∈ Set.range Sum.inl

case mpr.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inl → Sum.inr r ∈ Set.range Sum.inl
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : f a = a
x : α
hx : f x ≠ x
⊢ x ≠ a

Tactic:
rintro rfl

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
x : α
hx : f x ≠ x
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfa : f x = x
⊢ False
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
n : ℕ
ih : swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
⊢ swap ((⇑σ ∘ ⇑(σ ^ n)) x) ((⇑σ ∘ ⇑σ ∘ ⇑(σ ^ n)) x) = swap (σ ((σ ^ n) x)) (σ ((⇑σ ∘ ⇑(σ ^ n)) x))

Tactic:
comp_apply

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

Goal state before:
pp: α : Type u_2
f g : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, f x = g x
hx : f x = g x
hx' : x ∈ f.support
⊢ f = g

Tactic:
have hx'' : x ∈ g.support := by rwa [mem_support, ← hx, ← mem_support]
  have : f.support ⊆ g.support := by
    intro y hy
    obtain ⟨k, rfl⟩ := hf.exists_pow_eq (mem_support.mp hx') (mem_support.mp hy)
    rwa [pow_eq_on_of_mem_support h _ _ (mem_inter_of_mem hx' hx''), pow_apply_mem_support]
  rw [inter_eq_left.mpr this] at h
  exact hf.support_congr hg this h

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

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
⊢ f ^ n = 1 ↔ ∃ x, f x ≠ x ∧ (f ^ n) x = x

Tactic:
by
  classical
    cases nonempty_fintype β
    constructor
    · intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩
    · rintro ⟨x, hx, hx'⟩
      by_cases h : support (f ^ n) = support f
      · rw [← mem_support, ← h, mem_support] at hx
        contradiction
      · rw [hf.support_pow_eq_iff, Classical.not_not] at h
        obtain ⟨k, rfl⟩ := h
        rw [pow_mul, pow_orderOf_eq_one, one_pow]

Goal state after: