mathlib-initiative/mathlib-tactics huggingface dataset:
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)
r : (a : ι) → α a
hr : r ∈ piFinset A
hri₀ : ¬r i₀ = j₂
⊢ r ∈ piFinset B ∪ piFinset C

Tactic:
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
⊢ (hom (F.map f)) x.snd = (hom (F.map (𝟙 y.fst))) y.snd

Tactic:
rw [← h, Functor.map_id, id_apply]

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)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝ : DecidablePred P
h : DecidableEq { a // ¬P a }
m : (i : { a // ¬P a }) → M₁ ↑i
i : { a // ¬P a }
x y : M₁ ↑i
⊢ f.domDomRestrict P (update m i (x + y)) = f.domDomRestrict P (update m i x) + f.domDomRestrict P (update m i y)

Tactic:
ext v

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)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝ : DecidablePred P
h : DecidableEq { a // ¬P a }
m : (i : { a // ¬P a }) → M₁ ↑i
i : { a // ¬P a }
x y : M₁ ↑i
v : (i : { a // P a }) → M₁ ↑i
⊢ (f.domDomRestrict P (update m i (x + y))) v =
    (f.domDomRestrict P (update m i x) + f.domDomRestrict P (update m i y)) v
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)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝ : DecidablePred P
h : DecidableEq { a // ¬P a }
m : (i : { a // ¬P a }) → M₁ ↑i
i : { a // ¬P a }
c : R
x : M₁ ↑i
⊢ f.domDomRestrict P (update m i (c • x)) = c • f.domDomRestrict P (update m i x)

Tactic:
ext v

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)
f : MultilinearMap R M₁ M₂
P : ι → Prop
inst✝ : DecidablePred P
h : DecidableEq { a // ¬P a }
m : (i : { a // ¬P a }) → M₁ ↑i
i : { a // ¬P a }
c : R
x : M₁ ↑i
v : (i : { a // P a }) → M₁ ↑i
⊢ (f.domDomRestrict P (update m i (c • x))) v = (c • f.domDomRestrict P (update m i x)) v
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case convert_2.inr
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
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range).toFinset
h1 : ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)
a : m
ha : ¬∃ y, Sum.inl y = σ (Sum.inl a)
b : n
hx : σ (Sum.inl a) = Sum.inr b
⊢ ↑↑(sign σ) * ∏ i, fromBlocks A B 0 D (σ i) i = 0

Tactic:
rw [Finset.prod_eq_zero (Finset.mem_univ (Sum.inl a)), mul_zero]

Goal state after:
case convert_2.inr
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
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range).toFinset
h1 : ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)
a : m
ha : ¬∃ y, Sum.inl y = σ (Sum.inl a)
b : n
hx : σ (Sum.inl a) = Sum.inr b
⊢ fromBlocks A B 0 D (σ (Sum.inl a)) (Sum.inl a) = 0
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)
⊢ (ConcreteCategory.hom (t.ι.app (IsFiltered.max i j))) ((ConcreteCategory.hom (F.map (IsFiltered.leftToMax i j))) x) *
      (ConcreteCategory.hom (t.ι.app (IsFiltered.max i j)))
        ((ConcreteCategory.hom (F.map (IsFiltered.rightToMax i j))) y) =
    (ConcreteCategory.hom (t.ι.app i)) x * (ConcreteCategory.hom (t.ι.app j)) y

Tactic:
t.w_apply,

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)
⊢ (ConcreteCategory.hom (t.ι.app i)) x *
      (ConcreteCategory.hom (t.ι.app (IsFiltered.max i j)))
        ((ConcreteCategory.hom (F.map (IsFiltered.rightToMax i j))) y) =
    (ConcreteCategory.hom (t.ι.app i)) x * (ConcreteCategory.hom (t.ι.app j)) y
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
i : J
x : ↑((F ⋙ forget₂ CommMonCat MonCat).obj i)
j : J
y : ↑((F ⋙ forget₂ CommMonCat MonCat).obj j)
k : J := IsFiltered.max i j
f : i ⟶ IsFiltered.max i j := IsFiltered.leftToMax i j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨i, x⟩ *
      MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨j, y⟩ =
    MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨j, y⟩ *
      MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨i, x⟩

Tactic:
let g := IsFiltered.rightToMax i j

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommMonCat
i : J
x : ↑((F ⋙ forget₂ CommMonCat MonCat).obj i)
j : J
y : ↑((F ⋙ forget₂ CommMonCat MonCat).obj j)
k : J := IsFiltered.max i j
f : i ⟶ IsFiltered.max i j := IsFiltered.leftToMax i j
g : j ⟶ IsFiltered.max i j := IsFiltered.rightToMax i j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨i, x⟩ *
      MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨j, y⟩ =
    MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨j, y⟩ *
      MonCat.FilteredColimits.M.mk (F ⋙ forget₂ CommMonCat MonCat) ⟨i, x⟩
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
h : ∀ s ∈ F.sections, ∃! x, ∀ (j : J), (hom (c✝.π.app j)) x = s j
this : ∀ (c : Cone F) (y : c.pt), ∃! x, ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j
x : (c : Cone F) → c.pt → c✝.pt
hx :
  ∀ (c : Cone F) (y : c.pt),
    (fun x ↦ ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j) (x c y) ∧
      ∀ (y_1 : c✝.pt), (fun x ↦ ∀ (j : J), (hom (c✝.π.app j)) x = ↑(sectionOfCone c y) j) y_1 → y_1 = x c y
c : Cone F
f : c.pt ⟶ c✝.pt
hf : ∀ (j : J), f ≫ c✝.π.app j = c.π.app j
⊢ f = ↾x c

Tactic:
ext y; exact (hx c y).2 (f y) (fun j ↦ congr_hom (hf j) y)

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cone F
t : IsLimit c
x : ↑F.sections
j : J
⊢ (hom (c.π.app j)) ((isLimitEquivSections t).symm x) = ↑x j

Tactic:
by
  conv_rhs => rw [← (isLimitEquivSections t).right_inv x]
  rfl

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this✝¹ : (Cocone.functoriality K F).map f = i.hom
this✝ : IsIso ((Cocone.functoriality K F).map f)
this : IsIso f
⊢ IsColimit d

Tactic:
exact IsColimit.ofIsoColimit hd' (asIso f)

Goal state after:
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
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × ToType (F.obj j) → ToType D.pt := fun a ↦ (ConcreteCategory.hom (D.ι.app a.fst)) a.snd
x : ToType D.pt
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
⊢ ∃ a, ff a = x

Tactic:
obtain ⟨j, y, hy⟩ := Types.jointly_surjective_of_isColimit hE x

Goal state after:
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
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × ToType (F.obj j) → ToType D.pt := fun a ↦ (ConcreteCategory.hom (D.ι.app a.fst)) a.snd
x : ToType D.pt
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
j : J
y : (F ⋙ forget C).obj j
hy : (ConcreteCategory.hom (E.ι.app j)) y = x
⊢ ∃ a, ff a = x
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
⊢ (limit F).map f ≫ (limitObjIsoLimitCompEvaluation F j).hom =
    (limitObjIsoLimitCompEvaluation F i).hom ≫ limMap (F.whiskerLeft ((evaluation K C).map f))

Tactic:
limit_map_limitObjIsoLimitCompEvaluation_hom

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
⊢ (limitObjIsoLimitCompEvaluation F i).hom ≫ limMap (F.whiskerLeft ((evaluation K C).map f)) =
    (limitObjIsoLimitCompEvaluation F i).hom ≫ limMap (F.whiskerLeft ((evaluation K C).map f))
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.Full
inst✝ : L.Faithful
⊢ IsIso (whiskerRight h.counit R)

Tactic:
by
  have := h.right_triangle
  rw [← IsIso.eq_inv_comp, Iso.inv_comp_eq] at this
  rw [this]
  infer_instance

Goal state after:
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
X₁ Y₁ X₂ Y₂ : D
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ (fData.μIso X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (fData.μIso Y₁ Y₂).hom =
    ((fData.μIso X₁ X₂).inv ≫ F.map f ▷ F.obj X₂ ≫ (fData.μIso Y₁ X₂).hom) ≫ F.map (Y₁ ◁ g)

Tactic:
fData.whiskerLeft_eq

Goal state after:
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
X₁ Y₁ X₂ Y₂ : D
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ (fData.μIso X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (fData.μIso Y₁ Y₂).hom =
    ((fData.μIso X₁ X₂).inv ≫ F.map f ▷ F.obj X₂ ≫ (fData.μIso Y₁ X₂).hom) ≫
      (fData.μIso Y₁ X₂).inv ≫ F.obj Y₁ ◁ F.map g ≫ (fData.μIso Y₁ Y₂).hom
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
⊢ IsLimit ((forget₂ SemiRingCat MonCat).mapCone (limitCone F))

Tactic:
by
  let _ : Small.{u} (Functor.sections ((F ⋙ forget₂ _ MonCat) ⋙ forget MonCat)) :=
    inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget SemiRingCat))
  apply MonCat.HasLimits.limitConeIsLimit (F ⋙ forget₂ SemiRingCat MonCat.{u})

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
⊢ (∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)) → Linear R F

Tactic:
refine fun h => ⟨fun {X Y} f r => ?_⟩

Goal state after:
case mpr
R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
h : ∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)
X Y : C
f : X ⟶ Y
r : R
⊢ F.map (r • f) = r • F.map f
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
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ (biproduct.uniqueUpToIso ((tensorLeft X).obj ∘ f) (isBilimitOfPreserves (tensorLeft X) (biproduct.isBilimit f))).hom ≫
      biproduct.π (fun j ↦ X ⊗ f j) j✝ =
    (∑ j, X ◁ biproduct.π f j ≫ biproduct.ι (fun j ↦ X ⊗ f j) j) ≫ biproduct.π (fun j ↦ X ⊗ f j) j✝

Tactic:
biproduct.lift_π

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ { pt := X ⊗ (biproduct.bicone f).pt, π := fun j ↦ X ◁ biproduct.π f j, ι := fun j ↦ X ◁ biproduct.ι f j, ι_π := ⋯ }.π
      j✝ =
    (∑ j, X ◁ biproduct.π f j ≫ biproduct.ι (fun j ↦ X ⊗ f j) j) ≫ biproduct.π (fun j ↦ X ⊗ f j) j✝
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
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ (biproduct.uniqueUpToIso ((tensorRight X).obj ∘ f)
          (isBilimitOfPreserves (tensorRight X) (biproduct.isBilimit f))).hom ≫
      biproduct.π (fun j ↦ f j ⊗ X) j✝ =
    (∑ j, biproduct.π f j ▷ X ≫ biproduct.ι (fun j ↦ f j ⊗ X) j) ≫ biproduct.π (fun j ↦ f j ⊗ X) j✝

Tactic:
biproduct.lift_π

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ { pt := (biproduct.bicone f).pt ⊗ X, π := fun j ↦ biproduct.π f j ▷ X, ι := fun j ↦ biproduct.ι f j ▷ X, ι_π := ⋯ }.π
      j✝ =
    (∑ j, biproduct.π f j ▷ X ≫ biproduct.ι (fun j ↦ f j ⊗ X) j) ≫ biproduct.π (fun j ↦ f j ⊗ X) j✝
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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X Y Z : C
⊢ (μIso X Y).hom ▷ F.obj Z ≫ (μIso (X ⊗ Y) Z).hom ≫ F.map (α_ X Y Z).hom =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ (μIso Y Z).hom ≫ (μIso X (Y ⊗ Z)).hom

Tactic:
← cancel_epi ((μIso X Y).inv ▷ F.obj Z),

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
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X Y Z : C
⊢ (μIso X Y).inv ▷ F.obj Z ≫ (μIso X Y).hom ▷ F.obj Z ≫ (μIso (X ⊗ Y) Z).hom ≫ F.map (α_ X Y Z).hom =
    (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ (μIso Y Z).hom ≫ (μIso X (Y ⊗ Z)).hom
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : C ⥤ D
⊢ fst ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)) =
    (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt).hom ≫ (c.map G).fst

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : C ⥤ D
⊢ snd ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)) =
    (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt).hom ≫ (c.map G).snd

Tactic:
· dsimp only [fst]
        simp

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : C ⥤ D
⊢ snd ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)) =
    (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt).hom ≫ (c.map G).snd
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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ (adj.homEquiv (𝟙_ C ⊗ G.obj X) X).symm (λ_ (G.obj X)).hom =
    (adj.homEquiv (𝟙_ C ⊗ G.obj X) X).symm
      ((adj.homEquiv (𝟙_ C) (𝟙_ D)) (η F) ▷ G.obj X ≫
        (adj.homEquiv (G.obj (𝟙_ D) ⊗ G.obj X) (𝟙_ D ⊗ X))
            (δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X)) ≫
          G.map (λ_ X).hom)

Tactic:
rw [homEquiv_counit, homEquiv_counit, homEquiv_unit, homEquiv_unit, comp_whiskerRight,
      map_comp, map_comp, map_comp, map_comp, map_comp, map_comp, assoc, assoc, assoc, assoc,
      assoc, counit_naturality, counit_naturality_assoc, counit_naturality_assoc,
      left_triangle_components_assoc, ← δ_natural_left_assoc, ← δ_natural_left_assoc,
      tensorHom_def, assoc, ← MonoidalCategory.comp_whiskerRight_assoc,
      ← MonoidalCategory.comp_whiskerRight_assoc, assoc, counit_naturality,
      left_triangle_components_assoc, id_whiskerLeft, assoc, assoc, Iso.inv_hom_id, comp_id,
      left_unitality_hom_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
⊢ ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (β X Z).hom = (β X Y).hom ≫ f ▷ X

Tactic:
intros
    apply F.map_injective
    refine (cancel_epi (μ F ?_ ?_)).1 ?_
    rw [Functor.map_comp, ← μ_natural_right_assoc, w, Functor.map_comp,
      reassoc_of% w, braiding_naturality_right_assoc, μ_natural_left]

Goal state after: