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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' : g.support = {a, g a, g (g a)}
ha'' : [a, g a, g (g a)].Nodup
⊢ g (g a) ≠ a

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' : g.support = {a, g a, g (g a)}
ha'' : [a, g a, g (g a)].Nodup
⊢ g (g a) ≠ g a

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' : g.support = {a, g a, g (g a)}
ha'' : [a, g a, g (g a)].Nodup
x : α
h : x ∉ g.support
⊢ x ≠ g a

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' : g.support = {a, g a, g (g a)}
ha'' : [a, g a, g (g a)].Nodup
x : α
h : x ∉ g.support
⊢ x ≠ g (g a)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' : g.support = {a, g a, g (g a)}
ha'' : [a, g a, g (g a)].Nodup
x : α
h : x ∉ g.support
⊢ x ≠ a

Tactic:
by grind

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

Goal state before:
pp: case inl
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : (p : (i : ι) → κ i) → Module R (N p)
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
q : (i : ι) → κ i
m : (i : ι) → M i (q i)
⊢ ((dfinsuppFamily f) fun i ↦ DFinsupp.single (q i) (m i)) q = (DFinsupp.single q ((f q) m)) q

pp: case inr
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : (p : (i : ι) → κ i) → Module R (N p)
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : q ≠ p
⊢ ((dfinsuppFamily f) fun i ↦ DFinsupp.single (p i) (m i)) q = (DFinsupp.single p ((f p) m)) q

Tactic:
· simp

Goal state after:
case inr
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : (p : (i : ι) → κ i) → Module R (N p)
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : q ≠ p
⊢ ((dfinsuppFamily f) fun i ↦ DFinsupp.single (p i) (m i)) q = (DFinsupp.single p ((f p) m)) q
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ {2} + {2} = {2, 2}

pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ (swap z t).IsSwap

pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ (swap x y).IsSwap

Tactic:
· simp

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ (swap z t).IsSwap

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ (swap x y).IsSwap
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: case inl
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : (p : (i : ι) → κ i) → Module R (N p)
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap R (fun i ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ ((dfinsuppFamily (Pi.single p f)) x) p = (DFinsupp.single p (f fun i ↦ (x i) (p i))) p

pp: case inr
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : (p : (i : ι) → κ i) → Module R (N p)
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap R (fun i ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
p' : (i : ι) → κ i
hp : p ≠ p'
⊢ ((dfinsuppFamily (Pi.single p f)) x) p' = (DFinsupp.single p (f fun i ↦ (x i) (p i))) p'

Tactic:
· simp

Goal state after:
case inr
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : (p : (i : ι) → κ i) → Module R (N p)
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap R (fun i ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
p' : (i : ι) → κ i
hp : p ≠ p'
⊢ ((dfinsuppFamily (Pi.single p f)) x) p' = (DFinsupp.single p (f fun i ↦ (x i) (p i))) p'
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: case h0
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Fintype (κ i)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : DecidableEq ι'
inst✝ : Fintype ι'
f : Π₀ (x : ((i : ι) → κ i) × ι'), R
x : (i : ι) → Π₀ (x : κ i), R
⊢ (freeDFinsuppEquiv 0) x = ∑ p, 0 p • DFinsupp.single p.2 (∏ i, (x i) (p.1 i))

pp: case ha
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Fintype (κ i)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : DecidableEq ι'
inst✝ : Fintype ι'
f : Π₀ (x : ((i : ι) → κ i) × ι'), R
x : (i : ι) → Π₀ (x : κ i), R
⊢ ∀ (i : ((i : ι) → κ i) × ι') (b : R) (f : Π₀ (i : ((i : ι) → κ i) × ι'), R),
    f i = 0 →
      b ≠ 0 →
        (freeDFinsuppEquiv f) x = ∑ p, f p • DFinsupp.single p.2 (∏ i, (x i) (p.1 i)) →
          (freeDFinsuppEquiv (DFinsupp.single i b + f)) x =
            ∑ p, (DFinsupp.single i b + f) p • DFinsupp.single p.2 (∏ i, (x i) (p.1 i))

Tactic:
· simp

Goal state after:
case ha
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Fintype (κ i)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : DecidableEq ι'
inst✝ : Fintype ι'
f : Π₀ (x : ((i : ι) → κ i) × ι'), R
x : (i : ι) → Π₀ (x : κ i), R
⊢ ∀ (i : ((i : ι) → κ i) × ι') (b : R) (f : Π₀ (i : ((i : ι) → κ i) × ι'), R),
    f i = 0 →
      b ≠ 0 →
        (freeDFinsuppEquiv f) x = ∑ p, f p • DFinsupp.single p.2 (∏ i, (x i) (p.1 i)) →
          (freeDFinsuppEquiv (DFinsupp.single i b + f)) x =
            ∑ p, (DFinsupp.single i b + f) p • DFinsupp.single p.2 (∏ i, (x i) (p.1 i))
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
⊢ ∏ k, diagonal d k (1 k) = ∏ i, d i

pp: case h
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
d : n → R
⊢ 1 ∈ ofSign 1

pp: case h₀
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
d : n → R
⊢ ∀ b ∈ ofSign 1, b ≠ 1 → ∏ k, diagonal d k (b k) = 0

Tactic:
· simp

Goal state after:
case h
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
d : n → R
⊢ 1 ∈ ofSign 1

case h₀
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
d : n → R
⊢ ∀ b ∈ ofSign 1, b ≠ 1 → ∏ k, diagonal d k (b k) = 0
Module: Mathlib.LinearAlgebra.Matrix.Reindex

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
l' : Type u_5
m' : Type u_6
n' : Type u_7
o' : Type u_8
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : Fintype o
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq o
inst✝¹ : Semiring A
inst✝ : Algebra R A
e : m ≃ n
x✝ : R
⊢ (reindexRingEquiv A e).toFun ((algebraMap R (Matrix m m A)) x✝) = (algebraMap R (Matrix n n A)) x✝

Tactic:
by simp [algebraMap]

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

Goal state before:
pp: case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x x' : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s x.neg = descFunLift F s x'.neg

Tactic:
| neg_1 x x' r ih =>

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

Goal state before:
pp: case e_s
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
i : n
A : Matrix (Option n) (Option n) R
⊢ sign (swap none (some i)) * s = -s

pp: case e_A.e_c
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
i : n
A : Matrix (Option n) (Option n) R
⊢ ⇑(swap none (some i)) ∘ some = Function.update some i none

Tactic:
· simp

Goal state after:
case e_A.e_c
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
i : n
A : Matrix (Option n) (Option n) R
⊢ ⇑(swap none (some i)) ∘ some = Function.update some i none
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.neg_1
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x x' : Prequotient F
r : Relation F x x'
ih : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s x.neg = descFunLift F s x'.neg

Tactic:
| neg_1 x x' r ih =>

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

Goal state before:
pp: case refine_2
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ 1 ∉ univ → ↑↑(sign 1) * ∏ i, diagonal d (1 i) i = 0

pp: case refine_3
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ↑↑(sign 1) * ∏ i, diagonal d (1 i) i = ∏ i, d i

Tactic:
· simp

Goal state after:
case refine_3
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ↑↑(sign 1) * ∏ i, diagonal d (1 i) i = ∏ i, d i
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_3
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ↑↑(sign 1) * ∏ i, diagonal d (1 i) i = ∏ i, d i

Tactic:
· simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFilteredOrEmpty C
ι✝ : Type u_1
inst✝¹ : Finite ι✝
k₁ k₂ : C
ι : Type u_1
inst✝ : Fintype ι
IH : ∀ (j : ι → C) (f : (i : ι) → j i ⟶ k₁) (g : (i : ι) → j i ⟶ k₂), ∃ s α β, ∀ (i : ι), f i ≫ α = g i ≫ β
j : Option ι → C
f : (i : Option ι) → j i ⟶ k₁
g : (i : Option ι) → j i ⟶ k₂
s₁ : C
α₁ : k₁ ⟶ s₁
β₁ : k₂ ⟶ s₁
H₁ : ∀ (i : ι), f (some i) ≫ α₁ = g (some i) ≫ β₁
s₂ : C
α₂ : k₁ ⟶ s₂
β₂ : k₂ ⟶ s₂
H₂ : f none ≫ α₂ = g none ≫ β₂
t : C
α : s₁ ⟶ t
β : s₂ ⟶ t
h₁ : α₁ ≫ α = α₂ ≫ β
h₂ : β₁ ≫ α = β₂ ≫ β
⊢ f none ≫ α₁ ≫ α = g none ≫ β₁ ≫ α

Tactic:
by grind

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFilteredOrEmpty C
ι✝ : Type u_1
inst✝¹ : Finite ι✝
k₁ k₂ : C
ι : Type u_1
inst✝ : Fintype ι
IH : ∀ (j : ι → C) (f : (i : ι) → j i ⟶ k₁) (g : (i : ι) → j i ⟶ k₂), ∃ s α β, ∀ (i : ι), f i ≫ α = g i ≫ β
j : Option ι → C
f : (i : Option ι) → j i ⟶ k₁
g : (i : Option ι) → j i ⟶ k₂
s₁ : C
α₁ : k₁ ⟶ s₁
β₁ : k₂ ⟶ s₁
H₁ : ∀ (i : ι), f (some i) ≫ α₁ = g (some i) ≫ β₁
s₂ : C
α₂ : k₁ ⟶ s₂
β₂ : k₂ ⟶ s₂
H₂ : f none ≫ α₂ = g none ≫ β₂
t : C
α : s₁ ⟶ t
β : s₂ ⟶ t
h₁ : α₁ ≫ α = α₂ ≫ β
h₂ : β₁ ≫ α = β₂ ≫ β
⊢ ∀ (val : ι), f (some val) ≫ α₁ ≫ α = g (some val) ≫ β₁ ≫ α

Tactic:
by grind

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsFilteredOrEmpty C
ι : Type u_1
inst✝ : Finite ι
j : ι → C
k₁ k₂ : C
f : (i : ι) → j i ⟶ k₁
g : (i : ι) → j i ⟶ k₂
⊢ ∃ s α β, ∀ (i : ι), f i ≫ α = g i ≫ β

Tactic:
by
  induction ι using Finite.induction_empty_option with
  | @of_equiv ι₁ ι₂ e IH =>
    obtain ⟨s, α, β, H⟩ := IH (j ∘ e) (f <| e ·) (g <| e ·)
    exact ⟨s, α, β, e.forall_congr_right.mp H⟩
  | h_empty => exact ⟨max k₁ k₂, leftToMax k₁ k₂, rightToMax k₁ k₂, by simp⟩
  | @h_option ι _ IH =>
    obtain ⟨s₁, α₁, β₁, H₁⟩ := IH (j ·) (f ·) (g ·)
    obtain ⟨s₂, α₂, β₂, H₂⟩ := span (f .none) (g .none)
    obtain ⟨t, α, β, h₁, h₂⟩ := bowtie α₁ α₂ β₁ β₂
    exact ⟨t, α₁ ≫ α, β₁ ≫ α, Option.rec (by grind) (by grind)⟩

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

Tactic:
simp_rw [add_smul, ← smul_smul] at h

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) A • (B * adjp 1 B)) +
      (detp 1 A • detp (-1) B • 1 + 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.Determinant.Basic

Goal state before:
pp: case refine_1
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
i✝ j : Fin n.succ
i : Fin n
⊢ M i.succ j = N i.succ j

Tactic:
hsucc,

Goal state after:
case refine_1
R : Type v
inst✝ : CommRing R
n : ℕ
k : Fin (n + 1)
c : Fin n → R
hc : ∀ (i : Fin n), 0 < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
i✝ j : Fin n.succ
i : Fin n
⊢ N i.succ j + c i * M i.castSucc j = N i.succ j
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
⊢ M.det = N.det

Tactic:
have M_k : M (Fin.castSucc k) = M' (Fin.castSucc k) := (updateRow_ne k_ne_succ).symm

Goal state after:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
⊢ M.det = N.det
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).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)
Beq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i ↦ ∑ j ∈ B i, g i j
Ceq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i ↦ ∑ j ∈ C i, g i j
Brec : (f fun i ↦ ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i ↦ g i (r i)
Crec : (f fun i ↦ ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i ↦ g i (r i)
D : Disjoint (piFinset B) (piFinset C)
r : (a : ι) → α a
hr : r ∈ piFinset A
hri₀ : ¬r i₀ = j₂
i : ι
hi : i = i₀
⊢ r i₀ ∈ B i₀

Tactic:
simp [B, hri₀, mem_piFinset.1 hr i₀]

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)
Beq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i ↦ ∑ j ∈ B i, g i j
Ceq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i ↦ ∑ j ∈ C i, g i j
Brec : (f fun i ↦ ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i ↦ g i (r i)
Crec : (f fun i ↦ ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i ↦ g i (r i)
D : Disjoint (piFinset B) (piFinset C)
pi_BC : piFinset A = piFinset B ∪ piFinset C
⊢ ((∑ r ∈ piFinset B, f fun i ↦ g i (r i)) + ∑ r ∈ piFinset C, f fun i ↦ g i (r i)) =
    ∑ r ∈ piFinset B ∪ piFinset C, f fun i ↦ g i (r i)

Tactic:
rw [← Finset.sum_union D]

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

Goal state before:
pp: ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
⊢ (fun j ↦ if h : P j then update x i c ⟨j, h⟩ else z ⟨j, h⟩) =
    update (fun j ↦ if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) (↑i) c

Tactic:
by grind

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

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

Tactic:
have h' := congr_hom (s.ι.naturality l) y

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
x y z : (j : J) × F.obj j
x✝¹ : FilteredColimit.Rel F x y
x✝ : FilteredColimit.Rel F y z
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : (hom (F.map f)) x.snd = (hom (F.map g)) y.snd
k' : J
f' : y.fst ⟶ k'
g' : z.fst ⟶ k'
h' : (hom (F.map f')) y.snd = (hom (F.map g')) z.snd
l : J
fl : k ⟶ l
gl : k' ⟶ l
h✝ : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ (hom (F.map ((g ≫ fl) ≫ n))) y.snd = (hom (F.map ((f' ≫ gl) ≫ n))) y.snd

Tactic:
by rw [hn]

Goal state after: