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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝ : F.IsEquivalence
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
this✝ : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)
this : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e)
⊢ (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e) ≫ F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y = f

Tactic:
by
            simp only [Category.assoc, ← F.map_comp_assoc,
              MonoFactorisation.fac, fun_inv_map, id_obj, Iso.inv_hom_id_app, Category.comp_id,
              Iso.inv_hom_id_app_assoc]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P✝ : IsIsomorphic X 0
P : X ≅ 0
⊢ 0 ≫ 0 = P.hom ≫ 𝟙 0 ≫ P.inv

Tactic:
apply Eq.symm

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P✝ : IsIsomorphic X 0
P : X ≅ 0
⊢ P.hom ≫ 𝟙 0 ≫ P.inv = 0 ≫ 0
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : some j = j'
⊢ Finset (j' ⟶ j')

Tactic:
exact {Hom.id j'}

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝² : HasCokernel f✝
f g : X ⟶ Y
inst✝¹ : HasCokernel f
inst✝ : HasCokernel g
h : f = g
⊢ parallelPair f 0 ≅ parallelPair g 0

Tactic:
by simp [h]; rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone (pair X Y)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete WalkingPair), b.toCocone.ι.app j ≫ m = s.ι.app j
⊢ m = b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s

Tactic:
by
        have hₗ := h ⟨.left⟩
        have hᵣ := h ⟨.right⟩
        dsimp at hₗ hᵣ
        simpa [← hₗ, ← hᵣ] using total.symm =≫ m

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

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

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

Goal state before:
pp: case mpr
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
f : Fin (d + 1) → μ
hf : f 0 + ∑ i, f i.succ = n
⊢ ∃ a b, a + b = n ∧ ∃ a_1, ∑ i, a_1 i = b ∧ Fin.cons a a_1 = f

Tactic:
exact ⟨_, _, hf, _, rfl, Fin.cons_self_tail f⟩

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

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
⊢ f ∈ s.piAntidiag n ↔ s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Tactic:
by
  rw [piAntidiag]
  induction Fintype.truncEquivFinOfCardEq (Fintype.card_coe s) using Trunc.ind with | _ e
  simp only [Trunc.lift_mk, mem_map, mem_finAntidiagonal, Embedding.coeFn_mk]
  constructor
  · rintro ⟨f, ⟨hf, rfl⟩, rfl⟩
    rw [sum_dite_of_true fun _ ↦ id]
    exact ⟨Fintype.sum_equiv e _ _ (by simp), by simp +contextual⟩
  · rintro ⟨rfl, hf⟩
    refine ⟨f ∘ (↑) ∘ e.symm, ?_, by grind⟩
    rw [← sum_attach s]
    exact Fintype.sum_equiv e.symm _ _ (by simp)

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

Goal state before:
pp: case neg
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
i : ι
hi : i ∉ s
⊢ n ∣ f i

Tactic:
· rw [not_imp_comm.1 (hfsup _) hi]
      exact dvd_zero _

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
⊢ (f * g).support = f.support ∪ g.support

Tactic:
refine le_antisymm (support_mul_le _ _) fun a => ?_
  rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]
  exact
    (h a).elim (fun hf h => ⟨hf, f.apply_eq_iff_eq.mp (h.trans hf.symm)⟩) fun hg h =>
      ⟨(congr_arg f hg).symm.trans h, hg⟩

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

Goal state before:
pp: case pos
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∈ σ.support
⊢ ↑(f ⟨σ x, ?pos.hx✝⟩) = τ ↑(f ⟨x, ?pos.hx✝¹⟩)

Tactic:
exact hf x (Finset.mem_coe.2 hx)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g x y : Perm α
h : f.Disjoint g
hf : x.support ⊆ f.support
hg : y.support ⊆ g.support
⊢ x.Disjoint y

Tactic:
rw [disjoint_iff_disjoint_support] at h ⊢
  exact h.mono hf hg

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
w : l.Nodup
n i : ℕ
h : i < l.length
⊢ (l.formPerm ^ n) l[i] = l[(i + n) % l.length]

Tactic:
induction n with
  | zero => simp [Nat.mod_eq_of_lt h]
  | succ n hn =>
    simp [pow_succ', mul_apply, hn, formPerm_apply_getElem _ w,
      ← Nat.add_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Fintype α
⊢ ∀ (x : Equiv.Perm α), x ∈ permsOfFinset univ

Tactic:
by simp [mem_perms_of_finset_iff]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ (l.formPerm ^ l.length) l[k] = 1 l[k]

Tactic:
simp [formPerm_pow_apply_getElem _ hl, Nat.mod_eq_of_lt hk]

Goal state after:
Module: Mathlib.Data.Nat.GCD.BigOperators

Goal state before:
pp: l : List ℕ
k : ℕ
⊢ l.prod.Coprime k ↔ ∀ n ∈ l, n.Coprime k

Tactic:
by
  induction l <;> simp [Nat.coprime_mul_iff_left, *]

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ |↑(sign f)| = 1

Tactic:
rw [Int.abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]

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

Goal state before:
pp: α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
l : { l // l.prod = f.subtypePerm h₁ ∧ ∀ g ∈ l, g.IsSwap } := (f.subtypePerm h₁).truncSwapFactors.out
hl' : ∀ g' ∈ List.map ⇑ofSubtype ↑l, g'.IsSwap
⊢ sign (f.subtypePerm h₁) = sign f

Tactic:
have hl'₂ : (l.1.map ofSubtype).prod = f := by
    rw [l.1.prod_hom ofSubtype, l.2.1, ofSubtype_subtypePerm _ h₂]

Goal state after:
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
l : { l // l.prod = f.subtypePerm h₁ ∧ ∀ g ∈ l, g.IsSwap } := (f.subtypePerm h₁).truncSwapFactors.out
hl' : ∀ g' ∈ List.map ⇑ofSubtype ↑l, g'.IsSwap
hl'₂ : (List.map ⇑ofSubtype ↑l).prod = f
⊢ sign (f.subtypePerm h₁) = sign f
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
l : { l // l.prod = f.subtypePerm h₁ ∧ ∀ g ∈ l, g.IsSwap } := (f.subtypePerm h₁).truncSwapFactors.out
hl' : ∀ g' ∈ List.map ⇑ofSubtype ↑l, g'.IsSwap
hl'₂ : (List.map ⇑ofSubtype ↑l).prod = f
⊢ sign (↑l).prod = sign (List.map ⇑ofSubtype ↑l).prod

Tactic:
sign_prod_list_swap l.2.2,

Goal state after:
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
l : { l // l.prod = f.subtypePerm h₁ ∧ ∀ g ∈ l, g.IsSwap } := (f.subtypePerm h₁).truncSwapFactors.out
hl' : ∀ g' ∈ List.map ⇑ofSubtype ↑l, g'.IsSwap
hl'₂ : (List.map ⇑ofSubtype ↑l).prod = f
⊢ (-1) ^ (↑l).length = sign (List.map ⇑ofSubtype ↑l).prod
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case left.swap_mul
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih : sign (σa'.sumCongr 1) = sign σa'
⊢ sign ((swap a₁ a₂).sumCongr 1) * sign σa' = sign (swap a₁ a₂) * sign σa'

Tactic:
sumCongr_swap_one,

Goal state after:
case left.swap_mul
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih : sign (σa'.sumCongr 1) = sign σa'
⊢ sign (swap (Sum.inl a₁) (Sum.inl a₂)) * sign σa' = sign (swap a₁ a₂) * sign σa'
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case a
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)
this : DecidableEq ι := ⋯
⊢ mrange (noncommPiCoprod ϕ hcomm) ≤ ⨆ i, mrange (ϕ i)

pp: case a
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)
this : DecidableEq ι := ⋯
⊢ ⨆ i, mrange (ϕ i) ≤ mrange (noncommPiCoprod ϕ hcomm)

Tactic:
· rintro x ⟨f, rfl⟩
    refine Submonoid.noncommProd_mem _ _ _ (fun _ _ _ _ h => hcomm h _ _) (fun i _ => ?_)
    apply Submonoid.mem_sSup_of_mem
    · use i
    simp

Goal state after:
case a
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)
this : DecidableEq ι := ⋯
⊢ ⨆ i, mrange (ϕ i) ≤ mrange (noncommPiCoprod ϕ hcomm)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
a : α
n : ℕ
hn : n < #s
hx : a ∈ s ∧ (f ^ n) a ∈ s
⊢ (⇑f)^[n] a = (f ^ n) a

Tactic:
by rw [f.iterate_eq_pow]

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

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
⊢ ∃ (hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support), g.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport

Tactic:
have hgc' := mem_support_iff_of_commute hgc

Goal state after:
case mp
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
⊢ ∃ (hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support), g.subtypePerm hc' ∈ Subgroup.zpowers c.subtypePermOfSupport
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case h
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ c.support
⊢ ↑((c.subtypePerm ⋯ ^ i) ⟨x, hx⟩) = g x

Tactic:
rw [subtypePerm_apply_zpow_of_mem]

Goal state after:
case h
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
x : α
hx : x ∈ c.support
⊢ (c ^ i) x = g x
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)
⊢ -(-1) ^ a * (-1) ^ (s.sum + s.card) = (-1) ^ (a + s.sum + (s.card + 1))

Tactic:
simp only [pow_add, pow_one, neg_mul, mul_neg, mul_assoc, mul_one]

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

Goal state before:
pp: n : ℕ
α : Type u_1
x : Fin (n + 1) → α
p i : Fin (n + 1)
⊢ cons (x p) (p.removeNth x) i = (x ∘ ⇑(Equiv.symm p.cycleRange)) i

Tactic:
cases i using Fin.cons <;> simp [Fin.removeNth_apply]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.partition = τ.partition
⊢ σ.cycleType = τ.cycleType

Tactic:
· rw [← filter_parts_partition_eq_cycleType, ← filter_parts_partition_eq_cycleType, h]

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

Goal state before:
pp: case mpr.h₂.hnc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬g a = a
⊢ a ∉ {g a, g (g a)}

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton]
        contrapose ha
        rcases ha with ha | ha
        · exact ha.symm
        · suffices (g ^ 3) a = a by simpa [pow_succ, ← ha] using this
          simp [← hg3.orderOf]

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
d : n → R
⊢ detp 1 (diagonal d) = ∏ i, d i

Tactic:
by
  rw [detp, sum_eq_single_of_mem 1]
  · simp
  · simp [ofSign]
  · rintro σ - hσ1
    obtain ⟨i, hi⟩ := not_forall.mp (mt Perm.ext_iff.mpr hσ1)
    exact prod_eq_zero (mem_univ i) (diagonal_apply_ne' _ hi)

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
⊢ ⇑(MultilinearMap.alternatization ↑a) = ⇑((Fintype.card ι).factorial • a)

Tactic:
simp_rw [MultilinearMap.alternatization_def, ← coe_domDomCongr, domDomCongr_perm, coe_smul,
    smul_smul, Int.units_mul_self, one_smul, Finset.sum_const, Finset.card_univ, Fintype.card_perm,
    ← coe_multilinearMap, coe_smul]

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
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:
rw [mul_comm, sign_mul (τ * σ⁻¹)]
                simp only [Int.cast_mul, Units.val_mul]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type u_3
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
⊢ |(A.submatrix ⇑e₁ ⇑e₂).det| = |A.det|

Tactic:
by
  have hee : e₂ = e₁.trans (e₁.symm.trans e₂) := by ext; simp
  rw [hee]
  change |((A.submatrix id (e₁.symm.trans e₂)).submatrix e₁ e₁).det| = |A.det|
  rw [Matrix.det_submatrix_equiv_self, Matrix.det_permute', abs_mul, abs_unit_intCast, one_mul]

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

Goal state before:
pp: case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∉ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → T' mX ≫ f = T' mY
⊢ ∃ S T,
    ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
      ⟨X_1, ⟨Y_1, ⟨mX_1, ⟨mY_1, f_1⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H' → T mX_1 ≫ f_1 = T mY_1

Tactic:
refine ⟨eq (T' mX ≫ f) (T' mY), fun mZ => eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ, ?_⟩

Goal state after:
case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
O : Finset C
H H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
X Y : C
mX : X ∈ O
mY : Y ∈ O
f : X ⟶ Y
nmf : ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∉ H'
S' : C
T' : {X : C} → X ∈ O → (S' ⟶ X)
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → T' mX ≫ f = T' mY
⊢ ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
    ⟨X_1, ⟨Y_1, ⟨mX_1, ⟨mY_1, f_1⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H' →
      (fun {X_2} mZ ↦ eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mX_1 ≫ f_1 =
        (fun {X_2} mZ ↦ eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY_1
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case insert.x
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' : n
⊢ i' ∉ s → update c i 0 i' = 0

Tactic:
hi'

Goal state after:
case insert.x
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' : n
hi' : i' ∉ s
⊢ update c i 0 i' = 0
Module: Mathlib.CategoryTheory.Limits.Types.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
⊢ Nonempty (IsColimit c) ↔ (F.coconeTypesEquiv.symm c).IsColimit

Tactic:
by
  simp only [Functor.CoconeTypes.isColimit_iff, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F₁ F₂ : C × D ⥤ E
h : curry.obj F₁ = curry.obj F₂
⊢ F₁ = F₂

Tactic:
← uncurry_obj_curry_obj F₁,

Goal state after:
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F₁ F₂ : C × D ⥤ E
h : curry.obj F₁ = curry.obj F₂
⊢ uncurry.obj (curry.obj F₁) = F₂
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
inst✝ : CreatesColimit K F
c : Cocone (K ⋙ G)
t : IsColimit c
⊢ IsColimit ((Cocone.precompose (K.isoWhiskerLeft h).hom).obj c)

Tactic:
apply (IsColimit.precomposeHomEquiv _ _).symm t

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : Cᵒᵖ
g : X✝ ⟶ Y✝
⊢ uliftCoyoneda.{w', v, u}.map g ≫
      (NatIso.ofComponents (fun Y ↦ (Equiv.ulift.trans shrinkCoyonedaObjObjEquiv.symm).toIso) ⋯).hom =
    (NatIso.ofComponents (fun Y ↦ (Equiv.ulift.trans shrinkCoyonedaObjObjEquiv.symm).toIso) ⋯).hom ≫
      shrinkCoyoneda.{max w' v, v, u}.map g

Tactic:
by
      ext
      exact (shrinkCoyoneda_map_app_shrinkCoyonedaObjObjEquiv_symm _ _).symm

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

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ E
H : E ⥤ E'
inst✝² : F.LaxMonoidal
inst✝¹ : G.LaxMonoidal
inst✝ : H.LaxMonoidal
⊢ ε ((F ⋙ G) ⋙ H) ≫ (F.associator G H).hom.app (𝟙_ C) = ε (F ⋙ G ⋙ H)

Tactic:
simp only [comp_obj, comp_ε, assoc, Functor.map_comp, associator_hom_app, comp_id,
      Functor.comp_map]

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

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
E : Type u₃
inst✝⁶ : Category.{v₃, u₃} E
inst✝⁵ : MonoidalCategory E
E' : Type u₄
inst✝⁴ : Category.{v₄, u₄} E'
inst✝³ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝² : F₁.LaxMonoidal
inst✝¹ : F₂.LaxMonoidal
inst✝ : F₃.LaxMonoidal
X✝ Y✝ Z✝ : LaxMonoidalFunctor C D
α : X✝.Hom Y✝
β : Y✝.Hom Z✝
this : NatTrans.IsMonoidal α.hom
⊢ NatTrans.IsMonoidal (α.hom ≫ β.hom)

Tactic:
have := β.2

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
E : Type u₃
inst✝⁶ : Category.{v₃, u₃} E
inst✝⁵ : MonoidalCategory E
E' : Type u₄
inst✝⁴ : Category.{v₄, u₄} E'
inst✝³ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝² : F₁.LaxMonoidal
inst✝¹ : F₂.LaxMonoidal
inst✝ : F₃.LaxMonoidal
X✝ Y✝ Z✝ : LaxMonoidalFunctor C D
α : X✝.Hom Y✝
β : Y✝.Hom Z✝
this✝ : NatTrans.IsMonoidal α.hom
this : NatTrans.IsMonoidal β.hom
⊢ NatTrans.IsMonoidal (α.hom ≫ β.hom)
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ CommRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget CommRingCat).sections
⊢ IsLimit ((forget₂ CommRingCat CommSemiRingCat).mapCone (limitCone F))

Tactic:
by
  let _ : Small.{u} ((F ⋙ forget₂ _ CommSemiRingCat) ⋙ forget _).sections :=
    inferInstanceAs <| Small.{u} (F ⋙ forget _).sections
  apply CommSemiRingCat.limitConeIsLimit (F ⋙ forget₂ CommRingCat CommSemiRingCat.{u})

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : ModuleCat R
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
rw [epi_iff_range_eq_top, LinearMap.range_eq_top]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F G : C ⥤ D
i : F ≅ G
inst✝² : F.LaxBraided
inst✝¹ : G.LaxMonoidal
inst✝ : NatTrans.IsMonoidal i.hom
X Y : C
this : ∀ (X Y : C), μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)
⊢ μ G X Y ≫ G.map (β_ X Y).hom = (β_ (G.obj X) (G.obj Y)).hom ≫ μ G Y X

Tactic:
rw [this X Y, this Y X, ← braiding_naturality_assoc, ← Functor.LaxBraided.braided_assoc]

Goal state after:
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F G : C ⥤ D
i : F ≅ G
inst✝² : F.LaxBraided
inst✝¹ : G.LaxMonoidal
inst✝ : NatTrans.IsMonoidal i.hom
X Y : C
this : ∀ (X Y : C), μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)
⊢ ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)) ≫ G.map (β_ X Y).hom =
    (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ F.map (β_ X Y).hom ≫ i.hom.app (Y ⊗ X)