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

Goal state before:
pp: case unique_to.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ F ⟶ G

pp: case unique_to.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ (a : F ⟶ G), a = default

pp: case unique_from.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ G ⟶ F

pp: case unique_from.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ (a : G ⟶ F), a = default

Tactic:
· refine
      { app := fun X => (hF _).to_ _
        naturality := ?_ }
    intros
    exact (hF _).eq_of_src _ _

Goal state after:
case unique_to.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ (a : F ⟶ G), a = default

case unique_from.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ G ⟶ F

case unique_from.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ (a : G ⟶ F), a = default
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
F G H : C ⥤ D
η : G ⟶ H
⊢ 0 ≫ η = 0

Tactic:
by
    ext X; dsimp; apply zero_comp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
F : D ⥤ C
hF : F.FullyFaithful
X✝ Y✝ : D
f : X✝ ⟶ Y✝
x✝ : D
⊢ f ≫ 0 = 0

Tactic:
apply hF.map_injective

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
F : D ⥤ C
hF : F.FullyFaithful
X✝ Y✝ : D
f : X✝ ⟶ Y✝
x✝ : D
⊢ F.map (f ≫ 0) = F.map 0
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
F : D ⥤ C
hF : F.FullyFaithful
x✝² x✝¹ x✝ : D
f : x✝¹ ⟶ x✝
⊢ 0 ≫ f = 0

Tactic:
apply hF.map_injective

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
F : D ⥤ C
hF : F.FullyFaithful
x✝² x✝¹ x✝ : D
f : x✝¹ ⟶ x✝
⊢ F.map (0 ≫ f) = F.map 0
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Fork f g
⊢ c.ι ≫ (f - g) = c.ι ≫ 0

Tactic:
by rw [comp_sub, comp_zero, sub_eq_zero, c.condition]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ ¬P.Nonempty ↔ P = ⊥

Tactic:
rw [P.nonempty_iff_ne_bot, not_not]

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
g : X ⟶ Y
c : KernelFork g
hc : IsLimit c
X' Y' : C
g' : X' ⟶ Y'
e : X ≅ X'
iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0
W'✝ : C
s : W'✝ ⟶ X'
hs : s ≫ g' = 0
⊢ (s ≫ e.inv) ≫ g = 0

Tactic:
rw [iff, Category.assoc, Iso.inv_hom_id_assoc, hs]

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✝
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Z ⟶ X), g ≫ f = 0 → g = 0
s : Fork f 0
⊢ 0 ≫ Fork.ι (KernelFork.ofι 0 ⋯) = s.ι

Tactic:
by rw [hf _ _ (KernelFork.condition s), zero_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
W : C
g : W ⟶ X
h✝ : W ⟶ Y
c : CokernelCofork h✝
i : IsColimit c
hf : f ≫ Cofork.π c = 0
hfg : g ≫ f = h✝
s : Cofork f 0
m : (CokernelCofork.ofπ (Cofork.π c) hf).pt ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Cofork.π c) hf) ≫ m = s.π
⊢ m = i.desc (CokernelCofork.ofπ s.π ⋯)

Tactic:
apply Cofork.IsColimit.hom_ext i
      simpa using h

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
K : Type w'
inst✝ : HasBiproductsOfShape K C
e : J ≃ K
F : J → C
h : LimitBicone (F ∘ ⇑e.symm)
c : Bicone (F ∘ ⇑e.symm)
hc : c.IsBilimit
⊢ LimitBicone F

Tactic:
simpa only [Function.comp_def, e.symm_apply_apply] using
        LimitBicone.mk (c.whisker e) ((c.whiskerIsBilimitIff _).2 hc)

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 g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝¹ j✝ : J
h : j✝ = j✝¹
⊢ eqToHom ⋯ ≫ p j✝¹ = p j✝ ≫ eqToHom ⋯

pp: case neg
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝¹ j✝ : J
h : ¬j✝ = j✝¹
⊢ 0 ≫ p j✝¹ = p j✝ ≫ 0

Tactic:
· subst h; simp

Goal state after:
case neg
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝¹ j✝ : J
h : ¬j✝ = j✝¹
⊢ 0 ≫ p j✝¹ = p j✝ ≫ 0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
b b' : β
h : b' = b
⊢ ι (f ∘ ⇑ε) b' ≫ ((desc fun b ↦ ι f (ε b)) ≫ lift fun b ↦ π f (ε b)) ≫ π (f ∘ ⇑ε) b =
    ι (f ∘ ⇑ε) b' ≫ 𝟙 (⨁ f ∘ ⇑ε) ≫ π (f ∘ ⇑ε) b

pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
b b' : β
h : ¬b' = b
⊢ ι (f ∘ ⇑ε) b' ≫ ((desc fun b ↦ ι f (ε b)) ≫ lift fun b ↦ π f (ε b)) ≫ π (f ∘ ⇑ε) b =
    ι (f ∘ ⇑ε) b' ≫ 𝟙 (⨁ f ∘ ⇑ε) ≫ π (f ∘ ⇑ε) b

Tactic:
· subst h; simp

Goal state after:
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
b b' : β
h : ¬b' = b
⊢ ι (f ∘ ⇑ε) b' ≫ ((desc fun b ↦ ι f (ε b)) ≫ lift fun b ↦ π f (ε b)) ≫ π (f ∘ ⇑ε) b =
    ι (f ∘ ⇑ε) b' ≫ 𝟙 (⨁ f ∘ ⇑ε) ≫ π (f ∘ ⇑ε) b
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ map f g = map' f g

Tactic:
by
  ext
  · simp only [mapPair_left, IsColimit.ι_map, IsLimit.map_π,
      Category.assoc, ← BinaryBicone.toCone_π_app_left, ←
      BinaryBicone.toCocone_ι_app_left]
    simp
  · simp only [mapPair_left, IsColimit.ι_map, IsLimit.map_π,
      Category.assoc, ← BinaryBicone.toCone_π_app_right, ←
      BinaryBicone.toCocone_ι_app_left]
    simp
  · simp only [mapPair_right, IsColimit.ι_map, IsLimit.map_π,
      Category.assoc, ← BinaryBicone.toCone_π_app_left, ←
      BinaryBicone.toCocone_ι_app_right]
    simp
  · simp only [mapPair_right, IsColimit.ι_map, IsLimit.map_π,
      Category.assoc, ← BinaryBicone.toCone_π_app_right, ←
      BinaryBicone.toCocone_ι_app_right]
    simp

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

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

Tactic:
· intro h
    exact ⟨⟨biprod.fst, biprod.inl_fst, h.symm⟩⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
M N A✝ B✝ : ModuleCat R
f : A✝ ⟶ B✝
x✝ : IsIso ((forget₂ (ModuleCat R) AddCommGrpCat).map f)
⊢ IsIso f

Tactic:
have : IsIso ((forget _).map f) := by
      change IsIso ((forget _).map ((forget₂ _ AddCommGrpCat).map f))
      infer_instance
    apply isIso_of_reflects_iso _ (forget _)

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

Goal state before:
pp: case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x₁ : Fin k → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : Fin.cons (b.1 + 1) x₂ = Fin.cons (a.1 + 1) x₁
⊢ False

Tactic:
rw [Fin.cons_inj, Nat.succ_inj] at h₁₂

Goal state after:
case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x₁ : Fin k → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 = a.1 ∧ x₂ = x₁
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c.sizeUpTo 0 = 0

Tactic:
by simp [sizeUpTo]

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

Goal state before:
pp: α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
h : (f ^ n) x = f x
⊢ (f ^ (n + 1)) x = x

