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

Goal state before:
pp: case h₂
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryCoproduct W X
inst✝ : HasBinaryCoproduct Y Z
Z✝ : C
i₁ i₂ : Y ⨿ Z ⟶ Z✝
h : map f g ≫ i₁ = map f g ≫ i₂
⊢ inr ≫ i₁ = inr ≫ i₂

Tactic:
← cancel_epi g

Goal state after:
case h₂
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryCoproduct W X
inst✝ : HasBinaryCoproduct Y Z
Z✝ : C
i₁ i₂ : Y ⨿ Z ⟶ Z✝
h : map f g ≫ i₁ = map f g ≫ i₂
⊢ g ≫ inr ≫ i₁ = g ≫ inr ≫ i₂
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ (leftUnitor X).inv ≫ map (𝟙 (⊤_ C)) f = f ≫ (leftUnitor Y).inv

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.leftUnitor_hom_naturality]

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 : D
T : C ⥤ D
X Y : StructuredArrow S T
f : X ⟶ Y
⊢ X.hom ≫ T.map (Hom.right f) = Y.hom

Tactic:
by
  simpa using (CommaMorphism.w f).symm

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
⊢ ∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j

Tactic:
rintro ⟨j⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
j : WalkingPair
⊢ m ≫ s.π.app { as := j } = (BinaryFan.swap t).π.app { as := j }
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
⊢ (X : WalkingParallelPair) → F.obj X ≅ G.obj X

Tactic:
rintro ⟨j⟩

Goal state after:
case zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
⊢ F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero

case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
⊢ F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
i : IsIso (terminalComparison G)
⊢ IsTerminal (G.obj (⊤_ C))

Tactic:
exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (Functor.empty.{0} D)) i

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
i : IsIso (terminalComparison G)
⊢ PreservesLimit (Functor.empty C) G

Tactic:
apply preservesLimit_of_preserves_limit_cone terminalIsTerminal
  apply (isLimitMapConeEmptyConeEquiv _ _).symm _
  exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (Functor.empty.{0} D)) i

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
O : C
hO : IsZero O
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ 0 = 0

Tactic:
by
    change f ≫ (hO.from_ Y ≫ hO.to_ Z) = hO.from_ X ≫ hO.to_ Z
    rw [← Category.assoc]
    congr
    apply hO.eq_of_tgt

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ 0 = 0

Tactic:
change f ≫ (default : Y ⟶ 0) ≫ default = (default : X ⟶ 0) ≫ default

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ default ≫ default = default ≫ default
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f : X ⟶ Y
⊢ (isoSourceOfSelf f).inv ≫ ι f f = lift (𝟙 X) ⋯ ≫ ι f f

Tactic:
simp [equalizer.isoSourceOfSelf]

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : F.PreservesZeroMorphisms
⊢ F.biproductComparison' f ≫ F.biproductComparison f = 𝟙 (⨁ F.obj ∘ f)

Tactic:
ext
    simp [biproduct.ι_π, ← Functor.map_comp, eqToHom_map]

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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
k k' : K
⊢ c.ι (g k) ≫ c.π (g k') = if h : k = k' then eqToHom ⋯ else 0

Tactic:
simp only [c.ι_π]
    split_ifs with h h' h' <;> simp [Equiv.apply_eq_iff_eq g] at h h' <;> tauto

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)
inst✝ : DecidablePred p
⊢ toSubtype f p ≫ fromSubtype f p = map fun j ↦ if p j then 𝟙 (f j) else 0

Tactic:
by
  ext1 i
  by_cases h : p i
  · simp [h]
  · simp [h]

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

Goal state before:
pp: case mp
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
this : fst = inv inl
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl

Tactic:
rw [this, IsIso.inv_hom_id]

Goal state after:
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
T U : C
f : T ⟶ X
g : T ⟶ Y
h : X ⟶ U
i : Y ⟶ U
⊢ lift f g ≫ desc h i = f ≫ h + g ≫ i

Tactic:
simp [biprod.lift_eq, biprod.desc_eq]

Goal state after:
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
⊢ m = f ≫ b.inl + g ≫ b.inr

Tactic:
have h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0 := by simpa using sub_eq_zero.2 h₂

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
⊢ m = f ≫ b.inl + g ≫ b.inr
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
⊢ m = f ≫ b.inl + g ≫ b.inr

Tactic:
have h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0 := by simpa using sub_eq_zero.2 h₂

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
⊢ m = f ≫ b.inl + g ≫ b.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
⊢ (biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst) ≫ f = 𝟙 Y

Tactic:
by
        have t := congrArg (fun p : Y ⊞ Z ⟶ Y ⊞ Z => biprod.inl ≫ p ≫ biprod.fst)
          (IsIso.inv_hom_id (biprod.map f g))
        simp only [Category.id_comp, Category.assoc, biprod.map_fst] at t
        simp only [Category.assoc]
        simp [t]

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

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

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

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

Tactic:
· rename_i j
      have : q ≤ j.castSucc := by simpa [lt_succAbove_iff_le_castSucc] using hab
      simpa using hgt _ this

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

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

Goal state before:
pp: k n : ℕ
⊢ Pairwise (Pi.Lex (fun x1 x2 ↦ x1 < x2) fun x x1 x2 ↦ x1 < x2)
    (flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n))

Tactic:
List.pairwise_flatMap,

Goal state after:
k n : ℕ
⊢ (∀ a ∈ antidiagonal n,
      Pairwise (Pi.Lex (fun x1 x2 ↦ x1 < x2) fun x x1 x2 ↦ x1 < x2)
        (map (fun x ↦ Fin.cons a.1 x) (antidiagonalTuple k a.2))) ∧
    Pairwise
      (fun a₁ a₂ ↦
        ∀ x ∈ map (fun x ↦ Fin.cons a₁.1 x) (antidiagonalTuple k a₁.2),
          ∀ y ∈ map (fun x ↦ Fin.cons a₂.1 x) (antidiagonalTuple k a₂.2),
            Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun x x1 x2 ↦ x1 < x2) x y)
      (antidiagonal n)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
hf : f x = x
hg : f (g x) = g x
⊢ (f * g) x = (g * f) x

Tactic:
simp [mul_apply, hf, hg]

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

Goal state before:
pp: α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
hg : g x = x
hf : g (f x) = f x
⊢ (f * g) x = (g * f) x

Tactic:
simp [mul_apply, hf, 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, f ∈ map { toFun := fun f ↦ (↑f).update a a_1.1, inj' := ⋯ } (s.finsuppAntidiag a_1.2).attach

Tactic:
simp_rw [mem_map, mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk, exists_prop, and_comm,
    eq_comm]

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

Goal state before:
pp: case refl
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin c₁.length
c₂ : Composition n₁
i₂ : Fin c₂.length
hc : c₁ = c₂
hi : ↑i₁ = ↑i₂
⊢ c₁.blocksFun i₁ = c₂.blocksFun i₂

Tactic:
cases hc

Goal state after:
case refl.refl
n₁ : ℕ
c₁ : Composition n₁
i₁ i₂ : Fin c₁.length
hi : ↑i₁ = ↑i₂
⊢ c₁.blocksFun i₁ = c₁.blocksFun i₂
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : Fintype.card ↑s = Fintype.card ↑t
fs : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
ht : ∀ (x : α), x ∈ ft ↔ x ∈ t
hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t
hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s
hc : (fs \ ft).card = (ft \ fs).card
⊢ ↑(s \ t) ≃ ↑(t \ s)

Tactic:
← Fintype.subtype_card (fs \ ft) hst,

Goal state after:
α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : Fintype.card ↑s = Fintype.card ↑t
fs : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
ht : ∀ (x : α), x ∈ ft ↔ x ∈ t
hst : ∀ (x : α), x ∈ fs \ ft ↔ x ∈ s \ t
hts : ∀ (x : α), x ∈ ft \ fs ↔ x ∈ t \ s
hc : Fintype.card { x // x ∈ s \ t } = (ft \ fs).card
⊢ ↑(s \ t) ≃ ↑(t \ s)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ ns.sum = (drop n l).length

Tactic:
· rw [length_drop, ← h, add_tsub_cancel_left]

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

Goal state before:
pp: case mp.inr.inr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
j : Fin (n - 1)
hj1 : ⟨↑j + 1, ⋯⟩ ∈ c.boundaries
hj2 : ↑i = ↑j + 1
⊢ i ∈ c.boundaries

Tactic:
convert! hj1

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : x ∈ l
⊢ l.formPerm x ∈ l

Tactic:
rcases l with - | ⟨y, l⟩

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
h : x ∈ []
⊢ [].formPerm x ∈ []

case cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
h : x ∈ y :: l
⊢ (y :: l).formPerm x ∈ y :: l
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u : ℤˣ
⊢ u ^ 2 = 1

Tactic:
units_sq

Goal state after:
u : ℤˣ
⊢ 1 = 1
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u₁ u₂ : ℤˣ
⊢ u₁ / u₂ = u₁ * u₂

Tactic:
div_eq_mul_inv,

Goal state after:
u₁ u₂ : ℤˣ
⊢ u₁ * u₂⁻¹ = u₁ * u₂
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
⊢ False

Tactic:
have hxa : x ≠ g.symm x := fun h => (List.nodup_cons.1 hl).1 (h ▸ hx)

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

Goal state before:
pp: case cons.cons.cons.cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
hl : (x :: y :: l).Nodup
x' y' : α
l' : List α
hl' : (x' :: y' :: l').Nodup
⊢ (x :: y :: l).formPerm = (x' :: y' :: l').formPerm ↔
    x :: y :: l ~r x' :: y' :: l' ∨ (x :: y :: l).length ≤ 1 ∧ (x' :: y' :: l').length ≤ 1

Tactic:
· simp [-formPerm_cons_cons, formPerm_ext_iff hl hl']

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

Goal state before:
pp: α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x : α
hx : f x ≠ x
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
hx' : g x ≠ x
m : ℕ
hm : (g ^ m) x = z
h'' : ∀ x ∈ f.support ∩ g.support, f x = g x
⊢ (g ^ m) x ∈ f.support

Tactic:
←
      pow_eq_on_of_mem_support h'' _ x
        (mem_inter_of_mem (mem_support.mpr hx) (mem_support.mpr hx')),

Goal state after:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x : α
hx : f x ≠ x
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
hx' : g x ≠ x
m : ℕ
hm : (g ^ m) x = z
h'' : ∀ x ∈ f.support ∩ g.support, f x = g x
⊢ (f ^ m) x ∈ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f g : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, f x = g x
hx : f x = g x
hx' : x ∈ f.support
hx'' : x ∈ g.support
this : f.support ⊆ g.support
⊢ f = g

Tactic:
inter_eq_left.mpr this

Goal state after:
α : Type u_2
f g : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support, f x = g x
hx : f x = g x
hx' : x ∈ f.support
hx'' : x ∈ g.support
this : f.support ⊆ g.support
⊢ f = g
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
⊢ f ^ n = 1 → ∃ x, f x ≠ x ∧ (f ^ n) x = x

Tactic:
intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩

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

Goal state before:
pp: case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
⊢ f ^ a = f ^ b → ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x

Tactic:
intro h
      obtain ⟨x, hx, -⟩ := id hf
      exact ⟨x, hx, by simp [h]⟩

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

Goal state before:
pp: case pos
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h : f.SameCycle x y
⊢ (ofSubtype (f.subtypePerm ⋯)) y = f y

Tactic:
apply ofSubtype_apply_of_mem

Goal state after:
case pos
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h : f.SameCycle x y
⊢ f.SameCycle x y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case refine_1
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a b : α
hx : a ∈ s ∧ b ∈ s
⊢ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f)^[a_1] a_2 = b

Tactic:
obtain ⟨n, hn, rfl⟩ := hf.exists_pow_eq hx.1 hx.2

Goal state after:
case refine_1
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a : α
n : ℕ
hn : n < #s
hx : a ∈ s ∧ (f ^ n) a ∈ s
⊢ ∃ a_1 < #s, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f)^[a_1] a_2 = (f ^ n) a
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)
⊢ -(-1) ^ a * (Multiset.map (fun n ↦ -(-1) ^ n) s).prod = (-1) ^ ((a ::ₘ s).sum + (a ::ₘ s).card)

Tactic:
Multiset.sum_cons,

Goal state after:
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)
⊢ -(-1) ^ a * (Multiset.map (fun n ↦ -(-1) ^ n) s).prod = (-1) ^ (a + s.sum + (a ::ₘ s).card)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
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:
ofSubtype_apply_of_not_mem (subtypePerm c _ ^ n) hx,

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 = x
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
h : i < j
⊢ ((finRotate (↑i + 1)).extendDomain (castLEEmb ⋯).toEquivRange) j = j

Tactic:
Perm.extendDomain_apply_not_subtype

Goal state after:
n : ℕ
i j : Fin n
h : i < j
⊢ j = j

case h
n : ℕ
i j : Fin n
h : i < j
⊢ j ∉ Set.range ⇑(castLEEmb ⋯)
Module: Mathlib.Data.FunLike.Group

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : Mul F
inst✝¹ : Mul β
inst✝ : IsMulApply F α β
⊢ Function.Injective DFunLike.coe

Tactic:
exact DFunLike.coe_injective

Goal state after:
Module: Mathlib.Data.FunLike.Group

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : FunLike F α β
inst✝³ : MulOne F
inst✝² : MulOneClass β
inst✝¹ : IsOneApply F α β
inst✝ : IsMulApply F α β
⊢ Function.Injective DFunLike.coe

Tactic:
exact DFunLike.coe_injective

Goal state after: