mathlib-initiative/mathlib-tactics huggingface dataset:
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✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : D ⟶ (Functor.const J).obj X
c : Cone D
p : c.pt ⟶ X
hp : ∀ (j : J), c.π.app j ≫ s.app j = p
hc : IsLimit c
t : Cone (Over.lift D s)
⊢ hc.lift ((forget X).mapCone t) ≫ (liftCone D s c p hp).pt.hom = t.pt.hom

Tactic:
let j : J := Classical.arbitrary _

Goal state after:
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✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : D ⟶ (Functor.const J).obj X
c : Cone D
p : c.pt ⟶ X
hp : ∀ (j : J), c.π.app j ≫ s.app j = p
hc : IsLimit c
t : Cone (Over.lift D s)
j : J := Classical.arbitrary J
⊢ hc.lift ((forget X).mapCone t) ≫ (liftCone D s c p hp).pt.hom = t.pt.hom
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 : Under X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : (Functor.const J).obj X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
⊢ (liftCocone D s c p hp).pt.hom ≫ hc.desc ((forget X).mapCocone t) = t.pt.hom

Tactic:
let j : J := Classical.arbitrary _

Goal state after:
T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
X✝ : T
f g : Under X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : (Functor.const J).obj X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
j : J := Classical.arbitrary J
⊢ (liftCocone D s c p hp).pt.hom ≫ hc.desc ((forget X).mapCocone t) = t.pt.hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ s.fst = t.fst
hr' : m✝ ≫ s.snd = t.snd
⊢ hs.lift (mk t.fst t.snd ⋯) ≫ s.fst = t.fst

pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ s.fst = t.fst
hr' : m✝ ≫ s.snd = t.snd
⊢ hs.lift (mk t.fst t.snd ⋯) ≫ s.snd = t.snd

Tactic:
exacts [hs.fac _ WalkingCospan.left, hs.fac _ WalkingCospan.right]

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

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m✝ : (mk s.inl s.inr ⋯).pt ⟶ t.pt
hr : s.inl ≫ m✝ = t.inl
hr' : s.inr ≫ m✝ = t.inr
⊢ s.inl ≫ m✝ = s.inl ≫ hs.desc (mk t.inl t.inr ⋯)

Tactic:
simp only [hr]

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m✝ : (mk s.inl s.inr ⋯).pt ⟶ t.pt
hr : s.inl ≫ m✝ = t.inl
hr' : s.inr ≫ m✝ = t.inr
⊢ t.inl = s.inl ≫ hs.desc (mk t.inl t.inr ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f g).obj one

Tactic:
· exact ι ≫ f

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

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

Tactic:
apply ext_aux
  intro X Y
  have : (I.zero X Y).zero ≫ (J.zero Y Y).zero = (I.zero X Y).zero := by
    apply I.zero_comp X (J.zero Y Y).zero
  have that : (I.zero X Y).zero ≫ (J.zero Y Y).zero = (J.zero X Y).zero := by
    apply J.comp_zero (I.zero X Y).zero Y
  rw [← this, ← that]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
f g h : Arrow C
inst✝⁴ : HasImage f.hom
inst✝³ : HasImage g.hom
inst✝² : HasImage h.hom
sq1 : f ⟶ g
sq2 : g ⟶ h
inst✝¹ : HasImageMap sq1
inst✝ : HasImageMap sq2
⊢ (imageMap sq1).map ≫ image.ι g.hom ≫ Arrow.Hom.right sq2 = image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2)

Tactic:
ImageMap.map_ι_assoc,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
f g h : Arrow C
inst✝⁴ : HasImage f.hom
inst✝³ : HasImage g.hom
inst✝² : HasImage h.hom
sq1 : f ⟶ g
sq2 : g ⟶ h
inst✝¹ : HasImageMap sq1
inst✝ : HasImageMap sq2
⊢ image.ι f.hom ≫ Arrow.Hom.right sq1 ≫ Arrow.Hom.right sq2 = image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2)
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasStrongEpiMonoFactorisations C
X Y : C
f : X ⟶ Y
I' : C
e : X ⟶ I'
m : I' ⟶ Y
comm : e ≫ m = f
inst✝¹ : StrongEpi e
inst✝ : Mono m
⊢ (isoStrongEpiMono e m comm).hom ≫ ι f = m

Tactic:
dsimp [isoStrongEpiMono]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasStrongEpiMonoFactorisations C
X Y : C
f : X ⟶ Y
I' : C
e : X ⟶ I'
m : I' ⟶ Y
comm : e ≫ m = f
inst✝¹ : StrongEpi e
inst✝ : Mono m
⊢ { I := I', m := m, m_mono := inst✝, e := e, fac := ⋯, e_strong_epi := inst✝¹ }.toMonoIsImage.lift
        (Image.monoFactorisation f) ≫
      ι f =
    m
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
D : Type u'
F : D → C
x✝⁵ x✝⁴ x✝³ : InducedCategory C F
x✝² x✝¹ : x✝⁵ ⟶ x✝⁴
x✝ : x✝⁴ ⟶ x✝³
⊢ ((x✝² + x✝¹) ≫ x✝).hom = (x✝² ≫ x✝ + x✝¹ ≫ x✝).hom

Tactic:
apply add_comp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
Z : ObjectProperty C
x✝⁵ x✝⁴ x✝³ : Z.FullSubcategory
x✝² x✝¹ : x✝⁵ ⟶ x✝⁴
x✝ : x✝⁴ ⟶ x✝³
⊢ ((x✝² + x✝¹) ≫ x✝).hom = (x✝² ≫ x✝ + x✝¹ ≫ x✝).hom

Tactic:
apply add_comp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

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
J✝ : Type w
inst✝² : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
J : Type u
inst✝¹ : Finite J
inst✝ : PreservesFiniteProducts F
n : ℕ
e : J ≃ Fin n
⊢ PreservesLimitsOfShape (Discrete J) F

Tactic:
have := PreservesFiniteProducts.preserves (F := F) n

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
J✝ : Type w
inst✝² : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
J : Type u
inst✝¹ : Finite J
inst✝ : PreservesFiniteProducts F
n : ℕ
e : J ≃ Fin n
this : PreservesLimitsOfShape (Discrete (Fin n)) F
⊢ PreservesLimitsOfShape (Discrete J) F
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
⊢ ⊤.map P.ι X → P.isoClosure X

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
⊢ P.isoClosure X → ⊤.map P.ι X

Tactic:
· rintro ⟨⟨Y, hY⟩, _, ⟨e⟩⟩
    exact ⟨Y, hY, ⟨e.symm⟩⟩

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
⊢ P.isoClosure X → ⊤.map P.ι X
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: G : Type u_1
⊢ Injective (@toDivInvMonoid G)

Tactic:
rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: G : Type u_1
⊢ Injective (@toGroup G)

Tactic:
rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl

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

Goal state before:
pp: case pos
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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
k k' : K
h : g k = g k'
h' : k = k'
⊢ eqToHom ⋯ = eqToHom ⋯

Tactic:
simp [Equiv.apply_eq_iff_eq g] at h h'

Goal state after:
case pos
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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
k k' : K
h✝ : g k = g k'
h' h : k = k'
⊢ eqToHom ⋯ = eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case neg
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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
k k' : K
h : g k = g k'
h' : ¬k = k'
⊢ eqToHom ⋯ = 0

Tactic:
simp [Equiv.apply_eq_iff_eq g] at h h'

Goal state after:
case neg
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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
k k' : K
h✝ : g k = g k'
h' : ¬k = k'
h : k = k'
⊢ eqToHom ⋯ = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case pos
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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
k k' : K
h : ¬g k = g k'
h' : k = k'
⊢ 0 = eqToHom ⋯

Tactic:
simp [Equiv.apply_eq_iff_eq g] at h h'

Goal state after:
case pos
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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
k k' : K
h' : k = k'
h : ¬k = k'
⊢ 0 = eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case neg
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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
k k' : K
h : ¬g k = g k'
h' : ¬k = k'
⊢ 0 = 0

Tactic:
simp [Equiv.apply_eq_iff_eq g] at h h'

Goal state after:
case neg
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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
k k' : K
h' h : ¬k = k'
⊢ 0 = 0
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 g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Epi (p j)
⊢ Epi (map p)

Tactic:
by
  rw [show Pi.map p = (biproduct.isoProduct _).inv ≫ biproduct.map p ≫
    (biproduct.isoProduct _).hom by aesop]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Scalar

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq β
inst✝³ : DecidableEq γ
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Finset β
t : Finset γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
⊢ (op a • s) • t = s • a • t

Tactic:
ext
  simp [mem_smul, mem_smul_finset, h]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst✝ : IsIso f₁₁
⊢ (unipotentLower (-f₂₁ ≫ inv f₁₁)).hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ (unipotentUpper (-inv f₁₁ ≫ f₁₂)).hom =
    biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂)

