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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Small.{w, u} C
inst✝³ : LocallySmall.{w, v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Small.{w, u'} D
inst✝ : LocallySmall.{w, v', u'} D
F G : C ⥤ D
h : (fun F f ↦ Arrow.mk (F.map f.hom)) F = (fun F f ↦ Arrow.mk (F.map f.hom)) G
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
· have : Arrow.mk (F.map f) = Arrow.mk (G.map f) := congr_fun h (Arrow.mk f)
    rw [Arrow.mk_eq_mk_iff] at this
    tauto

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
⊢ Function.RightInverse (fun u ↦ { lift := fun s ↦ default, fac := ⋯, uniq := ⋯ }) fun t X ↦
    {
      default :=
        t.lift { pt := X, π := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } },
      uniq := ⋯ }

Tactic:
dsimp [Function.RightInverse, Function.LeftInverse]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
⊢ ∀ (x : (X : C) → Unique (X ⟶ Y)), (fun X ↦ { default := default, uniq := ⋯ }) = x
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
k : K
⊢ ι (E ⋙ F) k ≫ pre F E = ι F (E.obj k)

Tactic:
by
  simp [colimit.pre]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
⊢ post (E ⋙ F) G ≫ G.map (pre F E) = pre (F ⋙ G) E ≫ post F G

Tactic:
ext j
  rw [← assoc, colimit.ι_post, ← G.map_comp, colimit.ι_pre, ← assoc]
  have : HasColimit (E ⋙ F ⋙ G) := h
  erw [colimit.ι_pre (F ⋙ G) E j, colimit.ι_post]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPushout f₁ g₁
inst✝ : HasPushout f₂ g₂
⊢ (congrHom h₁ h₂).inv = map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯

Tactic:
ext <;> simp [Iso.comp_inv_eq]

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

Goal state before:
pp: case h₀
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u_1
inst✝⁴ : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst✝³ : HasPullback f g
inst✝² : HasPullback (F.map f) (F.map g)
inst✝¹ : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst✝ : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
⊢ pullbackComparison (F ⋙ G) f g ≫ pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g) =
    (G.map (pullbackComparison F f g) ≫ pullbackComparison G (F.map f) (F.map g)) ≫
      pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)

Tactic:
pullbackComparison_comp_fst

Goal state after:
case h₀
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u_1
inst✝⁴ : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst✝³ : HasPullback f g
inst✝² : HasPullback (F.map f) (F.map g)
inst✝¹ : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst✝ : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
⊢ (F ⋙ G).map (pullback.fst f g) =
    (G.map (pullbackComparison F f g) ≫ pullbackComparison G (F.map f) (F.map g)) ≫
      pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
⊢ { app := fun j ↦ data.mapZ (Arrow.homMk ((Arrow.Hom.left (𝟙 f)).app j) ((Arrow.Hom.right (𝟙 f)).app j) ⋯),
      naturality := ⋯ } =
    𝟙
      { obj := fun j ↦ (data.factorizationData (f.hom.app j)).Z,
        map := fun {X Y} φ ↦ data.mapZ (Arrow.homMk (f.left.map φ) (f.right.map φ) ⋯), map_id := ⋯, map_comp := ⋯ }

Tactic:
by
    ext j
    dsimp
    rw [← data.mapZ_id]
    congr 1

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).hom ≫ (imageMonoIsoSource f).inv) ≫ image.ι f = image.ι f

Tactic:
Iso.hom_inv_id,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ 𝟙 (image f) ≫ image.ι f = image.ι f
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasImages C
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
A B : C
h : A ⟶ B
h_mono : Mono h
x : X✝ ⟶ A
y : image f ⟶ B
sq : CommSq x (factorThruImage f) h y
⊢ factorThruImage f ≫
      image.lift
          { I := pullback h y, m := pullback.snd h y ≫ image.ι f, m_mono := ⋯,
            e := pullback.lift x (factorThruImage f) ⋯, fac := ⋯ } ≫
        pullback.fst h y =
    x

Tactic:
simp only [image.fac_lift_assoc, pullback.lift_fst]

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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
⊢ G.map (equalizer.ι f g ≫ f) = G.map (equalizer.ι f g ≫ g)

Tactic:
rw [equalizer.condition]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 ≫ F.map 0 = F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0

Tactic:
Iso.hom_inv_id,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 ≫ F.map 0 = F.map 0 ≫ 𝟙 (F.obj 0) ≫ F.map 0
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
X Y : C
e : X ≅ Y
hY : ∃ a, P a Y
⊢ ∃ a, (P a).isoClosure X

Tactic:
obtain ⟨a, hY⟩ := hY

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
X Y : C
e : X ≅ Y
a : α
hY : P a Y
⊢ ∃ a, (P a).isoClosure X
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this : m₁.toMulOneClass = m₂.toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ m₁ = m₂

Tactic:
have : m₁.npow = m₂.npow := by
    ext n x
    exact @MonoidHom.map_pow M M m₁ m₂ f x n

Goal state after:
M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this✝ : m₁.toMulOneClass = m₂.toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this : NPow.npow = NPow.npow
⊢ m₁ = m₂
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 ≫ (F.mapBiprod X Y).inv = F.map (lift f g)

