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

Goal state before:
pp: case cons.cons.nil.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝⁴ head✝³ : α
hx : [head✝⁴, head✝³].length = 2
head✝² head✝¹ head✝ : α
y : List α
hy : (head✝² :: head✝¹ :: head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝⁴, head✝³], hx⟩ ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝⁴, head✝³], hx⟩) (fromVector ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩)

Tactic:
exfalso

Goal state after:
case cons.cons.nil.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝⁴ head✝³ : α
hx : [head✝⁴, head✝³].length = 2
head✝² head✝¹ head✝ : α
y : List α
hy : (head✝² :: head✝¹ :: head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝⁴, head✝³], hx⟩ ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩
⊢ False
Module: Mathlib.Data.Sym.Sym2

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

Tactic:
exfalso

Goal state after:
case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ : Sym' α 2
head✝² head✝¹ head✝ : α
x : List α
hx : (head✝² :: head✝¹ :: head✝ :: x).length = 2
⊢ False
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₃
inst✝² : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F G : C ⥤ D
H : D ⥤ E
inst✝¹ : H.Full
inst✝ : H.Faithful
comp_iso : F ⋙ H ≅ G ⋙ H
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ H.map (F.map f ≫ (H.preimageIso (comp_iso.app Y✝)).hom) = H.map ((H.preimageIso (comp_iso.app X✝)).hom ≫ G.map f)

Tactic:
by simpa using! comp_iso.hom.naturality f

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
functor : C ⥤ D
inverse : D ⥤ C
unitIso : 𝟭 C ≅ functor ⋙ inverse
counitIso : inverse ⋙ functor ≅ 𝟭 D
functor_unitIso_comp :
  ∀ (X : C), counitIso.inv.app (functor.obj X) ≫ functor.map (unitIso.inv.app X) = 𝟙 (functor.obj X)
X : C
⊢ functor.map (unitIso.hom.app X) ≫ counitIso.hom.app (functor.obj X) = 𝟙 (functor.obj X)

Tactic:
by
    simpa [functor_unitIso_comp] using Iso.inv_eq_inv
      (functor.mapIso (unitIso.app X) ≪≫ counitIso.app (functor.obj X)) (Iso.refl _)

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f → IsIso f.1 ∧ IsIso f.2

Tactic:
rintro ⟨g, hfg, hgf⟩

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
⊢ IsIso f.1 ∧ IsIso f.2
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]
  intro X Y f _
  refine ⟨F.objPreimage X, F.objPreimage Y, F.preimage ?_, ⟨⟨⟩, ⟨?_⟩⟩⟩
  · exact (Functor.objObjPreimageIso F X).hom ≫ f ≫ (Functor.objObjPreimageIso F Y).inv
  · exact Arrow.isoMk' _ _ (Functor.objObjPreimageIso F X) (Functor.objObjPreimageIso F Y)
      (by simp)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ (isomorphisms C).op = isomorphisms Cᵒᵖ

Tactic:
ext
  apply isIso_unop_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:
by
    simp only [Functor.comp_obj, Functor.map_comp]
    rw [← assoc, ← Functor.comp_map, ← adj.unit.naturality]
    simp

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✝
F : J ⥤ C
s : Cone F
G : K ⥤ C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : J ≌ K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
⊢ Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) ≫
      P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t) =
    𝟙 s.pt

Tactic:
apply hom_ext P

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✝
F : J ⥤ C
s : Cone F
G : K ⥤ C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : J ≌ K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := ⋯
⊢ ∀ (j : J),
    (Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) ≫
          P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t)) ≫
        s.π.app j =
      𝟙 s.pt ≫ s.π.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 : Cone F
h : IsLimit t
W : C
p : { p // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' }
j j' : J
f : j ⟶ j'
⊢ ((const J).obj W).map f ≫ ↑p j' = ↑p j ≫ F.map f

Tactic:
dsimp; rw [id_comp]; exact (p.2 f).symm

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : Cᵒᵖ ⥤ Type v₁
⊢ Function.LeftInverse
    (fun ξ ↦ { app := fun x ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map (Quiver.Hom.op f))) ξ, naturality := ⋯ }) fun η ↦
    (ConcreteCategory.hom (η.app (op X))) (𝟙 X)

Tactic:
intro η
    ext Y f
    simp [← NatTrans.naturality_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
⊢ ∀ {X_1 Y : Cᵒᵖ ⥤ Type (max w v₁)} (f : X_1 ⟶ Y),
    ((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).obj X).map f ≫ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                  (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                    uliftFunctor.{u₁, max v₁ w}).obj
              X).map
          f

Tactic:
intros Y Z f
        ext g
        rw [← ULift.down_inj]
        simpa using uliftYonedaEquiv_comp _ _

Goal state after:
Module: Mathlib.CategoryTheory.Balanced

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Balanced C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
fmono : Mono f
fepi : Epi f
⊢ IsIso f

Tactic:
rw [← Quiver.Hom.op_unop f]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Balanced C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
fmono : Mono f
fepi : Epi f
⊢ IsIso f.unop.op
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasLimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : EssentiallySmall.{u₁, v₂, u₂} J
inst✝ : LocallySmall.{v₁, v₂, u₂} J
⊢ HasLimitsOfShape J C

Tactic:
by
  have := HasLimitsOfShape.of_small.{v₁, u₁} C (SmallModel.{u₁} J)
  exact hasLimitsOfShape_of_equivalence (equivSmallModel.{u₁} J).symm

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
⊢ IsLimit (mk X fun x ↦ e.hom)

Tactic:
refine Fan.IsLimit.mk _ (fun s ↦ s.proj default ≫ e.inv) (fun s j ↦ ?_) fun s m hm ↦ ?_

Goal state after:
case refine_1
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Fan fun x ↦ Y
j : J
⊢ (s.proj default ≫ e.inv) ≫ (mk X fun x ↦ e.hom).proj j = s.proj j

case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Fan fun x ↦ Y
m : s.pt ⟶ (mk X fun x ↦ e.hom).pt
hm : ∀ (j : J), m ≫ (mk X fun x ↦ e.hom).proj j = s.proj j
⊢ m = s.proj default ≫ e.inv
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst ≫ g) (snd ≫ g') = map g g'

Tactic:
rw [← prod.lift_map]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift fst snd ≫ map g g' = map g g'
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct (⊤_ C) P
⊢ snd ≫ lift (terminal.from P) (𝟙 P) = 𝟙 ((⊤_ C) ⨯ P)

Tactic:
apply prod.hom_ext <;> simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
P : C
inst✝ : HasBinaryProduct P (⊤_ C)
⊢ fst ≫ lift (𝟙 P) (terminal.from P) = 𝟙 (P ⨯ ⊤_ C)

Tactic:
apply prod.hom_ext <;> simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono g
W : C
h k : W ⟶ t.pt
i : h ≫ t.fst = k ≫ t.fst
⊢ h ≫ t.snd ≫ g = k ≫ t.snd ≫ g

Tactic:
← condition

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono g
W : C
h k : W ⟶ t.pt
i : h ≫ t.fst = k ≫ t.fst
⊢ h ≫ t.fst ≫ f = k ≫ t.fst ≫ f
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
⊢ g = h

Tactic:
have t : v ≫ q = 𝟙 (image f) :=
    (cancel_mono_id (image.ι f)).1
      (by
        convert! t₀ using 1
        rw [Category.assoc])

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ g = h
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case h₁
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g✝ f g : X ⟶ Y
Z : C
h✝ : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h✝
hc : IsLimit c
s' : Fork (h✝ ≫ f) (h✝ ≫ g)
m : s'.pt ⟶ (precompFork h✝ s c).pt
h : m ≫ (precompFork h✝ s c).ι = s'.ι
⊢ m ≫ c.snd = liftPrecomp h✝ hs hc s' ≫ c.snd

Tactic:
· simpa [liftPrecomp] using! h

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 Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inl ≫ snd X Y = 0

Tactic:
simp [coprod.snd]

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 Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ inr ≫ snd X Y = 𝟙 Y

Tactic:
simp [coprod.snd]

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 : Cone (Discrete.functor f)
j : Discrete J
⊢ (∑ j, s.π.app { as := j } ≫ b.ι j) ≫ b.toCone.π.app j = s.π.app j

Tactic:
by
        classical
        cases j
        simp only [sum_comp, Category.assoc, Bicone.toCone_π_app, b.ι_π, comp_dite]
        simp

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

Goal state before:
pp: case refine_4.p.x
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j : Fin n
hab : q.succAbove j < q
⊢ q.insertNth x f (q.succAbove j) < q.insertNth x f q

Tactic:
have : j.castSucc < q := by simpa [succAbove_lt_iff_castSucc_lt] using hab

Goal state after:
case refine_4.p.x
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j : Fin n
hab : q.succAbove j < q
this : j.castSucc < q
⊢ q.insertNth x f (q.succAbove j) < q.insertNth x f q
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: k n : ℕ
⊢ (∀ a ∈ antidiagonal n,
      Pairwise (fun a_2 b ↦ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun x x1 x2 ↦ x1 < x2) (Fin.cons a.1 a_2) (Fin.cons a.1 b))
        (antidiagonalTuple k a.2)) ∧
    Pairwise
      (fun a₁ a₂ ↦
        ∀ (x : Fin (k + 1) → ℕ),
          ∀ x_1 ∈ antidiagonalTuple k a₁.2,
            Fin.cons a₁.1 x_1 = x →
              ∀ (y : Fin (k + 1) → ℕ),
                ∀ x_2 ∈ antidiagonalTuple k a₂.2,
                  Fin.cons a₂.1 x_2 = y → Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun x x1 x2 ↦ x1 < x2) x y)
      (antidiagonal n)

Tactic:
forall_apply_eq_imp_iff₂

Goal state after:
k n : ℕ
⊢ (∀ a ∈ antidiagonal n,
      Pairwise (fun a_2 b ↦ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun x x1 x2 ↦ x1 < x2) (Fin.cons a.1 a_2) (Fin.cons a.1 b))
        (antidiagonalTuple k a.2)) ∧
    Pairwise
      (fun a₁ a₂ ↦
        ∀ a ∈ antidiagonalTuple k a₁.2,
          ∀ a_2 ∈ antidiagonalTuple k a₂.2,
            Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun x x1 x2 ↦ x1 < x2) (Fin.cons a₁.1 a) (Fin.cons a₂.1 a_2))
      (antidiagonal n)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case inr
n : ℕ
c : Composition n
i₁ i₂ : Fin c.length
h : i₁ ≠ i₂
this :
  ∀ {n : ℕ} (c : Composition n) {i₁ i₂ : Fin c.length},
    i₁ ≠ i₂ → i₁ < i₂ → _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))
h' : ¬i₁ < i₂
⊢ _root_.Disjoint (Set.range ⇑(c.embedding i₁)) (Set.range ⇑(c.embedding i₂))

Tactic:
exact (this c h.symm (h.lt_or_gt.resolve_left h')).symm

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
σ τ : Type
inst✝³ : Fintype τ
S : σ → C
inst✝² : HasBiproduct S
T : τ → C
inst✝¹ : HasBiproduct T
s : σ
nz : 𝟙 (S s) ≠ 0
f : ⨁ S ⟶ ⨁ T
inst✝ : IsIso f
⊢ Trunc ((t : τ) ×' biproduct.ι S s ≫ f ≫ biproduct.π T t ≠ 0)

Tactic:
by
  classical
    apply truncSigmaOfExists
    have t := Biproduct.column_nonzero_of_iso'.{v} s f
    by_contra h
    simp only [not_exists_not] at h
    exact nz (t h)

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

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

Tactic:
simp only [mem_support, not_iff_not, ← mul_apply]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hgc : Commute g c
x : α
⊢ (c * g) x = g x ↔ c x = x
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
hl : 1 < l.length
⊢ l.formPerm l[0] = l[1]

Tactic:
rcases l with (_ | ⟨x, _ | ⟨y, tl⟩⟩)

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
h : [].Nodup
hl : 1 < [].length
⊢ [].formPerm [][0] = [][1]

case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x : α
h : [x].Nodup
hl : 1 < [x].length
⊢ [x].formPerm [x][0] = [x][1]

case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
tl : List α
h : (x :: y :: tl).Nodup
hl : 1 < (x :: y :: tl).length
⊢ (x :: y :: tl).formPerm (x :: y :: tl)[0] = (x :: y :: tl)[1]
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
⊢ f heq_iff_eq ≠ heq_iff_eq → heq_iff_eq ∈ []

Tactic:
have : f = 1 := by simpa [permsOfList] using h

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
this : f = 1
⊢ f heq_iff_eq ≠ heq_iff_eq → heq_iff_eq ∈ []
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
h : List.Pairwise Disjoint l
⊢ #l.prod.support = (List.map (card ∘ support) l).sum

Tactic:
induction l with
  | nil => exact card_support_eq_zero.mpr rfl
  | cons a t ih =>
    obtain ⟨ha, ht⟩ := List.pairwise_cons.1 h
    rw [List.prod_cons, List.map_cons, List.sum_cons, ← ih ht]
    exact (disjoint_prod_right _ ha).card_support_mul

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
⊢ (l.rotate n).formPerm = l.formPerm

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    rw [← rotate_rotate, formPerm_rotate_one, hn]
    rwa [IsRotated.nodup_iff]
    exact IsRotated.forall l n

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
l : List α
h : (x :: l).Nodup
n : ℕ
⊢ ((x :: l).formPerm ^ n) x = (x :: l)[n % (x :: l).length]

Tactic:
convert! formPerm_pow_apply_getElem _ h n 0 (Nat.succ_pos _)

Goal state after:
case e'_3
α : Type u_1
inst✝ : DecidableEq α
x : α
l : List α
h : (x :: l).Nodup
n : ℕ
⊢ n = 0 + n
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f ↦ Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ f ((Equiv.symm g) x) = f a

Tactic:
hmeml hf₁,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f ↦ Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ f ((Equiv.symm g) x) = a
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y z : α
x✝¹ : f.SameCycle x y
x✝ : f.SameCycle y z
i : ℤ
hi : (f ^ i) x = y
j : ℤ
hj : (f ^ j) y = z
⊢ (f ^ (j + i)) x = z

Tactic:
zpow_add,

Goal state after:
α : Type u_2
f : Perm α
x y z : α
x✝¹ : f.SameCycle x y
x✝ : f.SameCycle y z
i : ℤ
hi : (f ^ i) x = y
j : ℤ
hj : (f ^ j) y = z
⊢ (f ^ j * f ^ i) x = z
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
⊢ l.formPerm = 1 ↔ l.length ≤ 1

Tactic:
rcases l with - | ⟨hd, tl⟩

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
hl : [].Nodup
⊢ [].formPerm = 1 ↔ [].length ≤ 1

case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm = 1 ↔ (hd :: tl).length ≤ 1
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inr.ha
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
⊢ ↑⟨x, ⋯⟩ ∈ ↑τ.support

pp: case intro.refine_2.inr.ha
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
⊢ ↑⟨(σ * τ) x, ⋯⟩ ∈ ↑τ.support

Tactic:
· rwa [Subtype.coe_mk, mem_coe, ← apply_mem_support, mem_support]

Goal state after:
case intro.refine_2.inr.ha
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
⊢ ↑⟨(σ * τ) x, ⋯⟩ ∈ ↑τ.support
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case succ.inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : f x ≠ b
this : f b ≠ b ∧ b ≠ x
hb' : (swap x (f x) * f) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
i : ℤ
hi : ((swap x (f x) * f) ^ i) (f x) = (Equiv.symm f) b
⊢ ((swap x (f x) * f) ^ (1 + i)) (f x) = b

Tactic:
zpow_add,

Goal state after:
case succ.inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : f x ≠ b
this : f b ≠ b ∧ b ≠ x
hb' : (swap x (f x) * f) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
i : ℤ
hi : ((swap x (f x) * f) ^ i) (f x) = (Equiv.symm f) b
⊢ ((swap x (f x) * f) ^ 1 * (swap x (f x) * f) ^ i) (f x) = b
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
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
y z : α
h5 : z = x
⊢ swap x y ∈ H

Tactic:
exact step3 y

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : f x ≠ x
hffx : f (f x) = x
y z : α
hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = f x
hy : ¬f y = y
j : ℤ
hj : (f ^ (j - i + i)) z = y
⊢ False

Tactic:
zpow_add,

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : f x ≠ x
hffx : f (f x) = x
y z : α
hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = f x
hy : ¬f y = y
j : ℤ
hj : (f ^ (j - i) * f ^ i) z = y
⊢ False