mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ Sum.inr ((ofInjective Sum.inr ⋯).symm (σ₂' ((ofInjective Sum.inr ⋯).symm.symm b))) = σ (Sum.inr b)

Tactic:
Equiv.symm_symm,

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 ((ofInjective Sum.inr ⋯).symm (σ₂' ((ofInjective Sum.inr ⋯) b))) = σ (Sum.inr b)
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ (l.rotate (n + 1)).formPerm = l.formPerm

Tactic:
← rotate_rotate,

Goal state after:
case succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ ((l.rotate n).rotate 1).formPerm = l.formPerm
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
g : Perm α
⊢ g ∈ ofSubtype.range ↔ ↑g.support ⊆ Set.ofPred p

Tactic:
by
  constructor
  · rintro ⟨k, rfl⟩ x
    simp only [Finset.mem_coe, mem_support_ofSubtype, Set.mem_ofPred_eq]
    exact fun ⟨hx, _⟩ ↦ hx
  · intro hg
    refine ⟨g.subtypePerm fun x ↦ ?_, ofSubtype_subtypePerm _ fun x hx ↦ hg (mem_support.mpr hx)⟩
    by_cases hx : g x = x
    · rw [hx]
    · refine iff_of_true (hg ?_) (hg ?_) <;> simpa

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : Finite α
f : Perm α
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
⊢ (fun x ↦ signAux2 l₁ f) ≍ fun x ↦ signAux2 l₂ f

Tactic:
rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩
    refine Function.hfunext (forall_congr fun _ ↦ propext h.mem_iff) fun h₁ h₂ _ ↦ ?_
    rw [← signAux_eq_signAux2 _ _ e fun _ _ => h₁ _, ← signAux_eq_signAux2 _ _ e fun _ _ => h₂ _]

Goal state after:
Module: Mathlib.Tactic.Group

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
n m : ℤ
⊢ a * b ^ n * b ^ m = a * b ^ (n + m)

Tactic:
by rw [mul_assoc, ← zpow_add]

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

Goal state before:
pp: case pos
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    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)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
ha' : a = a
⊢ (prodExtendRight a (σ a)) (a, b) = (a, (σ a) b)

Tactic:
prodExtendRight_apply_eq

Goal state after:
case pos
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    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)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
ha' : a = a
⊢ (a, (σ a) b) = (a, (σ a) b)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a a_1, σ.cycleFactorsFinset.val = {a_1}.val ∧ (Finset.card ∘ support) a_1 = a) ↔ σ.IsCycle

Tactic:
Finset.val_inj,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a a_1, σ.cycleFactorsFinset = {a_1} ∧ (Finset.card ∘ support) a_1 = a) ↔ σ.IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : g x ∈ c.support
⊢ x ∈ c.support

Tactic:
exact (hc' x).mp hx

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

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ f.cycleOf x ∈ f.cycleFactorsFinset

Tactic:
cycleOf_mem_cycleFactorsFinset_iff,

Goal state after:
case neg.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ x ∈ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ (m - n)) x = x ↔ ↑(#(g.cycleOf x).support) ∣ m - n

Tactic:
rw [← cycleOf_zpow_apply_self g x, cycle_zpow_mem_support_iff]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (m - n) % ↑(#(g.cycleOf x).support) = 0 ↔ ↑(#(g.cycleOf x).support) ∣ m - n

case hg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g.cycleOf x).IsCycle

case hx
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g.cycleOf x) x ≠ x
Module: Mathlib.GroupTheory.Perm.Fin

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

Tactic:
split_ifs with ch

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

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

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

Tactic:
have hj1 : (i + 1).1 = i.1 + 1 := val_add_one_of_lt' (by lia)
    have hj2 : (i.castLT (by lia) + 1 : Fin (j + 1)).1 =
      (i.castLT (by lia) : Fin (j + 1)) + 1 := val_add_one_of_lt' (by simp; lia)
    exact eq_of_val_eq (by simp [← this, hj1, hj2])

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

Goal state before:
pp: case succ
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
⊢ ↑(j.cycleRange i) = if i = j then 0 else ↑i + 1

Tactic:
rw [cycleRange_of_le h]

Goal state after:
case succ
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
⊢ ↑(if i = j then 0 else i + 1) = if i = j then 0 else ↑i + 1
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
⊢ ↑(Fin.cast ⋯ ((((j - i).castLT ⋯).cycleRange (subNat (↑i) (Fin.cast ⋯ k) ⋯)).addNat (n - (n - ↑i)))) =
    ↑(if k = j then i else k + 1)

Tactic:
split_ifs with ch

Goal state after:
case pos
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
ch : k = j
⊢ ↑(Fin.cast ⋯ ((((j - i).castLT ⋯).cycleRange (subNat (↑i) (Fin.cast ⋯ k) ⋯)).addNat (n - (n - ↑i)))) = ↑i

case neg
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
ch : ¬k = j
⊢ ↑(Fin.cast ⋯ ((((j - i).castLT ⋯).cycleRange (subNat (↑i) (Fin.cast ⋯ k) ⋯)).addNat (n - (n - ↑i)))) = ↑(k + 1)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Odd n
⊢ (-(-1) ^ n) ^ σ.cycleType.card =
    if Odd n then 1 else (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / n)

Tactic:
rw [if_pos h, h.neg_one_pow, neg_neg, one_pow]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ^ 2 = 1
⊢ sign σ = (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / 2)

Tactic:
rw [sign_of_cycleType_eq_replicate zero_lt_two (cycleType_of_pow_prime_eq_one hσ),
    if_neg (Nat.not_odd_iff.mpr rfl)]

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

Goal state before:
pp: case neg
α : Type u_4
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : ¬σ.IsCycle
⊢ σ ∈ l₁ ↔ σ ∈ l₂

Tactic:
exact iff_of_false (mt (h₁l₁ σ) hσ) (mt (h₁l₂ σ) hσ)

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

Goal state before:
pp: case neg
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this✝ :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
ch : ¬k = j
this : subNat (↑i) (Fin.cast ⋯ k) ⋯ < (j - i).castLT ⋯
⊢ ↑(Fin.cast ⋯ ((((j - i).castLT ⋯).cycleRange (subNat (↑i) (Fin.cast ⋯ k) ⋯)).addNat (n - (n - ↑i)))) = ↑(k + 1)

Tactic:
rw [cycleRange_of_lt this, subNat]

Goal state after:
case neg
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this✝ :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
ch : ¬k = j
this : subNat (↑i) (Fin.cast ⋯ k) ⋯ < (j - i).castLT ⋯
⊢ ↑(Fin.cast ⋯ ((⟨↑(Fin.cast ⋯ k) - ↑i, ⋯⟩ + 1).addNat (n - (n - ↑i)))) = ↑(k + 1)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ g.cycleOf x ≠ 1 ↔ g.cycleOf x ∈ g.cycleFactorsFinset

Tactic:
cycleOf_mem_cycleFactorsFinset_iff,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ g.cycleOf x ≠ 1 ↔ x ∈ g.support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.cycleFactorsFinset g.cycleFactorsFinset

Tactic:
rw [disjoint_iff_disjoint_support] at h

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
⊢ _root_.Disjoint f.cycleFactorsFinset g.cycleFactorsFinset
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.IsSwap ↔ σ.cycleType = {2}

Tactic:
by
  constructor
  · intro h
    simpa [h.isCycle.cycleType, card_support_eq_two] using h
  · intro h
    simp [← card_support_eq_two, ← sum_cycleType, h]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
⊢ ∀ (x : α), d x ∈ c.support ↔ x ∈ c.support

Tactic:
by
  intro x
  simp only [mem_support, not_iff_not]
  by_cases h : c = d
  · rw [← h, EmbeddingLike.apply_eq_iff_eq]
  · rw [← Perm.mul_apply,
      Commute.eq (cycleFactorsFinset_mem_commute g hc hd h),
      mul_apply, EmbeddingLike.apply_eq_iff_eq]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
fapply Quot.lift

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

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
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
fapply Quot.lift

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

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
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
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
i : ι
hi : i = i₀
⊢ B i ⊆ A i

Tactic:
rw [hi]
      simp only [B, Finset.sdiff_subset, update_self]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
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
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
A_eq_BC : (fun i ↦ ∑ j ∈ A i, g i j) = update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)
i : ι
hi : ¬i = i₀
⊢ update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) i = ∑ j ∈ B i, g i j

Tactic:
· simp only [B, hi, update_of_ne, Ne, not_false_iff]

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
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : ¬σ = τ⁻¹
⊢ IsAddUnit ((∏ k, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Tactic:
eq_inv_iff_mul_eq_one

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
h : ¬σ * τ = 1
⊢ IsAddUnit ((∏ k, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: case mp
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
⊢ (∃ k f g, (hom (F.map f)) x = (hom (F.map g)) y) → ∃ j f, (hom (F.map f)) x = (hom (F.map f)) y

Tactic:
rintro ⟨k, f, g, h⟩
    refine ⟨IsFiltered.coeq f g, f ≫ IsFiltered.coeqHom f g, ?_⟩
    conv_rhs => rw [IsFiltered.coeq_condition]
    simp [h]

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

Goal state before:
pp: case e'_3.refine_2
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ Set.InjOn (fun σ ↦ σ.1.sumCongr σ.2) ↑univ

pp: case e'_3.refine_3
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ Set.SurjOn (fun σ ↦ σ.1.sumCongr σ.2) ↑univ ↑(↑(sumCongrHom m n).range).toFinset

pp: case e'_3.refine_4
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ ∀ a ∈ univ,
    (↑↑(sign a.1) * ∏ i, A (a.1 i) i) * (↑↑(sign a.2) * ∏ i, D (a.2 i) i) =
      ↑↑(sign (a.1.sumCongr a.2)) * ∏ i, fromBlocks A B 0 D ((a.1.sumCongr a.2) i) i

Tactic:
· intro σ₁ _ σ₂ _
        dsimp only
        intro h
        have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x :=
          DFunLike.congr_fun h
        simp only [Sum.map_inr, Sum.map_inl, Perm.sumCongr_apply, Sum.forall, Sum.inl.injEq,
          Sum.inr.injEq] at h2
        ext x
        · exact h2.left x
        · exact h2.right x

Goal state after:
case e'_3.refine_3
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ Set.SurjOn (fun σ ↦ σ.1.sumCongr σ.2) ↑univ ↑(↑(sumCongrHom m n).range).toFinset

case e'_3.refine_4
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ ∀ a ∈ univ,
    (↑↑(sign a.1) * ∏ i, A (a.1 i) i) * (↑↑(sign a.2) * ∏ i, D (a.2 i) i) =
      ↑↑(sign (a.1.sumCongr a.2)) * ∏ i, fromBlocks A B 0 D ((a.1.sumCongr a.2) i) i
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y, sign (decomposeFin.symm (i.succ, y)) • ∏ x, A ((decomposeFin.symm (i.succ, y)) x) x =
    -1 *
      ∑ i_1,
        A i.succ 0 *
          sign i_1 • ∏ i_2, (of fun i_3 j ↦ A (i.succ.succAbove i_3) j.succ).submatrix (⇑i.cycleRange) id (i_1 i_2) i_2

Tactic:
Finset.mul_sum

Goal state after:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y, sign (decomposeFin.symm (i.succ, y)) • ∏ x, A ((decomposeFin.symm (i.succ, y)) x) x =
    ∑ i_1,
      -1 *
        (A i.succ 0 *
          sign i_1 • ∏ i_2, (of fun i_3 j ↦ A (i.succ.succAbove i_3) j.succ).submatrix (⇑i.cycleRange) id (i_1 i_2) i_2)
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ (k : Cᵒᵖ), PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (yoneda ⋙ (evaluation Cᵒᵖ (Type v)).obj k)

Tactic:
intro K

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Cᵒᵖ
⊢ PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (yoneda ⋙ (evaluation Cᵒᵖ (Type v)).obj K)
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ (k : C), PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (coyoneda ⋙ (evaluation C (Type v)).obj k)

Tactic:
intro K

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : C
⊢ PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (coyoneda ⋙ (evaluation C (Type v)).obj K)
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ (k : Cᵒᵖ),
    PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
      (uliftYoneda.{w', v, u} ⋙ (evaluation Cᵒᵖ (Type (max w' v))).obj k)

Tactic:
intro K

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Cᵒᵖ
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
    (uliftYoneda.{w', v, u} ⋙ (evaluation Cᵒᵖ (Type (max w' v))).obj K)
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ (k : C),
    PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
      (uliftCoyoneda.{w', v, u} ⋙ (evaluation C (Type (max w' v))).obj k)

Tactic:
intro K

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : C
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
    (uliftCoyoneda.{w', v, u} ⋙ (evaluation C (Type (max w' v))).obj K)
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: case refine_2.refine_2
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
⊢ ∀ (s : Cone F),
    (forget MonCat).map
        (ofHom
          {
            toFun :=
              ⇑(ConcreteCategory.hom
                  ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s))),
            map_one' := ⋯, map_mul' := ⋯ }) =
      (Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s)

Tactic:
· exact fun _ ↦ rfl

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : Category.{t, v} J
F : J ⥤ ModuleCat R
c : Cone F
hc : IsLimit ((forget₂ (ModuleCat R) AddCommGrpCat).mapCone c)
⊢ IsLimit c

Tactic:
have : HasLimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) := ⟨_, hc⟩
    have : Small.{w} (Functor.sections (F ⋙ forget (ModuleCat R))) := by
      simpa only [AddCommGrpCat.hasLimit_iff_small_sections] using! this
    have := reflectsLimit_of_reflectsIsomorphisms F (forget₂ (ModuleCat R) AddCommGrpCat)
    exact isLimitOfReflects _ hc

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

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
i : ι
⊢ ↟(f i i ⋯) = 𝟙 (of R (G i))

Tactic:
ext
    apply Module.DirectedSystem.map_self

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X = Y
Z : C
⊢ eqToHom f ▷ Z = eqToHom ⋯

Tactic:
cases f
  simp only [id_whiskerRight, eqToHom_refl]

Goal state after: