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

Goal state before:
pp: J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j : J
⊢ (isoProduct f).inv ≫ π f j = lift (Pi.π f) ≫ π f j

Tactic:
simp [Iso.inv_comp_eq]

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

Goal state before:
pp: case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
j : J
h : ¬k = e j
⊢ j ≠ e.symm k

pp: case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
j : J
h : ¬k = e j
⊢ e j ≠ k

Tactic:
· rintro rfl
      simp at h

Goal state after:
case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
j : J
h : ¬k = e j
⊢ e j ≠ k
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case neg.h
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ e.symm k ≠ j

Tactic:
· rintro rfl
      simp at h

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
t : Bicone f
ht : IsLimit t.toCone
j : Discrete J
⊢ (∑ j, t.π j ≫ t.ι j) ≫ t.toCone.π.app j = 𝟙 t.pt ≫ t.toCone.π.app j

Tactic:
by
      classical
      cases j
      simp [sum_comp, t.ι_π, comp_dite]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T : C
g : (j : J) → T ⟶ f j
⊢ lift g = ∑ j, g j ≫ ι f j

Tactic:
ext j

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T : C
g : (j : J) → T ⟶ f j
j : J
⊢ lift g ≫ π f j = (∑ j, g j ≫ ι f j) ≫ π f j
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T : C
g : (j : J) → f j ⟶ T
⊢ desc g = ∑ j, π f j ≫ g j

Tactic:
ext j

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T : C
g : (j : J) → f j ⟶ T
j : J
⊢ ι f j ≫ desc g = ι f j ≫ ∑ j, π f j ≫ g j
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoProd X Y).inv ≫ fst = lift prod.fst prod.snd ≫ fst

Tactic:
simp [Iso.inv_comp_eq]

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

Goal state before:
pp: case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ (isoProd X Y).inv ≫ snd = lift prod.fst prod.snd ≫ snd

Tactic:
simp [Iso.inv_comp_eq]

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✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W' : C
g' : W' ⟶ ⨁ f
w : g' ≫ biproduct.toSubtype f p = 0
⊢ (g' ≫ biproduct.toSubtype f pᶜ) ≫ biproduct.fromSubtype f pᶜ = g'

Tactic:
ext j

Goal state after:
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W' : C
g' : W' ⟶ ⨁ f
w : g' ≫ biproduct.toSubtype f p = 0
j : K
⊢ ((g' ≫ biproduct.toSubtype f pᶜ) ≫ biproduct.fromSubtype f pᶜ) ≫ biproduct.π f j = g' ≫ biproduct.π f j
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝⁷ : Category.{uC', uC} C
inst✝⁶ : HasZeroMorphisms C
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
P Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
⊢ Epi (map f g)

Tactic:
rw [show biprod.map f g =
    (biprod.isoCoprod _ _).hom ≫ coprod.map f g ≫ (biprod.isoCoprod _ _).inv by aesop]

Goal state after:
J : Type w
C : Type uC
inst✝⁷ : Category.{uC', uC} C
inst✝⁶ : HasZeroMorphisms C
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
P Q W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
⊢ Epi ((isoCoprod W X).hom ≫ coprod.map f g ≫ (isoCoprod Y Z).inv)
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
⊢ ∀ {W' : C} (g' : W' ⟶ ⨁ f),
    g' ≫ biproduct.toSubtype f p = 0 → (g' ≫ biproduct.toSubtype f pᶜ) ≫ biproduct.fromSubtype f pᶜ = g'

Tactic:
classical
        intro W' g' w
        ext j
        simp only [Category.assoc, biproduct.toSubtype_fromSubtype, Pi.compl_apply,
          biproduct.map_π]
        split_ifs with h
        · simp
        · replace w := w =≫ biproduct.π _ ⟨j, not_not.mp h⟩
          simpa using w.symm

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✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W : C
g' : ⨁ f ⟶ W
w : biproduct.fromSubtype f p ≫ g' = 0
⊢ biproduct.toSubtype f pᶜ ≫ biproduct.fromSubtype f pᶜ ≫ g' = g'

Tactic:
ext j

Goal state after:
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W : C
g' : ⨁ f ⟶ W
w : biproduct.fromSubtype f p ≫ g' = 0
j : K
⊢ biproduct.ι f j ≫ biproduct.toSubtype f pᶜ ≫ biproduct.fromSubtype f pᶜ ≫ g' = biproduct.ι f j ≫ g'
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝³ : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Ring S
inst✝ : Algebra S₀ S
M✝ N✝ x✝ M N : ModuleCat S
s₀ : S₀
f : x✝ ⟶ M
g : M ⟶ N
⊢ (s₀ • f) ≫ g = s₀ • f ≫ g

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
a b : Fin n
hab : a < b
⊢ f a < f b

pp: case refine_2
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
i : Fin n
hlt : i.castSucc < q
⊢ f i < x

pp: case refine_3
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
i : Fin n
hlt : q ≤ i.castSucc
⊢ x < f i

pp: case refine_4
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
⊢ (StrictMono f ∧ (∀ (i : Fin n), i.castSucc < q → f i < x) ∧ ∀ (i : Fin n), q ≤ i.castSucc → x < f i) →
    StrictMono (q.insertNth x f)

Tactic:
· simpa [hab] using h (a := q.succAbove a) (b := q.succAbove b)

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
i : Fin n
hlt : i.castSucc < q
⊢ f i < x

case refine_3
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono (q.insertNth x f)
i : Fin n
hlt : q ≤ i.castSucc
⊢ x < f i

case refine_4
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
⊢ (StrictMono f ∧ (∀ (i : Fin n), i.castSucc < q → f i < x) ∧ ∀ (i : Fin n), q ≤ i.castSucc → x < f i) →
    StrictMono (q.insertNth x f)
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Type u_2
inst✝ : LE α
⊢ insertNthOrderIso (fun x ↦ α) (last n) = snocOrderIso fun x ↦ α

Tactic:
by ext; simp

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

Goal state before:
pp: case e_a
n : ℕ
⊢ ∀ x < n, map (fun x_1 ↦ Fin.cons x x_1) (antidiagonalTuple 0 (n - x)) = []

Tactic:
List.map_eq_nil_iff

Goal state after:
case e_a
n : ℕ
⊢ ∀ x < n, antidiagonalTuple 0 (n - x) = []
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case e_a
x m : ℕ
hx : x < x + m + 1
⊢ antidiagonalTuple 0 (x + (m + 1) - x) = []

Tactic:
add_tsub_cancel_left,

Goal state after:
case e_a
x m : ℕ
hx : x < x + m + 1
⊢ antidiagonalTuple 0 (m + 1) = []
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case mpr
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s) →
    ∃ s_1, (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = n ∧ ∀ (x : ι), Multiset.count x s_1 = f x

Tactic:
· rintro ⟨rfl, hf⟩
    refine ⟨∑ a ∈ s, f a • {a}, ?_, ?_⟩
    · simp +contextual
    · simpa [Multiset.count_sum', Multiset.count_singleton, not_imp_comm, eq_comm (a := 0)] using hf

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (indiscrete n).parts = {n}

Tactic:
by
  simp [indiscrete, filter_eq_self, hn]

Goal state after:
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)
⊢ piComparison F f =
    (F.mapIso (biproduct.isoProduct f)).inv ≫ F.biproductComparison f ≫ (biproduct.isoProduct (F.obj ∘ f)).hom

Tactic:
ext j

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)
j : J
⊢ piComparison F f ≫ Pi.π (fun b ↦ F.obj (f b)) j =
    ((F.mapIso (biproduct.isoProduct f)).inv ≫ F.biproductComparison f ≫ (biproduct.isoProduct (F.obj ∘ f)).hom) ≫
      Pi.π (fun b ↦ F.obj (f b)) j
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 : μ
g : ι →₀ μ
hsum : (g.sum fun x x_1 ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ (((mapRange.addEquiv e).toEmbedding g).sum fun x x_1 ↦ x_1) = e n ∧ ((mapRange.addEquiv e).toEmbedding g).support ⊆ s

Tactic:
simp only [AddEquiv.toEquiv_eq_coe, mapRange.addEquiv_toEquiv, Equiv.coe_toEmbedding,
    mapRange.equiv_apply, EquivLike.coe_coe]

Goal state after:
ι : 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 : μ
g : ι →₀ μ
hsum : (g.sum fun x x_1 ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ ((mapRange ⇑e ⋯ g).sum fun x x_1 ↦ x_1) = e n ∧ (mapRange ⇑e ⋯ g).support ⊆ s
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
⊢ f (g x) ≠ x → f x ≠ x ∨ g x ≠ x

Tactic:
← not_and_or,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
⊢ f (g x) ≠ x → ¬(f x = x ∧ g x = x)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
⊢ x ∈ (f * g).support → x ∈ f.support ⊔ g.support

Tactic:
by
  simp only [sup_eq_union]
  rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]
  rintro ⟨hf, hg⟩
  rw [hg, hf]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
a : α
⊢ f a ≠ a ∨ g a ≠ a → f (g a) ≠ a

Tactic:
← not_and_or,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
a : α
⊢ ¬(f a = a ∧ g a = a) → f (g a) ≠ a
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : x ∈ l
⊢ l.formPerm x ∈ l

Tactic:
by
  rcases l with - | ⟨y, l⟩
  · simp at h
  induction l generalizing x y with
  | nil => simpa using h
  | cons z l IH =>
    by_cases hx : x ∈ z :: l
    · rw [formPerm_cons_cons, mul_apply, swap_apply_def]
      split_ifs
      · simp
      · simp
      · simp [*]
    · replace h : x = y := Or.resolve_right (mem_cons.1 h) hx
      simp [formPerm_apply_of_notMem hx, ← h]

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

Goal state before:
pp: case h.inl
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 σ₂'
a : m
⊢ ↑(σ₁' ((ofInjective Sum.inl ⋯) a)) = σ (Sum.inl a)

Tactic:
ofInjective_apply

Goal state after:
case h.inl
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 σ₂'
a : m
⊢ ↑(σ₁' ⟨Sum.inl a, ⋯⟩) = σ (Sum.inl a)
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case h.inr
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 σ₂'
b : n
⊢ ↑(σ₂' ((ofInjective Sum.inr ⋯) b)) = σ (Sum.inr b)

Tactic:
ofInjective_apply

Goal state after:
case h.inr
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 σ₂'
b : n
⊢ ↑(σ₂' ⟨Sum.inr b, ⋯⟩) = σ (Sum.inr b)
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro
α : Type u
inst✝ : Finite α
σ τ π ρ : Perm α
hc1 : IsConj σ π
hc2 : IsConj τ ρ
hd1 : σ.Disjoint τ
hd2 : π.Disjoint ρ
val✝ : Fintype α
⊢ IsConj (σ * τ) (π * ρ)

Tactic:
obtain ⟨f, rfl⟩ := isConj_iff.1 hc1

Goal state after:
case intro
α : Type u
inst✝ : Finite α
σ τ ρ : Perm α
hc2 : IsConj τ ρ
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint ρ
⊢ IsConj (σ * τ) (f * σ * f⁻¹ * ρ)
Module: Mathlib.Data.Int.Order.Units

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

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

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
⊢ (ofSubtype u) x = x ∨ g x = x

Tactic:
by_cases hx : x ∈ Function.fixedPoints g

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
hx : x ∈ fixedPoints ⇑g
⊢ (ofSubtype u) x = x ∨ g x = x

case neg
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
x : α
hx : x ∉ fixedPoints ⇑g
⊢ (ofSubtype u) x = x ∨ g x = x
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
f : Perm α
x✝ : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬s (swap x y) = -1
this✝ : ∀ (f : Perm α), f.IsSwap → s f = 1
g : Perm α
hg : s g = -1
l : List (Perm α)
hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap
this : ∀ a ∈ List.map (⇑s) l, a = 1
⊢ s l.prod = 1

Tactic:
rw [← l.prod_hom s, List.eq_replicate_length.2 this, List.prod_replicate, one_pow]

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

Goal state before:
pp: n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
⊢ IsNat (↑n * ⅟↑d).den d

Tactic:
constructor
    have : 0 < d := Nat.pos_iff_ne_zero.mpr <| by simpa using hi.ne_zero
    simp_rw [Rat.mul_den, Rat.den_intCast, invOf_eq_inv,
      Rat.inv_natCast_den_of_pos this, Rat.inv_natCast_num_of_pos this,
      Rat.num_intCast, one_mul, mul_one, Nat.cast_id, h, Nat.div_one]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i) x)
h : (i : ι) → N i
⊢ Commute m ((noncommPiCoprod ϕ hcomm) h)

Tactic:
dsimp only [MonoidHom.noncommPiCoprod, MonoidHom.coe_mk, OneHom.coe_mk]

Goal state after:
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i) x)
h : (i : ι) → N i
⊢ Commute m (Finset.univ.noncommProd (fun i ↦ (ϕ i) (h i)) ⋯)
Module: Mathlib.GroupTheory.NoncommPiCoprod

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

Tactic:
dsimp only [MonoidHom.noncommPiCoprod, MonoidHom.coe_mk, OneHom.coe_mk]

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

Goal state before:
pp: case inl
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
hs : (↑s).Subsingleton
⊢ (↑(range #s)).Subsingleton

Tactic:
simp_rw [Set.Subsingleton, mem_coe, ← card_le_one] at hs ⊢

Goal state after:
case inl
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
hs : #s ≤ 1
⊢ #(range #s) ≤ 1
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := ⋯
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
c : ℕ
hc : (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c
⊢ 1 = orderOf f * c

Tactic:
rw [← hc]

Goal state after:
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
c : ℕ
hc : (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i)) = orderOf f * c
⊢ 1 = (∏ j, Fintype.card (H ↑j)).gcd (Fintype.card (H i))
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : #σ.support < 2 * orderOf σ
⊢ σ.IsCycle

Tactic:
obtain ⟨n, hn⟩ := cycleType_prime_order h1

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : #σ.support < 2 * orderOf σ
n : ℕ
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle
Module: Mathlib.GroupTheory.Perm.Option

Goal state before:
pp: case some.none
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
h : σ (some x) = none
⊢ Option.map (⇑(removeNone σ)) (some x) = (swap none (σ none)) none

Tactic:
simp [removeNone_none _ h]

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

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

Tactic:
decomposeFin_symm_apply_succ,

Goal state after:
case succ.refine_2
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
⊢ (if i.succ = Fin.last (n✝ + 1) then 0 else ↑i.succ + 1) = ↑((swap 0 1) ((finRotate (n✝ + 1)) i).succ)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ cycleRange 0 = 1

Tactic:
ext j

Goal state after:
n : ℕ
inst✝ : NeZero n
j : Fin n
⊢ ↑((cycleRange 0) j) = ↑(1 j)