mathlib-initiative/mathlib-tactics huggingface dataset:
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 : D
S : C ⥤ D
f : CostructuredArrow S T
⊢ (map (𝟙 T)).obj f = f

Tactic:
rw [eq_mk f]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
f : CostructuredArrow S T
⊢ (map (𝟙 T)).obj (mk f.hom) = mk f.hom
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M : SemimoduleCat R
h : IsZero M
x : ↑M
⊢ LinearMap.id x = 0

Tactic:
← SemimoduleCat.hom_id

Goal state after:
R : Type u
inst✝ : Semiring R
M : SemimoduleCat R
h : IsZero M
x : ↑M
⊢ (Hom.hom (𝟙 M)) x = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
f g : Arrow C
inst✝⁵ : HasImage f.hom
inst✝⁴ : HasImage g.hom
sq : f ⟶ g
inst✝³ : HasImageMap sq
h : Arrow C
inst✝² : HasImage h.hom
sq' : g ⟶ h
inst✝¹ : HasImageMap sq'
inst✝ : HasImageMap (sq ≫ sq')
⊢ (HasImageMap.imageMap (sq ≫ sq')).map = (imageMapComp sq sq').map

Tactic:
congr; simp only [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
f : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImageMap (𝟙 f)
⊢ (HasImageMap.imageMap (𝟙 f)).map = (imageMapId f).map

Tactic:
congr; simp only [eq_iff_true_of_subsingleton]

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

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

Tactic:
apply hO.eq_of_src

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

Goal state before:
pp: M : Type u
⊢ Injective (@toMonoid M)

Tactic:
by
  rintro @⟨@⟨⟩⟩ @⟨@⟨⟩⟩ h
  congr <;> injection h

Goal state after:
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
X Y : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ PreservesColimit (pair X Y) G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (coprodIsCoprod X Y)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ IsColimit (G.mapCocone (BinaryCofan.mk coprod.inl coprod.inr))
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case pos
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
j : J
i : Subtype p
h : p j
h₁ : ↑i = j
h₂ : i = ⟨j, h⟩
⊢ eqToHom ⋯ = eqToHom ⋯

pp: case neg
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
j : J
i : Subtype p
h : p j
h₁ : ↑i = j
h₂ : ¬i = ⟨j, h⟩
⊢ eqToHom ⋯ = 0

pp: case pos
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
j : J
i : Subtype p
h : p j
h₁ : ¬↑i = j
h₂ : i = ⟨j, h⟩
⊢ 0 = eqToHom ⋯

pp: case neg
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
j : J
i : Subtype p
h : p j
h₁ : ¬↑i = j
h₂ : ¬i = ⟨j, h⟩
⊢ 0 = 0

Tactic:
exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

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

Goal state before:
pp: case pos
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
h₁ : ↑j✝ = ↑j
h₂ : j✝ = j
⊢ eqToHom ⋯ = eqToHom ⋯

pp: case neg
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
h₁ : ↑j✝ = ↑j
h₂ : ¬j✝ = j
⊢ eqToHom ⋯ = 0

pp: case pos
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
h₁ : ¬↑j✝ = ↑j
h₂ : j✝ = j
⊢ 0 = eqToHom ⋯

pp: case neg
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
h₁ : ¬↑j✝ = ↑j
h₂ : ¬j✝ = j
⊢ 0 = 0

Tactic:
exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

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

Goal state before:
pp: case pos
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
j : J
i : Subtype p
h : p j
h₁ : j = ↑i
h₂ : ⟨j, h⟩ = i
⊢ eqToHom ⋯ = eqToHom ⋯

pp: case neg
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
j : J
i : Subtype p
h : p j
h₁ : j = ↑i
h₂ : ¬⟨j, h⟩ = i
⊢ eqToHom ⋯ = 0

pp: case pos
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
j : J
i : Subtype p
h : p j
h₁ : ¬j = ↑i
h₂ : ⟨j, h⟩ = i
⊢ 0 = eqToHom ⋯

pp: case neg
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
j : J
i : Subtype p
h : p j
h₁ : ¬j = ↑i
h₂ : ¬⟨j, h⟩ = i
⊢ 0 = 0

Tactic:
exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

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

Goal state before:
pp: case pos
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
h₁ : ↑j = ↑j✝
h₂ : j = j✝
⊢ eqToHom ⋯ = eqToHom ⋯

pp: case neg
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
h₁ : ↑j = ↑j✝
h₂ : ¬j = j✝
⊢ eqToHom ⋯ = 0

pp: case pos
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
h₁ : ¬↑j = ↑j✝
h₂ : j = j✝
⊢ 0 = eqToHom ⋯

pp: case neg
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
h₁ : ¬↑j = ↑j✝
h₂ : ¬j = j✝
⊢ 0 = 0

Tactic:
exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J : Type
inst✝² : Fintype J
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
P : C
x : (j : J) → P ⟶ f j
m : (j : J) → (k : K) → f j ⟶ g k
⊢ lift x ≫ matrix m = lift fun k ↦ ∑ j, x j ≫ m j k

Tactic:
by
  ext
  simp [biproduct.lift_desc]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case cons
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i, x i = n
n : ℕ
⊢ (∃ a ∈ antidiagonal n, Fin.cons x₀ x ∈ map (fun x ↦ Fin.cons a.1 x) (antidiagonalTuple n✝ a.2)) ↔ x₀ + ∑ i, x i = n

Tactic:
List.mem_map,

Goal state after:
case cons
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i, x i = n
n : ℕ
⊢ (∃ a ∈ antidiagonal n, ∃ a_1 ∈ antidiagonalTuple n✝ a.2, Fin.cons a.1 a_1 = Fin.cons x₀ x) ↔ x₀ + ∑ i, x i = n
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
⊢ (↑(antidiagonal n)).PairwiseDisjoint fun p ↦
    map (addRightEmbedding fun j ↦ if j = i then p.1 else 0) (s.piAntidiag p.2)

Tactic:
rintro ⟨a, b⟩ hab ⟨c, d⟩ hcd

Goal state after:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a b : μ
hab : (a, b) ∈ ↑(antidiagonal n)
c d : μ
hcd : (c, d) ∈ ↑(antidiagonal n)
⊢ (a, b) ≠ (c, d) →
    (Disjoint on fun p ↦ map (addRightEmbedding fun j ↦ if j = i then p.1 else 0) (s.piAntidiag p.2)) (a, b) (c, d)
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: k n : ℕ
⊢ (∀ a ∈ antidiagonal n,
      Pairwise (fun a_2 b ↦ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun x x1 x2 ↦ x1 < x2) (Fin.cons a.1 a_2) (Fin.cons a.1 b))
        (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)

Tactic:
List.mem_map,

Goal state after:
k n : ℕ
⊢ (∀ a ∈ antidiagonal n,
      Pairwise (fun a_2 b ↦ Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun x x1 x2 ↦ x1 < x2) (Fin.cons a.1 a_2) (Fin.cons a.1 b))
        (antidiagonalTuple k a.2)) ∧
    Pairwise
      (fun a₁ a₂ ↦
        ∀ (x : Fin (k + 1) → ℕ),
          (∃ a ∈ antidiagonalTuple k a₁.2, Fin.cons a₁.1 a = x) →
            ∀ (y : Fin (k + 1) → ℕ),
              (∃ a ∈ antidiagonalTuple k a₂.2, Fin.cons a₂.1 a = y) →
                Pi.Lex (fun x1 x2 ↦ x1 < x2) (fun x x1 x2 ↦ x1 < x2) x y)
      (antidiagonal n)
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 μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
p : μ × μ
x✝¹ x✝ : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf : f ∈ s.finsuppAntidiag p.2
g : ι →₀ μ
hg : g ∈ s.finsuppAntidiag p.2
hfg : (fun f ↦ (↑f).update a p.1) ⟨f, hf⟩ = (fun f ↦ (↑f).update a p.1) ⟨g, hg⟩
⊢ ↑⟨f, hf⟩ = ↑⟨g, hg⟩

Tactic:
simp only [mem_finsuppAntidiag] at hf hg

Goal state after:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
p : μ × μ
x✝¹ x✝ : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf✝ : f ∈ s.finsuppAntidiag p.2
g : ι →₀ μ
hg✝ : g ∈ s.finsuppAntidiag p.2
hfg : (fun f ↦ (↑f).update a p.1) ⟨f, hf✝⟩ = (fun f ↦ (↑f).update a p.1) ⟨g, hg✝⟩
hf : s.sum ⇑f = p.2 ∧ f.support ⊆ s
hg : s.sum ⇑g = p.2 ∧ g.support ⊆ s
⊢ ↑⟨f, hf✝⟩ = ↑⟨g, hg✝⟩
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
⊢ σ * τ = 1 ↔ σ = 1 ∧ τ = 1

Tactic:
simp_rw [Perm.ext_iff, one_apply, hστ.mul_apply_eq_iff, forall_and]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ (∀ (a : α), ¬σ a ≠ a) ↔ σ = 1

Tactic:
not_not,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ (∀ (a : α), σ a = a) ↔ σ = 1
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case succ.nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
h : [].Nodup
hn : n + 1 + 1 < [].length
⊢ [].formPerm [][n + 1] = [][n + 1 + 1]

pp: case succ.cons.nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x : α
h : [x].Nodup
hn : n + 1 + 1 < [x].length
⊢ [x].formPerm [x][n + 1] = [x][n + 1 + 1]

pp: case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
⊢ (x :: y :: l).formPerm (x :: y :: l)[n + 1] = (x :: y :: l)[n + 1 + 1]

Tactic:
· simp at hn

Goal state after:
case succ.cons.nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x : α
h : [x].Nodup
hn : n + 1 + 1 < [x].length
⊢ [x].formPerm [x][n + 1] = [x][n + 1 + 1]

case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
⊢ (x :: y :: l).formPerm (x :: y :: l)[n + 1] = (x :: y :: l)[n + 1 + 1]
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
this : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
⊢ Equiv.refl α * f = f

Tactic:
← Perm.one_def,

Goal state after:
case neg.refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
this : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
⊢ 1 * f = f
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i]
hx₂ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[j]
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a l[i] * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a l[j] * g = x
hix : x a = l[i]
⊢ x a = l[j]

Tactic:
← hg.2,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i]
hx₂ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[j]
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a l[i] * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a l[j] * g = x
hix : x a = l[i]
⊢ (Equiv.swap a l[j] * g) a = l[j]
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inl.refine_2
α : 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⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxσ : σ x ≠ x
h : (g * τ * g⁻¹) (f x) = f x
⊢ τ x = (Equiv.symm f) (g (τ ((Equiv.symm g) (f x))))

pp: case intro.refine_2.inl.refine_1
α : 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⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxσ : σ x ≠ x
⊢ ¬(f * σ * f⁻¹) (f x) = f x

Tactic:
· rw [mul_apply, mul_apply, coe_inv] at h
        rw [h, symm_apply_apply, (hd1 x).resolve_left hxσ]

Goal state after:
case intro.refine_2.inl.refine_1
α : 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⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxσ : σ x ≠ x
⊢ ¬(f * σ * f⁻¹) (f x) = f x
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : 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
n : ℕ
ih : swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
⊢ swap ((σ * σ ^ n) x) ((σ * (σ * σ ^ n)) x) = swap (σ ((σ ^ n) x)) (σ ((σ * σ ^ n) x))

Tactic:
coe_mul,

Goal state after:
α : 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
n : ℕ
ih : swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
⊢ swap ((⇑σ ∘ ⇑(σ ^ n)) x) ((⇑σ ∘ ⇑σ ∘ ⇑(σ ^ n)) x) = swap (σ ((σ ^ n) x)) (σ ((⇑σ ∘ ⇑(σ ^ n)) x))
Module: Mathlib.Data.Nat.GCD.BigOperators

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

Tactic:
coprime_comm (n := k),

Goal state after:
k : ℕ
l : List ℕ
⊢ l.prod.Coprime k ↔ ∀ n ∈ l, n.Coprime k
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case pos
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
ha' : a = a'
⊢ a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, b)

Tactic:
rw [← ha'] at *

Goal state after:
case pos
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
ha' : a = a
⊢ a ∈ a :: l ∧ (prodExtendRight a (σ a)) (a, b) = (a, (σ a) b) ∨ a ∉ a :: l ∧ (prodExtendRight a (σ a)) (a, b) = (a, b)
Module: Mathlib.GroupTheory.NoncommPiCoprod

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

Tactic:
rw [Finset.noncommProd_insert_of_notMem _ _ _ _ (Finset.notMem_erase i _)]

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

Goal state before:
pp: case h
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ c.support
⊢ ↑((c.subtypePerm ⋯ ^ i) ⟨x, hx⟩) = g x

Tactic:
subtypePerm_apply_zpow_of_mem

Goal state after:
case h
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ c.support
⊢ (c ^ i) x = g x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
hx : f x = x
⊢ x = (f ^ n) x

Tactic:
pow_apply_eq_self_of_apply_eq_self hx

Goal state after:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
hx : f x = x
⊢ x = x
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i.cycleRange (i.succAbove j) = j.succ

Tactic:
Fin.succAbove_of_le_castSucc _ _ h,

Goal state after:
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i.cycleRange j.succ = j.succ
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
⊢ Trunc.lift (fun l ↦ { val := ↑↑l, nodup := ⋯ }) ⋯ σ.truncCycleFactors = l'.toFinset

Tactic:
← hl,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
⊢ Trunc.lift (fun l ↦ { val := ↑↑l, nodup := ⋯ }) ⋯ (Trunc.mk ⟨l', ⋯⟩) = l'.toFinset
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: G : Type u_2
inst✝ : Group G
⊢ vectorsProdEqOne G 1 = {1 ::ᵥ Vector.nil}

Tactic:
simp_rw [Set.eq_singleton_iff_unique_mem, mem_iff, List.Vector.toList_singleton,
    List.prod_singleton, List.Vector.head_cons, true_and]
  exact fun v hv => v.cons_head_tail.symm.trans (congr_arg₂ Vector.cons hv v.tail.eq_nil)

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

Goal state before:
pp: n : ℕ
i : Fin n
inst✝ : NeZero n
⊢ i.cycleIcc i = 1

Tactic:
ext k

Goal state after:
n : ℕ
i : Fin n
inst✝ : NeZero n
k : Fin n
⊢ ↑((i.cycleIcc i) k) = ↑(1 k)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g1 g2 : Perm α
h1 : g1 ∈ f.cycleFactorsFinset
h2 : g2 ∈ f.cycleFactorsFinset
h : g1 ≠ g2
⊢ Commute g1 g2

Tactic:
exact Equiv.Perm.cycleFactorsFinset_mem_commute f h1 h2 h

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

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ sign σ = ∏ j, ∏ i < j, if σ i < σ j then 1 else -1

Tactic:
by
  suffices h : σ.sign = σ.signAux by
    rw [h, Finset.prod_sigma', Equiv.Perm.signAux]
    convert! rfl using 2 with x hx
    · simp [Finset.ext_iff, Equiv.Perm.mem_finPairsLT]
    simp [← ite_not (p := _ ≤ _)]
  refine σ.swap_induction_on (by simp) fun π i j hne h_eq ↦ ?_
  rw [Equiv.Perm.signAux_mul, Equiv.Perm.sign_mul, h_eq, Equiv.Perm.sign_swap hne,
    Equiv.Perm.signAux_swap hne]

Goal state after: