mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : MonoidalCategory D
F G : D ⥤ ((i : I) → C i)
inst✝² : F.LaxMonoidal
inst✝¹ : G.LaxMonoidal
τ : (i : I) → F ⋙ eval C i ⟶ G ⋙ eval C i
inst✝ : ∀ (i : I), NatTrans.IsMonoidal (τ i)
X Y : D
⊢ Functor.LaxMonoidal.μ F X Y ≫ (NatTrans.pi' τ).app (X ⊗ Y) =
    ((NatTrans.pi' τ).app X ⊗ₘ (NatTrans.pi' τ).app Y) ≫ Functor.LaxMonoidal.μ G X Y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Finite α
f : α → ι
i : ι
⊢ o.matrixDecomposition (𝟙 (⨁ fun a ↦ s (f a))) i = 1

Tactic:
by

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

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ (x✝¹ + 1) • x✝ = x✝¹ • x✝ + x✝

Tactic:
by

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

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
n : ℤ
α : u ⟶ v
⊢ L.map (n • α.left) ≫ v.hom = u.hom ≫ R.map (n • α.right)

Tactic:
by

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

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ x✝ : u ⟶ v
⊢ x✝¹ - x✝ = x✝¹ + -x✝

Tactic:
by

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

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
⊢ ∀ (a : u ⟶ v), 0 • a = 0

Tactic:
by

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

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ ↑x✝¹.succ • x✝ = ↑x✝¹ • x✝ + x✝

Tactic:
by

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

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ Int.negSucc x✝¹ • x✝ = -(↑x✝¹.succ • x✝)

Tactic:
by

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

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝ : u ⟶ v
⊢ -x✝ + x✝ = 0

Tactic:
by

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

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ x✝ : u ⟶ v
⊢ x✝¹ + x✝ = x✝ + x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
M N : DMatrix m n α
h : M = N
⊢ ∀ (i : m) (j : n), M i j = N i j

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
M : DMatrix m n α
β : m → n → Type w
γ : m → n → Type z
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
g : ⦃i : m⦄ → ⦃j : n⦄ → β i j → γ i j
⊢ (M.map f).map g = M.map fun x x_1 x_2 ↦ g (f x_2)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → Zero (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → Zero (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
h : ∀ (i : m) (j : n), f 0 = 0
⊢ map 0 f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
⊢ ((M + N).map fun i j ↦ ⇑f) = (M.map fun i j ↦ ⇑f) + N.map fun i j ↦ ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
⊢ ((M - N).map fun i j ↦ ⇑f) = (M.map fun i j ↦ ⇑f) - N.map fun i j ↦ ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝ : IsEmpty m
M N : DMatrix m n α
⊢ M = N

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝ : IsEmpty n
M N : DMatrix m n α
⊢ M = N

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
⊢ (DMatrix.map 0 fun i j ↦ ⇑f) = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
i : ι
⊢ o.matrixDecomposition (z ≫ w) i = o.matrixDecomposition w i * o.matrixDecomposition z i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteBiproducts C
R : Type u_2
inst✝³ : Semiring R
inst✝² : Linear R C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
w : R
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
⊢ o.matrixDecompositionAddEquiv.toFun (w • z) = (RingHom.id R) w • o.matrixDecompositionAddEquiv.toFun z

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a ↦ s (f a)) ≅ ⨁ fun b ↦ s (g b)
c : ι
val✝¹ : Fintype α
val✝ : Fintype β
⊢ o.matrixDecomposition i.inv c * o.matrixDecomposition i.hom c = 1

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a ↦ s (f a)) ≅ ⨁ fun b ↦ s (g b)
c : ι
val✝¹ : Fintype α
val✝ : Fintype β
⊢ o.matrixDecomposition i.hom c * o.matrixDecomposition i.inv c = 1

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a ↦ s (f a)) ≅ ⨁ fun b ↦ s (g b)
⊢ ∃ e, ∀ (a : α), g (e a) = f a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.EckmannHilton

Goal state before:
pp: X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
⊢ e₁ = e₂

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.EckmannHilton

Goal state before:
pp: X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.EckmannHilton

Goal state before:
pp: X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ (m₂ a e₁) (m₂ e₁ b) = m₂ a b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.EckmannHilton

Goal state before:
pp: X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
⊢ m₁ = m₂

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.EckmannHilton

Goal state before:
pp: X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₂ a b = m₂ b a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.EckmannHilton

Goal state before:
pp: X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b c : X
⊢ m₂ (m₂ a b) c = m₂ a (m₂ b c)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
⊢ ∀ (f : X ⟶ Y), biprod.lift f 0 = f ≫ biprod.inl

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
hl : ∀ (f : X ⟶ Y), biprod.lift f 0 = f ≫ biprod.inl
f : X ⟶ Y
⊢ leftAdd X Y 0 f = f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
hl : ∀ (f : X ⟶ Y), biprod.lift f 0 = f ≫ biprod.inl
f : X ⟶ Y
⊢ leftAdd X Y f 0 = f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ EckmannHilton.IsUnital (fun x1 x2 ↦ leftAdd X Y x1 x2) 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
h₂ : ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f
⊢ ∀ (f : X ⟶ Y), biprod.desc f 0 = biprod.fst ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
h₂ : ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f
h₁ : ∀ (f : X ⟶ Y), biprod.desc f 0 = biprod.fst ≫ f
f : X ⟶ Y
⊢ rightAdd X Y 0 f = f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
h₂ : ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f
h₁ : ∀ (f : X ⟶ Y), biprod.desc f 0 = biprod.fst ≫ f
f : X ⟶ Y
⊢ rightAdd X Y f 0 = f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ EckmannHilton.IsUnital (fun x1 x2 ↦ rightAdd X Y x1 x2) 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
⊢ biprod.inl ≫ diag = biprod.lift f h

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
⊢ biprod.inr ≫ diag = biprod.lift g k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
this : HasLiftingProperty 0 p
⊢ 0 ≫ p = 0 ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
⊢ biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
this : HasLiftingProperty 0 p
sq : CommSq 0 0 p f
⊢ sq.lift ≫ p = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
i : Z ⟶ P
hZ : IsZero Z
⊢ Projective P ↔ (MorphismProperty.epimorphisms C).llp i

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
diag : X ⊞ X ⟶ Y ⊞ Y := biprod.lift (biprod.desc f g) (biprod.desc h k)
hd₁ : biprod.inl ≫ diag = biprod.lift f h
hd₂ : biprod.inr ≫ diag = biprod.lift g k
h₁ : biprod.lift (rightAdd X Y f g) (rightAdd X Y h k) = biprod.lift (𝟙 X) (𝟙 X) ≫ diag
⊢ diag ≫ biprod.desc (𝟙 Y) (𝟙 Y) = biprod.desc (leftAdd X Y f h) (leftAdd X Y g k)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
I : IsIso f
⊢ f ≠ 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
f : End X
hf : f ≠ 0
⊢ (f * if h : f = 0 then 0 else inv f) = 1

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : DivisionRing 𝕜
inst✝³ : HasKernels C
inst✝² : Linear 𝕜 C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
h : ∀ (a : X ≅ Y), False
f : X ⟶ Y
⊢ f = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
⊢ IsIso (𝟙 X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f g h k : X ⟶ Y
⊢ leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
⊢ finrank 𝕜 (X ⟶ X) = 1

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ (f + g) ≫ h = f ≫ h + g ≫ h

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : IsAlgClosed 𝕜
inst✝² : Linear 𝕜 C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
I : FiniteDimensional 𝕜 (X ⟶ X)
f g : End X
⊢ f * g = g * f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : IsAlgClosed 𝕜
inst✝² : Linear 𝕜 C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
I : FiniteDimensional 𝕜 (X ⟶ X)
⊢ Field (End X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ f ≫ (g + h) = f ≫ g + f ≫ h

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
c : 𝕜
w : c • 𝟙 X = g ≫ inv f
⊢ c • f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Adjunction

Goal state before:
pp: C : Type u
D : Type u'
inst✝⁴ : Category.{v, u} C
inst✝³ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
X : C
inst✝¹ : IsCardinalPresentable X κ
inst✝ : G.IsCardinalAccessible κ
⊢ IsCardinalPresentable (F.obj X) κ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Adjunction

Goal state before:
pp: C : Type u
D : Type u'
inst✝⁴ : Category.{v, u} C
inst✝³ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
X : C
inst✝¹ : IsCardinalPresentable X κ
inst✝ : G.IsCardinalAccessible κ
⊢ IsCardinalPresentable (F.obj X) κ

Tactic:
by
  rw [isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj.{v}]
  exact Functor.isCardinalAccessible_of_natIso
    (show G ⋙ _ ≅ _ from (Adjunction.compUliftCoyonedaIso.{0} adj).symm.app (op X)) κ

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Adjunction

Goal state before:
pp: C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
P : ObjectProperty C
hP : P.IsCardinalFilteredGenerator κ
inst✝² : G.IsCardinalAccessible κ
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ P.map F ≤ isCardinalPresentable D κ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Adjunction

Goal state before:
pp: C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
P : ObjectProperty C
hP : P.IsCardinalFilteredGenerator κ
inst✝² : G.IsCardinalAccessible κ
inst✝¹ : G.Full
inst✝ : G.Faithful
Y : D
⊢ ∃ J x, ∃ (_ : IsCardinalFiltered J κ), (P.map F).colimitsOfShape J Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Adjunction

Goal state before:
pp: C : Type u
D : Type u'
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
inst✝³ : HasCardinalFilteredGenerator C κ
inst✝² : G.IsCardinalAccessible κ
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ ∃ P, ∃ (_ : ObjectProperty.EssentiallySmall.{w, v', u'} P), P.IsCardinalFilteredGenerator κ

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Adjunction

Goal state before:
pp: C : Type u
D : Type u'
inst✝² : Category.{v, u} C
inst✝¹ : Category.{v', u'} D
e : C ≌ D
inst✝ : IsLocallyPresentable.{w, v, u} C
⊢ IsLocallyPresentable.{w, v', u'} D

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Adjunction

Goal state before:
pp: C : Type u
D : Type u'
inst✝² : Category.{v, u} C
inst✝¹ : Category.{v', u'} D
e : C ≌ D
inst✝ : IsAccessibleCategory.{w, v, u} C
⊢ IsAccessibleCategory.{w, v', u'} D

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ whiskerRight (M.whiskerLeft f) P =
    (M.associatorBimod N P).hom ≫ M.whiskerLeft (whiskerRight f P) ≫ (M.associatorBimod N' P).inv

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 1 ↔ Nonempty (X ≅ Y)

Tactic:
by

Goal state after: