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

Goal state before:
pp: case refine_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x) y ≠ y
hg'y : g' y ≠ y
hxy : g.SameCycle x y
⊢ False

Tactic:
have hg'm : g' :: m.erase g' ~ m := List.cons_perm_iff_perm_erase.2 ⟨hg', .refl _⟩

Goal state after:
case refine_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x) y ≠ y
hg'y : g' y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
⊢ False
Module: Mathlib.GroupTheory.Perm.Fin

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

Tactic:
ext j

Goal state after:
n : ℕ
α : Type u_1
p : Fin (n + 1)
a : α
x : Fin n → α
j : Fin (n + 1)
⊢ (p.insertNth a x ∘ ⇑(Equiv.symm p.cycleRange)) j = cons a x j
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case intro.mpr
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
hσl : σ.support ⊆ l.prod.support
⊢ σ ∈ l

Tactic:
obtain ⟨a, ha, -⟩ := id h3

Goal state after:
case intro.mpr
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
hσl : σ.support ⊆ l.prod.support
a : α
ha : σ a ≠ a
⊢ σ ∈ l
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
⊢ σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ

Tactic:
by
  obtain ⟨⟨l', hp', hc', hd'⟩, hl⟩ := Trunc.exists_rep σ.truncCycleFactors
  have ht : cycleFactorsFinset σ = l'.toFinset := by
    rw [cycleFactorsFinset, ← hl, Trunc.lift_mk, Multiset.toFinset_eq, List.toFinset_coe]
  rw [ht]
  constructor
  · intro h
    have hn' : l'.Nodup := nodup_of_pairwise_disjoint_cycles hc' hd'
    have hperm : l ~ l' := List.perm_of_nodup_nodup_toFinset_eq hn hn' h.symm
    refine ⟨?_, ?_, ?_⟩
    · exact fun _ h => hc' _ (hperm.subset h)
    · rwa [hperm.pairwise_iff symm]
    · rw [← hp', hperm.symm.prod_eq']
      exact hd'.imp Disjoint.commute
  · rintro ⟨hc, hd, hp⟩
    refine List.toFinset_eq_of_perm _ _ ?_
    refine list_cycles_perm_list_cycles ?_ hc' hc hd' hd
    rw [hp, hp']

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
h : (n ::ₘ σ.cycleType.erase n).sum = 3
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
⊢ σ.IsThreeCycle

Tactic:
h1,

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
h : (n ::ₘ 0).sum = 3
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
⊢ σ.IsThreeCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
h : n = 3
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
⊢ n ::ₘ σ.cycleType.erase n = {3}

Tactic:
h1,

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h0 : ¬σ.cycleType = 0
n : ℕ
h : n = 3
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
⊢ n ::ₘ 0 = {3}
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_3.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = τ a
x : α
⊢ σ x = x ∨ (τ * f⁻¹) x = x

Tactic:
rcases hd x with hx | hx

Goal state after:
case refine_3.inr.inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = τ a
x : α
hx : σ x = x
⊢ σ x = x ∨ (τ * f⁻¹) x = x

case refine_3.inr.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = τ a
x : α
hx : τ x = x
⊢ σ x = x ∨ (τ * f⁻¹) x = x
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
f : M [⋀^ι]→ₗ[R] N
v : ι → M
i₁ i₂ : ι
heq : v i₁ = v i₂
hne : i₁ ≠ i₂
⊢ f v = 0

Tactic:
exact f.map_eq_zero_of_eq v heq hne

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
⊢ detp 1 1 = 1

Tactic:
by
  rw [← diagonal_one, detp_one_diagonal, prod_const_one]

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
P : Type u_4
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
M' : Type u_5
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ (let __src := ∑ σ, Perm.sign σ • domDomCongr σ 0;
    { toFun := ⇑(∑ σ, Perm.sign σ • domDomCongr σ 0), map_update_add' := ⋯, map_update_smul' := ⋯,
      map_eq_zero_of_eq' := ⋯ }) =
    0

Tactic:
by ext; simp

Goal state after:
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₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
⊢ update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'

Tactic:
ext j

Goal state after:
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₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
j : ι
⊢ update (t.piecewise (m + m') m') i (m' i) j = t.piecewise (m + m') m' j
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₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
⊢ update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m''

Tactic:
ext j

Goal state after:
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₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
j : ι
⊢ update (t.piecewise (m + m') m') i (m i) j = t.piecewise (m + m'') m'' j
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
P : Type u_4
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
M' : Type u_5
inst✝¹² : AddCommGroup M'
inst✝¹¹ : Module R M'
N' : Type u_6
inst✝¹⁰ : AddCommGroup N'
inst✝⁹ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : AddCommMonoid N''
inst✝⁴ : AddCommMonoid N₂''
inst✝³ : Module R' M''
inst✝² : Module R' M₂''
inst✝¹ : Module R' N''
inst✝ : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x✝¹ x✝ : M'' [⋀^ι]→ₗ[R'] N''
⊢ (↑e).compAlternatingMap (x✝¹ + x✝) = (↑e).compAlternatingMap x✝¹ + (↑e).compAlternatingMap x✝

Tactic:
by ext; simp

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
P : Type u_4
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
M' : Type u_5
inst✝¹² : AddCommGroup M'
inst✝¹¹ : Module R M'
N' : Type u_6
inst✝¹⁰ : AddCommGroup N'
inst✝⁹ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : AddCommMonoid N''
inst✝⁴ : AddCommMonoid N₂''
inst✝³ : Module R' M''
inst✝² : Module R' M₂''
inst✝¹ : Module R' N''
inst✝ : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x✝¹ : R'
x✝ : M'' [⋀^ι]→ₗ[R'] N''
⊢ (↑e).compAlternatingMap (x✝¹ • x✝) = (RingHom.id R') x✝¹ • (↑e).compAlternatingMap x✝

Tactic:
by ext; simp

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
P : Type u_4
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
M' : Type u_5
inst✝¹² : AddCommGroup M'
inst✝¹¹ : Module R M'
N' : Type u_6
inst✝¹⁰ : AddCommGroup N'
inst✝⁹ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : AddCommMonoid N''
inst✝⁴ : AddCommMonoid N₂''
inst✝³ : Module R' M''
inst✝² : Module R' M₂''
inst✝¹ : Module R' N''
inst✝ : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x✝ : M'' [⋀^ι]→ₗ[R'] N''
⊢ (fun f ↦ (↑e.symm).compAlternatingMap f) ((fun f ↦ (↑e).compAlternatingMap f) x✝) = x✝

Tactic:
by ext; simp

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
P : Type u_4
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
M' : Type u_5
inst✝¹² : AddCommGroup M'
inst✝¹¹ : Module R M'
N' : Type u_6
inst✝¹⁰ : AddCommGroup N'
inst✝⁹ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : AddCommMonoid N''
inst✝⁴ : AddCommMonoid N₂''
inst✝³ : Module R' M''
inst✝² : Module R' M₂''
inst✝¹ : Module R' N''
inst✝ : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x✝ : M'' [⋀^ι]→ₗ[R'] N₂''
⊢ (fun f ↦ (↑e).compAlternatingMap f) ((fun f ↦ (↑e.symm).compAlternatingMap f) x✝) = x✝

Tactic:
by ext; simp

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

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
p q : n
hpq : p ≠ q
hcol : A.col p = A.col q
s t : ℤˣ
⊢ detp s A = detp t A

Tactic:
simpa using detp_eq_of_row_eq (A := Aᵀ) hpq hcol s t

Goal state after:
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₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
⊢ (insert i s).piecewise m m' = s.piecewise m m''

Tactic:
ext j

Goal state after:
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₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
j : ι
⊢ (insert i s).piecewise m m' j = s.piecewise m m'' j
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j : J
⊢ coconeFun F j 1 = 1

Tactic:
by apply Quot.sound; apply Relation.one

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
s : ℤˣ
A : Matrix (Option n) (Option n) R
i : Option n
σ : Perm (Option n)
x✝ : sign σ = s ∧ σ none = i
⊢ sign (removeNone σ) = sign (swap none i) * s ∧ decomposeOption.symm (i, removeNone σ) = σ

Tactic:
by rw [← optionCongr_sign]; aesop

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j : J
⊢ coconeFun F j 1 = 1

Tactic:
by apply Quot.sound; apply Relation.one

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 v
inst✝ : CommRing R
e e' : m ≃ n
M : Matrix m m R
⊢ ((reindex e' e') ((reindex (e.trans e'.symm) (Equiv.refl m)) M)).det = ↑↑(sign (e'.trans e.symm)) * M.det

Tactic:
simp_rw [det_reindex_self, reindex_apply, Equiv.refl_symm, Equiv.coe_refl, det_permute]

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 v
inst✝ : CommRing R
e e' : m ≃ n
M : Matrix m m R
⊢ ↑↑(sign (e.trans e'.symm).symm) * M.det = ↑↑(sign (e'.trans e.symm)) * M.det
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
⊢ IsAddUnit (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B))

Tactic:
suffices h : ∀ {s t}, s ≠ t → IsAddUnit (detp s A • (B * adjp t B)) from
    (h (by decide)).add (h (by decide))

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
⊢ ∀ {s t : ℤˣ}, s ≠ t → IsAddUnit (detp s A • (B * adjp t B))
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
key : adjp 1 B + A * detp (-1) B • 1 = adjp (-1) B + A * detp 1 B • 1
⊢ detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B

Tactic:
Matrix.mul_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
key : adjp 1 B + detp (-1) B • (A * 1) = adjp (-1) B + detp 1 B • (A * 1)
⊢ detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsCofilteredOrEmpty C
I : Type u_1
inst✝ : Finite I
i : C
j : I → C
f : (x : I) → j x ⟶ i
⊢ ∃ k fki g, ∀ (x : I), g x ≫ f x = fki

Tactic:
have : IsCofiltered C := { nonempty := ⟨i⟩ }
  classical
  cases nonempty_fintype I
  obtain ⟨k, fk, hk⟩ := IsCofiltered.inf_exists (insert i (Finset.univ.image j))
    (Finset.univ.image fun x ↦ ⟨j x, i, by simp, by simp, f x⟩)
  exact ⟨k, _, _, fun x ↦ hk _ _ (Finset.mem_image_of_mem _ (Finset.mem_univ _))⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ (IsFiltered.coeqHom f.unop g.unop).op ≫ f = (IsFiltered.coeqHom f.unop g.unop).op ≫ g

Tactic:
rw [show f = f.unop.op by simp, show g = g.unop.op by simp, ← op_comp, ← op_comp]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ (f.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop).op =
    (g.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop).op
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ f ≫ (IsCofiltered.eqHom f.unop g.unop).op = g ≫ (IsCofiltered.eqHom f.unop g.unop).op

Tactic:
rw [show f = f.unop.op by simp, show g = g.unop.op by simp, ← op_comp, ← op_comp]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ f.unop).op =
    (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ g.unop).op
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: case mp
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ Function.Surjective (F.descColimitType c) → ∀ (z : c.pt), ∃ i x, c.ι i x = z

Tactic:
intro h z

Goal state after:
case mp
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
h : Function.Surjective (F.descColimitType c)
z : c.pt
⊢ ∃ i x, c.ι i x = z
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: case mpr
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (z : c.pt), ∃ i x, c.ι i x = z) → Function.Surjective (F.descColimitType c)

Tactic:
intro h z

Goal state after:
case mpr
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
h : ∀ (z : c.pt), ∃ i x, c.ι i x = z
z : c.pt
⊢ ∃ a, F.descColimitType c a = z
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✝¹³ : Semiring R
inst✝¹² : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹¹ : (i : ι) → Module R (M₁ i)
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R M₂
inst✝⁸ : Semiring S
inst✝⁷ : Module S M₂
inst✝⁶ : SMulCommClass R S M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module S M₃
inst✝³ : Module R M₃
inst✝² : SMulCommClass R S M₃
inst✝¹ : LinearMap.CompatibleSMul M₂ M₃ S R
inst✝ : LinearMap.CompatibleSMul M₃ M₂ S R
g : M₂ ≃ₗ[R] M₃
x✝ : MultilinearMap R M₁ M₂
⊢ (LinearMap.compMultilinearMapₗ S ↑g.symm) ((LinearMap.compMultilinearMapₗ S ↑g).toFun x✝) = x✝

Tactic:
by ext; simp

Goal state after:
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✝¹³ : Semiring R
inst✝¹² : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹¹ : (i : ι) → Module R (M₁ i)
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R M₂
inst✝⁸ : Semiring S
inst✝⁷ : Module S M₂
inst✝⁶ : SMulCommClass R S M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module S M₃
inst✝³ : Module R M₃
inst✝² : SMulCommClass R S M₃
inst✝¹ : LinearMap.CompatibleSMul M₂ M₃ S R
inst✝ : LinearMap.CompatibleSMul M₃ M₂ S R
g : M₂ ≃ₗ[R] M₃
x✝ : MultilinearMap R M₁ M₃
⊢ (LinearMap.compMultilinearMapₗ S ↑g).toFun ((LinearMap.compMultilinearMapₗ S ↑g.symm) x✝) = x✝

Tactic:
by ext; simp

Goal state after:
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₂
inst✝¹ : (i : ι) → AddCommMonoid (M₁' i)
inst✝ : (i : ι) → Module R (M₁' i)
e : (i : ι) → M₁ i ≃ₗ[R] M₁' i
x✝ : MultilinearMap R M₁' M₂
⊢ (compLinearMapₗ fun x ↦ ↑(e x).symm) ((compLinearMapₗ fun x ↦ ↑(e x)).toFun x✝) = x✝

Tactic:
by ext; simp

Goal state after:
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₂
inst✝¹ : (i : ι) → AddCommMonoid (M₁' i)
inst✝ : (i : ι) → Module R (M₁' i)
e : (i : ι) → M₁ i ≃ₗ[R] M₁' i
x✝ : MultilinearMap R M₁ M₂
⊢ (compLinearMapₗ fun x ↦ ↑(e x)).toFun ((compLinearMapₗ fun x ↦ ↑(e x).symm) x✝) = x✝

Tactic:
by ext; simp

Goal state after: