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
σ τ : Type
inst✝³ : Finite τ
S : σ → C
inst✝² : HasBiproduct S
T : τ → C
inst✝¹ : HasBiproduct T
s : σ
f : ⨁ S ⟶ ⨁ T
inst✝ : IsIso f
val✝ : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
⊢ x = 0

Tactic:
dsimp [x]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
σ τ : Type
inst✝³ : Finite τ
S : σ → C
inst✝² : HasBiproduct S
T : τ → C
inst✝¹ : HasBiproduct T
s : σ
f : ⨁ S ⟶ ⨁ T
inst✝ : IsIso f
val✝ : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
⊢ biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s = 0
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n a : ℕ
ha1 : 1 ≤ a
ha : a ≤ n
p : { p // a ∈ p.parts }
⊢ ((partitionWithPartEquiv ha1 ha) p).parts = (↑p).parts.erase a

Tactic:
dsimp [partitionWithPartEquiv]

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

Goal state before:
pp: n a : ℕ
ha1 : 1 ≤ a
ha : a ≤ n
p : (n - a).Partition
⊢ (↑((partitionWithPartEquiv ha1 ha).symm p)).parts = a ::ₘ p.parts

Tactic:
dsimp [partitionWithPartEquiv]

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

Goal state before:
pp: case h₁
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✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Mono (F.biprodComparison X Y)
⊢ prodComparison F X Y ≫ prod.fst =
    ((F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom) ≫ prod.fst

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h₂
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✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Mono (F.biprodComparison X Y)
⊢ prodComparison F X Y ≫ prod.snd =
    ((F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom) ≫ prod.snd

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: α : Type u_1
l : List α
c : Composition l.length
i : ℕ
⊢ (take i (map length (l.splitWrtComposition c))).sum = c.sizeUpTo i

Tactic:
by
  congr
  exact map_length_splitWrtComposition l c

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 α}, (n :: ns).sum = l.length → (l.splitWrtCompositionAux (n :: ns)).flatten = l

Tactic:
intro l

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 α
⊢ (n :: ns).sum = l.length → (l.splitWrtCompositionAux (n :: ns)).flatten = l
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
this : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
⊢ Equiv.swap a (f a) * (Equiv.swap a (f a) * f) = f

Tactic:
rw [← mul_assoc, mul_def (Equiv.swap a (f a)) (Equiv.swap a (f a)), Equiv.swap_swap,
      ← Perm.one_def, one_mul]

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

Goal state before:
pp: case zero
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
⊢ swap ((σ ^ 0) x) ((σ ^ (0 + 1)) x) ∈ H

Tactic:
exact subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))

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

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
hf' : Nat.Prime (orderOf f)
n : ℕ
hn : 0 < n
hn' : n < orderOf f
⊢ (f ^ n).IsCycle

Tactic:
cases nonempty_fintype β
  have : n.Coprime (orderOf f) := by
    refine Nat.Coprime.symm ?_
    rw [Nat.Prime.coprime_iff_not_dvd hf']
    exact Nat.not_dvd_of_pos_of_lt hn hn'
  exact (pow_iff hf).mpr this

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case insert.inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i✝ : ι
s : Finset ι
hnotMem : i✝ ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i✝ s)).Pairwise (Function.onFun Commute f)
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem : f i✝ ∈ K i✝ ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1 : f i✝ * s.noncommProd f ⋯ = 1
hnotMem' : i✝ ∉ ↑s
heq1i : f i✝ = 1
heq1S : s.noncommProd f hcomm = 1
i : ι
h : i ∈ s
⊢ f i = 1

Tactic:
· refine ih hcomm hmem.2 heq1S _ h

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case convert_4
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)
f g : (i : ι) → N i
⊢ (↑Finset.univ).Pairwise fun x y ↦ Commute ((ϕ x) (g x)) ((ϕ y) (f y))

Tactic:
· rintro i - j - h
      exact hcomm h _ _

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ (ofSign 1).disjUnion (ofSign (-1)) ⋯ = univ

Tactic:
ext σ

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ σ ∈ (ofSign 1).disjUnion (ofSign (-1)) ⋯ ↔ σ ∈ univ
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ n / ↑1 = ↑n

Tactic:
Nat.cast_one,

Goal state after:
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ n / 1 = ↑n
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
a b : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ ↑s
hb : b ∈ ↑s
⊢ ∃ n, (f ^ n) a = b

Tactic:
obtain ⟨n, -, hn⟩ := hf.exists_pow_eq ha hb

Goal state after:
α : Type u_2
f : Perm α
a b : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ ↑s
hb : b ∈ ↑s
n : ℕ
hn : (f ^ n) a = b
⊢ ∃ n, (f ^ n) a = b
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
s : Finset ι
σ : Perm ι
hσ : σ.IsCycleOn ↑s
f : ι → α
g : ι → β
⊢ ∑ i ∈ s, ∑ j ∈ s, f i • g j = ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i)

Tactic:
← sum_product'

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
s : Finset ι
σ : Perm ι
hσ : σ.IsCycleOn ↑s
f : ι → α
g : ι → β
⊢ ∑ x ∈ s ×ˢ s, f x.1 • g x.2 = ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : f x = x
this : Nonempty α
⊢ ∃ m < Fintype.card α, (f ^ m) x = y

Tactic:
exact ⟨0, Fintype.card_pos, hxy.eq_of_left hx⟩

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

Goal state before:
pp: case mpr
ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
⊢ f.SameCycle x y → ∃ m < Fintype.card α, (f ^ m) x = y

Tactic:
intro hxy
      by_cases hx : x ∈ f.support
      case pos =>
        -- we can't invoke the aux lemmas above without obtaining the decidable instance we are
        -- already building; but now we've left the data, so we can do this non-constructively
        -- without sacrificing computability.
        let _inst (f : Perm α) : DecidableRel (SameCycle f) := Classical.decRel _
        rcases hxy.exists_pow_eq_of_mem_support_aux hx with ⟨i, hixy, hi⟩
        refine ⟨i, lt_of_lt_of_le hixy (card_le_univ _), hi⟩
      case neg =>
        have : Nonempty α := ⟨x⟩
        rw [notMem_support] at hx
        exact ⟨0, Fintype.card_pos, hxy.eq_of_left hx⟩

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

Goal state before:
pp: n : ℕ
⊢ (finRotate (n + 2)).IsCycle

Tactic:
by
  refine ⟨0, by simp, fun x hx' => ⟨x, ?_⟩⟩
  clear hx'
  obtain ⟨x, hx⟩ := x
  rw [zpow_natCast, Fin.ext_iff, Fin.val_mk]
  induction x with
  | zero => rfl
  | succ x ih =>
    rw [pow_succ', Perm.mul_apply, coe_finRotate_of_ne_last, ih (lt_trans x.lt_succ_self hx)]
    rw [Ne, Fin.ext_iff, ih (lt_trans x.lt_succ_self hx), Fin.val_last]
    exact ne_of_lt (Nat.lt_of_succ_lt_succ hx)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
m : ℕ
hm : orderOf σ = p ^ m
l : ℕ
hk : p ^ l ∈ σ.cycleType
⊢ p ∣ p ^ l

Tactic:
exact dvd_pow_self _ fun h => (one_lt_of_mem_cycleType hk).ne <| by rw [h, pow_zero]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ n = 1
this : fixedPoints f = ↑(support σ)ᶜ
⊢ Fintype.card ↑(fixedPoints f) = #(support σ)ᶜ

Tactic:
by
    simp only [this]; apply Fintype.card_coe

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

Goal state before:
pp: case refine_1
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
⊢ (∃ a, ∃ b < a, max (σ a) (σ b) = x1 ∧ min (σ a) (σ b) = x2) → x2 < x1

Tactic:
rintro ⟨i, j, hij, rfl, rfl⟩

Goal state after:
case refine_1
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
i j : Fin n
hij : j < i
⊢ min (σ i) (σ j) < max (σ i) (σ j)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h : IsThreeCycle 1
⊢ False

Tactic:
simpa using h.cycleType

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

Goal state before:
pp: case intro
β : Type u_3
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val✝ : Fintype β
⊢ ∀ (l : List (Perm β)), (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod

Tactic:
intro l

Goal state after:
case intro
β : Type u_3
inst✝ : Finite β
P : Perm β → Prop
σ : Perm β
base_one : P 1
base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ
induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)
val✝ : Fintype β
l : List (Perm β)
⊢ (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
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
⊢ ∏ i, ∏ j > i, f (σ i) (σ j) = ↑↑(sign σ) * ∏ i, ∏ j > i, f i j

Tactic:
convert! σ.prod_Iio_comp_eq_sign_mul_prod hf using 1

Goal state after:
case e'_2
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
⊢ ∏ i, ∏ j > i, f (σ i) (σ j) = ∏ j, ∏ i < j, f (σ i) (σ j)

case e'_3
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
⊢ ↑↑(sign σ) * ∏ i, ∏ j > i, f i j = ↑↑(sign σ) * ∏ j, ∏ i < j, f i j
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case e'_3
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
⊢ ↑↑(sign σ) * ∏ i, ∏ j > i, f i j = ↑↑(sign σ) * ∏ j, ∏ i < j, f i j

Tactic:
convert! rfl using 2

Goal state after:
case e'_3
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
⊢ ∏ j, ∏ i < j, f i j = ∏ i, ∏ j > i, f i j
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : Nonempty ι
i : ι
h✝ : i ∈ Set.univ
⊢ f 0 = 0

Tactic:
exact map_coord_zero f i rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: case e'_2.h
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix (Option n) (Option n) R
i : Option n
⊢ {x ∈ ofSign s | x none = i} = Finset.image (fun σ ↦ decomposeOption.symm (i, σ)) (ofSign (sign (swap none i) * s))

Tactic:
ext σ

Goal state after:
case e'_2.h
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix (Option n) (Option n) R
i : Option n
σ : Perm (Option n)
⊢ σ ∈ {x ∈ ofSign s | x none = i} ↔
    σ ∈ Finset.image (fun σ ↦ decomposeOption.symm (i, σ)) (ofSign (sign (swap none i) * s))
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case f
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
⊢ Prequotient F → ↑s.pt

pp: case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
⊢ ∀ (a b : Prequotient F), (colimitSetoid F) a b → ?f a = ?f b

Tactic:
· exact descFunLift F s

Goal state after:
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
⊢ ∀ (a b : Prequotient F), (colimitSetoid F) a b → descFunLift F s a = descFunLift F s b
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case pos
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
Ai_singleton : ∀ (i : ι), #(A i) ≤ 1
⊢ (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)

pp: case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
Ai_singleton : ∃ i, 1 < #(A i)
⊢ (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)

Tactic:
· have Ai_card : ∀ i, #(A i) = 1 := by
      intro i
      have pos : #(A i) ≠ 0 := by rw [Finset.card_ne_zero]; exact Ai_empty i
      have : #(A i) ≤ 1 := Ai_singleton i
      exact le_antisymm this (Nat.succ_le_of_lt (_root_.pos_iff_ne_zero.mpr pos))
    have :
      ∀ r : ∀ i, α i, r ∈ piFinset A → (f fun i => g i (r i)) = f fun i => ∑ j ∈ A i, g i j := by
      intro r hr
      congr with i
      have : ∀ j ∈ A i, g i j = g i (r i) := by
        intro j hj
        congr
        apply Finset.card_le_one_iff.1 (Ai_singleton i) hj
        exact mem_piFinset.mp hr i
      simp only [Finset.sum_congr rfl this, Finset.sum_const, Ai_card i, one_nsmul]
    simp only [Finset.sum_congr rfl this, Ai_card, card_piFinset, prod_const_one, one_nsmul,
      Finset.sum_const]

Goal state after:
case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
Ai_singleton : ∃ i, 1 < #(A i)
⊢ (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case f
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
⊢ Prequotient F → ↑s.pt

pp: case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
⊢ ∀ (a b : Prequotient F), (colimitSetoid F) a b → ?f a = ?f b

Tactic:
· exact descFunLift F s

Goal state after:
case a
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
⊢ ∀ (a b : Prequotient F), (colimitSetoid F) a b → descFunLift F s a = descFunLift F s b
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
σ : Perm n
x✝ : σ ∈ univ
τ : Perm n
this : ∏ j, M (τ j) (σ j) = ∏ j, M ((τ * σ⁻¹) j) j
⊢ ↑↑(sign σ) * ↑↑(sign (τ * σ⁻¹)) = ↑↑(sign (τ * σ⁻¹ * σ))

Tactic:
by
                rw [mul_comm, sign_mul (τ * σ⁻¹)]
                simp only [Int.cast_mul, Units.val_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix (Option n) (Option n) R
⊢ ∑ j, A none j * adjp s A j none =
    A none none * detp s (A.submatrix some some) +
      ∑ k, A none (some k) * detp (-s) (A.submatrix some (Function.update some k none))

Tactic:
Fintype.sum_option,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix (Option n) (Option n) R
⊢ A none none * adjp s A none none + ∑ i, A none (some i) * adjp s A (some i) none =
    A none none * detp s (A.submatrix some some) +
      ∑ k, A none (some k) * detp (-s) (A.submatrix some (Function.update some k none))
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
u v : n → R
⊢ (M.updateCol j (u + v)).det = (M.updateCol j u).det + (M.updateCol j v).det

Tactic:
rw [← det_transpose, ← updateRow_transpose, det_updateRow_add]
  simp [updateRow_transpose, det_transpose]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
j : n
c : n → R
⊢ ∑ k, c k • A k = c j • A j + ∑ k ∈ univ.erase j, c k • A k

Tactic:
rw [← Finset.univ.add_sum_erase _ (Finset.mem_univ j)]

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ (IsFiltered.coeqHom f.unop g.unop).op ≫ f = (IsFiltered.coeqHom f.unop g.unop).op ≫ g

Tactic:
show f = f.unop.op by simp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ (IsFiltered.coeqHom f.unop.op.unop g.unop).op ≫ f.unop.op = (IsFiltered.coeqHom f.unop.op.unop g.unop).op ≫ g
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ f ≫ (IsCofiltered.eqHom f.unop g.unop).op = g ≫ (IsCofiltered.eqHom f.unop g.unop).op

Tactic:
show f = f.unop.op by simp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ f.unop.op ≫ (IsCofiltered.eqHom f.unop.op.unop g.unop).op = g ≫ (IsCofiltered.eqHom f.unop.op.unop g.unop).op
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: case mpr.refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : F.CoconeTypes
hc : Limits.IsColimit (F.coconeTypesEquiv c)
x y : F.ColimitType
h : F.descColimitType c x = F.descColimitType c y
⊢ x = y

Tactic:
let f (z : F.ColimitType) : ULift.{u} Bool := ULift.up (x = z)
      suffices f x = f y by simpa [f] using this
      suffices ∀ z, hc.desc (F.coconeTypesEquiv (F.coconeTypes.postcomp f))
          (F.descColimitType c z) = f z by rw [← this x, h, ← this y]
      intro z
      obtain ⟨j, z, rfl⟩ := F.ιColimitType_jointly_surjective z
      exact ConcreteCategory.congr_hom (hc.fac _ j) z

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : (hom (F.map f)) x.snd = (hom (F.map g)) y.snd
⊢ Relation.EqvGen F.ColimitTypeRel x y

Tactic:
refine Relation.EqvGen.trans _ ⟨k, F.map f x.2⟩ _ ?_ ?_

Goal state after:
case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : (hom (F.map f)) x.snd = (hom (F.map g)) y.snd
⊢ Relation.EqvGen F.ColimitTypeRel x ⟨k, (hom (F.map f)) x.snd⟩

case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : (hom (F.map f)) x.snd = (hom (F.map g)) y.snd
⊢ Relation.EqvGen F.ColimitTypeRel ⟨k, (hom (F.map f)) x.snd⟩ y
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
hsurj : ∀ (x : t.pt), ∃ i xi, x = (hom (t.ι.app i)) xi
hinj :
  ∀ (i j : J) (xi : (fun X ↦ X) (F.obj i)) (xj : (fun X ↦ X) (F.obj j)),
    (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj → ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj
α : t.pt → J := fun x ↦ ⋯.choose
f : (x : t.pt) → F.obj (α x) := fun x ↦ ⋯.choose
hf : ∀ (x : t.pt), x = (hom (t.ι.app (α x))) (f x)
s : Cocone F
j : J
y : F.obj j
k : J
l : j ⟶ k
g : α ((hom (t.ι.app j)) y) ⟶ k
eq : (hom (F.map l)) y = (hom (F.map g)) (f ((hom (t.ι.app j)) y))
h :
  (hom (s.ι.app k)) ((hom (F.map g)) (f ((hom (t.ι.app j)) y))) =
    (hom (s.ι.app (α ((hom (t.ι.app j)) y)))) (f ((hom (t.ι.app j)) y))
h' : (hom (s.ι.app k)) ((hom (F.map l)) y) = (hom (s.ι.app j)) y
⊢ (hom (s.ι.app (α ((hom (t.ι.app j)) y)))) (f ((hom (t.ι.app j)) y)) = (hom (s.ι.app j)) y

Tactic:
rw [← h, ← eq, h']

Goal state after: