mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mp.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : n ∈ l.prod.cycleType
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n

Tactic:
rw [cycleType_eq _ rfl hlc hld, Multiset.mem_coe, List.mem_map] at h

Goal state after:
case mp.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : ∃ a ∈ l, (Finset.card ∘ support) a = n
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: G : Type u_2
inst✝ : Group G
⊢ vectorsProdEqOne G 1 = {1 ::ᵥ Vector.nil}

Tactic:
Set.eq_singleton_iff_unique_mem,

Goal state after:
G : Type u_2
inst✝ : Group G
⊢ 1 ::ᵥ Vector.nil ∈ vectorsProdEqOne G 1 ∧ ∀ x ∈ vectorsProdEqOne G 1, x = 1 ::ᵥ Vector.nil
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : x ∈ f.support
y : α
hy : (f.cycleOf x) y ≠ y
H : ¬f.SameCycle x y
⊢ y = f y

Tactic:
· rw [cycleOf_apply_of_not_sameCycle H] at hy
      contradiction

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
bc : b ≠ c
x : α
hx : x ∈ {a, b, c}
⊢ x ∈ (swap a b * swap a c).support

Tactic:
simp only [mem_support, coe_mul]
    grind

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_3
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
x✝ : ι → M₂
⊢ (f.compLinearMap 0) x✝ = 0 x✝

Tactic:
compLinearMap_apply,

Goal state after:
R : Type u_1
inst✝⁷ : Semiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
N : Type u_3
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
x✝ : ι → M₂
⊢ (f fun i ↦ 0 (x✝ i)) = 0 x✝
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.left_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x * (descFunLift F s y + descFunLift F s z) =
    descFunLift F s x * descFunLift F s y + descFunLift F s x * descFunLift F s z

Tactic:
rw [mul_add]

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

Goal state before:
pp: case a.zero_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (zero.mul x) = descFunLift F s zero

Tactic:
dsimp; rw [zero_mul]

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

Goal state before:
pp: case a.left_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x * (descFunLift F s y + descFunLift F s z) =
    descFunLift F s x * descFunLift F s y + descFunLift F s x * descFunLift F s z

Tactic:
rw [mul_add]

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

Goal state before:
pp: case a.zero_mul
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (zero.mul x) = descFunLift F s zero

Tactic:
dsimp; rw [zero_mul]

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 : Matrix n n R
⊢ ∑ x ∈ ofSign 1, sign ((Equiv.inv (Perm n)) x) • ∏ i, M (((Equiv.inv (Perm n)) x) i) i +
      ∑ x ∈ ofSign (-1), sign ((Equiv.inv (Perm n)) x) • ∏ i, M (((Equiv.inv (Perm n)) x) i) i =
    detp 1 M - detp (-1) M

Tactic:
inv_apply,

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∑ x ∈ ofSign 1, sign x⁻¹ • ∏ x_1, M (x⁻¹ x_1) x_1 + ∑ x ∈ ofSign (-1), sign x⁻¹ • ∏ x_1, M (x⁻¹ x_1) x_1 =
    detp 1 M - detp (-1) M
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
⊢ ∑ x ∈ ofSign 1, sign x • ∏ x_1, M (x⁻¹ x_1) x_1 + ∑ x ∈ ofSign (-1), sign x • ∏ x_1, M (x⁻¹ x_1) x_1 =
    ∑ σ ∈ ofSign 1, ∏ k, M k (σ k) + -∑ σ ∈ ofSign (-1), ∏ k, M k (σ k)

Tactic:
← sum_neg_distrib

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∑ x ∈ ofSign 1, sign x • ∏ x_1, M (x⁻¹ x_1) x_1 + ∑ x ∈ ofSign (-1), sign x • ∏ x_1, M (x⁻¹ x_1) x_1 =
    ∑ σ ∈ ofSign 1, ∏ k, M k (σ k) + ∑ x ∈ ofSign (-1), -∏ k, M k (x k)
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
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
h :
  ∀ (s : ℤˣ),
    detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp s B + detp (-1) A * detp (-s) B)
σ : n → n
hσ✝ : ¬Function.Injective σ
i j : n
hσ : σ i = σ j
hij : i ≠ j
k : n
⊢ σ ((swap i j) k) = σ k

Tactic:
rw [swap_apply_def]

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
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
h :
  ∀ (s : ℤˣ),
    detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp s B + detp (-1) A * detp (-s) B)
σ : n → n
hσ✝ : ¬Function.Injective σ
i j : n
hσ : σ i = σ j
hij : i ≠ j
k : n
⊢ σ (if k = i then j else if k = j then i else k) = σ k
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 : Matrix n n R
i j : n
h : i ≠ j
⊢ (adjp 1 A * A) i j = (adjp (-1) A * A) i j

Tactic:
← transpose_apply (_ * _) j i,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
⊢ (adjp 1 A * A)ᵀ j i = (adjp (-1) A * A)ᵀ j i
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
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |(A.submatrix ⇑e₁ ⇑(e₁.trans (e₁.symm.trans e₂))).det| = |A.det|

Tactic:
change |((A.submatrix id (e₁.symm.trans e₂)).submatrix e₁ e₁).det| = |A.det|

Goal state after:
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
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |((A.submatrix id ⇑(e₁.symm.trans e₂)).submatrix ⇑e₁ ⇑e₁).det| = |A.det|
Module: Mathlib.CategoryTheory.Filtered.Basic

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

Tactic:
obtain ⟨t, k₁t, k₂t, ht⟩ := cospan f₁ g₁

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
j₁ j₂ k₁ k₂ : C
f₁ : k₁ ⟶ j₁
g₁ : k₂ ⟶ j₁
f₂ : k₁ ⟶ j₂
g₂ : k₂ ⟶ j₂
t : C
k₁t : t ⟶ k₁
k₂t : t ⟶ k₂
ht : k₁t ≫ f₁ = k₂t ≫ g₁
⊢ ∃ s α β, α ≫ f₁ = β ≫ g₁ ∧ α ≫ f₂ = β ≫ g₂
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 A • detp (-1) B • 1 +
        (detp (-1) A • (B * adjp 1 B) + detp (-1) A • 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_add,

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) A • 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) A • 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_add,

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 • detp (-1) B • 1 +
      (detp (-1) A • (B * adjp (-1) B) + detp (-1) A • detp 1 B • 1)
⊢ B * A = 1

Tactic:
← smul_add,

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) B • 1) + (detp (-1) A • (B * adjp (-1) B) + 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) B • 1) + (detp (-1) A • (B * adjp (-1) B) + detp (-1) A • detp 1 B • 1)
⊢ B * A = 1

Tactic:
← smul_add,

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) B • 1) + detp (-1) A • (B * adjp (-1) B + 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 A • detp (-1) B • 1 +
        (detp (-1) A • (B * adjp 1 B) + detp (-1) A • detp 1 B • 1)) =
    detp 1 A • (B * adjp (-1) B) + detp 1 A • detp 1 B • 1 +
      (detp (-1) A • (B * adjp 1 B) + detp (-1) A • detp (-1) B • 1)
⊢ B * A = 1

Tactic:
← smul_add,

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) A • detp 1 B • 1)) =
    detp 1 A • (B * adjp (-1) B) + detp 1 A • detp 1 B • 1 +
      (detp (-1) A • (B * adjp 1 B) + 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) A • detp 1 B • 1)) =
    detp 1 A • (B * adjp (-1) B) + detp 1 A • detp 1 B • 1 +
      (detp (-1) A • (B * adjp 1 B) + detp (-1) A • detp (-1) B • 1)
⊢ B * A = 1

Tactic:
← smul_add,

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 • detp 1 B • 1 +
      (detp (-1) A • (B * adjp 1 B) + detp (-1) A • detp (-1) B • 1)
⊢ B * A = 1
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹⁰ : CommSemiring R
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
f f' : MultilinearMap R M₁ M₂
A : Type u_1
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : ι → A
i : ι
c : R
x : A
⊢ ∏ i_1, update m i (c • x) i_1 = c • ∏ i_1, update m i x i_1

Tactic:
simp [Finset.prod_update_of_mem]

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : Small.{u, max u v} ↑F.sections
x✝¹ : Cone F
x✝ : x✝¹.pt ⟶ (limitCone F).pt
w : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = x✝¹.π.app j
⊢ x✝ = ↾fun v ↦ (equivShrink ↑F.sections) ⟨fun j ↦ (hom (x✝¹.π.app j)) v, ⋯⟩

Tactic:
ext x j
    simpa using! congr_hom (w j) x

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

Goal state before:
pp: case insert
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ f a - (f (s.piecewise b a) - f (update (s.piecewise b a) k (s.piecewise b a k - b k))) =
    ∑ i ∈ insert k s, f fun j ↦ if j ∈ insert k s → j < i then a j else if i = j then a j - b j else b j

Tactic:
← sub_add,

Goal state after:
case insert
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
⊢ f a - f (s.piecewise b a) + f (update (s.piecewise b a) k (s.piecewise b a k - b k)) =
    ∑ i ∈ insert k s, f fun j ↦ if j ∈ insert k s → j < i then a j else if i = j then a j - b j else b j
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 : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
i : ι
h₁ : i = k ∨ i ∈ s → i < k
⊢ update (s.piecewise b a) k (s.piecewise b a k - b k) i = a i

Tactic:
rw [update_of_ne, Finset.piecewise_eq_of_notMem]

Goal state after:
case pos.hi
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
i : ι
h₁ : i = k ∨ i ∈ s → i < k
⊢ i ∉ s

case pos.h
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
i : ι
h₁ : i = k ∨ i ∈ s → i < k
⊢ i ≠ k
Module: Mathlib.CategoryTheory.Limits.Types.Yoneda

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
X : C
t : F ⟶ (const J).obj X
⊢ (fun j ↦ t.app (unop j)) ∈ (F.op ⋙ yoneda.obj X).sections

Tactic:
simp [Functor.sections]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), Mono (h.unit.app X)
X Y : C
f g : X ⟶ Y
hfg : L.map f = L.map g
⊢ f ≫ h.unit.app Y = g ≫ h.unit.app Y

Tactic:
apply (h.homEquiv X (L.obj Y)).symm.injective

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), Mono (h.unit.app X)
X Y : C
f g : X ⟶ Y
hfg : L.map f = L.map g
⊢ (h.homEquiv X (L.obj Y)).symm (f ≫ h.unit.app Y) = (h.homEquiv X (L.obj Y)).symm (g ≫ h.unit.app Y)
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (ρ_ X).inv ▷ Y ≫ (α_ X (𝟙_ C) Y).hom = X ◁ (λ_ Y).inv

Tactic:
by
  simp [← cancel_mono (X ◁ (λ_ Y).hom)]

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

Goal state before:
pp: case h₁
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 G : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
⊢ (ε (F.prod' H)).1 ≫ ((prod' α β).app (𝟙_ C)).1 = (ε (G.prod' K)).1

Tactic:
prod'_ε_fst,

Goal state after:
case h₁
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 G : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
⊢ ε F ≫ ((prod' α β).app (𝟙_ C)).1 = (ε (G.prod' K)).1