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

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
h₁ : F.map fst ≫ s.ι.app left = s.ι.app zero
h₂ : F.map fst ≫ t.ι.app left = t.ι.app zero ≫ 𝟙 t.pt
⊢ s.ι.app none ≫ i.hom = t.ι.app none

Tactic:
simp only [Category.comp_id] at h₂

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
h₁ : F.map fst ≫ s.ι.app left = s.ι.app zero
h₂ : F.map fst ≫ t.ι.app left = t.ι.app zero
⊢ s.ι.app none ≫ i.hom = t.ι.app none
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
⊢ ∀ {X Y : WalkingCospan} (f : X ⟶ Y),
    F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

Tactic:
rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) f

Goal state after:
case none.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : none ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

case none.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : none ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

case none.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : none ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

case some.left.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : some WalkingPair.left ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

case some.left.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

case some.left.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

case some.right.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : some WalkingPair.right ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

case some.right.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f

case some.right.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (cospan (F.map inl) (F.map inr)).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
⊢ ∀ {X Y : WalkingSpan} (f : X ⟶ Y), F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

Tactic:
rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) f

Goal state after:
case none.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : none ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

case none.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : none ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

case none.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : none ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

case some.left.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.left ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

case some.left.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

case some.left.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

case some.right.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.right ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

case some.right.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

case some.right.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

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

Tactic:
apply hom_ext

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ lift (fst f g) (snd f g) ⋯ ≫ fst f g = 𝟙 (pullback f g) ≫ fst f g

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ lift (fst f g) (snd f g) ⋯ ≫ snd f g = 𝟙 (pullback f g) ≫ snd f g
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ desc (inl f g) (inr f g) ⋯ = 𝟙 (pushout f g)

Tactic:
apply hom_ext

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ inl f g ≫ desc (inl f g) (inr f g) ⋯ = inl f g ≫ 𝟙 (pushout f g)

case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ inr f g ≫ desc (inl f g) (inr f g) ⋯ = inr f g ≫ 𝟙 (pushout f g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case op.op
i j : WalkingParallelPair
f : op i ⟶ op j
g : unop (op j) ⟶ unop (op i) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

Tactic:
cases i <;> cases j

Goal state after:
case op.op.zero.zero
f : op zero ⟶ op zero
g : unop (op zero) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

case op.op.zero.one
f : op zero ⟶ op one
g : unop (op one) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

case op.op.one.zero
f : op one ⟶ op zero
g : unop (op zero) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

case op.op.one.one
f : op one ⟶ op one
g : unop (op one) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op
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✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
hG : IsZero G
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c✝ : Cone K
x✝ : IsLimit c✝
⊢ IsLimit (G.mapCone c✝)

Tactic:
Functor.isZero_iff

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
hG : ∀ (X : C), IsZero (G.obj X)
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c✝ : Cone K
x✝ : IsLimit c✝
⊢ IsLimit (G.mapCone c✝)
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✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
hG : IsZero G
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c✝ : Cocone K
x✝ : IsColimit c✝
⊢ IsColimit (G.mapCocone c✝)

Tactic:
Functor.isZero_iff

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
hG : ∀ (X : C), IsZero (G.obj X)
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c✝ : Cocone K
x✝ : IsColimit c✝
⊢ IsColimit (G.mapCocone c✝)
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
⊢ m₁ = m₂

Tactic:
have : m₁.toMulOneClass = m₂.toMulOneClass := MulOneClass.ext h_mul

Goal state after:
M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this : m₁.toMulOneClass = m₂.toMulOneClass
⊢ m₁ = m₂
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
W : C
k : Y ⟶ W
h : f ≫ k = 0
inst✝ : Epi k
Z : C
g g' : W ⟶ Z
w : desc f k h ≫ g = desc f k h ≫ g'
⊢ g = g'

Tactic:
by
    replace w := cokernel.π f ≫= w
    simp only [cokernel.π_desc_assoc] at w
    exact (cancel_epi k).1 w

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✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
⊢ ((desc fun b ↦ ι f (ε b)) ≫ lift fun b ↦ π f (ε b)) = 𝟙 (⨁ f ∘ ⇑ε)

Tactic:
ext b b'
    by_cases h : b' = b
    · subst h; simp
    · have : ε b' ≠ ε b := by simp [h]
      simp [biproduct.ι_π_ne _ h, biproduct.ι_π_ne _ this]

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

Goal state before:
pp: case h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ snd = (inr ≫ map' f g) ≫ snd

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

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝⁴ : Category.{uC', uC} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
hY : IsZero X
⊢ biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y)

Tactic:
apply CategoryTheory.Limits.biprod.hom_ext <;>
      simp only [Category.assoc, biprod.inr_snd, Category.comp_id, Category.id_comp, biprod.inr_fst,
        comp_zero]
    apply hY.eq_of_tgt

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

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
⊢ HasBinaryBiproduct X X

Tactic:
convert! (inferInstance : HasBinaryBiproduct X X)

Goal state after:
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
⊢ preadditiveHasZeroMorphisms = inst✝¹
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
⊢ HasBinaryBiproduct X X

Tactic:
convert! (inferInstance : HasBinaryBiproduct X X)

Goal state after:
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
⊢ preadditiveHasZeroMorphisms = inst✝¹
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ c.sizeUpTo i < c.sizeUpTo (i + 1)

Tactic:
c.sizeUpTo_succ h

Goal state after:
n : ℕ
c : Composition n
i : ℕ
h : i < c.length
⊢ c.sizeUpTo i < c.sizeUpTo i + c.blocks[i]
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
h₀ : x = 0
⊢ False

Tactic:
exact nz (h₁.symm.trans h₀)

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
t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → 𝟙 (S s) = 0
h : ¬∃ a, biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0
⊢ False

Tactic:
simp only [not_exists_not] at h

Goal state after:
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
t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → 𝟙 (S s) = 0
h : ∀ (x : τ), biproduct.ι S s ≫ f ≫ biproduct.π T x = 0
⊢ False
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✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Mono (F.biproductComparison f)
⊢ PreservesBiproduct f F

Tactic:
by
  have : HasProduct fun b => F.obj (f b) := by
    change HasProduct (F.obj ∘ f)
    infer_instance
  have that : piComparison F f =
      (F.mapIso (biproduct.isoProduct f)).inv ≫
        biproductComparison F f ≫ (biproduct.isoProduct _).hom := by
    ext j
    convert! piComparison_comp_π F f j; simp [← Function.comp_def, ← Functor.map_comp]
  have : IsIso (biproductComparison F f) := isIso_of_mono_of_isSplitEpi _
  have : IsIso (piComparison F f) := by
    rw [that]
    infer_instance
  have := PreservesProduct.of_iso_comparison F f
  apply preservesBiproduct_of_preservesProduct

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

Goal state before:
pp: case neg
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : ¬p b
⊢ (σ.extendDomain f) b = b ∨ (τ.extendDomain f) b = b

Tactic:
left

Goal state after:
case neg
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : ¬p b
⊢ (σ.extendDomain f) b = b
Module: Mathlib.Data.Fintype.Perm

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

Tactic:
exact (List.nodup_cons.1 hl).1 <| mem_of_mem_permsOfList hg.1 (by simpa using hxa)

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

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
hx : x ∉ fixedPoints ⇑g
⊢ (ofSubtype u) x = x ∨ g x = x

Tactic:
left

Goal state after:
case neg
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
hx : x ∉ fixedPoints ⇑g
⊢ (ofSubtype u) x = x
Module: Mathlib.Data.Set.Pairwise.List

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
l✝ : List α
inst✝ : Std.Symm r
a : α
l : List α
ih : l.Nodup → ({a | a ∈ l}.Pairwise r ↔ Pairwise r l)
hl : ¬a ∈ l ∧ l.Nodup
⊢ {a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)

Tactic:
have : ∀ b ∈ l, ¬a = b → r a b ↔ r a b := fun b hb =>
    imp_iff_right (ne_of_mem_of_not_mem hb hl.1).symm

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
l✝ : List α
inst✝ : Std.Symm r
a : α
l : List α
ih : l.Nodup → ({a | a ∈ l}.Pairwise r ↔ Pairwise r l)
hl : ¬a ∈ l ∧ l.Nodup
this : ∀ (b : α), b ∈ l → (¬a = b → r a b ↔ r a b)
⊢ {a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)
Module: Mathlib.Data.Nat.GCD.BigOperators

Goal state before:
pp: k : ℕ
m : Multiset ℕ
⊢ k.Coprime m.prod ↔ ∀ n ∈ m, k.Coprime n

Tactic:
by
  induction m using Quotient.inductionOn; simpa using coprime_list_prod_right_iff

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

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℤ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
⊢ f.IsCycle

Tactic:
by
  cases n
  · exact h1.of_pow h2
  · simp only [zpow_negSucc, Perm.support_inv] at h1 h2
    exact (inv_inv (f ^ _) ▸ h1.inv).of_pow h2

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

Goal state before:
pp: case inl
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Subsingleton
⊢ (f.subtypePerm ⋯).IsCycleOn _root_.Set.univ

pp: case inr
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ (f.subtypePerm ⋯).IsCycleOn _root_.Set.univ

Tactic:
· have := hs.coe_sort
    exact isCycleOn_of_subsingleton _ _

Goal state after:
case inr
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ (f.subtypePerm ⋯).IsCycleOn _root_.Set.univ
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
ι : Type u_2
inst✝² : Fintype ι
N : ι → Type u_3
inst✝¹ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝ : DecidableEq ι
i : ι
y : N i
⊢ Finset.univ.noncommProd (fun j ↦ (ϕ j) (Pi.mulSingle i y j)) ⋯ = (ϕ i) y

Tactic:
← Finset.insert_erase (Finset.mem_univ i)

Goal state after:
M : Type u_1
inst✝³ : Monoid M
ι : Type u_2
inst✝² : Fintype ι
N : ι → Type u_3
inst✝¹ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝ : DecidableEq ι
i : ι
y : N i
⊢ (insert i (Finset.univ.erase i)).noncommProd (fun j ↦ (ϕ j) (Pi.mulSingle i y j)) ⋯ = (ϕ i) y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
⊢ (f.cycleOf x) y = if f.SameCycle x y then f y else y

Tactic:
dsimp only [cycleOf]
  split_ifs with h
  · apply ofSubtype_apply_of_mem
    exact h
  · apply ofSubtype_apply_of_not_mem
    exact h

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

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : (Multiset.map (fun n ↦ -(-1) ^ n) s).prod = (-1) ^ (s.sum + s.card)
⊢ (Multiset.map (fun n ↦ -(-1) ^ n) (a ::ₘ s)).prod = (-1) ^ ((a ::ₘ s).sum + (a ::ₘ s).card)

Tactic:
| cons a s ihs =>

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

Goal state before:
pp: n x : ℕ
hx : x < n + 2
⊢ (finRotate (n + 2) ^ ↑↑⟨x, hx⟩) 0 = ⟨x, hx⟩

Tactic:
rw [zpow_natCast, Fin.ext_iff, Fin.val_mk]

Goal state after:
n x : ℕ
hx : x < n + 2
⊢ ↑((finRotate (n + 2) ^ ↑⟨x, hx⟩) 0) = ↑⟨x, hx⟩
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ
n✝ : ℕ
i j : Fin (n✝ + 1)
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Tactic:
rcases lt_trichotomy j i with (hlt | heq | hgt)

Goal state after:
case succ.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

case succ.inr.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
heq : j = i
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

case succ.inr.inr
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ Multiset.filter (fun n ↦ 2 ≤ n) σ.partition.parts = σ.cycleType

Tactic:
parts_partition,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ Multiset.filter (fun n ↦ 2 ≤ n) (σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1) = σ.cycleType
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
⊢ σ.partition.parts = τ.partition.parts

Tactic:
parts_partition,

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
⊢ σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1 = τ.partition.parts
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
⊢ σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1 = τ.partition.parts

Tactic:
parts_partition,

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
⊢ σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1 =
    τ.cycleType + Multiset.replicate (Fintype.card α - #τ.support) 1
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
x : α
hx : ¬f x = x
⊢ (g * f⁻¹) x = x ∨ f x = x

Tactic:
left

Goal state after:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
x : α
hx : ¬f x = x
⊢ (g * f⁻¹) x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
hc : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ x ∈ (g.cycleOf x).support

Tactic:
rw [mem_support, cycleOf_apply_self, ne_eq, ← cycleOf_eq_one_iff]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
hc : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ ¬g.cycleOf x = 1