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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ F.map (prod.map f g) ≫ prod.lift (F.map prod.fst) (F.map prod.snd) =
    prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g))

Tactic:
prod.comp_lift,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ prod.lift (F.map (prod.map f g) ≫ F.map prod.fst) (F.map (prod.map f g) ≫ F.map prod.snd) =
    prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g))
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{w, u₂} D
F : C ⥤ D
A B : C
inst✝² : HasBinaryProduct A B
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
H : C ⥤ D
inst✝ : HasBinaryProduct (H.obj A) (H.obj B)
α : F ⟶ H
⊢ α.app (A ⨯ B) ≫ prod.lift (H.map prod.fst) (H.map prod.snd) =
    prod.lift (F.map prod.fst ≫ α.app A) (F.map prod.snd ≫ α.app B)

Tactic:
prod.comp_lift,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{w, u₂} D
F : C ⥤ D
A B : C
inst✝² : HasBinaryProduct A B
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
H : C ⥤ D
inst✝ : HasBinaryProduct (H.obj A) (H.obj B)
α : F ⟶ H
⊢ prod.lift (α.app (A ⨯ B) ≫ H.map prod.fst) (α.app (A ⨯ B) ≫ H.map prod.snd) =
    prod.lift (F.map prod.fst ≫ α.app A) (F.map prod.snd ≫ α.app B)
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 : D
T : C ⥤ D
X Y : StructuredArrow S T
h : X = Y
⊢ Hom.right (eqToHom h) = eqToHom ⋯

Tactic:
by
  subst h
  simp only [eqToHom_refl, id_right]

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:
by simpa using f.w

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
X : T
f✝ g : Over X
φ : f✝ ⟶ g
F : T ⥤ D
h : F.FullyFaithful
A B : Over X
f : (post F).obj A ⟶ (post F).obj B
⊢ F.map (h.preimage (Hom.left f) ≫ B.hom) = F.map A.hom

Tactic:
by simpa using Over.w f

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:
by simpa using f.w

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:
by simpa using f.w

Goal state after:
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✝¹ inst✝ : HasImage f
⊢ (image.eqToHom ⋯ ≫ image.eqToHom ⋯) ≫ image.ι f = 𝟙 (image f) ≫ image.ι f

Tactic:
simp [image.eqToHom, Category.assoc, Category.id_comp]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ Mono (preComp f g ≫ ι g)

Tactic:
simp only [image.preComp_ι]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ Mono (ι (f ≫ g))
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:

Tactic:
f = f ≫ 𝟙 _ := (Category.comp_id _).symm
    _ = f ≫ 0 := by congr!; subsingleton
    _ = 0 := HasZeroMorphisms.comp_zero _ _

Goal state after:
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
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F : C ⥤ D
inst✝ : F.Full
X Y : C
⊢ F.map 0 = F.map (0 ≫ F.preimage 0)

Tactic:
rw [zero_comp]

Goal state after:
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
X : C
f : End X
⊢ 0 ≫ f = 0

Tactic:
exact HasZeroMorphisms.zero_comp _ f

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasFiniteColimits C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ HasColimitsOfShape J C

Tactic:
refine @hasColimitsOfShape_of_equivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasFiniteColimits C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ HasColimitsOfShape (FinCategory.AsType J) C
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

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

Tactic:
intro K
    have : PreservesLimit (pair (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)) G :=
      PreservesLimitPair.of_iso_prod_comparison ..
    apply preservesLimit_of_iso_diagram G (diagramIsoPair K).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ₗ D
G : D ⥤ₗ E
⊢ leftExactFunctor C E (F.obj ⋙ G.obj)

Tactic:
exact comp_preservesFiniteLimits _ _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : D ⥤ₗ E
G : C ⥤ₗ D
⊢ leftExactFunctor C E (G.obj ⋙ F.obj)

Tactic:
exact comp_preservesFiniteLimits _ _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ₑ D
G : D ⥤ₑ E
⊢ leftExactFunctor C E (F.obj ⋙ G.obj)

Tactic:
exact comp_preservesFiniteLimits _ _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : D ⥤ₑ E
G : C ⥤ₑ D
⊢ leftExactFunctor C E (G.obj ⋙ F.obj)

Tactic:
exact comp_preservesFiniteLimits _ _

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
⊢ ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ (Iso.refl X).hom ≫ g' = 0

Tactic:
by simpa using 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✝¹ : HasZeroObject C
inst✝ : Mono f
s : Fork f 0
⊢ 0 ≫ Fork.ι (zeroKernelFork f) = s.ι

Tactic:
rw [zero_comp]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ : HasZeroObject C
inst✝ : Mono f
s : Fork f 0
⊢ 0 = s.ι
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products

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

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

Tactic:
· refine Discrete.natIso fun j => Iso.refl (G.obj (f j.as))

Goal state after:
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 (Discrete.natIso fun j ↦ Iso.refl (G.obj (f j.as))).hom).obj (G.mapCocone (Cofan.mk P g)) ≅
    Cofan.mk (G.obj P) fun j ↦ G.map (g j)
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
⊢ ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ (Iso.refl Y).hom ≫ φ = 0

Tactic:
by simpa using 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
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
Z : C
h : Z ⟶ X
w : h ≫ f = 0
⊢ G.map h ≫ G.map f = 0

Tactic:
simp only [← G.map_comp, w, Functor.map_zero]

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
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
Z : C
h : Y ⟶ Z
w : f ≫ h = 0
⊢ G.map f ≫ G.map h = 0

Tactic:
simp only [← G.map_comp, w, Functor.map_zero]

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

Goal state before:
pp: case pos.refl
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
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasBiproduct (g i)
inst✝ : HasBiproduct fun i ↦ ⨁ g i
x✝¹ x✝ : (i : ι) × f i
j : ι
x y : f j
h : ¬x = y
⊢ (biproduct.ι (g ⟨j, x⟩.fst) ⟨j, x⟩.snd ≫ biproduct.ι (fun i ↦ ⨁ g i) ⟨j, x⟩.fst) ≫
      biproduct.π (fun i ↦ ⨁ g i) ⟨j, y⟩.fst ≫ biproduct.π (g ⟨j, y⟩.fst) ⟨j, y⟩.snd =
    0

Tactic:
simp [biproduct.ι_π_ne _ h]

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 : C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ : BinaryBicone P Q
t : (functoriality P Q F).obj X✝ ⟶ (functoriality P Q F).obj Y✝
⊢ F.map (F.preimage t.hom ≫ Y✝.snd) = F.map X✝.snd

Tactic:
by simpa using! t.wsnd

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

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
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Cofork (ι f i) 0
⊢ ∀ {m : (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯).pt ⟶ s.pt},
    Cofork.π (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯) ≫ m = s.π → m = (fromSubtype f fun j ↦ j ≠ i) ≫ s.π

Tactic:
intro m hm
      rw [← hm, CokernelCofork.π_ofπ, ← Category.assoc, biproduct.fromSubtype_toSubtype]
      exact (Category.id_comp _).symm

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 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:
by
  rw [show coprod.map f g = (biprod.isoCoprod _ _).inv ≫ biprod.map f g ≫
    (biprod.isoCoprod _ _).hom by simp]
  infer_instance

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

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
n✝ : ℕ
f : Fin (n✝ + 1) → α✝
a : α✝
n : ℕ
α : Fin (n + 1) → Type u_2
inst✝ : (i : Fin (n + 1)) → LE (α i)
p : Fin (n + 1)
⊢ ∀ {a b : α p × ((i : Fin n) → α (p.succAbove i))}, (insertNthEquiv α p) a ≤ (insertNthEquiv α p) b ↔ a ≤ b

Tactic:
simp [Pi.le_def, Prod.le_def, p.forall_iff_succAbove]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι →₀ μ
⊢ f ∈ s.finsuppAntidiag n ↔ (f.sum fun x x_1 ↦ x_1) = n ∧ f.support ⊆ s

Tactic:
by
  simp only [mem_finsuppAntidiag, and_congr_left_iff]
  rintro hf
  rw [sum_of_support_subset (N := μ) f hf (fun _ x ↦ x) fun _ _ ↦ rfl]

Goal state after:
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:
rw [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.Combinatorics.Enumerative.Composition

Goal state before:
pp: n✝ : ℕ
c : Composition n✝
n i : ℕ
hi : i ∈ replicate n 1
⊢ 0 < i

Tactic:
simp [List.eq_of_mem_replicate hi]

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, 1 < ∑ i, c.blocksFun i

Tactic:
{

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

Goal state before:
pp: case e'_2.e'_3
ι : 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 : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := (mapRange.addEquiv e).toEquiv
hh : h = (mapRange.addEquiv e).toEquiv
hf : f ∈ s.finsuppAntidiag (e n)
this : n = e.symm (e n)
⊢ (mapRange.addEquiv e.symm).toEmbedding.trans (mapRange.addEquiv e).toEmbedding = Embedding.refl (ι →₀ μ')

Tactic:
apply Function.Embedding.equiv_symm_toEmbedding_trans_toEmbedding

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : 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 : μ
⊢ map (mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) = s.finsuppAntidiag (e n)

Tactic:
ext f
  constructor
  · apply mapRange_finsuppAntidiag_subset
  · 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.Logic.Equiv.Fintype

Goal state before:
pp: β : Type u_2
s t : Finset β
h : s.card = t.card
⊢ ∃ σ, Finset.map (Equiv.toEmbedding σ) s = t

Tactic:
obtain ⟨σ, hσ⟩ := Perm.exists_extending_pair
    (fun x : s => (x : β)) (fun x : s => ((s.equivOfCardEq h) x : β))
    Subtype.val_injective (Subtype.val_injective.comp (s.equivOfCardEq h).injective)
  refine ⟨σ, Finset.eq_of_subset_of_card_le (fun b hb => ?_) (by simp [h])⟩
  obtain ⟨a, ha, rfl⟩ := Finset.mem_map.mp hb
  exact (hσ ⟨a, ha⟩) ▸ ((s.equivOfCardEq h) ⟨a, ha⟩).2

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y x✝ : α
⊢ ¬f x✝ = x✝ → ¬(x✝ = x ∨ x✝ = y) → ¬(swap x y) (f x✝) = x✝

Tactic:
push Not

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y x✝ : α
⊢ f x✝ ≠ x✝ → x✝ ≠ x ∧ x✝ ≠ y → (swap x y) (f x✝) ≠ x✝
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ ¬#f.support = 1 → f = 1 ↔ f = 1

Tactic:
imp_iff_right f.card_support_ne_one

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ f = 1 ↔ f = 1
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro
α : Type u
inst✝ : Finite α
σ τ ρ : Perm α
hc2 : IsConj τ ρ
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint ρ
⊢ IsConj (σ * τ) (f * σ * f⁻¹ * ρ)

Tactic:
obtain ⟨g, rfl⟩ := isConj_iff.1 hc2

Goal state after:
case intro
α : 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⁻¹)
⊢ IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case a
α : 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
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
| (k + 1 + n) % (x :: y :: l).length

Tactic:
← Nat.mod_eq_of_lt hk'

Goal state after:
case a
α : 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
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
| ((k + 1) % (x' :: y' :: l').length + n) % (x :: y :: l).length
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : DecidableEq β✝
α : Type u_4
β : Type u_5
inst✝⁵ : Mul α
inst✝⁴ : Mul β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
me : α ≃* β
⊢ (if h : ∀ (a b : α), me.toEquiv (a * b) = me.toEquiv a * me.toEquiv b then
      some { toEquiv := me.toEquiv, map_mul' := h }
    else none) =
    some me

Tactic:
{

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : DecidableEq β✝
α : Type u_4
β : Type u_5
inst✝⁵ : Mul α
inst✝⁴ : Mul β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
me : α ≃* β
⊢ (if h : ∀ (a b : α), me.toEquiv (a * b) = me.toEquiv a * me.toEquiv b then
      some { toEquiv := me.toEquiv, map_mul' := h }
    else none) =
    some me
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case a
α : 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
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
| k + 1

Tactic:
← Nat.mod_eq_of_lt hk'

Goal state after:
case a
α : 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
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
| (k + 1) % (x' :: y' :: l').length
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
⊢ ∃ i < orderOf f, (f ^ i) x = (f ^ k) x

Tactic:
use (k % orderOf f).natAbs

Goal state after:
case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
⊢ (k % ↑(orderOf f)).natAbs < orderOf f ∧ (f ^ (k % ↑(orderOf f)).natAbs) x = (f ^ k) x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
n : ℤ
hn : (f ^ n) x = y
⊢ (f ^ (n % ↑(orderOf f)).toNat) x = y

Tactic:
{

Goal state after:
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
n : ℤ
hn : (f ^ n) x = y
⊢ (f ^ (n % ↑(orderOf f)).toNat) x = y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DecidableEq α
a b : α
⊢ (swap a b).IsSwap → a ≠ b

Tactic:
intro h hab

Goal state after:
case mp
α : Type u_2
inst✝ : DecidableEq α
a b : α
h : (swap a b).IsSwap
hab : a = b
⊢ False
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case right
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ sign (sumCongr 1 σb) = sign σb

Tactic:
· induction σb using swap_induction_on with
    | one => simp
    | swap_mul σb' b₁ b₂ hb ih =>
      rw [← one_mul (1 : Perm α), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_one_swap,
        sign_swap hb, sign_swap (Sum.inr_injective.ne_iff.mpr hb)]

Goal state after: