mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hg : Surjective ⇑g
h : P → N
hfg : Exact ⇑f ⇑g
hgh : RightInverse h ⇑g
r : R
p : P
q : Q
⊢ ((TensorProduct.mk R N Q) (h (r • p))) q - (fun x ↦ (RingHom.id R) r • x) (((TensorProduct.mk R N Q) (h p)) q) ∈
    (rTensor Q f).range

Tactic:
by
      change h (r • p) ⊗ₜ[R] q - r • h p ⊗ₜ[R] q ∈ range (rTensor Q f)
      rw [TensorProduct.smul_tmul', ← TensorProduct.sub_tmul]
      apply le_comap_range_rTensor f
      rw [exact_iff] at hfg
      simp only [← hfg, mem_ker, map_sub, map_smul, hgh _, sub_self]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Balance

Goal state before:
pp: case inl
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
h✝ : IsEmpty ι
⊢ ∑ x, balance f x = 0

Tactic:
simp [balance_apply]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Balance

Goal state before:
pp: case inr
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
h✝ : Nonempty ι
⊢ ∑ x, balance f x = 0

Tactic:
simp [balance_apply]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Field

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Fintype β
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (s.biUnion t).dens ≤ ∑ a ∈ s, (t a).dens

Tactic:
simp only [dens, ← sum_div]
  gcongr
  exact mod_cast card_biUnion_le

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
⊢ map (⇑(Sym2.equivSym α)) xs.sym2 = List.sym 2 xs

Tactic:
by
  induction xs with
  | nil => simp only [List.sym, map_eq_nil_iff, sym2_eq_nil_iff]
  | cons x xs ih =>
    rw [List.sym, ← ih, sym_one_eq, map_map, List.sym2, map_append, map_map]
    rfl

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α
f✝ : α → β
r r₁ r₂ : α → α → Prop
sym : Std.Symm r
f : α → β
hf : r ≤ ⇑(Setoid.ker f)
z : ↑(fromRel sym)
a₁ a₂ : α
h : r a₁ a₂
⊢ ⟨f a₁, ⟨s(⟨a₁, ⋯⟩, ⟨a₂, ⋯⟩), h⟩⟩ = ⟨f a₂, ⟨s(⟨a₂, ⋯⟩, ⟨a₁, ⋯⟩), ⋯⟩⟩

Tactic:
rw! [

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α
f✝ : α → β
r r₁ r₂ : α → α → Prop
sym : Std.Symm r
f : α → β
hf : r ≤ ⇑(Setoid.ker f)
z : ↑(fromRel sym)
a₁ a₂ : α
h : r a₁ a₂
⊢ ⟨f a₁, ⟨s(⟨a₁, ⋯⟩, ⟨a₂, ⋯⟩), h⟩⟩ = ⟨f a₂, ⟨s(⟨a₂, ⋯⟩, ⟨a₁, ⋯⟩), ⋯⟩⟩
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
x✝ y✝ : α
h : x✝ = y✝
⊢ #s(x✝, y✝).toFinset = 1

Tactic:
simp [Sym2.toFinset_mk_eq, h]

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
x✝ y✝ : α
h : ¬x✝ = y✝
⊢ #s(x✝, y✝).toFinset = 2

Tactic:
simp [Sym2.toFinset_mk_eq, h]

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

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

Tactic:
convert! cancel_epi f

Goal state after:
case e'_1.e'_3
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : Y ⟶ Y
⊢ f = f ≫ 𝟙 Y
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_2
R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring S'
inst✝⁷ : Algebra R R'
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra R S'
inst✝³ : IsScalarTower R R' S'
inst✝² : IsScalarTower R S S'
H : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
⊢ ∀ (m : R'), f ((toAlgHom R R' S').toLinearMap m) = g ((toAlgHom R R' S').toLinearMap m)

Tactic:
exact AlgHom.congr_fun h₁

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

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
ι : Type u'
X : ι → C
F : C ⥤ D
Y : D
⊢ (ofObj X).strictMap F Y ↔ ofObj (F.obj ∘ X) Y

Tactic:
simp [ofObj_iff, strictMap_iff]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X : Push σ),
    Φ.obj X =
      { obj := τ, map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x ↦ τ X ⟶ τ Y) fun X Y f ↦ ⋯.mpr (⋯.mpr (φ.map f)) }.obj
        X

pp: case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X Y : Push σ) (f : X ⟶ Y),
    Φ.map f =
      Eq.recOn ⋯
        (Eq.recOn ⋯
          ({ obj := τ,
                map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x ↦ τ X ⟶ τ Y) fun X Y f ↦ ⋯.mpr (⋯.mpr (φ.map f)) }.map
            f))

Tactic:
· intro X
    simp only
    rw [Φ₀]

Goal state after:
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X Y : Push σ) (f : X ⟶ Y),
    Φ.map f =
      Eq.recOn ⋯
        (Eq.recOn ⋯
          ({ obj := τ,
                map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x ↦ τ X ⟶ τ Y) fun X Y f ↦ ⋯.mpr (⋯.mpr (φ.map f)) }.map
            f))
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
L : C ⥤ D
inst✝ : L.EssSurj
h : ∀ ⦃X₁ X₂ : C⦄ (f g : L.obj X₁ ⟶ L.obj X₂), F.map f = F.map g → f = g
X✝ Y✝ : D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hfg : F.map a₁✝ = F.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
← cancel_mono (L.objObjPreimageIso _).inv,

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
L : C ⥤ D
inst✝ : L.EssSurj
h : ∀ ⦃X₁ X₂ : C⦄ (f g : L.obj X₁ ⟶ L.obj X₂), F.map f = F.map g → f = g
X✝ Y✝ : D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hfg : F.map a₁✝ = F.map a₂✝
⊢ a₁✝ ≫ (L.objObjPreimageIso Y✝).inv = a₂✝ ≫ (L.objObjPreimageIso Y✝).inv
Module: Mathlib.CategoryTheory.Whiskering

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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
inst✝ : IsIso α
⊢ whiskerRight (inv α) F ≫ whiskerRight α F = 𝟙 (H ⋙ F)

Tactic:
simp [← whiskerRight_comp]

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Sort u_1
W : ι → MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ iSup W f ↔ ∃ i, W i f

Tactic:
by
  simp [← sSup_range]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsGroupoid C → isomorphisms C = ⊤

Tactic:
rw [eq_top_iff]

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsGroupoid C → ⊤ ≤ isomorphisms C
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ Hom.left sq ≫ Hom.left (inv sq) = 𝟙 f.left ∧ Hom.left (inv sq) ≫ Hom.left sq = 𝟙 g.left

Tactic:
by simp [← comp_left]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
⊢ ⊤.map F = ⊤

Tactic:
rw [eq_top_iff]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
⊢ ⊤ ≤ ⊤.map F
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ Hom.left sq ≫ Hom.left (inv sq) = 𝟙 f.left

Tactic:
by simp [← comp_left]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ (adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g

Tactic:
rw [← Equiv.eq_symm_apply]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = (adj.homEquiv X' Y).symm (f ≫ (adj.homEquiv X Y) g)
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
r t : Cone F
P : IsLimit r
i : r ≅ t
s : Cone F
m : s ⟶ t
⊢ m = P.liftConeMorphism s ≫ i.hom

Tactic:
rw [← i.comp_inv_eq]

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
r t : Cone F
P : IsLimit r
i : r ≅ t
s : Cone F
m : s ⟶ t
⊢ m ≫ i.inv = P.liftConeMorphism s
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ (adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g

Tactic:
rw [← Equiv.eq_symm_apply]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = (adj.homEquiv X' Y).symm (f ≫ (adj.homEquiv X Y) g)
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquivUnitCounit F G
X : C
⊢ F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)

Tactic:
rw [← adj.homEquiv_counit, (adj.homEquiv _ _).symm_apply_eq, adj.homEquiv_unit]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquivUnitCounit F G
X : C
⊢ adj.unit.app X = adj.unit.app X ≫ G.map (𝟙 (F.obj X))
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (F.map g.op)) (yonedaEquiv f) = yonedaEquiv (yoneda.map g ≫ f)

Tactic:
by
  simp [yonedaEquiv, ← f.naturality_apply]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsInitial X
f : Y ⟶ X
⊢ Epi f

Tactic:
have := t.isSplitEpi_to f; infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
⊢ m = I.lift (BinaryFan.swap t)

Tactic:
by
    have h := I.uniq (BinaryFan.swap t) m
    rw [h]
    rintro ⟨j⟩
    specialize w ⟨WalkingPair.swap j⟩
    cases j <;> exact w

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x✝ : Over Y
⊢ (mapId Y).hom.app x✝ = eqToHom ⋯

Tactic:
by ext; simp [eqToHom_left]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
x✝ : Over X
⊢ (mapComp f g).hom.app x✝ = eqToHom ⋯

Tactic:
by ext; simp [eqToHom_left]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
⊢ IsIso (pullback.fst (f ≫ i) i)

Tactic:
have := limit.isoLimitCone_hom_π ⟨_, pullbackIsPullbackOfCompMono f (𝟙 _) i⟩ WalkingCospan.left

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
this :
  (limit.isoLimitCone
          { cone := mk (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
            isLimit := pullbackIsPullbackOfCompMono f (𝟙 Z) i }).hom ≫
      { cone := mk (pullback.fst f (𝟙 Z)) (pullback.snd f (𝟙 Z)) ⋯,
                isLimit := pullbackIsPullbackOfCompMono f (𝟙 Z) i }.cone.π.app
        WalkingCospan.left =
    limit.π (cospan (f ≫ i) (𝟙 Z ≫ i)) WalkingCospan.left
⊢ IsIso (pullback.fst (f ≫ i) i)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
⊢ IsIso (pullback.fst (f ≫ i) i)

Tactic:
have := limit.isoLimitCone_hom_π ⟨_, pullbackIsPullbackOfCompMono f (𝟙 _) i⟩ WalkingCospan.left
  convert! (congrArg IsIso (show _ ≫ pullback.fst f (𝟙 Z) = _ from this)).mp inferInstance
  · exact (Category.id_comp _).symm
  · exact (Category.id_comp _).symm

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
t : Fork f g
lift : (s : Fork f g) → s.pt ⟶ t.pt
fac : ∀ (s : Fork f g), lift s ≫ t.ι = s.ι
uniq : ∀ (s : Fork f g) (m : s.pt ⟶ t.pt), m ≫ t.ι = s.ι → m = lift s
s : Cone (parallelPair f g)
j : WalkingParallelPair
⊢ lift s ≫ t.π.app one = s.π.app one

Tactic:
by
        simp [← Category.assoc, fac]

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

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ 𝟙 Y = 0 → f = 0

pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ f = 0 → 𝟙 Y = 0

Tactic:
· intro h
    rw [← Category.comp_id f, h, comp_zero]

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
⊢ f = 0 → 𝟙 Y = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
hX : IsTerminal X
⊢ IsZero X

Tactic:
rw [IsZero.iff_id_eq_zero]
  apply hX.hom_ext

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
hX : IsInitial X
⊢ IsZero X

Tactic:
rw [IsZero.iff_id_eq_zero]
  apply hX.hom_ext

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
inst✝ : HasBinaryCoproduct X Y
Z✝ : C
x✝¹ x✝ : Y ⟶ Z✝
e : coprod.snd X Y ≫ x✝¹ = coprod.snd X Y ≫ x✝
⊢ x✝¹ = x✝

Tactic:
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
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 ((colimit.isColimit F).desc c)
⊢ IsColimit c

Tactic:
by
      apply IsColimit.ofPointIso (colimit.isColimit F)

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

Goal state before:
pp: C : Type u_1
D : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} J
K : J ⥤ C
L L' : C ⥤ D
α : L ⟶ L'
inst✝² : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst✝¹ : PreservesColimit K L
inst✝ : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt :=
  (isColimitOfPreserves L hc).coconePointsIsoOfNatIso (isColimitOfPreserves L' hc) (asIso (K.whiskerLeft α))
⊢ IsIso (α.app c.pt)

Tactic:
convert! (inferInstance : IsIso e.hom)

Goal state after:
case e'_5
C : Type u_1
D : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} J
K : J ⥤ C
L L' : C ⥤ D
α : L ⟶ L'
inst✝² : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst✝¹ : PreservesColimit K L
inst✝ : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt := ⋯
e_3✝ : L.obj c.pt = (L.mapCocone c).pt
e_4✝ : L'.obj c.pt = (L'.mapCocone c).pt
⊢ α.app c.pt = e.hom
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasBinaryProducts D
i : ∀ {X Y : C}, IsIso (prodComparison G X Y)
⊢ ∀ {K : Discrete WalkingPair ⥤ C}, PreservesLimit K G

Tactic:
intro K

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasBinaryProducts D
i : ∀ {X Y : C}, IsIso (prodComparison G X Y)
K : Discrete WalkingPair ⥤ C
⊢ PreservesLimit K G
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasBinaryCoproducts D
i : ∀ {X Y : C}, IsIso (coprodComparison G X Y)
⊢ ∀ {K : Discrete WalkingPair ⥤ C}, PreservesColimit K G

Tactic:
intro K

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasBinaryCoproducts D
i : ∀ {X Y : C}, IsIso (coprodComparison G X Y)
K : Discrete WalkingPair ⥤ C
⊢ PreservesColimit K G
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
F : C ⥤ D
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
⊢ exactFunctor C D F

Tactic:
by simp only [exactFunctor_iff]; constructor <;> assumption

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

Goal state before:
pp: n : ℕ
⊢ flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple 0 ni.2)) (antidiagonal n) = [![n]]

Tactic:
antidiagonal,

Goal state after:
n : ℕ
⊢ flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple 0 ni.2))
      (map (fun i ↦ (i, n - i)) (range (n + 1))) =
    [![n]]
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case inr
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
p : μ × μ
x✝¹ x✝ : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf✝ : f ∈ s.finsuppAntidiag p.2
g : ι →₀ μ
hg✝ : g ∈ s.finsuppAntidiag p.2
hf : s.sum ⇑f = p.2 ∧ f.support ⊆ s
hg : s.sum ⇑g = p.2 ∧ g.support ⊆ s
hfg : ∀ (x : ι), (f.update a p.1) x = (g.update a p.1) x
x : ι
hx : x ≠ a
⊢ f x = g x

Tactic:
· simpa only [coe_update, Function.update, dif_neg hx] using hfg x

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ⊆ s
x : α
hx' : x ∈ c.support
⊢ c x ∈ s ↔ x ∈ s

Tactic:
simp only [hcs hx', hcs (apply_mem_support.mpr hx')]

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

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
⊢ c.boundary ⟨0, ⋯⟩ = 0

Tactic:
boundary,

Goal state after:
n : ℕ
c : CompositionAsSet n
⊢ (c.boundaries.orderEmbOfFin ⋯) ⟨0, ⋯⟩ = 0
Module: Mathlib.GroupTheory.Perm.List

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

Tactic:
exact .head _

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

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

Tactic:
exact .head _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
⊢ (zipWith Equiv.swap l l').prod.support ⊆ l.toFinset ⊔ l'.toFinset

Tactic:
intro x hx
  have hx' : x ∈ { x | (zipWith Equiv.swap l l').prod x ≠ x } := by simpa using hx
  simpa using zipWith_swap_prod_support' _ _ hx'

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
hx : ¬f x = x
z : α
⊢ z ∈ (swap x (f x) * f).support ↔ z ∈ f.support \ {x}

Tactic:
by_cases hzx : z = x

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
hx : ¬f x = x
z : α
hzx : z = x
⊢ z ∈ (swap x (f x) * f).support ↔ z ∈ f.support \ {x}

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
hx : ¬f x = x
z : α
hzx : ¬z = x
⊢ z ∈ (swap x (f x) * f).support ↔ z ∈ f.support \ {x}
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case h.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := σ.subtypePermOfFintype h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := σ.subtypePermOfFintype h3
σ₁ : Perm m := (ofInjective Sum.inl ⋯).symm.permCongr σ₁'
σ₂ : Perm n := (ofInjective Sum.inr ⋯).symm.permCongr σ₂'
a : m
⊢ Sum.inl ((ofInjective Sum.inl ⋯).symm (σ₁' ((ofInjective Sum.inl ⋯).symm.symm a))) = σ (Sum.inl a)

Tactic:
Equiv.symm_symm,

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

Goal state before:
pp: case succ.cons.cons
α : 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] = (y :: l)[n + 1]
⊢ (y :: l).formPerm (x :: y :: l)[n + 1] = (Equiv.swap x y) (x :: y :: l)[n + 1 + 1]

Tactic:
simp only [getElem_cons_succ] at *

Goal state after:
case succ.cons.cons
α : 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] = (Equiv.swap x y) l[n]