mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
head✝ : α
hx : [head✝].length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨[head✝], hx⟩⟧) = ⟦⟨[head✝], hx⟩⟧

pp: case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ : Sym' α 2
head✝¹ head✝ : α
x : List α
hx : (head✝¹ :: head✝ :: x).length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨head✝¹ :: head✝ :: x, hx⟩⟧) =
    ⟦⟨head✝¹ :: head✝ :: x, hx⟩⟧

Tactic:
· simp at hx

Goal state after:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ : Sym' α 2
head✝¹ head✝ : α
x : List α
hx : (head✝¹ :: head✝ :: x).length = 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦⟨head✝¹ :: head✝ :: x, hx⟩⟧) =
    ⟦⟨head✝¹ :: head✝ :: x, hx⟩⟧
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
hF h₁ h₂ : F.FullyFaithful
⊢ h₁ = h₂

Tactic:
by
    have := h₁.faithful
    cases h₁ with | mk f₁ hf₁ _ => cases h₂ with | mk f₂ hf₂ _ =>
    simp only [Functor.FullyFaithful.mk.injEq]
    ext
    apply F.map_injective
    rw [hf₁, hf₂]

Goal state after:
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.obj (L.obj X₁) ⟶ F.obj (L.obj X₂)), ∃ f, F.map f = φ
X₁ : D
⊢ ∀ {Y : D}, Function.Surjective F.map

Tactic:
X₂

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.obj (L.obj X₁) ⟶ F.obj (L.obj X₂)), ∃ f, F.map f = φ
X₁ X₂ : D
⊢ Function.Surjective F.map
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
W : ι → MorphismProperty C
⊢ (⨆ i, W i).toSet = ⋃ i, (W i).toSet

Tactic:
ext
  simp [mem_toSet_iff]

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 : C
Y : D
g : X ⟶ G.obj Y
⊢ (fun f ↦ adj.unit.app X ≫ G.map f) ((fun g ↦ F.map g ≫ adj.counit.app Y) g) = g

Tactic:
simp only [Functor.comp_obj, Functor.map_comp]
    rw [← assoc, ← Functor.comp_map, ← adj.unit.naturality]
    simp

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

Goal state before:
pp: case mk
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
unit✝ : 𝟭 C ⟶ F ⋙ G
counit✝ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝ : ∀ (X : C), F.map (unit✝.app X) ≫ counit✝.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝ : ∀ (Y : D), unit✝.app (G.obj Y) ≫ G.map (counit✝.app Y) = 𝟙 (G.obj Y)
h :
  { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.unit =
    adj'.unit
h' :
  { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.counit =
    adj'.counit
⊢ { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
      right_triangle_components := right_triangle_components✝ } =
    adj'

Tactic:
cases adj'

Goal state after:
case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
unit✝¹ : 𝟭 C ⟶ F ⋙ G
counit✝¹ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝¹ : ∀ (X : C), F.map (unit✝¹.app X) ≫ counit✝¹.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝¹ : ∀ (Y : D), unit✝¹.app (G.obj Y) ≫ G.map (counit✝¹.app Y) = 𝟙 (G.obj Y)
unit✝ : 𝟭 C ⟶ F ⋙ G
counit✝ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝ : ∀ (X : C), F.map (unit✝.app X) ≫ counit✝.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝ : ∀ (Y : D), unit✝.app (G.obj Y) ≫ G.map (counit✝.app Y) = 𝟙 (G.obj Y)
h :
  { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
        right_triangle_components := right_triangle_components✝¹ }.unit =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.unit
h' :
  { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
        right_triangle_components := right_triangle_components✝¹ }.counit =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.counit
⊢ { unit := unit✝¹, counit := counit✝¹, left_triangle_components := left_triangle_components✝¹,
      right_triangle_components := right_triangle_components✝¹ } =
    { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
      right_triangle_components := right_triangle_components✝ }
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 Y' : D
f : X' ⟶ X
g : X ⟶ G.obj Y'
h : X' ⟶ G.obj Y
k : Y ⟶ Y'
w : F.map f ≫ (adj.homEquiv X Y').symm g = (adj.homEquiv X' Y).symm h ≫ k
⊢ f ≫ g = h ≫ G.map k

Tactic:
simpa only [Equiv.apply_symm_apply]
      using homEquiv_naturality_left_square adj _ _ _ _ w

Goal state after:
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
t : Cone F
X : C
h : F.cones.RepresentableBy X
j : J
pt✝ : C
π✝ : (const J).obj pt✝ ⟶ F
h₁ : { pt := pt✝, π := π✝ }.pt = pt✝
h₂ : (const J).map (homOfCone h { pt := pt✝, π := π✝ }) ≫ (limitCone h).π = π✝
| { pt := pt✝, π := π✝ }.π.app j

Tactic:
← h₂

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
t : Cone F
X : C
h : F.cones.RepresentableBy X
j : J
pt✝ : C
π✝ : (const J).obj pt✝ ⟶ F
h₁ : { pt := pt✝, π := π✝ }.pt = pt✝
h₂ : (const J).map (homOfCone h { pt := pt✝, π := π✝ }) ≫ (limitCone h).π = π✝
| { pt := pt✝, π := (const J).map (homOfCone h { pt := pt✝, π := π✝ }) ≫ (limitCone h).π }.π.app j
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
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
j : J
pt✝ : C
ι✝ : F ⟶ (const J).obj pt✝
h₁ : { pt := pt✝, ι := ι✝ }.pt = pt✝
h₂ : (colimitCocone h).ι ≫ (const J).map (homOfCocone h { pt := pt✝, ι := ι✝ }) = ι✝
| { pt := pt✝, ι := ι✝ }.ι.app j

Tactic:
← h₂

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
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
j : J
pt✝ : C
ι✝ : F ⟶ (const J).obj pt✝
h₁ : { pt := pt✝, ι := ι✝ }.pt = pt✝
h₂ : (colimitCocone h).ι ≫ (const J).map (homOfCocone h { pt := pt✝, ι := ι✝ }) = ι✝
| { pt := pt✝, ι := (colimitCocone h).ι ≫ (const J).map (homOfCocone h { pt := pt✝, ι := ι✝ }) }.ι.app j
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (T : C), Function.Bijective fun x ↦ x ≫ f

Tactic:
by
  refine ⟨fun _ ↦ ?_, fun hf ↦ isIso_of_yoneda_map_bijective f hf⟩
  intro T
  rw [bijective_iff_isIso_ofHom]
  exact inferInstanceAs (IsIso ((yoneda.map f).app _))

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
⊢ k = l

Tactic:
by
  apply hs.hom_ext
  rintro (_ | j)
  · exact hbase
  · exact hπ j

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
S✝ S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
S : C
F : B ⥤ C
G : C ⥤ D
inst✝ : G.Faithful
X✝ Y✝ : StructuredArrow S F
f : (post S F G).obj X✝ ⟶ (post S F G).obj Y✝
⊢ G.map (X✝.hom ≫ F.map (Hom.right f)) = G.map Y✝.hom

Tactic:
simpa using f.w

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ (congrHom h₁ h₂).inv = map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯

Tactic:
ext <;> simp [Iso.inv_comp_eq]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S✝ S' : C ⥤ D
A : Type u₃
inst✝² : Category.{v₃, u₃} A
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
S : C
inst✝ : G.Faithful
X✝ Y✝ : CostructuredArrow F S
f : (post F G S).obj X✝ ⟶ (post F G S).obj Y✝
⊢ G.map (F.map f.left ≫ Y✝.hom) = G.map X✝.hom

Tactic:
simpa using f.w

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

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

Tactic:
rw [IsIso.inv_comp_eq, ← pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]

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

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : C ⥤ T
G : D ⥤ T
c : C
X✝ Y✝ : CostructuredArrow (Comma.fst F G) c
f : X✝ ⟶ Y✝
⊢ f.left.left ≫ { left := Over.mk Y✝.hom, right := Y✝.left.right, hom := Y✝.left.hom }.left.hom =
    { left := Over.mk X✝.hom, right := X✝.left.right, hom := X✝.left.hom }.left.hom

Tactic:
simpa using f.w

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
w : Zero.zero = Zero.zero
⊢ zero X Y = zero X Y

Tactic:
apply congrArg Zero.mk w

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:
rw [ι_colimMap_assoc, parallelPairHom_app_one, coequalizer.π_desc]

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
f : X ⟶ ⊥_ C
⊢ f ≫ 𝟙 (⊥_ C) = f ≫ 0

Tactic:
by congr!; subsingleton

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
f : ⊤_ C ⟶ X
⊢ 𝟙 (⊤_ C) ≫ f = 0 ≫ f

Tactic:
by congr!; subsingleton

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
β : Type w
inst✝¹ : DecidableEq β
f : β → C
inst✝ : HasCoproduct f
b : β
⊢ ι f b ≫ π f b = 𝟙 (f b)

Tactic:
by
  simp [Sigma.π]

Goal state after:
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
X Y : C
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ IsIso ((limit.isLimit (pair (G.obj X) (G.obj Y))).lift (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)))

Tactic:
apply i

Goal state after:
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
X Y : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ IsIso ((colimit.isColimit (pair (G.obj X) (G.obj Y))).desc (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)))

