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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
⊢ m ≫ 𝟙 b.toCone.pt = ∑ j, s.π.app { as := j } ≫ b.ι j

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
⊢ m ≫ 𝟙 b.pt = ∑ j, s.π.app { as := j } ≫ b.ι j
Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : HasBinaryBiproducts C
F : C ⥤ D
h : rightExactFunctor C D F
⊢ additiveFunctor C D F

Tactic:
simp only [rightExactFunctor_iff] at h

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : HasBinaryBiproducts C
F : C ⥤ D
h : PreservesFiniteColimits F
⊢ additiveFunctor C D F
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
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cocone (Discrete.functor f)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete J), b.toCocone.ι.app j ≫ m = s.ι.app j
⊢ 𝟙 b.toCocone.pt ≫ m = ∑ j, b.π j ≫ s.ι.app { as := j }

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cocone (Discrete.functor f)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete J), b.toCocone.ι.app j ≫ m = s.ι.app j
⊢ 𝟙 b.pt ≫ m = ∑ j, b.π j ≫ s.ι.app { as := 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 X Y : C
c : BinaryBicone X Y
i : IsLimit c.toCone
s : Fork c.fst 0
⊢ (s.ι ≫ c.snd) ≫ Fork.ι c.fstKernelFork = s.ι

Tactic:
by apply BinaryFan.IsLimit.hom_ext i <;> simp

Goal state after:
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 X Y : C
c : BinaryBicone X Y
i : IsLimit c.toCone
s : Fork c.snd 0
⊢ (s.ι ≫ c.fst) ≫ Fork.ι c.sndKernelFork = s.ι

Tactic:
by apply BinaryFan.IsLimit.hom_ext i <;> simp

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

Goal state before:
pp: case refine_1
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✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasFiniteBiproducts C
X : C
⊢ ∀ (a : ⨁ Empty.elim ⟶ X), a = default

Tactic:
intro a; apply biproduct.hom_ext'; simp

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
r : R
⊢ (forget₂ (ModuleCat R) AddCommGrpCat).map f ≫ N.smul r = M.smul r ≫ (forget₂ (ModuleCat R) AddCommGrpCat).map f

Tactic:
ext x
  exact (f.hom.map_smul r x).symm

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
q₁ q₂ : (j : Fin (n + 1)) → α j
hx : ¬x ∈ Icc (q₁ i) (q₂ i)
p : (j : Fin n) → α (i.succAbove j)
⊢ p ∈ i.insertNth x ⁻¹' Icc q₁ q₂ ↔ p ∈ ∅

Tactic:
by
    simp only [mem_preimage, insertNth_mem_Icc, hx, false_and, mem_empty_iff_false]

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

Goal state before:
pp: α : Type u_1
n : ℕ
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
a : α
⊢ ((fun x1 x2 ↦ x1 < x2) ⇒ r) (vecCons a f) (vecCons a f) ↔ r a (f 0) ∧ ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f

Tactic:
simp only [liftFun_iff_succ r, forall_iff_succ, cons_val_succ, cons_val_zero, ← succ_castSucc,
    castSucc_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case refine_1
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
s : Finset ι
n : μ
e : ↥s ≃ Fin #s
⊢ Injective fun f i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0

Tactic:
rw [Injective]

Goal state after:
case refine_1
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
s : Finset ι
n : μ
e : ↥s ≃ Fin #s
⊢ ∀ ⦃a₁ a₂ : Fin #s → μ⦄,
    ((fun i ↦ if hi : i ∈ s then a₁ (e ⟨i, hi⟩) else 0) = fun i ↦ if hi : i ∈ s then a₂ (e ⟨i, hi⟩) else 0) → a₁ = a₂
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a c : μ
f : ι → μ
hab : (a, s.sum f) ∈ ↑(antidiagonal n)
g : ι → μ
hcd : (c, s.sum g) ∈ ↑(antidiagonal n)
hfg : ¬s.sum f = s.sum g
hgf : (g + fun j ↦ if j = i then c else 0) = f + fun j ↦ if j = i then a else 0
⊢ False

Tactic:
exact hfg <| by simpa [sum_add_distrib, hi] using congr_arg (∑ j ∈ s, · j) hgf.symm

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

Goal state before:
pp: n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ (fun j ↦ ⟨c.index j, c.invEmbedding j⟩) ((fun x ↦ (c.embedding x.fst) x.snd) ⟨i, y⟩) = ⟨i, y⟩

Tactic:
dsimp

Goal state after:
n : ℕ
c : Composition n
i : Fin c.length
y : Fin (c.blocksFun i)
⊢ ⟨c.index ((c.embedding i) y), c.invEmbedding ((c.embedding i) y)⟩ = ⟨i, y⟩
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cone (pair X Y)
hc : IsLimit c
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
        (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)).toCone).pt ≅
    (F.mapCone c).pt

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cone (pair X Y)
hc : IsLimit c
⊢ F.obj c.pt ≅ F.obj c.pt
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesLimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).pt ≅ (F.mapBinaryBicone b).toCone.pt

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesLimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ F.obj b.pt ≅ F.obj b.pt
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cocone (pair X Y)
hc : IsColimit c
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
        (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)).toCocone).pt ≅
    (F.mapCocone c).pt

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cocone (pair X Y)
hc : IsColimit c
⊢ F.obj c.pt ≅ F.obj c.pt
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n m : ℕ
c : Composition m
hmn : m = n
⊢ c.cast hmn ≍ c

Tactic:
by subst m; rfl

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

Goal state before:
pp: case e'_2
n✝¹ : ℕ
c✝¹ : Composition n✝¹
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n✝ : ℕ
c✝ : Composition n✝
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
e_1✝ : k + 1 + n = n + (k + 1)
⊢ (c.reverse.append (single (k + 1) ⋯).reverse).cast ⋯ ≍ c.reverse.append (single (k + 1) ⋯)

Tactic:
reverse_single

Goal state after:
case e'_2
n✝¹ : ℕ
c✝¹ : Composition n✝¹
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n✝ : ℕ
c✝ : Composition n✝
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
e_1✝ : k + 1 + n = n + (k + 1)
⊢ (c.reverse.append (single (k + 1) ⋯)).cast ⋯ ≍ c.reverse.append (single (k + 1) ⋯)
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
rw [h a ha, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]

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

Goal state before:
pp: case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ (take n l :: (drop n l).splitWrtCompositionAux ns).flatten = l

Tactic:
dsimp

Goal state after:
case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ take n l ++ ((drop n l).splitWrtCompositionAux ns).flatten = l
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case succ
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.boundaries.card
⊢ (take (i + 1) c.blocks).sum = ↑(c.boundary ⟨i + 1, h⟩)

Tactic:
have A : i < c.blocks.length := by
      rw [c.card_boundaries_eq_succ_length] at h
      simp [blocks, Nat.lt_of_succ_lt_succ h]

Goal state after:
case succ
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
⊢ (take (i + 1) c.blocks).sum = ↑(c.boundary ⟨i + 1, h⟩)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : List.Pairwise Disjoint tl → tl.prod.support = List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support tl)
h : List.Pairwise Disjoint (hd :: tl)
⊢ (hd :: tl).prod.support = List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support (hd :: tl))

Tactic:
| cons hd tl hl =>

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

Goal state before:
pp: case mpr
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ (∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j) → j ∈ c.boundaries

Tactic:
rintro ⟨i, hi, H⟩

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

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : tl.prod.support ⊆ List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support tl)
⊢ (hd :: tl).prod.support ⊆ List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support (hd :: tl))

Tactic:
| cons hd tl hl =>

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i) x = y
⊢ closure {σ, swap x ((σ ^ i) x)} = ⊤

Tactic:
refine closure_cycle_coprime_swap
    (Nat.Coprime.symm (h0.coprime_iff_not_dvd.mpr fun h => h4 ?_)) h1 h2 x

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i) x = y
h : Fintype.card α ∣ i
⊢ x = y
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
this :
  a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
    a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
⊢ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (prodCongrRight σ) (a, b)

Tactic:
by
    obtain ⟨_, prod_eq⟩ := Or.resolve_right this (not_and.mpr fun h _ => h (mem_l a))
    rw [prod_eq, prodCongrRight_apply]

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

Goal state before:
pp: case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
⊢ (∃ x, f x ≠ x ∧ (f ^ n) x = x) → f ^ n = 1

Tactic:
· rintro ⟨x, hx, hx'⟩
      by_cases h : support (f ^ n) = support f
      · rw [← mem_support, ← h, mem_support] at hx
        contradiction
      · rw [hf.support_pow_eq_iff, Classical.not_not] at h
        obtain ⟨k, rfl⟩ := h
        rw [pow_mul, pow_orderOf_eq_one, one_pow]

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

Goal state before:
pp: case inl
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Subsingleton
⊢ (f.subtypePerm ⋯).IsCycleOn _root_.Set.univ

Tactic:
have := hs.coe_sort

Goal state after:
case inl
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Subsingleton
this : Subsingleton ↑s
⊢ (f.subtypePerm ⋯).IsCycleOn _root_.Set.univ
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x y : α
hx : x ∈ g.support
hy : y ∈ g.support
h : g.cycleOf x = g.cycleOf y
⊢ y ∈ (g.cycleOf y).support

Tactic:
mem_support_cycleOf_iff' (mem_support.mp hy)

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x y : α
hx : x ∈ g.support
hy : y ∈ g.support
h : g.cycleOf x = g.cycleOf y
⊢ g.SameCycle y y
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : (Multiset.map (fun n ↦ -(-1) ^ n) s).prod = (-1) ^ (s.sum + s.card)
⊢ (Multiset.map (fun n ↦ -(-1) ^ n) (a ::ₘ s)).prod = (-1) ^ ((a ::ₘ s).sum + (a ::ₘ s).card)

Tactic:
Multiset.map_cons,

Goal state after:
case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : (Multiset.map (fun n ↦ -(-1) ^ n) s).prod = (-1) ^ (s.sum + s.card)
⊢ (-(-1) ^ a ::ₘ Multiset.map (fun n ↦ -(-1) ^ n) s).prod = (-1) ^ ((a ::ₘ s).sum + (a ::ₘ s).card)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
x1 x2 : Fin n
hlt : x2 < x1
hle : (Equiv.symm σ) x2 ≤ (Equiv.symm σ) x1
⊢ (Equiv.symm σ) x2 ≠ (Equiv.symm σ) x1

Tactic:
by simp [hlt.ne]

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
hφD : Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D = D
x : (_ : Fin n) × Fin n
hx : x ∈ ↑D
y : (_ : Fin n) × Fin n
hy : y ∈ ↑D
⊢ (Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D).card = D.card

Tactic:
rw [hφD]

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ (σ : Perm α),
    σ.IsCycle → ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}

pp: case refine_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ (σ τ : Perm α),
    σ.Disjoint τ →
      σ.IsCycle →
        (∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}) →
          (∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}) →
            ∀ {f : Perm α},
              f ∈ (σ * τ).cycleFactorsFinset → (σ * τ * f⁻¹).cycleFactorsFinset = (σ * τ).cycleFactorsFinset \ {f}

Tactic:
· intro σ hσ f hf
    simp only [cycleFactorsFinset_eq_singleton_self_iff.mpr hσ, mem_singleton] at hf ⊢
    simp [hf]

Goal state after:
case refine_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ : Perm α
⊢ ∀ (σ τ : Perm α),
    σ.Disjoint τ →
      σ.IsCycle →
        (∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}) →
          (∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}) →
            ∀ {f : Perm α},
              f ∈ (σ * τ).cycleFactorsFinset → (σ * τ * f⁻¹).cycleFactorsFinset = (σ * τ).cycleFactorsFinset \ {f}
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: case intro
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁶ : Finite ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : AddCommMonoid N
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : Module R N
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ DFinsupp.lsingle (p i)) = g.compLinearMap fun i ↦ DFinsupp.lsingle (p i)
x : (i : ι) → Π₀ (j : κ i), M i j
val✝ : Fintype ι
⊢ (f fun i ↦ ∑ i_1 ∈ (x i).support, DFinsupp.single i_1 ((x i) i_1)) =
    g fun i ↦ ∑ i_1 ∈ (x i).support, DFinsupp.single i_1 ((x i) i_1)

Tactic:
MultilinearMap.map_sum_finset

Goal state after:
case intro
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁶ : Finite ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : AddCommMonoid N
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : Module R N
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ DFinsupp.lsingle (p i)) = g.compLinearMap fun i ↦ DFinsupp.lsingle (p i)
x : (i : ι) → Π₀ (j : κ i), M i j
val✝ : Fintype ι
⊢ (∑ r ∈ Fintype.piFinset fun i ↦ (x i).support, f fun i ↦ DFinsupp.single (r i) ((x i) (r i))) =
    ∑ r ∈ Fintype.piFinset fun i ↦ (x i).support, g fun i ↦ DFinsupp.single (r i) ((x i) (r i))
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
x y : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ { toFun := fun p ↦ (f p) fun i_1 ↦ (Function.update m i (x + y) i_1) (p i_1),
        support' :=
          Trunc.map (fun s ↦ ⟨Multiset.map (fun f i ↦ f i ⋯) (Finset.univ.val.pi fun i_1 ↦ ↑(s i_1)), ⋯⟩)
            (Trunc.finChoice fun i_1 ↦ (Function.update m i (x + y) i_1).support') }
      p =
    ({ toFun := fun p ↦ (f p) fun i_1 ↦ (Function.update m i x i_1) (p i_1),
          support' :=
            Trunc.map (fun s ↦ ⟨Multiset.map (fun f i ↦ f i ⋯) (Finset.univ.val.pi fun i_1 ↦ ↑(s i_1)), ⋯⟩)
              (Trunc.finChoice fun i_1 ↦ (Function.update m i x i_1).support') } +
        { toFun := fun p ↦ (f p) fun i_1 ↦ (Function.update m i y i_1) (p i_1),
          support' :=
            Trunc.map (fun s ↦ ⟨Multiset.map (fun f i ↦ f i ⋯) (Finset.univ.val.pi fun i_1 ↦ ↑(s i_1)), ⋯⟩)
              (Trunc.finChoice fun i_1 ↦ (Function.update m i y i_1).support') })
      p

Tactic:
dsimp

Goal state after:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
x y : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ ((f p) fun i_1 ↦ (Function.update m i (x + y) i_1) (p i_1)) =
    ((f p) fun i_1 ↦ (Function.update m i x i_1) (p i_1)) + (f p) fun i_1 ↦ (Function.update m i y i_1) (p i_1)
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
c : R
x : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ { toFun := fun p ↦ (f p) fun i_1 ↦ (Function.update m i (c • x) i_1) (p i_1),
        support' :=
          Trunc.map (fun s ↦ ⟨Multiset.map (fun f i ↦ f i ⋯) (Finset.univ.val.pi fun i_1 ↦ ↑(s i_1)), ⋯⟩)
            (Trunc.finChoice fun i_1 ↦ (Function.update m i (c • x) i_1).support') }
      p =
    (c •
        { toFun := fun p ↦ (f p) fun i_1 ↦ (Function.update m i x i_1) (p i_1),
          support' :=
            Trunc.map (fun s ↦ ⟨Multiset.map (fun f i ↦ f i ⋯) (Finset.univ.val.pi fun i_1 ↦ ↑(s i_1)), ⋯⟩)
              (Trunc.finChoice fun i_1 ↦ (Function.update m i x i_1).support') })
      p

Tactic:
dsimp

Goal state after:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
c : R
x : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ ((f p) fun i_1 ↦ (Function.update m i (c • x) i_1) (p i_1)) = c • (f p) fun i_1 ↦ (Function.update m i x i_1) (p i_1)