mathlib-initiative/mathlib-tactics huggingface dataset:
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
X Y : C
b : Bicone (pairFunction X Y)
x✝ : b.toBinaryBicone.IsBilimit
h : IsLimit b.toBinaryBicone.toCone
h' : IsColimit b.toBinaryBicone.toCocone
⊢ (fun h ↦
        { isLimit := b.toBinaryBiconeIsLimit.symm h.isLimit, isColimit := b.toBinaryBiconeIsColimit.symm h.isColimit })
      ((fun h ↦ { isLimit := b.toBinaryBiconeIsLimit h.isLimit, isColimit := b.toBinaryBiconeIsColimit h.isColimit })
        { isLimit := h, isColimit := h' }) =
    { isLimit := h, isColimit := h' }

Tactic:
by dsimp only; 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
X Y : C
b : Bicone (pairFunction X Y)
x✝ : b.IsBilimit
h : IsLimit b.toCone
h' : IsColimit b.toCocone
⊢ (fun h ↦ { isLimit := b.toBinaryBiconeIsLimit h.isLimit, isColimit := b.toBinaryBiconeIsColimit h.isColimit })
      ((fun h ↦
          { isLimit := b.toBinaryBiconeIsLimit.symm h.isLimit,
            isColimit := b.toBinaryBiconeIsColimit.symm h.isColimit })
        { isLimit := h, isColimit := h' }) =
    { isLimit := h, isColimit := h' }

Tactic:
by dsimp only; simp

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

Goal state before:
pp: J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D✝ : Type uD
inst✝⁸ : Category.{uD', uD} D✝
inst✝⁷ : HasZeroMorphisms D✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
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
⊢ HasZeroObject C

Tactic:
refine ⟨⟨biproduct Empty.elim, fun X => ⟨⟨⟨0⟩, ?_⟩⟩, fun X => ⟨⟨⟨0⟩, ?_⟩⟩⟩⟩
  · intro a; apply biproduct.hom_ext'; simp
  · intro a; apply biproduct.hom_ext; simp

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

Goal state before:
pp: case refine_2
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
s : Finset ι
n : μ
e₁ e₂ : ↥s ≃ Fin #s
⊢ map { toFun := fun f i ↦ if hi : i ∈ s then f (e₁ ⟨i, hi⟩) else 0, inj' := ⋯ } (finAntidiagonal (#s) n) =
    map { toFun := fun f i ↦ if hi : i ∈ s then f (e₂ ⟨i, hi⟩) else 0, inj' := ⋯ } (finAntidiagonal (#s) n)

Tactic:
ext f
    simp only [mem_map, mem_finAntidiagonal]
    refine Equiv.exists_congr ((e₁.symm.trans e₂).arrowCongr <| .refl _) fun g ↦ ?_
    have := Fintype.sum_equiv (e₂.symm.trans e₁) _ g fun _ ↦ rfl
    simp_all

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

Goal state before:
pp: α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
⊢ (f * g) x = x ∨ h x = x

Tactic:
cases H1 x <;> cases H2 x <;> simp [*]

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

Goal state before:
pp: α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
⊢ (f ^ (n + 1 + 1)) x = f x ∨ x = (f ^ (n + 1) * f) x

Tactic:
← pow_succ,

Goal state after:
α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
⊢ (f ^ (n + 1 + 1)) x = f x ∨ x = (f ^ (n + 1 + 1)) x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
⊢ (s.noncommProd k ⋯).support = s.biUnion fun i ↦ (k i).support

Tactic:
induction s using Finset.induction_on with

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
⊢ (s.noncommProd k ⋯).support = s.biUnion fun i ↦ (k i).support

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi hrec =>
    have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
      hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.biUnion_insert]
    rw [Equiv.Perm.Disjoint.support_mul, hrec hs']
    apply disjoint_noncommProd_right
    intro j hj
    apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
      simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ ↑l.formPerm.support = ↑l.toFinset

Tactic:
convert! support_formPerm_of_nodup' _ h h'

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ ↑l.formPerm.support = {x | l.formPerm x ≠ x}
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case cons.nil.inl
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
h : [x] ~r l'
⊢ l'.length ≤ 1

Tactic:
simp [← h.perm.length_eq]

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

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
n : ℤ
hn : (f ^ n) x = y
⊢ (f ^ (n % ↑(orderOf f)).toNat) x = y

Tactic:
by
        {have := n.emod_nonneg (Int.natCast_ne_zero.mpr (ne_of_gt (orderOf_pos f)))
         rwa [← zpow_natCast, Int.toNat_of_nonneg this, zpow_mod_orderOf]}

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

Goal state before:
pp: x y : Fin 0
_hxy✝ : x ≠ y
⊢ (swap x y).signAux = -1

Tactic:
exact Fin.elim0 x

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

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

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
    simp [formPerm_pow_apply_getElem _ hl, Nat.mod_eq_of_lt hk]

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

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

Tactic:
disjoint_iff_eq_or_eq

Goal state after:
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
⊢ ∀ (x : α), (ofSubtype u) x = x ∨ g x = x
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
this : (e.symm.trans (swap x (f x) * f)).trans e = swap (e x) (e (f x)) * (e.symm.trans f).trans e
hefx : e x ≠ e (f x)
⊢ signAux ((e.symm.trans f).trans e) = -signAux2 l (swap x (f x) * f)

Tactic:
← signAux_eq_signAux2 _ _ e hy,

Goal state after:
case neg
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
this : (e.symm.trans (swap x (f x) * f)).trans e = swap (e x) (e (f x)) * (e.symm.trans f).trans e
hefx : e x ≠ e (f x)
⊢ signAux ((e.symm.trans f).trans e) = -signAux ((e.symm.trans (swap x (f x) * f)).trans e)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : f x ≠ x
hffx : f (f x) = x
y z : α
hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = f x
⊢ f y = (swap x (f x)) y

Tactic:
swap_apply_of_ne_of_ne hyx hfyx

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : f x ≠ x
hffx : f (f x) = x
y z : α
hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = f x
⊢ f y = y
Module: Mathlib.GroupTheory.Perm.Sign

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

Tactic:
refine Or.inr ⟨List.not_mem_nil, ?_⟩

Goal state after:
case nil
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
hl : [].Nodup
⊢ (List.map (fun a ↦ prodExtendRight a (σ a)) []).prod (a, b) = (a, b)
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
f : ι → G
comm : (↑s).Pairwise (Function.onFun Commute f)
K : ι → Subgroup G
hind : iSupIndep K
hmem : ∀ x ∈ s, f x ∈ K x
⊢ s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1

Tactic:
induction s using Finset.induction_on with

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

Goal state before:
pp: case refine_1
α : Type u_2
f : Perm α
hf : f.IsCycle
⊢ {x | f x ≠ x}.Nontrivial

Tactic:
obtain ⟨a, ha⟩ := hf
    exact ⟨f a, f.injective.ne ha.1, a, ha.1, ha.1⟩

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

Goal state before:
pp: case negSucc
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
z : ℕ
⊢ (f.cycleOf x ^ (z + 1))⁻¹ x = (f ^ Int.negSucc z) x

Tactic:
← inv_pow,

Goal state after:
case negSucc
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
z : ℕ
⊢ ((f.cycleOf x)⁻¹ ^ (z + 1)) x = (f ^ Int.negSucc z) x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case negSucc
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
z : ℕ
⊢ (f⁻¹.cycleOf x ^ (z + 1)) x = (f ^ (z + 1))⁻¹ x

Tactic:
← inv_pow,

Goal state after:
case negSucc
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
z : ℕ
⊢ (f⁻¹.cycleOf x ^ (z + 1)) x = (f⁻¹ ^ (z + 1)) x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
g : Perm α
s : Finset α
hs : ∀ (x : α), g x ∈ s ↔ x ∈ s
n : ℕ
x : α
hx : x ∈ s
⊢ ↑((g.subtypePerm hs ^ n) ⟨x, hx⟩) = (g ^ n) x

Tactic:
by
  simp only [subtypePerm_pow, subtypePerm_apply]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑s).Pairwise fun i j ↦ Commute (k i) (k j)
⊢ (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType

Tactic:
induction s using Finset.induction_on with

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

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
right✝ : ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a
hc : f.cycleOf x = 1
⊢ ¬(f.cycleOf x).IsCycle

Tactic:
simp [hc]

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
g : M [⋀^ι]→ₗ[R] N'
v : ι → M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
σ : Equiv.Perm ι
⊢ g v = Equiv.Perm.sign σ • g (v ∘ ⇑σ)

Tactic:
rw [g.map_perm, smul_smul]

Goal state after:
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
g : M [⋀^ι]→ₗ[R] N'
v : ι → M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
σ : Equiv.Perm ι
⊢ g v = (Equiv.Perm.sign σ * Equiv.Perm.sign σ) • g v
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'
⊢ ⇑(∑ x, Equiv.Perm.sign x • Equiv.Perm.sign x • ↑a) = ⇑((Fintype.card ι).factorial • a)

Tactic:
smul_smul,

Goal state after:
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'
⊢ ⇑(∑ x, (Equiv.Perm.sign x * Equiv.Perm.sign x) • ↑a) = ⇑((Fintype.card ι).factorial • a)
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'
⊢ ⇑(∑ x, 1 • ↑a) = ⇑((Fintype.card ι).factorial • a)

Tactic:
one_smul,

Goal state after:
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'
⊢ ⇑(∑ x, ↑a) = ⇑((Fintype.card ι).factorial • a)
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₂
α : ι → 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 = ∅
i : ι
hi : A i = ∅
⊢ ∑ j ∈ A i, g i j = 0

Tactic:
simp [hi]

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

Goal state before:
pp: case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered 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 → (X ⟶ S')
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → f ≫ T' mY = T' mX
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
⊢ ∀ {f_1 : X' ⟶ Y'},
    ⟨X', ⟨Y', ⟨mX', ⟨mY', f_1⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H' →
      f_1 ≫ (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mY' =
        (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'

Tactic:
f'

Goal state after:
case insert
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered 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 → (X ⟶ S')
w' : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H' → f ≫ T' mY = T' mX
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
⊢ ⟨X', ⟨Y', ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H' →
    f' ≫ (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mY' =
      (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: m : Type u_1
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M N : Matrix m m R
⊢ (M * N).det = (N * M).det

Tactic:
rw [det_mul, det_mul, mul_comm]

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
i : ι
hi : ¬i = 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

Tactic:
simp [hi]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β

Tactic:
obtain ⟨s, ts, hs⟩ := IsFilteredOrEmpty.cocone_maps (f₂ ≫ k₁t) (g₂ ≫ k₂t)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : j₁ ⟶ k₁
g₁ : j₁ ⟶ k₂
f₂ : j₂ ⟶ k₁
g₂ : j₂ ⟶ k₂
t : C
k₁t : k₁ ⟶ t
k₂t : k₂ ⟶ t
ht : f₁ ≫ k₁t = g₁ ≫ k₂t
s : C
ts : t ⟶ s
hs : (f₂ ≫ k₁t) ≫ ts = (g₂ ≫ k₂t) ≫ ts
⊢ ∃ s α β, f₁ ≫ α = g₁ ≫ β ∧ f₂ ≫ α = g₂ ≫ β
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
s : Finset n
hj : j ∉ s
c : n → R
a : R
⊢ (M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det

Tactic:
induction s using Finset.induction_on with

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 B C : Matrix n n R
hC : C.det = 1
hA : A = B * C
⊢ B.det * C.det = B.det

Tactic:
rw [hC, mul_one]

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
X' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
⊢ ∀ {f_1 : X' ⟶ Y'},
    ⟨X', ⟨Y', ⟨mX', ⟨mY', f_1⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H' →
      (fun {X_1} mZ ↦ eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mX' ≫ f_1 =
        (fun {X_1} mZ ↦ eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY'

Tactic:
f'

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' Y' : C
mX' : X' ∈ O
mY' : Y' ∈ O
f' : X' ⟶ Y'
⊢ ⟨X', ⟨Y', ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H' →
    (fun {X_1} mZ ↦ eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mX' ≫ f' = (fun {X_1} mZ ↦ eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY'
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
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  1 • A + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) =
    (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • A + (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B

Tactic:
one_smul,

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
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  A + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) =
    (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) • A + (detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B)
⊢ A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B + detp (-1) B • 1) + detp (-1) A • (B * adjp 1 B + detp 1 B • 1)) =
    detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B) +
      (detp 1 A • detp 1 B • 1 + detp (-1) A • detp (-1) B • 1)
⊢ B * A = 1

Tactic:
smul_smul,

Goal state after:
n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B + detp (-1) B • 1) + detp (-1) A • (B * adjp 1 B + detp 1 B • 1)) =
    detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B) +
      ((detp 1 A * detp 1 B) • 1 + detp (-1) A • detp (-1) B • 1)
⊢ B * A = 1
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B + detp (-1) B • 1) + detp (-1) A • (B * adjp 1 B + detp 1 B • 1)) =
    detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B) +
      ((detp 1 A * detp 1 B) • 1 + detp (-1) A • detp (-1) B • 1)
⊢ B * A = 1

Tactic:
smul_smul,

Goal state after:
n✝ : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n✝
inst✝ : CommSemiring R
s : ℤˣ
A✝ B✝ : Matrix n✝ n✝ R
i j : n✝
a b c : R
n : ℕ
A B : Matrix (Fin n) (Fin n) R
hAB : A * B = 1
h0 : 1 + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp 1 A * detp 1 B + detp (-1) A * detp (-1) B
h :
  B * A + (detp 1 A • (B * adjp (-1) B + detp (-1) B • 1) + detp (-1) A • (B * adjp 1 B + detp 1 B • 1)) =
    detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B) +
      ((detp 1 A * detp 1 B) • 1 + (detp (-1) A * detp (-1) B) • 1)
⊢ B * A = 1