Tactic:
rw [pow_succ', mul_apply, h, hffx]

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

Goal state before:
pp: α : Type u
f : Perm α
p : α → Prop
inst✝ : Finite { x // p x }
h : ∀ (x : α), p x → p (f x)
x : α
hx : p x
⊢ p ((Equiv.symm f) x)

Tactic:
have : Finite { x | p x } := by simpa

Goal state after:
α : Type u
f : Perm α
p : α → Prop
inst✝ : Finite { x // p x }
h : ∀ (x : α), p x → p (f x)
x : α
hx : p x
this : Finite ↑{x | p x}
⊢ p ((Equiv.symm f) x)
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
h : (x :: y :: xs).Nodup
⊢ (x :: y :: xs).formPerm x = y

Tactic:
by simp [formPerm_apply_of_notMem h.notMem]

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
⊢ (permsOfList (a :: l)).Nodup

Tactic:
have hl' : l.Nodup := hl.of_cons

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
⊢ (permsOfList (a :: l)).Nodup
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case succ.cons.cons.a
α : 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
IH : (y :: l).formPerm (y :: l)[n] = l[n]
⊢ (y :: l).formPerm (y :: l)[n] ≠ x

Tactic:
· intro hx
        rw [← hx, IH] at h
        simp [getElem_mem] at h

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

Goal state before:
pp: case succ.cons.cons.a
α : 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
IH : (y :: l).formPerm (y :: l)[n] = l[n]
⊢ (y :: l).formPerm (y :: l)[n] ≠ y

Tactic:
· intro hx
        rw [← hx, IH] at h
        simp [getElem_mem] at h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ f = 1 ∨ #f.support = 1 ↔ f = 1

Tactic:
or_iff_not_imp_right,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ ¬#f.support = 1 → f = 1 ↔ f = 1
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
constructor <;> intro h

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

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = y
ha : f a = a
⊢ f a = (swap x y) a

Tactic:
have ha' := not_or.mp (mt (key a).mpr (not_not.mpr ha))

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = y
ha : f a = a
ha' : ¬a = x ∧ ¬a = y
⊢ f a = (swap x y) a
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case neg.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
y : α
ht : #{y} = 1
a : α
ha : ¬f a = a
hmem : ¬a = y
hins : {a, y} = f.support
key : ∀ (b : α), f b ≠ b ↔ b = a ∨ b = y
ha' : f a = a ∨ f a = y
⊢ f a = (swap a y) a

pp: case neg.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x a : α
ha : ¬f a = a
hmem : ¬x = a
hins : {x, a} = f.support
ht : #{a} = 1
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = a
ha' : f a = x ∨ f a = a
⊢ f a = (swap x a) a

Tactic:
· rw [Or.resolve_left ha' ha, swap_apply_left]

Goal state after:
case neg.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x a : α
ha : ¬f a = a
hmem : ¬x = a
hins : {x, a} = f.support
ht : #{a} = 1
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = a
ha' : f a = x ∨ f a = a
⊢ f a = (swap x a) a
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
x✝ : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ (f ^ (-i)) y = x

Tactic:
by simp [zpow_neg, ← hi]

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

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
hx : f x ≠ x
hf : f.IsCycle
y : α
x✝ : f.SameCycle x y
hy : f y = y
i : ℤ
hi : x = y
⊢ f y = y

Tactic:
hy

Goal state after:
α : Type u_2
f : Perm α
x : α
hx : f x ≠ x
hf : f.IsCycle
y : α
x✝ : f.SameCycle x y
hy : f y = y
i : ℤ
hi : x = y
⊢ y = y
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
n : ℕ
e : α ≃ Fin n
⊢ (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun x y ↦ (swap x y).signAux3 hs = -1

Tactic:
induction s using Quotient.inductionOn with | _ l => ?_

Goal state after:
case h
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
⊢ (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun x y ↦ (swap x y).signAux3 hs = -1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

Tactic:
hy

Goal state after:
α : Type u_2
f g : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, f x = g x
hx : f x = g x
hx' : x ∈ f.support
hx'' : x ∈ g.support
y : α
hy : y ∈ f.support
⊢ y ∈ g.support
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
⊢ s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1

Tactic:
induction s using Finset.induction_on with
    | empty => simp
    | insert i s hnotMem ih =>
      have hcomm := comm.mono (Finset.coe_subset.2 <| Finset.subset_insert _ _)
      simp only [Finset.forall_mem_insert] at hmem
      have hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ (s : Set ι), K i := by
        refine Subgroup.noncommProd_mem _ _ ?_
        intro x hx
        have : K x ≤ ⨆ i ∈ (s : Set ι), K i := le_iSup₂ (f := fun i _ => K i) x hx
        exact this (hmem.2 x hx)
      intro heq1
      rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hnotMem] at heq1
      have hnotMem' : i ∉ (s : Set ι) := by simpa
      obtain ⟨heq1i : f i = 1, heq1S : s.noncommProd f _ = 1⟩ :=
        Subgroup.disjoint_iff_mul_eq_one.mp (hind.disjoint_biSup hnotMem') hmem.1 hmem_bsupr heq1
      intro i h
      simp only [Finset.mem_insert] at h
      rcases h with (rfl | h)
      · exact heq1i
      · refine ih hcomm hmem.2 heq1S _ h

Goal state after:
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ (↑n).num * (↑d)⁻¹.num / ↑(((↑n).num * (↑d)⁻¹.num).natAbs.gcd (1 * (↑d)⁻¹.den)) = ↑n

Tactic:
Rat.inv_natCast_den_of_pos this,

Goal state after:
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ (↑n).num * (↑d)⁻¹.num / ↑(((↑n).num * (↑d)⁻¹.num).natAbs.gcd (1 * d)) = ↑n
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ 1 * (↑d)⁻¹.den / ((↑n).num * (↑d)⁻¹.num).natAbs.gcd (1 * (↑d)⁻¹.den) = ↑d

Tactic:
Rat.inv_natCast_den_of_pos this,

Goal state after:
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ 1 * d / ((↑n).num * (↑d)⁻¹.num).natAbs.gcd (1 * d) = ↑d
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 ι
f : (i : ι) → H i
⊢ (noncommPiCoprod ϕ hcomm) f ∈ ⨆ i, (ϕ i).range

Tactic:
refine Subgroup.noncommProd_mem _ (fun _ _ _ _ h => hcomm h _ _) ?_

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 ι := Classical.decEq ι
f : (i : ι) → H i
⊢ ∀ c ∈ Finset.univ, (ϕ c) (f c) ∈ ⨆ i, (ϕ i).range
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : f x ≠ x
this : (f.cycleOf x) x ≠ x
y : α
h : (f.cycleOf x) y ≠ y
hxy : ¬f.SameCycle x y
⊢ (f.cycleOf x).SameCycle x y

Tactic:
rw [cycleOf_apply_of_not_sameCycle hxy] at h
        exact (h rfl).elim

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
⊢ y ∈ (f.cycleOf x).support → y ∈ f.support

Tactic:
hy

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : y ∈ (f.cycleOf x).support
⊢ y ∈ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
hx : ¬f x = x
⊢ (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x

Tactic:
rw [← cycleOf_pow_apply_self, ← cycleOf_pow_apply_self f, ← (isCycle_cycleOf f hx).orderOf,
      pow_mod_orderOf]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
comm : Pairwise fun i j ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
u : (i : ι) → ↥(H i)
⊢ (noncommPiCoprod comm) u = Finset.univ.noncommProd (fun i ↦ ↑(u i)) ⋯

Tactic:
by
  simp only [Subgroup.noncommPiCoprod, MonoidHom.noncommPiCoprod,
    coe_subtype, MonoidHom.coe_mk, OneHom.coe_mk]

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
y : α
⊢ g y ≠ y → y ∈ l

Tactic:
hy

Goal state after:
ι : 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
y : α
hy : g y ≠ y
⊢ y ∈ l
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
y : α
⊢ ((g.cycleOf x)⁻¹ * g) y ≠ y → y ∈ l

Tactic:
hy

Goal state after:
ι : 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
y : α
hy : ((g.cycleOf x)⁻¹ * g) y ≠ y
⊢ y ∈ l
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ.refine_2
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
⊢ ↑((finRotate (n✝ + 1).succ) i.succ) = ↑((decomposeFin.symm (1, finRotate (n✝ + 1))) i.succ)

Tactic:
rw [coe_finRotate, decomposeFin_symm_apply_succ, if_congr i.succ_eq_last_succ rfl rfl]

Goal state after:
case succ.refine_2
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
⊢ (if i = Fin.last n✝ then 0 else ↑i.succ + 1) = ↑((swap 0 1) ((finRotate (n✝ + 1)) i).succ)
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
y : α
⊢ ((g.cycleOf x)⁻¹ * g) y ≠ y → f.cycleOf y = ((g.cycleOf x)⁻¹ * g).cycleOf y

Tactic:
hy

Goal state after:
ι : 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
y : α
hy : ((g.cycleOf x)⁻¹ * g) y ≠ y
⊢ f.cycleOf y = ((g.cycleOf x)⁻¹ * g).cycleOf y