Tactic:
by ext <;> simp; abel

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

Goal state before:
pp: n : ℕ
c : Composition n
⊢ 0 ∈ c.boundaries

Tactic:
simp only [boundaries, Finset.mem_univ, Finset.mem_map]

Goal state after:
n : ℕ
c : Composition n
⊢ ∃ a, True ∧ c.boundary.toEmbedding a = 0
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ Fin.last n ∈ c.boundaries

Tactic:
simp only [boundaries, Finset.mem_univ, Finset.mem_map]

Goal state after:
n : ℕ
c : Composition n
⊢ ∃ a, True ∧ c.boundary.toEmbedding a = Fin.last n
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
⊢ ↑j < c.blocksFun (c.index j) + c.sizeUpTo ↑(c.index j)

pp: n : ℕ
c : Composition n
j : Fin n
⊢ c.sizeUpTo ↑(c.index j) ≤ ↑j

Tactic:
add_comm,

Goal state after:
n : ℕ
c : Composition n
j : Fin n
⊢ ↑j < c.sizeUpTo ↑(c.index j) + c.blocksFun (c.index j)

n : ℕ
c : Composition n
j : Fin n
⊢ c.sizeUpTo ↑(c.index j) ≤ ↑j
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
⊢ x = f x ∨ g x = x

Tactic:
eq_comm

Goal state after:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
⊢ f x = x ∨ g x = x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f : Perm α
l : List (Perm α)
h : ∀ g ∈ l, f.Disjoint g
⊢ f.Disjoint l.prod

Tactic:
by
  induction l with
  | nil => exact disjoint_one_right _
  | cons g l ih =>
    rw [List.prod_cons]
    exact (h _ List.mem_cons_self).mul_right (ih fun g hg => h g (List.mem_cons_of_mem _ hg))

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 μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ (∃ m ∈ antidiagonal n, ∃ g, f = g.update a m.1 ∧ g ∈ s.finsuppAntidiag m.2) ↔
    ∃ a_1 ∈ antidiagonal n, ∃ a_2, a_2.update a a_1.1 = f ∧ a_2 ∈ s.finsuppAntidiag a_1.2

Tactic:
eq_comm

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

Goal state before:
pp: case mpr
n : ℕ
c : Composition n
⊢ (∀ i ∈ c.blocks, i = 1) → c = ones n

Tactic:
intro H

Goal state after:
case mpr
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
⊢ c = ones n
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n : ℕ
c : Composition n
⊢ ¬c = ones n → ¬c.length = n

Tactic:
intro H

Goal state after:
case mpr
n : ℕ
c : Composition n
H : ¬c = ones n
⊢ ¬c.length = n
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
h : 0 < n
c : Composition n
⊢ c = single n h → c.length = 1

Tactic:
intro H

Goal state after:
case mp
n : ℕ
h : 0 < n
c : Composition n
H : c = single n h
⊢ c.length = 1
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n : ℕ
h : 0 < n
c : Composition n
⊢ c.length = 1 → c = single n h

Tactic:
intro H

Goal state after:
case mpr
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
⊢ c = single n h
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
⊢ (f ^ n) x ∈ f.support ↔ x ∈ f.support

Tactic:
simp only [mem_support, ne_eq, apply_pow_apply_eq_iff]

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

Goal state before:
pp: n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : ↑i + 1 ≠ n
⊢ i ∈ {i | ⟨1 + ↑i, ⋯⟩ ∈ {i | i = 0 ∨ i = Fin.last n ∨ ∃ j, ∃ (_ : j ∈ s), ↑i = ↑j + 1}.toFinset}.toFinset ↔ i ∈ s

Tactic:
add_comm,

Goal state after:
n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : ↑i + 1 ≠ n
⊢ i ∈ {i | ⟨↑i + 1, ⋯⟩ ∈ {i | i = 0 ∨ i = Fin.last n ∨ ∃ j, ∃ (_ : j ∈ s), ↑i = ↑j + 1}.toFinset}.toFinset ↔ i ∈ s
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
h : x ≠ y
⊢ (swap x y).support = {x, y}

Tactic:
grind [support]

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

Goal state before:
pp: case mp.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
l : m
hx : σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inr → Sum.inl l ∈ Set.range Sum.inr

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
case mp.inl
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inl) (Set.range Sum.inl)
l : m
a : n
hx : σ (Sum.inr a) = Sum.inl l
⊢ Sum.inl l ∈ Set.range Sum.inr
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y x✝ : α
⊢ x✝ ∈ f.support \ {x, y} → x✝ ∈ (swap x y * f).support

Tactic:
simp only [and_imp, Perm.coe_mul, Function.comp_apply, Ne, mem_support, mem_insert, mem_sdiff,
    mem_singleton]

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.Finite

Goal state before:
pp: case mpr.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inl → Sum.inr r ∈ Set.range Sum.inl

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
case mpr.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
r : n
a : m
hx : σ (Sum.inl a) = Sum.inr r
⊢ Sum.inr r ∈ Set.range Sum.inl
Module: Mathlib.GroupTheory.Perm.List

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

Tactic:
formPerm_apply_getLast

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ x = x
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:
formPerm_apply_getLast

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
⊢ (y :: l).formPerm x = y ↔ (y :: l).formPerm x = y
Module: Mathlib.GroupTheory.Perm.List

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

Tactic:
intro H

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
⊢ False
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: x : ℤ
⊢ IsUnit x ↔ |x| = 1

Tactic:
by
  rw [isUnit_iff_natAbs_eq, abs_eq_natAbs, ← Int.ofNat_one, natCast_inj]

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ {s : Finset α} {f : Equiv.Perm α}, f ∈ permsOfFinset s ↔ ∀ {x : α}, f x ≠ x → x ∈ s

Tactic:
rintro ⟨⟨l⟩, hs⟩ f; exact mem_permsOfList_iff

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

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

Tactic:
add_comm,

Goal state after:
α : Type u_2
f : Perm α
x y : α
x✝ : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ f x = x ↔ (f ^ (i + 1)) x = (f ^ i) x
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
⊢ x ∉ {x | (l.formPerm ^ l.length) x ≠ x}

Tactic:
intro H

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
H : x ∈ {x | (l.formPerm ^ l.length) x ≠ x}
⊢ False
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) ^ (i + 1)) (f x) = b

Tactic:
add_comm,

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 + i)) (f x) = b
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case neg
α : 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 y z ∈ H

Tactic:
by_cases h6 : z = y

Goal state after:
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
h6 : z = y
⊢ swap y z ∈ H

case neg
α : 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
h6 : ¬z = y
⊢ swap y z ∈ H
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
⊢ (if f⁻¹ ((Equiv.symm f) b) = x then (Equiv.symm f) x
    else if f⁻¹ ((Equiv.symm f) b) = (Equiv.symm f) x then x else f⁻¹ ((Equiv.symm f) b)) ≠
    (Equiv.symm f) b

Tactic:
split_ifs <;> simp [symm_apply_eq, eq_symm_apply] at * <;> tauto

Goal state after:
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).Nodup
⊢ {a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)

Tactic:
| cons a l ih =>

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).Nodup
⊢ {a_1 | a_1 ∈ a :: l}.Pairwise r ↔ Pairwise r (a :: l)