mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } })
s : Cocone { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
m : { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.pt ⟶ s.pt
w : ∀ (j : J), { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j ≫ m = s.ι.app j
⊢ m = h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } }

Tactic:
rcases s with ⟨_, _, _⟩

Goal state after:
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝¹ : C
app✝¹ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝¹).obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝¹ Y =
      app✝¹ X ≫ ((Functor.const J).obj pt✝¹).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝¹, ι := { app := app✝¹, naturality := naturality✝¹ } })
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
m :
  { pt := pt✝¹, ι := { app := app✝¹, naturality := naturality✝¹ } }.pt ⟶
    { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.pt
w :
  ∀ (j : J),
    { pt := pt✝¹, ι := { app := app✝¹, naturality := naturality✝¹ } }.ι.app j ≫ m =
      { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j
⊢ m =
    h.desc
      { pt := { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.pt,
        ι :=
          { app := fun j ↦ { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j, naturality := ⋯ } }
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : (-f) ≫ g = (-f) ≫ g'
⊢ g = g'

Tactic:
neg_comp,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : -f ≫ g = (-f) ≫ g'
⊢ g = g'
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : -f ≫ g = (-f) ≫ g'
⊢ g = g'

Tactic:
neg_comp,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : -f ≫ g = -f ≫ g'
⊢ g = g'
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Fork f g
⊢ c.ι ≫ f - c.ι ≫ g = 0

Tactic:
sub_eq_zero,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Fork f g
⊢ c.ι ≫ f = c.ι ≫ g
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ f ≫ c.π - g ≫ c.π = 0

Tactic:
sub_eq_zero,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ f ≫ c.π = g ≫ c.π
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
⊢ IsColimit (G.mapCocone (Cofan.mk P g)) ≃ IsColimit (Cofan.mk (G.obj P) fun j ↦ G.map (g j))

Tactic:
refine (IsColimit.precomposeHomEquiv ?_ _).symm.trans (IsColimit.equivIsoColimit ?_)

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
⊢ (Discrete.functor fun j ↦ G.obj (f j)) ≅ Discrete.functor f ⋙ G

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
⊢ (Cocone.precompose (Iso.hom ?refine_1)).obj (G.mapCocone (Cofan.mk P g)) ≅ Cofan.mk (G.obj P) fun j ↦ G.map (g j)
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (j : J) → f j ⟶ g j
j : J
⊢ ι f j ≫ map p = p j ≫ ι g j

Tactic:
by
  rw [biproduct.map_eq_map']
  apply
    Limits.IsColimit.ι_map (biproduct.isColimit f) (biproduct.bicone g).toCocone
    (Discrete.natTrans fun j => p j.as) (Discrete.mk j)

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

Goal state before:
pp: J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j j✝ : Subtype p
⊢ (ι f ↑j ≫ toSubtype f p) ≫ π (Subtype.restrict p f) j✝ = ι (Subtype.restrict p f) j ≫ π (Subtype.restrict p f) j✝

Tactic:
rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π, biproduct.ι_π]

Goal state after:
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j j✝ : Subtype p
⊢ (if h : ↑j = ↑j✝ then eqToHom ⋯ else 0) = if h : j = j✝ then eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
as✝ : J
⊢ ∑ x, (if h : as✝ = x then eqToHom ⋯ else 0) ≫ t.ι x = t.ι as✝ ≫ 𝟙 t.pt

Tactic:
dite_comp

Goal state after:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
as✝ : J
⊢ (∑ x, if h : as✝ = x then eqToHom ⋯ ≫ t.ι x else 0 ≫ t.ι x) = t.ι as✝ ≫ 𝟙 t.pt
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ t.fst ≫ t.inl + t.snd ≫ t.inr = 𝟙 t.pt

Tactic:
refine BinaryFan.IsLimit.hom_ext ht ?_ ?_

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ (t.fst ≫ t.inl + t.snd ≫ t.inr) ≫ BinaryFan.fst t.toCone = 𝟙 t.pt ≫ BinaryFan.fst t.toCone

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ (t.fst ≫ t.inl + t.snd ≫ t.inr) ≫ BinaryFan.snd t.toCone = 𝟙 t.pt ≫ BinaryFan.snd t.toCone
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 W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
⊢ Mono (map f g)

Tactic:
rw [show coprod.map f g = (biprod.isoCoprod _ _).inv ≫ biprod.map f g ≫
    (biprod.isoCoprod _ _).hom by simp]

Goal state after:
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 W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Mono f
inst✝² : Mono g
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
⊢ Mono ((biprod.isoCoprod W X).inv ≫ biprod.map f g ≫ (biprod.isoCoprod Y Z).hom)
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

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

Tactic:
hq,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ X
hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)
⊢ ((m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst) ≫ b.inl = 0
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 Y
⊢ biprod.fst ≫ biprod.inl = 𝟙 (X ⊞ Y)

Tactic:
apply CategoryTheory.Limits.biprod.hom_ext <;>
      simp only [Category.assoc, biprod.inl_fst, Category.comp_id, Category.id_comp, biprod.inl_snd,
        comp_zero]

Goal state after:
case h₁
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 Y
⊢ 0 = biprod.snd
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

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

Tactic:
hq,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ Y
hq : q ≫ b.inr = m - (f ≫ b.inl + g ≫ b.inr)
⊢ ((m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd) ≫ b.inr = 0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

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

Tactic:
hq,

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

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

Tactic:
hq,

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

Goal state before:
pp: case a.mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : ↥s ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ ∃ a, ∑ i, a i = s.sum f ∧ (fun i ↦ if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f

Tactic:
refine ⟨f ∘ (↑) ∘ e.symm, ?_, by grind⟩

Goal state after:
case a.mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : ↥s ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ ∑ i, (f ∘ Subtype.val ∘ ⇑e.symm) i = s.sum f
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
σ : Type u_1
s : Sym σ n
inst✝ : DecidableEq σ
⊢ (map (fun a ↦ count a ↑s) (↑s).dedup).sum = n

Tactic:
by
    change ∑ a ∈ s.1.toFinset, count a s.1 = n
    rw [toFinset_sum_count_eq]
    exact s.2

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

Goal state before:
pp: α : Type u_1
f g : Perm α
⊢ f.Disjoint g → g.Disjoint f

Tactic:
by simp only [Disjoint, or_comm, imp_self]

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

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

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

pp: 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]

Tactic:
· simp at hl

Goal state after:
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.GroupTheory.Perm.List

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

pp: 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]

Tactic:
· simp at hl

Goal state after:
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.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
⊢ (y :: l).formPerm x = y ↔ (y :: l).formPerm x = (y :: l).formPerm ((y :: l).getLast ⋯)

Tactic:
by rw [formPerm_apply_getLast]

Goal state after:
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
y : α
hy : f y ≠ y
h : y = x
⊢ False

Tactic:
simp [h, hfx.symm] at hy

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
⊢ [].formPerm = l'.formPerm ↔ [] ~r l' ∨ [].length ≤ 1 ∧ l'.length ≤ 1

Tactic:
suffices l'.length ≤ 1 ↔ l' = nil ∨ l'.length ≤ 1 by
      simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero_iff]

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
⊢ l'.length ≤ 1 ↔ l' = [] ∨ l'.length ≤ 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
n : ℤ
⊢ ((fun x ↦ σ ^ x) n) (Classical.choose hσ) ∈ σ.support

Tactic:
zpow_apply_mem_support,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
n : ℤ
⊢ Classical.choose hσ ∈ σ.support
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), f x ≠ x → x ∈ []
this : f = 1
⊢ signAux (e.symm.trans e) = signAux2 [] (Equiv.refl α)

Tactic:
Equiv.symm_trans_self,

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), f x ≠ x → x ∈ []
this : f = 1
⊢ signAux (Equiv.refl (Fin n)) = signAux2 [] (Equiv.refl α)
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
⊢ closure {σ | σ.IsCycle} = ⊤

Tactic:
cases nonempty_fintype β
    exact
      top_le_iff.mp (le_trans (ge_of_eq closure_isSwap) (closure_mono fun _ => IsSwap.isCycle))

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h✝ : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : x = f x
y : α
hy : f y ≠ y
h : y = x
⊢ False

Tactic:
simp [h, hfx.symm] at hy

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 : -1 = 1
⊢ False

Tactic:
exact absurd this (by simp_all)

Goal state after:
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: x y d m : ℕ
hd : x.gcd y = d
d0 : d.beq 0 = false
dm : x * y = d * m
⊢ d * x.lcm y = d * m

Tactic:
← dm,

Goal state after:
x y d m : ℕ
hd : x.gcd y = d
d0 : d.beq 0 = false
dm : x * y = d * m
⊢ d * x.lcm y = x * y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
g : Perm α
s : Finset α
hs : ∀ (x : α), g x ∈ s ↔ x ∈ s
n : ℕ
x : α
hx : x ∈ s
⊢ ↑((g.subtypePerm hs ^ n) ⟨x, hx⟩) = (g ^ n) x

Tactic:
simp only [subtypePerm_pow, subtypePerm_apply]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : f ∈ Set.range ⇑(ϕ i)
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
⊢ f ∈ ⊥

Tactic:
obtain ⟨g', hg'f⟩ := hxi

Goal state after:
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
⊢ f ∈ ⊥
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ ∃ n, σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)

Tactic:
refine ⟨Multiset.card σ.cycleType - 1, eq_replicate.2 ⟨?_, fun n hn ↦ ?_⟩⟩

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ σ.cycleType.card = σ.cycleType.card - 1 + 1

case refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
n : ℕ
hn : n ∈ σ.cycleType
⊢ n = orderOf σ
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∈ s
⊢ (c ^ n) x = (ofSubtype (c.subtypePerm ⋯ ^ n)) x

pp: case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∉ s
⊢ (c ^ n) x = (ofSubtype (c.subtypePerm ⋯ ^ n)) x

Tactic:
· rw [ofSubtype_apply_of_mem (subtypePerm c _ ^ n) hx,
        subtypePerm_zpow, subtypePerm_apply]

Goal state after:
case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∉ s
⊢ (c ^ n) x = (ofSubtype (c.subtypePerm ⋯ ^ n)) x
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ.refine_2
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
⊢ ↑((finRotate (n✝ + 1).succ) i.succ) = ↑((decomposeFin.symm (1, finRotate (n✝ + 1))) i.succ)

Tactic:
coe_finRotate,

Goal state after:
case succ.refine_2
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
⊢ (if i.succ = Fin.last (n✝ + 1) then 0 else ↑i.succ + 1) = ↑((decomposeFin.symm (1, finRotate (n✝ + 1))) i.succ)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case neg
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
h : ¬i = Fin.last n✝
⊢ ↑i + 1 + 1 = (swap ↑0 ↑1) (↑((finRotate (n✝ + 1)) i) + 1)

Tactic:
coe_finRotate,

Goal state after:
case neg
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
h : ¬i = Fin.last n✝
⊢ ↑i + 1 + 1 = (swap ↑0 ↑1) ((if i = Fin.last n✝ then 0 else ↑i + 1) + 1)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ (finRotate n).support = Finset.univ

Tactic:
obtain ⟨m, rfl⟩ := exists_add_of_le h

Goal state after:
m : ℕ
h : 2 ≤ 2 + m
⊢ (finRotate (2 + m)).support = Finset.univ