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

Goal state before:
pp: case pos
α : 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
hfx : f x = x
⊢ (τ * f⁻¹) x = x

pp: case neg
α : 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
hfx : ¬f x = x
⊢ (τ * f⁻¹) x = x

Tactic:
· rw [← hfx]
            simpa [hx] using hfx.symm

Goal state after:
case neg
α : 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
hfx : ¬f x = x
⊢ (τ * f⁻¹) x = x
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
a b c : R
inst✝ : IsCancelAdd R
hab : A.IsDetpBalanced a b
hbc : A.IsDetpBalanced b c
⊢ A.IsDetpBalanced a c

Tactic:
by
  rw [IsDetpBalanced] at *
  apply add_left_cancel (a := b * detp 1 A + b * detp (-1) A)
  convert congr($hab + $hbc) using 1 <;> abel

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
⊢ Aᵀ.Nonsingular ↔ A.Nonsingular

Tactic:
by simp [Nonsingular]

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
A : Matrix n n R
e₁ e₂ : m ≃ n
⊢ (A.submatrix ⇑e₁ ⇑e₂).Nonsingular ↔ A.Nonsingular

Tactic:
by simp [Nonsingular]

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

Goal state before:
pp: case neg
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'
mf' : ⟨X', ⟨Y', ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H'
h : ¬(X = X' ∧ Y = Y')
⊢ (f' ≫ T' mY') ≫ coeqHom (f ≫ T' mY) (T' mX) = (fun {X_1} mZ ↦ T' mZ ≫ coeqHom (f ≫ T' mY) (T' mX)) mX'

Tactic:
rw [@w' _ _ mX' mY' f' _]

Goal state after:
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'
mf' : ⟨X', ⟨Y', ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H'
h : ¬(X = X' ∧ Y = Y')
⊢ ⟨X', ⟨Y', ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ H'
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
s t : ℤˣ
h : s ≠ t
σ : Perm n
hσ : σ ∈ ofSign s
τ : Perm n
⊢ τ ∈ ofSign t → IsAddUnit ((∏ k, A k (σ k)) * ∏ k, B k (τ k))

Tactic:
hτ

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 : ℤˣ
h : s ≠ t
σ : Perm n
hσ : σ ∈ ofSign s
τ : Perm n
hτ : τ ∈ ofSign t
⊢ IsAddUnit ((∏ k, A k (σ k)) * ∏ k, B k (τ k))
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case insert
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
c : n → R
a : R
k : n
s✝ : Finset n
hk : k ∉ s✝
h_ind : j ∉ s✝ → (M.updateRow j (a • M j + ∑ k ∈ s✝, c k • M k)).det = a • M.det
hj : j ∉ insert k s✝
⊢ (M.updateRow j (a • M j + ∑ k ∈ insert k s✝, c k • M k)).det = a • M.det

Tactic:
have h : k ≠ j := fun h ↦ (h ▸ hj) (Finset.mem_insert_self _ _)

Goal state after:
case insert
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
c : n → R
a : R
k : n
s✝ : Finset n
hk : k ∉ s✝
h_ind : j ∉ s✝ → (M.updateRow j (a • M j + ∑ k ∈ s✝, c k • M k)).det = a • M.det
hj : j ∉ insert k s✝
h : k ≠ j
⊢ (M.updateRow j (a • M j + ∑ k ∈ insert k s✝, c k • M k)).det = a • 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
s t : ℤˣ
h : s ≠ t
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : σ ∈ {x ∈ ofSign t | x j = k}
τ : Perm n
⊢ τ ∈ ofSign s → IsAddUnit ((∏ k, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Tactic:
hτ

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 : ℤˣ
h : s ≠ t
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : σ ∈ {x ∈ ofSign t | x j = k}
τ : Perm n
hτ : τ ∈ ofSign s
⊢ IsAddUnit ((∏ k, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))
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
⊢ (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)

Tactic:
have Brec : (f fun i => ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i => g i (r i) := by
    have : ∑ i, #(B i) < ∑ i, #(A i) := by
      refine sum_lt_sum (fun i _ => card_le_card (B_subset_A i)) ⟨i₀, mem_univ _, ?_⟩
      have : {j₂} ⊆ A i₀ := by simp [hj₂]
      simp only [B, Finset.card_sdiff_of_subset this, Function.update_self, Finset.card_singleton]
      exact Nat.pred_lt (ne_of_gt (lt_trans Nat.zero_lt_one hi₀))
    rw [h] at this
    exact IH _ this B rfl

Goal state after:
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)
⊢ (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: case neg
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'
mf' : ⟨X', ⟨Y', ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H'
h : ¬(X = X' ∧ Y = Y')
⊢ eqHom (T' mX ≫ f) (T' mY) ≫ T' mX' ≫ f' = (fun {X_1} mZ ↦ eqHom (T' mX ≫ f) (T' mY) ≫ T' mZ) mY'

Tactic:
rw [@w' _ _ mX' mY' f' _]

Goal state after:
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'
mf' : ⟨X', ⟨Y', ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ insert ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ H'
h : ¬(X = X' ∧ Y = Y')
⊢ ⟨X', ⟨Y', ⟨mX', ⟨mY', f'⟩⟩⟩⟩ ∈ H'
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case H₁
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) := ⋯
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) := ⋯
C : (a : ι) → Finset (α a) := ⋯
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)
⊢ piFinset A ⊆ piFinset B ∪ piFinset C

Tactic:
intro r hr
      by_cases hri₀ : r i₀ = j₂
      · apply Finset.mem_union_right
        refine mem_piFinset.2 fun i => ?_
        by_cases hi : i = i₀
        · have : r i₀ ∈ C i₀ := by simp [C, hri₀]
          rwa [hi]
        · simp [C, hi, mem_piFinset.1 hr i]
      · apply Finset.mem_union_left
        refine mem_piFinset.2 fun i => ?_
        by_cases hi : i = i₀
        · have : r i₀ ∈ B i₀ := by simp [B, hri₀, mem_piFinset.1 hr i₀]
          rwa [hi]
        · simp [B, hi, mem_piFinset.1 hr i]

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
x y : (j : J) × F.obj j
x✝ : F.ColimitTypeRel x y
f : x.fst ⟶ y.fst
h : y.snd = (hom (F.map f)) x.snd
⊢ y.snd = (hom (F.map (𝟙 y.fst))) y.snd

Tactic:
Functor.map_id,

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
x y : (j : J) × F.obj j
x✝ : F.ColimitTypeRel x y
f : x.fst ⟶ y.fst
h : y.snd = (hom (F.map f)) x.snd
⊢ y.snd = (hom (𝟙 (F.obj y.fst))) y.snd
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₃
ι' : Type u_1
σ : ι ≃ ι'
c : S
f : MultilinearMap R M₁ M₂
⊢ { toFun := ⇑(c • f) ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ } =
    (RingHom.id S) c • { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ }

Tactic:
ext
    simp only [Function.comp, coe_mk, smul_apply, RingHom.id_apply]

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) ⟨⋯.some, 1⟩.snd = (ConcreteCategory.hom (F.map g)) ⟨j, 1⟩.snd

Tactic:
refine ⟨max' _ j, IsFiltered.leftToMax _ j, IsFiltered.rightToMax _ j, ?_⟩

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j : J
⊢ (ConcreteCategory.hom (F.map (IsFiltered.leftToMax ⟨⋯.some, 1⟩.fst j))) ⟨⋯.some, 1⟩.snd =
    (ConcreteCategory.hom (F.map (IsFiltered.rightToMax ⟨⋯.some, 1⟩.fst j))) ⟨j, 1⟩.snd
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)
inst✝ : DecidableEq ι
f : (i : ι) → M₁ i →ₗ[R] M₁' i
i : ι
⊢ ∀ (c : R) (x : M₁ i →ₗ[R] M₁' i), compLinearMapₗ (update f i (c • x)) = c • compLinearMapₗ (update f i x)

Tactic:
a

Goal state after:
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)
inst✝ : DecidableEq ι
f : (i : ι) → M₁ i →ₗ[R] M₁' i
i : ι
a : R
⊢ ∀ (x : M₁ i →ₗ[R] M₁' i), compLinearMapₗ (update f i (a • x)) = a • compLinearMapₗ (update f i x)
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
      (M.mk F ⟨i, x⟩ * M.mk F ⟨j, y⟩) =
    (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
        (M.mk F ⟨i, x⟩) *
      (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
        (M.mk F ⟨j, y⟩)

Tactic:
rw [colimit_mul_mk_eq F ⟨i, x⟩ ⟨j, y⟩ (max' i j) (IsFiltered.leftToMax i j)
        (IsFiltered.rightToMax i j)]

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
      (M.mk F
        ⟨IsFiltered.max i j,
          (ConcreteCategory.hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd *
            (ConcreteCategory.hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩) =
    (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
        (M.mk F ⟨i, x⟩) *
      (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
        (M.mk F ⟨j, y⟩)
Module: Mathlib.CategoryTheory.Limits.Types.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
⊢ (∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c.π.app j)) x = s j) ↔ ∀ (b : ↑F.sections), ∃! a, sectionOfCone c a = b

Tactic:
Subtype.forall,

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
⊢ (∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c.π.app j)) x = s j) ↔
    ∀ (a : (j : J) → F.obj j) (b : a ∈ F.sections), ∃! a_1, sectionOfCone c a_1 = ⟨a, b⟩
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case empty
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
⊢ f a - f a = 0

Tactic:
sub_self

Goal state after:
case empty
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
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case pos.refl
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
h₁ : ¬(k = k ∨ k ∈ s → k < k)
⊢ s.piecewise b a k - b k = a k - b k

Tactic:
s.piecewise_eq_of_notMem _ _ (lt_irrefl _ <| hk k ·)

Goal state after:
case pos.refl
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
h₁ : ¬(k = k ∨ k ∈ s → k < k)
⊢ a k - b k = a k - b k
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
J : Type w
inst✝ : Category.{r, w} J
F : J ⥤ C
D : Cocone F
i j : J
x : ToType (F.obj i)
y : ToType (F.obj j)
h : ∃ k f g, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) y
⊢ (ConcreteCategory.hom (D.ι.app i)) x = (ConcreteCategory.hom (D.ι.app j)) y

Tactic:
by
  let E := (forget C).mapCocone D
  obtain ⟨k, f, g, (hfg : (F ⋙ forget C).map f x = F.map g y)⟩ := h
  let h1 : (F ⋙ forget C).map f ≫ E.ι.app k = E.ι.app i := E.ι.naturality f
  let h2 : (F ⋙ forget C).map g ≫ E.ι.app k = E.ι.app j := E.ι.naturality g
  change E.ι.app i x = E.ι.app j y
  rw [← h1, comp_apply, hfg]
  exact ConcreteCategory.congr_hom h2 y

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 = g

Tactic:
by
    apply Mono.right_cancellation (f := h.unit.app Y)
    apply (h.homEquiv X (L.obj Y)).symm.injective
    simpa using hfg

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Finite J
val✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
⊢ ∑ j, ((tensorLeft X).mapBicone b).π j ≫ ((tensorLeft X).mapBicone b).ι j = 𝟙 ((tensorLeft X).mapBicone b).pt

Tactic:
dsimp
            simp_rw [← id_tensorHom]
            simp only [tensorHom_comp_tensorHom, Category.comp_id, ← tensor_sum, ← id_tensorHom_id,
              IsBilimit.total i]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z = F.map (𝟙 (X ⊗ Y ⊗ Z)) ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z

Tactic:
Functor.map_id,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z = 𝟙 (F.obj (X ⊗ Y ⊗ Z)) ≫ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
f g h i j : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
θ : i ⟶ j
ι : h ⟶ j
e_ι : ηs ≫ θ = ι
⊢ (α.hom ≫ η ≫ ηs) ≫ θ = α.hom ≫ η ≫ ι

Tactic:
simp [e_ι]

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).1 ≫ F.map (𝟙 (𝟙_ (C × C)).1) = ε F

Tactic:
Functor.map_id,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).1 ≫ 𝟙 (F.obj (𝟙_ (C × C)).1) = ε F
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).2 ≫ G.map (𝟙 (𝟙_ (C × C)).2) = ε G

Tactic:
Functor.map_id,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).2 ≫ 𝟙 (G.obj (𝟙_ (C × C)).2) = ε G