mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Category.Preorder

Goal state before:
pp: X : Type u
inst✝ : Preorder X
x y : X
h : x = y
⊢ IsIso (homOfLE ⋯)

Tactic:
by
  subst h
  change IsIso (𝟙 _)
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ uliftYonedaEquiv (uliftYoneda.{w, v₁, u₁}.map f) = { down := f }

Tactic:
simp [uliftYonedaEquiv, uliftYoneda]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : Cᵒᵖ) (p : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ P), p ≫ f = p ≫ g
X : C
x : P.obj X
⊢ (ConcreteCategory.hom (f.app X)).toFun x = (ConcreteCategory.hom (g.app X)).toFun x

Tactic:
simpa [uliftCoyonedaEquiv]
    using congr_arg uliftCoyonedaEquiv.{w} (h _ (uliftCoyonedaEquiv.symm x))

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Fan fun j ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan fun i ↦ (c i).pt
hc' : IsLimit c'
⊢ IsLimit (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2)

Tactic:
by
  refine Fan.IsLimit.mk _ (fun t ↦ ?_) ?_ fun t m hm ↦ ?_
  · exact Fan.IsLimit.lift hc' fun i ↦ Fan.IsLimit.lift (hc i) fun j ↦ t.proj (i, j)
  · simp
  · refine Fan.IsLimit.hom_ext hc' _ _ fun i ↦ ?_
    exact Fan.IsLimit.hom_ext (hc i) _ _ fun j ↦ (by simpa using hm (i, j))

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

Goal state before:
pp: case refine_1
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan fun j ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan fun i ↦ (c i).pt
hc' : IsColimit c'
t : Cofan fun p ↦ X p.1 p.2
⊢ (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).pt ⟶ t.pt

pp: case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan fun j ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan fun i ↦ (c i).pt
hc' : IsColimit c'
⊢ ∀ (t : Cofan fun p ↦ X p.1 p.2) (j : ι × ι'),
    (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).inj j ≫ ?refine_1 = t.inj j

pp: case refine_3
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan fun j ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan fun i ↦ (c i).pt
hc' : IsColimit c'
t : Cofan fun p ↦ X p.1 p.2
m : (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).pt ⟶ t.pt
hm : ∀ (j : ι × ι'), (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).inj j ≫ m = t.inj j
⊢ m = ?refine_1

Tactic:
· exact Cofan.IsColimit.desc hc' fun i ↦ Cofan.IsColimit.desc (hc i) fun j ↦ t.inj (i, j)

Goal state after:
case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan fun j ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan fun i ↦ (c i).pt
hc' : IsColimit c'
⊢ ∀ (t : Cofan fun p ↦ X p.1 p.2) (j : ι × ι'),
    ((Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).inj j ≫ desc hc' fun i ↦ desc (hc i) fun j ↦ t.inj (i, j)) =
      t.inj j

case refine_3
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan fun j ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan fun i ↦ (c i).pt
hc' : IsColimit c'
t : Cofan fun p ↦ X p.1 p.2
m : (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).pt ⟶ t.pt
hm : ∀ (j : ι × ι'), (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).inj j ≫ m = t.inj j
⊢ m = desc hc' fun i ↦ desc (hc i) fun j ↦ t.inj (i, j)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹¹ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝¹⁰ : Category.{w, u₂} D
E : Type u₃
inst✝⁹ : Category.{w', u₃} E
F : C ⥤ D
G : D ⥤ E
A✝ A' B B' : C
inst✝⁸ : HasBinaryProduct A✝ B
inst✝⁷ : HasBinaryProduct A' B'
inst✝⁶ : HasBinaryProduct (F.obj A✝) (F.obj B)
inst✝⁵ : HasBinaryProduct (F.obj A') (F.obj B')
inst✝⁴ : HasBinaryProduct (G.obj (F.obj A✝)) (G.obj (F.obj B))
inst✝³ : HasBinaryProduct ((F ⋙ G).obj A✝) ((F ⋙ G).obj B)
inst✝² : HasBinaryProducts C
inst✝¹ : HasBinaryProducts D
A : C
inst✝ : ∀ (B : C), IsIso (prodComparison F A B)
⊢ prod.functor.obj A ⋙ F ≅ F ⋙ prod.functor.obj (F.obj A)

Tactic:
by
  refine { @asIso _ _ _ _ _ (?_) with hom := prodComparisonNatTrans F A }
  apply NatIso.isIso_of_isIso_app

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
F : C ⥤ D
d : D
⊢ ∀ {X Y : (StructuredArrow d F)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (StructuredArrow d F)ᵒᵖ).map f ≫ (StructuredArrow.isoMk (Iso.refl (unop Y).right) ⋯).op.hom =
      (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op.hom ≫
        (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f

Tactic:
by
      rintro ⟨X⟩ ⟨Y⟩ f
      obtain ⟨X, x, rfl⟩ := X.mk_surjective
      obtain ⟨Y, y, rfl⟩ := Y.mk_surjective
      exact Quiver.Hom.unop_inj (by ext; apply Quiver.Hom.op_inj (by simp))

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageMonoIsoSource f).inv ≫ image.ι f = f

Tactic:
by
  simp [imageMonoIsoSource]

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
F : C ⥤ D
d : D
⊢ ∀ {X Y : (CostructuredArrow F d)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (CostructuredArrow F d)ᵒᵖ).map f ≫ (CostructuredArrow.isoMk (Iso.refl (unop Y).left) ⋯).op.hom =
      (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op.hom ≫
        (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f

Tactic:
by
      rintro ⟨X⟩ ⟨Y⟩ f
      obtain ⟨X, x, rfl⟩ := X.mk_surjective
      obtain ⟨Y, y, rfl⟩ := Y.mk_surjective
      exact Quiver.Hom.unop_inj (by ext; apply Quiver.Hom.op_inj (by simp))

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

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s : Fork f g
⊢ s.π.app zero ≫ (parallelPair f g).map right = s.π.app zero ≫ g

Tactic:
parallelPair_map_right

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s : Fork f g
⊢ s.π.app zero ≫ g = s.π.app zero ≫ g
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s : Cofork f g
⊢ (parallelPair f g).map right ≫ s.ι.app one = g ≫ s.ι.app one

Tactic:
parallelPair_map_right

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s : Cofork f g
⊢ g ≫ s.ι.app one = g ≫ s.ι.app 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✝¹ : HasInitial C
inst✝ : HasInitial D
i : IsIso (initialComparison G)
⊢ IsInitial (G.obj (⊥_ C))

Tactic:
exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (Functor.empty.{0} D)) i

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

Goal state before:
pp: C : Type u
X Y : C
inst✝² : Category.{v, u} C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
X' Y' Z : C
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : X ⟶ X'
q : Y ⟶ Y'
wf : f ≫ q = p ≫ f'
wg : g ≫ q = p ≫ g'
h : Y' ⟶ Z
wh : f' ≫ h = g' ≫ h
⊢ q ≫ colimit.ι (parallelPair f' g') one ≫ desc h wh = q ≫ h

Tactic:
coequalizer.π_desc

Goal state after:
C : Type u
X Y : C
inst✝² : Category.{v, u} C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
X' Y' Z : C
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : X ⟶ X'
q : Y ⟶ Y'
wf : f ≫ q = p ≫ f'
wg : g ≫ q = p ≫ g'
h : Y' ⟶ Z
wh : f' ≫ h = g' ≫ h
⊢ q ≫ h = q ≫ h
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
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ F.map (lift f g) ≫ (F.mapBiprod X Y).hom = lift (F.map f) (F.map g)

Tactic:
by
  ext <;> simp [mapBiprod, ← F.map_comp]

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
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ (F.mapBiprod X Y).inv ≫ F.map (desc f g) = desc (F.map f) (F.map g)

Tactic:
by
  ext <;> simp [mapBiprod, ← F.map_comp]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
⊢ f ≫ cokernel.π (image.ι f) = 0

Tactic:
by
        conv =>
          lhs
          congr
          rw [← image.fac f]
        rw [Category.assoc, cokernel.condition, HasZeroMorphisms.comp_zero]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasCokernels C
f g : Arrow C
u : f ⟶ g
⊢ f.hom ≫ Arrow.Hom.right u ≫ cokernel.π g.hom = 0

Tactic:
by simp [← Arrow.w_assoc u]

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
f : X ⟶ Y
inst✝ : IsSplitEpi f
c : KernelFork f
i : IsLimit c
⊢ (Fork.ι c ≫
      let c' := KernelFork.ofι (Fork.ι c) ⋯;
      let i' := isKernelCompMono i (section_ f) ⋯;
      let i'' := isLimitForkOfKernelFork i';
      (splitMonoOfIdempotentOfIsLimitFork C ⋯ i'').retraction) =
    𝟙 c.pt

Tactic:
apply SplitMono.id

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

Goal state before:
pp: n : ℕ
⊢ flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple 1 ni.2)) (antidiagonal n) =
    map (fun i ↦ ![i.1, i.2]) (antidiagonal n)

Tactic:
antidiagonalTuple_one,

Goal state after:
n : ℕ
⊢ flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) [![ni.2]]) (antidiagonal n) =
    map (fun i ↦ ![i.1, i.2]) (antidiagonal n)
Module: Mathlib.GroupTheory.Perm.Basic

Goal state before:
pp: α : Type u_1
f : Perm α
s : Set α
⊢ MapsTo (⇑f) s s → ∀ (n : ℕ), MapsTo (⇑(f ^ n)) s s

Tactic:
by
  simp_rw [Equiv.Perm.coe_pow]; exact MapsTo.iterate

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

Goal state before:
pp: α : Type u_1
f : Perm α
n : ℕ
x : α
⊢ (f ^ n) (f x) = (f ^ n) x ↔ f x = x

Tactic:
apply_eq_iff_eq

Goal state after:
α : Type u_1
f : Perm α
n : ℕ
x : α
⊢ f x = x ↔ f x = x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f : Perm α
n : ℤ
x : α
⊢ (f ^ n) (f x) = (f ^ n) x ↔ f x = x

Tactic:
apply_eq_iff_eq

Goal state after:
α : Type u_1
f : Perm α
n : ℤ
x : α
⊢ f x = x ↔ f x = x
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := (mapRange.addEquiv e).toEquiv
hh : h = (mapRange.addEquiv e).toEquiv
hf : f ∈ s.finsuppAntidiag (e n)
this : n = e.symm (e n)
⊢ map ((mapRange.addEquiv e.symm).toEmbedding.trans (mapRange.addEquiv e).toEmbedding) (s.finsuppAntidiag (e n)) =
    s.finsuppAntidiag (e n)

Tactic:
convert! map_refl

Goal state after:
case e'_2.e'_3
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := (mapRange.addEquiv e).toEquiv
hh : h = (mapRange.addEquiv e).toEquiv
hf : f ∈ s.finsuppAntidiag (e n)
this : n = e.symm (e n)
⊢ (mapRange.addEquiv e.symm).toEmbedding.trans (mapRange.addEquiv e).toEmbedding = Embedding.refl (ι →₀ μ')
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
apply_eq_iff_eq

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ ¬f x = x ↔ ¬f x = x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
hn : 0 < n
⊢ ∃ i, n ≤ (single n hn).blocksFun i

Tactic:
exact ⟨⟨0, by simp⟩, by simp⟩

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
a : α
⊢ (e.viaFintypeEmbedding f) (f a) = f (e a)

Tactic:
rw [Equiv.Perm.viaFintypeEmbedding]
  convert! Equiv.Perm.extendDomain_apply_image e (Function.Embedding.toEquivRange f) a

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

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = ↑j
⊢ ↑(c.boundary ⟨i, hi⟩) = ↑j

Tactic:
← c.blocks_partial_sum hi

Goal state after:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = ↑j
⊢ (take i c.blocks).sum = ↑j
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x✝ : [].Nodup
⊢ (permsOfList []).Nodup

Tactic:
by simp [permsOfList]

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

Goal state before:
pp: α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
⊢ (σ.extendDomain f).Disjoint (τ.extendDomain f)

Tactic:
intro b
  by_cases pb : p b
  · refine (h (f.symm ⟨b, pb⟩)).imp ?_ ?_ <;>
      · intro h
        rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]
  · left
    rw [extendDomain_apply_not_subtype _ _ pb]

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

Goal state before:
pp: case cons.inr.e_i
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ i + 1 = (i + 1) % (x :: xs).length

Tactic:
rw [Nat.mod_eq_of_lt]

Goal state after:
case cons.inr.e_i
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ i + 1 < (x :: xs).length
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
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 (σ x) = f x

Tactic:
apply_eq_iff_eq

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
⊢ ¬σ x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
n : ℕ
⊢ f.SameCycle ((f ^ ↑n) x) y ↔ f.SameCycle x y

Tactic:
sameCycle_zpow_left

Goal state after:
α : Type u_2
f : Perm α
x y : α
n : ℕ
⊢ f.SameCycle x y ↔ f.SameCycle x y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
n : ℤ
⊢ (g.extendDomain f ^ n) ↑(f x) = ↑(f y) ↔ (g ^ n) x = y

Tactic:
← extendDomain_zpow,

Goal state after:
α : Type u_2
β : Type u_3
g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
n : ℤ
⊢ ((g ^ n).extendDomain f) ↑(f x) = ↑(f y) ↔ (g ^ n) x = y
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

Tactic:
rcases n with (_ | _ | n)
  · norm_num at hn
  · norm_num at hn
  · exact signAux_swap_zero_one' n

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

Goal state before:
pp: case intro.refine_2.inr.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
⊢ ¬g (τ (τ x)) = g (τ x)

Tactic:
apply_eq_iff_eq

Goal state after:
case intro.refine_2.inr.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
⊢ ¬τ (τ x) = τ x
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case succ
α : 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 + 1)) x) ((σ ^ (n + 1 + 1)) x) ∈ H

Tactic:
| succ n ih =>

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

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

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: case succ
α : Type u_1
f : α → α
n✝ n : ℕ
ih : ∀ (a : α), iterate f a (n + n✝) = iterate f a n ++ iterate f (f^[n] a) n✝
a : α
⊢ iterate f a (n + 1 + n✝) = iterate f a (n + 1) ++ iterate f (f^[n + 1] a) n✝

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case a
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)
this : DecidableEq ι := Classical.decEq ι
i : ι
y : N i
⊢ (ϕ i) y ∈ mrange (noncommPiCoprod ϕ hcomm)

Tactic:
exact ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case a
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := ⋯
⊢ (noncommPiCoprod ϕ hcomm).range ≤ ⨆ i, (ϕ i).range

pp: case a
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := ⋯
⊢ ⨆ i, (ϕ i).range ≤ (noncommPiCoprod ϕ hcomm).range

Tactic:
· rintro x ⟨f, rfl⟩
    refine Subgroup.noncommProd_mem _ (fun _ _ _ _ h => hcomm h _ _) ?_
    intro i _hi
    apply Subgroup.mem_sSup_of_mem
    · use i
    simp

Goal state after:
case a
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := ⋯
⊢ ⨆ i, (ϕ i).range ≤ (noncommPiCoprod ϕ hcomm).range
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case a
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := Classical.decEq ι
i : ι
y : H i
⊢ (ϕ i) y ∈ (noncommPiCoprod ϕ hcomm).range

Tactic:
exact ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩

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

Goal state before:
pp: case e_s
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s).Pairwise Disjoint), s.noncommProd id ⋯ = σ

Tactic:
exact ⟨h1, h2, h0⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
⊢ n ∣ orderOf σ

Tactic:
rw [← lcm_cycleType]
  exact dvd_lcm h

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

Goal state before:
pp: case succ.succ
n : ℕ
ih : sign (finRotate (n + 1)) = (-1) ^ (n + 1 - 1)
⊢ sign (finRotate (n + 1 + 1)) = (-1) ^ (n + 1 + 1 - 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
⊢ ∀ {x_1 : α}, ((f.cycleOf x)⁻¹ * g) x_1 ≠ x_1 → f.cycleOf x_1 = ((f.cycleOf x)⁻¹ * g).cycleOf x_1

Tactic:
by
            rw [hfg hx]
            intro y hy
            simp [symm_apply_eq, cycleOf_apply, eq_comm (a := g y)] at hy
            rw [hfg (Ne.symm hy.right), ← mul_inv_eq_one (a := g.cycleOf y), cycleOf_inv]
            simp_rw [mul_inv_rev]
            rw [inv_inv, cycleOf_mul_of_apply_right_eq_self, ← cycleOf_inv, mul_inv_eq_one]
            · rw [Commute.inv_left_iff, commute_iff_eq]
              ext z; by_cases hz : SameCycle g x z
              · simp [cycleOf_apply, hz]
              · simp [cycleOf_apply_of_not_sameCycle, hz]
            · exact cycleOf_apply_of_not_sameCycle hy.left

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

Goal state before:
pp: case succ.inr.inr
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Tactic:
rw [Fin.cycleRange_of_gt hgt, Fin.succAbove_of_le_castSucc, swap_apply_of_ne_of_ne]

Goal state after:
case succ.inr.inr.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ j.succ ≠ 0

case succ.inr.inr.a
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ j.succ ≠ i.succ

case succ.inr.inr.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hgt : i < j
⊢ i.succ ≤ j.castSucc