mathlib-initiative/mathlib-tactics huggingface dataset:
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₁₁
inst✝ : IsIso (ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂
R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂
g : X₂ ⟶ Y₂
w : L.hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = biprod.map f₁₁ g
⊢ X₂ ≅ Y₂

Tactic:
letI : IsIso (biprod.map f₁₁ g) := by
    rw [← w]
    infer_instance

Goal state after:
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₁₁
inst✝ : IsIso (ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂
R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂
g : X₂ ⟶ Y₂
w : L.hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = biprod.map f₁₁ g
this : IsIso (biprod.map f₁₁ g) := isoElim'._proof_1 f₁₁ f₁₂ f₂₁ f₂₂ L R g w
⊢ X₂ ≅ Y₂
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
⊢ x = 𝟙 W

Tactic:
simp [x]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
c : Composition n
⊢ (↑c.blocks).sum = n

Tactic:
rw [Multiset.sum_coe, c.blocks_sum]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
l : Multiset ℕ
hl : l.sum = n
lz : (filter (fun x ↦ x = 0) l).sum = 0
⊢ (filter (fun x ↦ x ≠ 0) l).sum = n

Tactic:
← filter_add_not (· = 0) l,

Goal state after:
n : ℕ
l : Multiset ℕ
hl : (filter (fun x ↦ x = 0) l + filter (fun a ↦ ¬a = 0) l).sum = n
lz : (filter (fun x ↦ x = 0) l).sum = 0
⊢ (filter (fun x ↦ x ≠ 0) l).sum = n
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c.length ≤ n

Tactic:
by
  conv_rhs => rw [← c.blocks_sum]
  exact length_le_sum_of_one_le _ fun i hi => c.one_le_blocks hi

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

Goal state before:
pp: case mp
n : ℕ
c : Composition n
⊢ c.blocks = [] → n = 0

Tactic:
intro h

Goal state after:
case mp
n : ℕ
c : Composition n
h : c.blocks = []
⊢ n = 0
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
p q : n.Partition
h :
  (fun p ↦ { support := p.parts.toFinset, toFun := fun m ↦ count m p.parts * m, mem_support_toFun := ⋯ }) p =
    (fun p ↦ { support := p.parts.toFinset, toFun := fun m ↦ count m p.parts * m, mem_support_toFun := ⋯ }) q
⊢ p = q

Tactic:
rw [Finsupp.mk.injEq] at h

Goal state after:
n : ℕ
p q : n.Partition
h : p.parts.toFinset = q.parts.toFinset ∧ (fun m ↦ count m p.parts * m) = fun m ↦ count m q.parts * m
⊢ p = q
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : (fun m ↦ count m p.parts * m) = fun m ↦ count m q.parts * m
m : ℕ
⊢ count m p.parts = count m q.parts

Tactic:
obtain rfl | h0 := Nat.eq_zero_or_pos m

Goal state after:
case inl
n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : (fun m ↦ count m p.parts * m) = fun m ↦ count m q.parts * m
⊢ count 0 p.parts = count 0 q.parts

case inr
n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : (fun m ↦ count m p.parts * m) = fun m ↦ count m q.parts * m
m : ℕ
h0 : m > 0
⊢ count m p.parts = count m q.parts
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ j ∈ Set.range ⇑(c.embedding i) → c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ

Tactic:
intro h

Goal state after:
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : j ∈ Set.range ⇑(c.embedding i)
⊢ c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ → j ∈ Set.range ⇑(c.embedding i)

Tactic:
intro h

Goal state after:
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
⊢ j ∈ Set.range ⇑(c.embedding i)
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
σ τ : Type
inst✝³ : Finite τ
S : σ → C
inst✝² : HasBiproduct S
T : τ → C
inst✝¹ : HasBiproduct T
s : σ
f : ⨁ S ⟶ ⨁ T
inst✝ : IsIso f
val✝ : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
⊢ x = 𝟙 (S s)

Tactic:
simp [x]

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

Goal state before:
pp: case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ ¬i = c.index j → j ∉ Set.range ⇑(c.embedding i)

Tactic:
intro h

Goal state after:
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : ¬i = c.index j
⊢ j ∉ Set.range ⇑(c.embedding i)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ i = c.index j → j ∈ Set.range ⇑(c.embedding i)

Tactic:
intro h

Goal state after:
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : i = c.index j
⊢ j ∈ Set.range ⇑(c.embedding i)
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type u_1
inst✝³ : Finite J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Mono (F.biproductComparison f)
this✝ : HasProduct fun b ↦ F.obj (f b)
that :
  piComparison F f =
    (F.mapIso (biproduct.isoProduct f)).inv ≫ F.biproductComparison f ≫ (biproduct.isoProduct (F.obj ∘ f)).hom
this : IsIso (F.biproductComparison f)
⊢ IsIso (piComparison F f)

Tactic:
that

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type u_1
inst✝³ : Finite J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Mono (F.biproductComparison f)
this✝ : HasProduct fun b ↦ F.obj (f b)
that :
  piComparison F f =
    (F.mapIso (biproduct.isoProduct f)).inv ≫ F.biproductComparison f ≫ (biproduct.isoProduct (F.obj ∘ f)).hom
this : IsIso (F.biproductComparison f)
⊢ IsIso ((F.mapIso (biproduct.isoProduct f)).inv ≫ F.biproductComparison f ≫ (biproduct.isoProduct (F.obj ∘ f)).hom)
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Mono (F.biprodComparison X Y)
that :
  prodComparison F X Y =
    (F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom
this : IsIso (F.biprodComparison X Y)
⊢ IsIso (prodComparison F X Y)

Tactic:
that

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Preadditive C
D : Type u'
inst✝⁵ : Category.{v', u'} D
inst✝⁴ : Preadditive D
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Mono (F.biprodComparison X Y)
that :
  prodComparison F X Y =
    (F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom
this : IsIso (F.biprodComparison X Y)
⊢ IsIso ((F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ⊆ s
x : α
⊢ c x ∈ s ↔ x ∈ s

Tactic:
by_cases hx' : x ∈ c.support

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ⊆ s
x : α
hx' : x ∈ c.support
⊢ c x ∈ s ↔ x ∈ s

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ⊆ s
x : α
hx' : x ∉ c.support
⊢ c x ∈ s ↔ x ∈ s
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
⊢ (∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x) →
    c.support ⊆ s ∧ ((∀ (x : α), c x ∈ s ↔ x ∈ s) → ∀ a ∈ s, c a = g a)

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
⊢ c.support ⊆ s ∧ ((∀ (x : α), c x ∈ s ↔ x ∈ s) → ∀ a ∈ s, c a = g a)
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 : Fintype.card { x // x ∈ s \ t } = Fintype.card { x // x ∈ t \ s }
⊢ ↑(s \ t) ≃ ↑(t \ s)

Tactic:
exact ((Fintype.card_eq (_F := (_)) (_G := (_))).mp hc).some

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

Goal state before:
pp: case succ.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
x : α
hx : x ∈ f.support ∩ g.support
⊢ g x ∈ f.support ∧ g x ∈ g.support

Tactic:
apply_mem_support,

Goal state after:
case succ.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
x : α
hx : x ∈ f.support ∩ g.support
⊢ g x ∈ f.support ∧ x ∈ g.support
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case succ.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
x : α
hx : x ∈ f.support ∩ g.support
⊢ f x ∈ f.support ∧ x ∈ g.support

Tactic:
apply_mem_support,

Goal state after:
case succ.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, (f ^ k) x = (g ^ k) x
x : α
hx : x ∈ f.support ∩ g.support
⊢ x ∈ f.support ∧ x ∈ g.support
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mp
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl) → Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr)

Tactic:
intro h

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

Goal state before:
pp: case mpr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr) → Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)

Tactic:
intro h

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

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

Tactic:
· rw [getElem_cons_zero, formPerm_apply_head _ _ _ h, getElem_cons_succ, getElem_cons_zero]

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

Goal state before:
pp: case pos.refine_1
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : p b
⊢ σ (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩ → (σ.extendDomain f) b = b

Tactic:
intro h

Goal state after:
case pos.refine_1
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h✝ : σ.Disjoint τ
b : β
pb : p b
h : σ (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩
⊢ (σ.extendDomain f) b = b
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case pos.refine_2
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : p b
⊢ τ (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩ → (τ.extendDomain f) b = b

Tactic:
intro h

Goal state after:
case pos.refine_2
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h✝ : σ.Disjoint τ
b : β
pb : p b
h : τ (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩
⊢ (τ.extendDomain f) b = b
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ #f.support = 2 → f.IsSwap

Tactic:
intro h

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
⊢ f.IsSwap
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ f.IsSwap → #f.support = 2

Tactic:
intro h

Goal state after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.IsSwap
⊢ #f.support = 2
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case refine_2
α : 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
⊢ ∀ x ∈ l, (List.map (fun f ↦ Equiv.swap a x * f) (permsOfList l)).Nodup

pp: case refine_3
α : 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),
    i < j → (List.Disjoint on fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i] l[j]

pp: case refine_4
α : 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
⊢ (permsOfList l).Disjoint (flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l)

Tactic:
· exact fun _ _ => hln'.map fun _ _ => mul_left_cancel

Goal state after:
case refine_3
α : 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),
    i < j → (List.Disjoint on fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i] l[j]

case refine_4
α : 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
⊢ (permsOfList l).Disjoint (flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l)
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u : ℤˣ
⊢ ↑u * ↑u = 1

Tactic:
by
  rw [← Units.val_mul, units_mul_self, Units.val_one]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∉ l.rotate 1
⊢ (l.rotate 1).formPerm x = l.formPerm x

Tactic:
rw [formPerm_apply_of_notMem hx, formPerm_apply_of_notMem]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∉ l.rotate 1
⊢ x ∉ l
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ []
x : α
⊢ [].prod x = f x

Tactic:
List.prod_nil

Goal state after:
α : Type u
inst✝ : DecidableEq α
β : Type v
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ []
x : α
⊢ 1 x = f x
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inl.ha
α : 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
⊢ σ x ∈ σ.support

Tactic:
apply_mem_support,

Goal state after:
case intro.refine_2.inl.ha
α : 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
⊢ x ∈ σ.support
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm hd = hd → (hd :: tl).formPerm = 1

Tactic:
intro h

Goal state after:
case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
h : (hd :: tl).formPerm hd = hd
⊢ (hd :: tl).formPerm = 1
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

Goal state after:
case mp
α : Type u_2
inst✝ : DecidableEq α
a b : α
h : (swap a b).IsSwap
⊢ a ≠ b
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

Tactic:
intro h

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
n : ℕ
hn : 2 ≤ n
⊢ 0 < 2

Tactic:
by decide

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
n : ℕ
hn : 2 ≤ n
⊢ 1 < 2

Tactic:
by decide

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

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

Tactic:
mul_def,

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(((e.symm.trans (Equiv.trans f (swap x (f x)))).trans e) x✝) =
    ↑(((e.symm.trans (swap x (f x))).trans e * (e.symm.trans f).trans e) x✝)
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
⊢ signAux ((e.symm.trans f).trans e) = if x = f x then signAux2 l f else -signAux2 l (swap x (f x) * f)

Tactic:
have hy : ∀ y : α, (swap x (f x) * f) y ≠ y → y ∈ l := fun y hy =>
        have : f y ≠ y ∧ y ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hy
        List.mem_of_ne_of_mem this.2 (h _ this.1)
      have : (e.symm.trans (swap x (f x) * f)).trans e =
          swap (e x) (e (f x)) * (e.symm.trans f).trans e := by
        ext
        rw [← Equiv.symm_trans_swap_trans, mul_def, Equiv.symm_trans_swap_trans, mul_def]
        repeat (rw [trans_apply])
        simp [swap, swapCore]
        split_ifs <;> rfl
      have hefx : e x ≠ e (f x) := mt e.injective.eq_iff.1 hfx
      rw [if_neg hfx, ← signAux_eq_signAux2 _ _ e hy, this, signAux_mul, signAux_swap hefx]
      simp only [neg_neg, one_mul, neg_mul]

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

Goal state before:
pp: case mp
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
⊢ (f ^ n).support = f.support → ¬f ^ n = 1

Tactic:
intro h

Goal state after:
case mp
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
h : (f ^ n).support = f.support
⊢ ¬f ^ n = 1
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), e (f x) = g (e x)
hg : g = (e.symm.trans f).trans e
⊢ sign f = sign ((e.symm.trans f).trans e)

Tactic:
sign_symm_trans_trans

Goal state after:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), e (f x) = g (e x)
hg : g = (e.symm.trans f).trans e
⊢ sign f = sign f
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).IsCycle → n.Coprime (orderOf f)

Tactic:
intro h

Goal state after:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
⊢ n.Coprime (orderOf f)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
⊢ n.Coprime (orderOf f) → (f ^ n).IsCycle

Tactic:
intro h

Goal state after:
case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : n.Coprime (orderOf f)
⊢ (f ^ n).IsCycle
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

Goal state after:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : f ^ n = 1
⊢ ∃ x, f x ≠ x ∧ (f ^ n) x = x
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

Goal state after:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
h : f ^ a = f ^ b
⊢ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
f : ι → G
comm : (↑s).Pairwise (Function.onFun Commute f)
K : ι → Subgroup G
hind : iSupIndep K
hmem : ∀ x ∈ s, f x ∈ K x
heq1 : s.noncommProd f comm = 1
⊢ ∀ i ∈ s, f i = 1

Tactic:
revert heq1

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
f : ι → G
comm : (↑s).Pairwise (Function.onFun Commute f)
K : ι → Subgroup G
hind : iSupIndep K
hmem : ∀ x ∈ s, f x ∈ K x
⊢ s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1