Tactic:
Iso.hom_inv_id,

Goal state after:
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.obj (X ⊞ Y)) = F.map (lift f g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsLimit t.toCone
j : J
j' : Discrete J
⊢ t.ι j ≫ t.toCone.π.app j' = ht.lift (Fan.mk (f j) fun j' ↦ if h : j = j' then eqToHom ⋯ else 0) ≫ t.toCone.π.app j'

Tactic:
rw [ht.fac]

Goal state after:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsLimit t.toCone
j : J
j' : Discrete J
⊢ t.ι j ≫ t.toCone.π.app j' = (Fan.mk (f j) fun j' ↦ if h : j = j' then eqToHom ⋯ else 0).π.app j'
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
j : J
j' : Discrete J
⊢ t.toCocone.ι.app j' ≫ t.π j =
    t.toCocone.ι.app j' ≫ ht.desc (Cofan.mk (f j) fun j' ↦ if h : j' = j then eqToHom ⋯ else 0)

Tactic:
rw [ht.fac]

Goal state after:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
j : J
j' : Discrete J
⊢ t.toCocone.ι.app j' ≫ t.π j = (Cofan.mk (f j) fun j' ↦ if h : j' = j then eqToHom ⋯ else 0).ι.app j'
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : ⨁ f ⟶ ⨁ g
⊢ (matrix fun j k ↦ components m j k) = m

Tactic:
by
  ext
  simp [biproduct.components]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst✝¹ : IsIso f₁₁
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₂

Tactic:
letI : IsIso g := isIso_right_of_isIso_biprod_map f₁₁ g

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
this : IsIso g := isIso_right_of_isIso_biprod_map f₁₁ g
⊢ X₂ ≅ Y₂
Module: Mathlib.Combinatorics.Enumerative.Composition

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

Tactic:
· intro H
    ext1
    have A : c.blocks.length = 1 := H ▸ c.blocks_length
    have B : c.blocks.sum = n := c.blocks_sum
    rw [eq_cons_of_length_one A] at B ⊢
    simpa [single_blocks] using B

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

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

Tactic:
simp only [mem_support, ne_eq, apply_zpow_apply_eq_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ {x | l.formPerm x ≠ x} ⊆ ↑l.toFinset

Tactic:
refine (zipWith_swap_prod_support' l l.tail).trans ?_

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ ↑(l.toFinset ⊔ l.tail.toFinset) ⊆ ↑l.toFinset
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: 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)
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := σ.subtypePermOfFintype h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := σ.subtypePermOfFintype h3
σ₁ : Perm m := (ofInjective Sum.inl ⋯).symm.permCongr σ₁'
⊢ σ ∈ (sumCongrHom m n).range

Tactic:
let σ₂ := permCongr (Equiv.ofInjective _ Sum.inr_injective).symm σ₂'

Goal state after:
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)
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := σ.subtypePermOfFintype h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := σ.subtypePermOfFintype h3
σ₁ : Perm m := (ofInjective Sum.inl ⋯).symm.permCongr σ₁'
σ₂ : Perm n := (ofInjective Sum.inr ⋯).symm.permCongr σ₂'
⊢ σ ∈ (sumCongrHom m n).range
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : (↑x.truncSwapFactors.out).prod = x
h2 : ∀ g ∈ ↑x.truncSwapFactors.out, g.IsSwap
⊢ (↑x.truncSwapFactors.out).prod ∈ Submonoid.closure {σ | σ.IsSwap}

Tactic:
exact Submonoid.list_prod_mem _ fun y hy ↦ Submonoid.subset_closure (h2 y hy)

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
n : ℤ
⊢ ↑⟨(fun x ↦ σ ^ x) n, ⋯⟩ (Classical.choose hσ) ∈ σ.support

Tactic:
rw [Subtype.coe_mk, zpow_apply_mem_support, mem_support]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
n : ℤ
⊢ σ (Classical.choose hσ) ≠ Classical.choose hσ
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
by_cases h : (l.formPerm ^ n) x = x
  · simpa [h] using hx
  · have h : x ∈ { x | (l.formPerm ^ n) x ≠ x } := h
    rw [← set_support_apply_mem] at h
    replace h := set_support_zpow_subset _ _ h
    simpa using support_formPerm_le' _ h

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

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
⊢ orderOf f = #f.support

Tactic:
← Fintype.card_zpowers,

Goal state after:
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
⊢ Fintype.card ↥(Subgroup.zpowers f) = #f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case succ.inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : f x ≠ b
this : f b ≠ b ∧ b ≠ x
hb' : (swap x (f x) * f) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
i : ℤ
hi : ((swap x (f x) * f) ^ i) (f x) = (Equiv.symm f) b
⊢ ((swap x (f x) * f) ^ (i + 1)) (f x) = b

Tactic:
rw [add_comm, zpow_add, mul_apply, hi, zpow_one, mul_apply, apply_symm_apply,
      swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 hfbx.symm]

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

Goal state before:
pp: α : Type u
g p : Perm α
x : α
hp : p * g = g * p
⊢ g (p x) = p x ↔ g x = x

Tactic:
rw [← mul_apply, ← hp, mul_apply, EmbeddingLike.apply_eq_iff_eq]

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : a ∈ closure S
b : Perm α
hb : b ∈ closure T
key1 : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
key2 : ↑b.support ⊆ ⋃ b ∈ T, ↑b.support
key : (∀ i ∈ S, ∀ i_2 ∈ T, _root_.Disjoint ↑i.support ↑i_2.support) → _root_.Disjoint ↑a.support ↑b.support
⊢ _root_.Disjoint a.support b.support

Tactic:
Finset.disjoint_coe

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : a ∈ closure S
b : Perm α
hb : b ∈ closure T
key1 : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
key2 : ↑b.support ⊆ ⋃ b ∈ T, ↑b.support
key : (∀ i ∈ S, ∀ i_2 ∈ T, _root_.Disjoint i.support i_2.support) → _root_.Disjoint a.support b.support
⊢ _root_.Disjoint a.support b.support
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
⊢ signAux ((e.symm.trans f).trans e) = signAux2 (x :: l) f

Tactic:
by
    rw [signAux2]
    by_cases hfx : x = f x
    · rw [if_pos hfx]
      exact
        signAux_eq_signAux2 l f _ fun y (hy : f y ≠ y) =>
          List.mem_of_ne_of_mem (fun h : y = x => by simp [h, hfx.symm] at hy) (h y hy)
    · 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.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ True ↔ σ ∈ univ

Tactic:
mem_univ

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

Goal state before:
pp: case refine_1
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
hx : a ∈ s ∧ b ∈ s
⊢ ∃ i, ∃ x ∈ s, (x, (f ^ i) x) = (a, b)

pp: case refine_2
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
⊢ (∃ i, ∃ x ∈ s, (x, (f ^ i) x) = (a, b)) → a ∈ s ∧ b ∈ s

Tactic:
· obtain ⟨n, rfl⟩ := hf.2 hx.1 hx.2
    exact ⟨_, _, hx.1, rfl⟩

Goal state after:
case refine_2
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
⊢ (∃ i, ∃ x ∈ s, (x, (f ^ i) x) = (a, b)) → a ∈ s ∧ b ∈ s
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
⊢ f.cycleOf x = f.cycleOf y

Tactic:
ext z
  rw [Equiv.Perm.cycleOf_apply]
  split_ifs with hz
  · exact (h.symm.trans hz).cycleOf_apply.symm
  · exact (cycleOf_apply_of_not_sameCycle (mt h.trans hz)).symm

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

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
k : ℤ
a : α
ha : a ∉ c.support
⊢ a ∈ c.support → (c ^ k) a = g a ↔ (c ^ k) a = (ofSubtype (g.subtypePerm ⋯)) a

Tactic:
rw [iff_true_left (fun b ↦ (ha b).elim), ofSubtype_apply_of_not_mem, ← notMem_support]
    · exact Finset.notMem_mono (support_zpow_le c k) ha
    · exact ha

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

Goal state before:
pp: case neg
n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
ch : ¬i = j
⊢ ↑⟨(castLEEmb ⋯) ((finRotate (↑j + 1)) ((castLEEmb ⋯).toEquivRange.symm ⟨i, iin⟩)), ⋯⟩ = i + 1

Tactic:
have hj1 : (i + 1).1 = i.1 + 1 := val_add_one_of_lt' (by lia)

Goal state after:
case neg
n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
ch : ¬i = j
hj1 : ↑(i + 1) = ↑i + 1
⊢ ↑⟨(castLEEmb ⋯) ((finRotate (↑j + 1)) ((castLEEmb ⋯).toEquivRange.symm ⟨i, iin⟩)), ⋯⟩ = i + 1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ Multiset.filter (fun n ↦ 2 ≤ n) σ.partition.parts = σ.cycleType

Tactic:
rw [parts_partition, filter_add, Multiset.filter_eq_self.2 fun _ => two_le_of_mem_cycleType,
    Multiset.filter_eq_nil.2 fun a h => ?_, add_zero]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
a : ℕ
h : a ∈ Multiset.replicate (Fintype.card α - #σ.support) 1
⊢ ¬2 ≤ a
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_3.inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
⊢ (τ * σ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f} ∪ σ.cycleFactorsFinset \ {f}

Tactic:
sdiff_singleton_eq_erase,

Goal state after:
case refine_3.inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
⊢ (τ * σ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset.erase f ∪ σ.cycleFactorsFinset \ {f}
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_3.inl.inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = σ a
x : α
hx : τ x = x
⊢ τ x = x ∨ (σ * f⁻¹) x = x

Tactic:
exact Or.inl hx

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

Goal state before:
pp: case refine_3.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ τ.cycleFactorsFinset
⊢ (σ * τ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f} ∪ τ.cycleFactorsFinset \ {f}

Tactic:
sdiff_singleton_eq_erase,

Goal state after:
case refine_3.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f ∈ τ.cycleFactorsFinset
⊢ (σ * τ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset.erase f ∪ τ.cycleFactorsFinset \ {f}