Tactic:
apply i

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✝
X Y : C
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
X' Y' : C
g' : X' ⟶ Y'
e : X ≅ X'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0
⊢ (Fork.ι c ≫ e.hom) ≫ g' = 0

Tactic:
by simp [← iff]

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✝
X Y : C
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
Y' : C
g' : X ⟶ Y'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ g' = 0
⊢ Fork.ι c ≫ g' = 0

Tactic:
by simp [← iff]

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✝
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
X' Y' : C
f' : X' ⟶ Y'
e : Y' ≅ Y
iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ e.hom ≫ φ = 0
⊢ f' ≫ e.hom ≫ Cofork.π c = 0

Tactic:
by simp [← iff]

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✝
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
X' : C
f' : X' ⟶ Y
iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ φ = 0
⊢ f' ≫ Cofork.π c = 0

Tactic:
by simp [← iff]

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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : Epi f
inst✝ : HasCokernel g
⊢ g ≫ cokernel.π (f ≫ g) = 0

Tactic:
by
        rw [← cancel_epi f, ← Category.assoc]
        simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cocone (Discrete.functor f)
j : Discrete J
⊢ b.toCocone.ι.app j ≫ ∑ j, b.π j ≫ s.ι.app { as := j } = s.ι.app j

Tactic:
cases j
        simp only [comp_sum, ← Category.assoc, Bicone.toCocone_ι_app, b.ι_π, dite_comp]
        simp

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoProd X Y).inv = lift prod.fst prod.snd

Tactic:
ext <;> simp [Iso.inv_comp_eq]

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

Goal state before:
pp: n : ℕ
⊢ antidiagonalTuple 2 n = map (fun i ↦ ![i.1, i.2]) (antidiagonal n)

Tactic:
by
  rw [antidiagonalTuple]
  simp_rw [antidiagonalTuple_one, List.map_singleton]
  rw [List.map_eq_flatMap]
  rfl

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

Goal state before:
pp: n : ℕ
c : Composition n
j : ℕ
h : j < n
length_pos : 0 < c.blocks.length
this : c.length - 1 + 1 = c.length
⊢ j < c.sizeUpTo (c.length.pred + 1)

Tactic:
simp [this, h]

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

Goal state before:
pp: n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
hi : i ∈ Set.range c.blocksFun
i_blocks : 1 < i
⊢ ∑ i, 1 < ∑ i, c.blocksFun i

Tactic:
Set.mem_range

Goal state after:
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
i : ℕ
hi : ∃ y, c.blocksFun y = i
i_blocks : 1 < i
⊢ ∑ i, 1 < ∑ i, c.blocksFun i
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mpr
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
⊢ f ∈ s.finsuppAntidiag (e n) → f ∈ map (mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n)

Tactic:
· set h := (mapRange.addEquiv e).toEquiv with hh
    intro hf
    have : n = e.symm (e n) := (AddEquiv.eq_symm_apply e).mpr rfl
    rw [mem_map_equiv, this]
    apply mapRange_finsuppAntidiag_subset
    rw [← mem_map_equiv]
    convert! hf
    rw [map_map, hh]
    convert! map_refl
    apply Function.Embedding.equiv_symm_toEmbedding_trans_toEmbedding

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

Goal state before:
pp: case a.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ = l.length
h : ⟨0, ⋯⟩ = ⟨n, hn⟩
⊢ n.succ = 1

Tactic:
(Fin.mk.inj_iff.mp h).symm

Goal state after:
case a.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ = l.length
h : ⟨0, ⋯⟩ = ⟨n, hn⟩
⊢ Nat.succ 0 = 1
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ ↑l.formPerm.support = {x | l.formPerm x ≠ x}

Tactic:
simp [Set.ext_iff]

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ []
x : α
⊢ [].prod x = f x

Tactic:
rw [List.prod_nil]

Goal state after:
α : Type u
inst✝ : DecidableEq α
β : Type v
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ []
x : α
⊢ 1 x = f x
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
m : { l // l.prod = swap x (f x) * f ∧ ∀ g ∈ l, g.IsSwap } := swapFactorsAux l (swap x (f x) * f) ⋯
⊢ (swap x (f x) :: ↑m).prod = f

Tactic:
rw [List.prod_cons, m.2.1, ← mul_assoc, mul_def (swap x (f x)), swap_swap, ← one_def,
          one_mul]

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

Goal state before:
pp: case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : (↑x.truncSwapFactors.out).prod = x
h2 : ∀ g ∈ ↑x.truncSwapFactors.out, g.IsSwap
⊢ x ∈ Submonoid.closure {σ | σ.IsSwap}

Tactic:
← h1

Goal state after:
case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : (↑x.truncSwapFactors.out).prod = x
h2 : ∀ g ∈ ↑x.truncSwapFactors.out, g.IsSwap
⊢ (↑x.truncSwapFactors.out).prod ∈ Submonoid.closure {σ | σ.IsSwap}
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case h.h
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
⊢ ∀ (i : ℕ) (h₁ : i < ((x :: y :: l).rotate n).length) (h₂ : i < (x' :: y' :: l').length),
    ((x :: y :: l).rotate n)[i] = (x' :: y' :: l')[i]

Tactic:
intro k hk hk'
    rw [getElem_rotate]
    induction k with
    | zero =>
      refine Eq.trans ?_ hx'
      congr
      simpa using hn
    | succ k IH =>
      conv => congr <;> · arg 2; (rw [← Nat.mod_eq_of_lt hk'])
      rw [← formPerm_apply_getElem _ hd' k (k.lt_succ_self.trans hk'),
        ← IH (k.lt_succ_self.trans hk), ← h, formPerm_apply_getElem _ hd]
      congr 1
      rw [hl, Nat.mod_eq_of_lt hk', add_right_comm]
      apply Nat.add_mod

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l.formPerm l[k] = l[k] ↔ l.length ≤ 1

Tactic:
formPerm_apply_getElem _ hl k hk,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l[(k + 1) % l.length] = l[k] ↔ l.length ≤ 1
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case pos
α : 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
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : x = (σ ^ n) x
⊢ swap x (σ x) ∈ H

Tactic:
exact h4

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
f : Perm α
x✝ : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬s (swap x y) = -1
this✝¹ : ∀ (f : Perm α), f.IsSwap → s f = 1
g : Perm α
hg : s g = -1
l : List (Perm α)
hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap
this✝ : ∀ a ∈ List.map (⇑s) l, a = 1
this : s g = 1
⊢ False

Tactic:
hg

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
f : Perm α
x✝ : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬s (swap x y) = -1
this✝¹ : ∀ (f : Perm α), f.IsSwap → s f = 1
g : Perm α
hg : s g = -1
l : List (Perm α)
hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap
this✝ : ∀ a ∈ List.map (⇑s) l, a = 1
this : -1 = 1
⊢ False
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
⊢ IsConj σ τ

Tactic:
by
  refine
    isConj_of_support_equiv
      (hσ.zpowersEquivSupport.symm.trans <|
        (zpowersEquivZPowers <| by rw [hσ.orderOf, h, hτ.orderOf]).trans hτ.zpowersEquivSupport)
      ?_
  intro x hx
  simp only [Equiv.trans_apply]
  obtain ⟨n, rfl⟩ := hσ.exists_pow_eq (Classical.choose_spec hσ).1 (mem_support.1 hx)
  simp [← Perm.mul_apply, ← pow_succ']

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
hind : iSupIndep fun i ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ (noncommPiCoprod ϕ hcomm).ker
this : ∀ i ∈ Finset.univ, (ϕ i) (f i) = 1
i : ι
⊢ f i = 1 i

Tactic:
apply hinj

Goal state after:
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
hind : iSupIndep fun i ↦ (ϕ i).range
hinj : ∀ (i : ι), Function.Injective ⇑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ (noncommPiCoprod ϕ hcomm).ker
this : ∀ i ∈ Finset.univ, (ϕ i) (f i) = 1
i : ι
⊢ (ϕ i) (f i) = (ϕ i) (1 i)