mathlib-initiative/mathlib-tactics huggingface dataset:
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 ∈ τ.cycleFactorsFinset
⊢ σ.Disjoint (τ * f⁻¹)

Tactic:
rw [mem_cycleFactorsFinset_iff] at hf

Goal state after:
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
⊢ σ.Disjoint (τ * f⁻¹)
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
M₂ : Type u_10
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_11
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f✝ f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
σ : ι ≃ ι'
f : M [⋀^ι]→ₗ[R] N
⊢ domDomCongr σ.symm (domDomCongr σ f) = f

Tactic:
by
    ext
    simp [Function.comp_def]

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
M₂ : Type u_10
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_11
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
σ : ι ≃ ι'
m : M [⋀^ι']→ₗ[R] N
⊢ domDomCongr σ (domDomCongr σ.symm m) = m

Tactic:
by
    ext
    simp [Function.comp_def]

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

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.succ
x y : M 0
⊢ f (update (Fin.cons x m) 0 x) + f (update (Fin.cons x m) 0 y) = f (Fin.cons x m) + f (Fin.cons y m)

Tactic:
update_cons_zero

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

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.succ
c : R
x : M 0
⊢ c • f (update (Fin.cons x m) 0 x) = c • f (Fin.cons x m)

Tactic:
update_cons_zero

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''
⊢ f ((insert i t).piecewise (m + m') m') = ∑ s ∈ (insert i t).powerset, f (s.piecewise m m')

Tactic:
rw [A, f.map_update_add, B, C, Finset.sum_powerset_insert hit, Hrec, Hrec, add_comm (_ : M₂)]

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 ∈ t.powerset, f (s.piecewise m m') + ∑ s ∈ t.powerset, f (s.piecewise m m'') =
    ∑ t ∈ t.powerset, f (t.piecewise m m') + ∑ t ∈ t.powerset, f ((insert i t).piecewise m m')
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₂
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 : ι
h : ¬j = i
⊢ (insert i s).piecewise m m' j = s.piecewise m m'' j

Tactic:
by_cases h' : j ∈ s

Goal state after:
case pos
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 : ι
h : ¬j = i
h' : j ∈ s
⊢ (insert i s).piecewise m m' j = s.piecewise m m'' j

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₂
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 : ι
h : ¬j = i
h' : j ∉ s
⊢ (insert i s).piecewise m m' j = s.piecewise m m'' j
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
hij : i ≠ j
hσ : ∀ (k : n), σ ((swap i j) k) = σ k
⊢ ∑ τ ∈ ofSign 1, ∏ i, A i (σ i) * B (σ i) (τ i) =
    ∑ τ ∈ Finset.map (mulRightEmbedding (swap i j)) (ofSign 1), ∏ i, A i (σ i) * B (σ i) (τ i)

Tactic:
sum_map

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
hij : i ≠ j
hσ : ∀ (k : n), σ ((swap i j) k) = σ k
⊢ ∑ τ ∈ ofSign 1, ∏ i, A i (σ i) * B (σ i) (τ i) =
    ∑ x ∈ ofSign 1, ∏ i_1, A i_1 (σ i_1) * B (σ i_1) (((mulRightEmbedding (swap i j)) x) i_1)
Module: Mathlib.CategoryTheory.Filtered.Basic

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

Tactic:
have : IsFiltered C := { nonempty := ⟨i⟩ }

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsFilteredOrEmpty C
I : Type u_1
inst✝ : Finite I
i : C
j : I → C
f : (x : I) → i ⟶ j x
this : IsFiltered C
⊢ ∃ k fik g, ∀ (x : I), f x ≫ g x = fik
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsCofilteredOrEmpty C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ (h.homEquiv (eq (R.map f) (R.map g)) X).symm (eqHom (R.map f) (R.map g)) ≫ f =
    (h.homEquiv (eq (R.map f) (R.map g)) X).symm (eqHom (R.map f) (R.map g)) ≫ g

Tactic:
by
        rw [← h.homEquiv_naturality_right_symm, ← h.homEquiv_naturality_right_symm, eq_condition]

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

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimit
z : F.ColimitType
⊢ ∃ j x, c.ι j x = hc.equiv z

Tactic:
obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective z

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimit
j : J
x : F.obj j
⊢ ∃ j_1 x_1, c.ι j_1 x_1 = hc.equiv (F.ιColimitType j x)
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimitCore
G : J ⥤ Type w₀'
e : (j : J) → G.obj j ≃ F.obj j
naturality :
  ∀ {j j' : J} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)
T : Type w₂
f g : (c.precompose (fun {j'} ↦ ⇑(e j')) ⋯).pt → T
h : ∀ (j : J), f ∘ (c.precompose (fun {j'} ↦ ⇑(e j')) ⋯).ι j = g ∘ (c.precompose (fun {j'} ↦ ⇑(e j')) ⋯).ι j
j : J
⊢ f ∘ c.ι j = g ∘ c.ι j

Tactic:
by
    ext x
    obtain ⟨y, rfl⟩ := (e j).surjective x
    exact congr_fun (h j) y

Goal state after:
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 B ∪ piFinset C ⊆ piFinset A

Tactic:
· exact
        Finset.union_subset (piFinset_subset _ _ fun i => B_subset_A i)
          (piFinset_subset _ _ fun i => C_subset_A i)

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 : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
α : Type u_2
inst✝ : DecidableEq ι
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
a✝ : α
s✝ : Finset α
has : a✝ ∉ s✝
ih : f (update m i (∑ a ∈ s✝, g a)) = ∑ a ∈ s✝, f (update m i (g a))
⊢ f (update m i (∑ a ∈ insert a✝ s✝, g a)) = ∑ a ∈ insert a✝ s✝, f (update m i (g a))

Tactic:
| insert _ _ has ih =>

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
⊢ 1 = M.mk F ⟨j, 1⟩

Tactic:
by
  apply M.mk_eq
  refine ⟨max' _ j, IsFiltered.leftToMax _ j, IsFiltered.rightToMax _ j, ?_⟩
  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₂
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
m : Fin n → A
i : Fin n
c : R
x : A
⊢ (List.ofFn (update m i (c • x))).prod = c • (List.ofFn (update m i x)).prod

Tactic:
simp [List.ofFn_eq_map, (List.nodup_finRange n).map_update, List.prod_set]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ Y₁ : C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
ψ : X₂ ⟶ Y₂
⊢ (bifunctorComp₁₂Obj F₁₂ G X₁).map ψ ≫ { app := fun X₃ ↦ (G.map ((F₁₂.map φ).app Y₂)).app X₃, naturality := ⋯ } =
    { app := fun X₃ ↦ (G.map ((F₁₂.map φ).app X₂)).app X₃, naturality := ⋯ } ≫ (bifunctorComp₁₂Obj F₁₂ G Y₁).map ψ

Tactic:
ext X₃

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ Y₁ : C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
ψ : X₂ ⟶ Y₂
X₃ : C₃
⊢ ((bifunctorComp₁₂Obj F₁₂ G X₁).map ψ ≫ { app := fun X₃ ↦ (G.map ((F₁₂.map φ).app Y₂)).app X₃, naturality := ⋯ }).app
      X₃ =
    ({ app := fun X₃ ↦ (G.map ((F₁₂.map φ).app X₂)).app X₃, naturality := ⋯ } ≫ (bifunctorComp₁₂Obj F₁₂ G Y₁).map ψ).app
      X₃
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G G' : C₁₂ ⥤ C₃ ⥤ C₄
φ : G ⟶ G'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
⊢ ((bifunctorComp₁₂ F₁₂ G).obj X₁).map f ≫ { app := fun X₃ ↦ (φ.app ((F₁₂.obj X₁).obj Y₂)).app X₃, naturality := ⋯ } =
    { app := fun X₃ ↦ (φ.app ((F₁₂.obj X₁).obj X₂)).app X₃, naturality := ⋯ } ≫ ((bifunctorComp₁₂ F₁₂ G').obj X₁).map f

Tactic:
ext X₃

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G G' : C₁₂ ⥤ C₃ ⥤ C₄
φ : G ⟶ G'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ (((bifunctorComp₁₂ F₁₂ G).obj X₁).map f ≫
          { app := fun X₃ ↦ (φ.app ((F₁₂.obj X₁).obj Y₂)).app X₃, naturality := ⋯ }).app
      X₃ =
    ({ app := fun X₃ ↦ (φ.app ((F₁₂.obj X₁).obj X₂)).app X₃, naturality := ⋯ } ≫
          ((bifunctorComp₁₂ F₁₂ G').obj X₁).map f).app
      X₃
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
⊢ (((bifunctorComp₁₂FunctorObj F₁₂).obj G).obj X₁).map f ≫
      { app := fun X₃ ↦ (G.map ((φ.app X₁).app Y₂)).app X₃, naturality := ⋯ } =
    { app := fun X₃ ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ } ≫
      (((bifunctorComp₁₂FunctorObj F₁₂').obj G).obj X₁).map f

Tactic:
ext X₃

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ ((((bifunctorComp₁₂FunctorObj F₁₂).obj G).obj X₁).map f ≫
          { app := fun X₃ ↦ (G.map ((φ.app X₁).app Y₂)).app X₃, naturality := ⋯ }).app
      X₃ =
    ({ app := fun X₃ ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ } ≫
          (((bifunctorComp₁₂FunctorObj F₁₂').obj G).obj X₁).map f).app
      X₃
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ G₂₃' : C₂ ⥤ C₃ ⥤ C₂₃
φ : G₂₃ ⟶ G₂₃'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
⊢ ((bifunctorComp₂₃ F G₂₃).obj X₁).map f ≫ { app := fun X₃ ↦ (F.obj X₁).map ((φ.app Y₂).app X₃), naturality := ⋯ } =
    { app := fun X₃ ↦ (F.obj X₁).map ((φ.app X₂).app X₃), naturality := ⋯ } ≫ ((bifunctorComp₂₃ F G₂₃').obj X₁).map f

Tactic:
ext X₃

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ G₂₃' : C₂ ⥤ C₃ ⥤ C₂₃
φ : G₂₃ ⟶ G₂₃'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ (((bifunctorComp₂₃ F G₂₃).obj X₁).map f ≫ { app := fun X₃ ↦ (F.obj X₁).map ((φ.app Y₂).app X₃), naturality := ⋯ }).app
      X₃ =
    ({ app := fun X₃ ↦ (F.obj X₁).map ((φ.app X₂).app X₃), naturality := ⋯ } ≫
          ((bifunctorComp₂₃ F G₂₃').obj X₁).map f).app
      X₃
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✝ : L.IsEquivalence
⊢ IsIso h.unit

Tactic:
have := h.isEquivalence_right_of_isEquivalence_left

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✝ : L.IsEquivalence
this : R.IsEquivalence
⊢ IsIso h.unit
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
E : Type u_1
inst✝² : Category.{v_1, u_1} E
T : C ⥤ E
S : E ⥤ D
X : C
adj2 : T ⊣ S ⋙ R
inst✝¹ : R.Faithful
inst✝ : R.Full
⊢ IsIso (T.map (h.unit.app X))

Tactic:
let FF := FullyFaithful.ofFullyFaithful R

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
E : Type u_1
inst✝² : Category.{v_1, u_1} E
T : C ⥤ E
S : E ⥤ D
X : C
adj2 : T ⊣ S ⋙ R
inst✝¹ : R.Faithful
inst✝ : R.Full
FF : R.FullyFaithful := FullyFaithful.ofFullyFaithful R
⊢ IsIso (T.map (h.unit.app X))
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
W X Y Z : D
⊢ F.map ((α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom) =
    F.map ((α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom)

Tactic:
simp only [Functor.map_comp, fData.whiskerRight_eq, fData.associator_eq, Iso.trans_assoc,
      Iso.trans_hom, Iso.symm_hom, tensorIso_hom, Iso.refl_hom, tensorHom_id, id_tensorHom,
      comp_whiskerRight, whisker_assoc, assoc, fData.whiskerLeft_eq, whiskerLeft_comp,
      Iso.hom_inv_id_assoc, whiskerLeft_hom_inv_assoc, hom_inv_whiskerRight_assoc,
      Iso.inv_hom_id_assoc, Iso.cancel_iso_inv_left]
    slice_lhs 5 6 =>
      rw [← whiskerLeft_comp, hom_inv_whiskerRight]
    rw [whisker_exchange_assoc]
    simp

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

Goal state before:
pp: M : Type u
inst✝ : Monoid M
X x✝¹ x✝ : Discrete M
f : x✝¹ ⟶ x✝
⊢ { as := X.as * x✝¹.as } = { as := X.as * x✝.as }

Tactic:
by rw [eq_of_hom f]

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

Goal state before:
pp: M : Type u
inst✝ : Monoid M
X₁✝ X₂✝ : Discrete M
f : X₁✝ ⟶ X₂✝
X : Discrete M
⊢ { as := X₁✝.as * X.as } = { as := X₂✝.as * X.as }

Tactic:
by rw [eq_of_hom f]

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.LaxMonoidal
X Y Z : C
⊢ μ F X Y ▷ F.obj Z ≫ μ F (X ⊗ Y) Z =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv

Tactic:
rw [← associativity_assoc, ← F.map_comp, Iso.hom_inv_id, map_id, Category.comp_id]

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.Monoidal
X Y Z : C
⊢ F.map (α_ X Y Z).hom =
    δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z)

Tactic:
by
  rw [← LaxMonoidal.associativity F, whiskerRight_δ_μ_assoc, δ_μ_assoc]

Goal state after: