mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: case refine_2
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
⊢ Epi (F.map f) → localEpi (fun x ↦ x ∈ Set.range G.obj) (G.map (F.map f))

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
⊢ Epi (F.map f) → localEpi (fun x ↦ x ∈ Set.range G.obj) (G.map (F.map f))
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
⊢ localEpi (fun x ↦ x ∈ Set.range G.obj) f ↔ (MorphismProperty.epimorphisms D).inverseImage F f

Tactic:
localEpi_mem_range_iff_epi adj

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
⊢ Epi (F.map f) ↔ (MorphismProperty.epimorphisms D).inverseImage F f
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
G : ℕ ⥤ MonoOver X
⊢ IsFiltered.IsEventuallyConstant G

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ MonoOver X), IsFiltered.IsEventuallyConstant F
F : ℕ →o Subobject X
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → F n = F m

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
G : ℕ ⥤ MonoOver X
⊢ IsFiltered.IsEventuallyConstant G
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ MonoOver X), IsFiltered.IsEventuallyConstant F
F : ℕ →o Subobject X
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → F n = F m

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ MonoOver X), IsFiltered.IsEventuallyConstant F
F : ℕ →o Subobject X
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → F n = F m
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w✝³ : SmallCategory J₁
w✝² : IsFiltered J₁
D₁ : J₁ ⥤ C
s₁ : (Functor.const J₁).obj X ⟶ D₁
t₁ : D₁ ⟶ (Functor.const J₁).obj Y
ht₁ : IsColimit { pt := Y, ι := t₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w✝¹ : SmallCategory J₂
w✝ : IsFiltered J₂
D₂ : J₂ ⥤ C
s₂ : (Functor.const J₂).obj Y ⟶ D₂
t₂ : D₂ ⟶ (Functor.const J₂).obj Z
ht₂ : IsColimit { pt := Z, ι := t₂ }
h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
j₂ : J₂
q : T ⟶ D₂.obj j₂
hcomp : p ≫ q = ((Functor.const J₂).map f ≫ s₂).app j₂
hu : q ≫ { pt := Z, ι := t₂ }.ι.app j₂ = u
j₁ : J₁
W : C
f' : D₁.obj j₁ ⟶ W
g' : W ⟶ D₂.obj j₂
h : IsPushout ({ pt := Y, ι := t₁ }.ι.app j₁) f' (s₂.app j₂) g'
hf' : P f'
D' : Under j₁ ⥤ C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend
    h.isoPushout.inv
hc' : IsColimit c' :=
  IsColimit.extendIso h.isoPushout.inv
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
s' : (Functor.const (Under j₁)).obj X ⟶ D' :=
  { app := fun k ↦ s₁.app k.right ≫ pushout.inl ((Under.post D₁).obj k).hom f', naturality := ⋯ }
j₃ : Under j₁
v : T ⟶ D'.obj j₃
hcomp' : p ≫ v = s'.app j₃
hq : v ≫ c'.ι.app j₃ = q
⊢ P (p ≫ v)

Tactic:
rw [hcomp']
      exact P.comp_mem _ _ (h₁ _).left (P.pushout_inl _ _ hf')

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝³ : AddGroup A
inst✝² : HasShift C A
α : Type u_3
J : α → Type u_4
inst✝¹ : (i : α) → Category.{u_5, u_4} (J i)
inst✝ : P.IsStableUnderShift A
a : A
X : C
hX : P.limitsClosure J X
⊢ (P.limitsClosure J).shift a X

Tactic:
induction hX with
    | of_mem X hX => exact limitsClosure.of_mem _ (IsStableUnderShiftBy.le_shift X hX)
    | of_isoClosure e hX hX' => exact limitsClosure.of_isoClosure ((shiftFunctor C a).mapIso e) hX'
    | of_limitPresentation pres h h' =>
      exact limitsClosure.of_limitPresentation (pres.map (shiftFunctor C a)) h'

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u v : Arrow V
f✝ g✝ : u ⟶ v
inst✝ : HasZeroObject V
x✝¹ x✝ : V
f g : x✝¹ ⟶ x✝
eq : (functor V).map f = (functor V).map g
⊢ f = g

Tactic:
dsimp at eq

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u v : Arrow V
f✝ g✝ : u ⟶ v
inst✝ : HasZeroObject V
x✝¹ x✝ : V
f g : x✝¹ ⟶ x✝
eq : (quotient V).map (homMk 0 f ⋯) = (quotient V).map (homMk 0 g ⋯)
⊢ f = g
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case pos
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
j : β
k : α
h : f k = g j
⊢ (eqToHom ⋯ ≫ biproduct.components z k j ≫ eqToHom ⋯) ≫ eqToHom ⋯ =
    biproduct.ι (fun a ↦ s (f a)) k ≫ z ≫ biproduct.π (fun b ↦ s (g b)) j

pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
j : β
k : α
h : ¬f k = g j
⊢ 0 = biproduct.ι (fun a ↦ s (f a)) k ≫ z ≫ biproduct.π (fun b ↦ s (g b)) j

Tactic:
·

Goal state after:
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
j : β
k : α
h : f k = g j
⊢ (eqToHom ⋯ ≫ biproduct.components z k j ≫ eqToHom ⋯) ≫ eqToHom ⋯ =
    biproduct.ι (fun a ↦ s (f a)) k ≫ z ≫ biproduct.π (fun b ↦ s (g b)) j
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
j : β
k : α
h : ¬f k = g j
⊢ 0 = biproduct.ι (fun a ↦ s (f a)) k ≫ z ≫ biproduct.π (fun b ↦ s (g b)) j

Tactic:
·

Goal state after:
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
j : β
k : α
h : ¬f k = g j
⊢ 0 = biproduct.ι (fun a ↦ s (f a)) k ≫ z ≫ biproduct.π (fun b ↦ s (g b)) j
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case pos
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : β
k : α
w : j ∈ g ⁻¹' {f k}
h : f k = g j
⊢ (z (f k) ⟨j, ⋯⟩ ⟨k, ⋯⟩ ≫ eqToHom ⋯) ≫ eqToHom ⋯ = z (f k) ⟨j, w⟩ ⟨k, ⋯⟩

pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : β
k : α
w : j ∈ g ⁻¹' {f k}
h : ¬f k = g j
⊢ 0 ≫ eqToHom ⋯ = z (f k) ⟨j, w⟩ ⟨k, ⋯⟩

Tactic:
·

Goal state after:
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : β
k : α
w : j ∈ g ⁻¹' {f k}
h : f k = g j
⊢ (z (f k) ⟨j, ⋯⟩ ⟨k, ⋯⟩ ≫ eqToHom ⋯) ≫ eqToHom ⋯ = z (f k) ⟨j, w⟩ ⟨k, ⋯⟩
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : β
k : α
w : j ∈ g ⁻¹' {f k}
h : ¬f k = g j
⊢ 0 ≫ eqToHom ⋯ = z (f k) ⟨j, w⟩ ⟨k, ⋯⟩

Tactic:
·

Goal state after:
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : β
k : α
w : j ∈ g ⁻¹' {f k}
h : ¬f k = g j
⊢ 0 ≫ eqToHom ⋯ = z (f k) ⟨j, w⟩ ⟨k, ⋯⟩
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case pos
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 : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ⟨b, ⋯⟩ = ⟨a, j_property✝⟩
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b = 𝟙 (s (f b))

pp: case neg
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 : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ¬⟨b, ⋯⟩ = ⟨a, j_property✝⟩
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b = 0

Tactic:
·

Goal state after:
case pos
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 : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ⟨b, ⋯⟩ = ⟨a, j_property✝⟩
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b = 𝟙 (s (f b))
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case neg
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 : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ¬⟨b, ⋯⟩ = ⟨a, j_property✝⟩
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b = 0

Tactic:
·

Goal state after:
case neg
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 : α → ι
b a : α
j_property✝ : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ¬⟨b, ⋯⟩ = ⟨a, j_property✝⟩
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a ↦ s (f a)) a ≫ biproduct.π (fun b ↦ s (f b)) b = 0
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case w
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)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
⊢ ∀ (x : β) (hx : x ∈ g ⁻¹' {h c}),
    eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫
            ((biproduct.π (fun b ↦ s (g b)) x ≫ biproduct.ι (fun b ↦ s (g b)) x) ≫ w) ≫
              biproduct.π (fun b ↦ s (h b)) c =
      eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫
            biproduct.π (fun b ↦ s (g b)) ↑⟨x, hx⟩ ≫
              biproduct.ι (fun a ↦ s (g a)) ↑⟨x, hx⟩ ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c

pp: case w'
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)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
⊢ ∀ x ∉ g ⁻¹' {h c},
    eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫
            ((biproduct.π (fun b ↦ s (g b)) x ≫ biproduct.ι (fun b ↦ s (g b)) x) ≫ w) ≫
              biproduct.π (fun b ↦ s (h b)) c =
      0

Tactic:
·

Goal state after:
case w
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)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
⊢ ∀ (x : β) (hx : x ∈ g ⁻¹' {h c}),
    eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫
            ((biproduct.π (fun b ↦ s (g b)) x ≫ biproduct.ι (fun b ↦ s (g b)) x) ≫ w) ≫
              biproduct.π (fun b ↦ s (h b)) c =
      eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫
            biproduct.π (fun b ↦ s (g b)) ↑⟨x, hx⟩ ≫
              biproduct.ι (fun a ↦ s (g a)) ↑⟨x, hx⟩ ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case w'
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)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
⊢ ∀ x ∉ g ⁻¹' {h c},
    eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫
            ((biproduct.π (fun b ↦ s (g b)) x ≫ biproduct.ι (fun b ↦ s (g b)) x) ≫ w) ≫
              biproduct.π (fun b ↦ s (h b)) c =
      0

Tactic:
·

Goal state after:
case w'
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)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
⊢ ∀ x ∉ g ⁻¹' {h c},
    eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫
            ((biproduct.π (fun b ↦ s (g b)) x ≫ biproduct.ι (fun b ↦ s (g b)) x) ≫ w) ≫
              biproduct.π (fun b ↦ s (h b)) c =
      0
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

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

pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f : X ⟶ Y
⊢ biprod.lift 0 f ≫ biprod.snd = (f ≫ biprod.inr) ≫ biprod.snd

Tactic:
·

Goal state after:
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f : X ⟶ Y
⊢ biprod.lift 0 f ≫ biprod.fst = (f ≫ biprod.inr) ≫ biprod.fst
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

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

Tactic:
·

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f : X ⟶ Y
⊢ biprod.lift 0 f ≫ biprod.snd = (f ≫ biprod.inr) ≫ biprod.snd
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

Goal state before:
pp: case h₀
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 ≫ biprod.fst = (f ≫ biprod.inl) ≫ biprod.fst

pp: case h₁
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 ≫ biprod.snd = (f ≫ biprod.inl) ≫ biprod.snd

Tactic:
·

Goal state after:
case h₀
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 ≫ biprod.fst = (f ≫ biprod.inl) ≫ biprod.fst
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

Goal state before:
pp: case h₁
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 ≫ biprod.snd = (f ≫ biprod.inl) ≫ biprod.snd

Tactic:
·

Goal state after:
case h₁
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 ≫ biprod.snd = (f ≫ biprod.inl) ≫ biprod.snd
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

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

pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f : X ⟶ Y
⊢ biprod.inr ≫ biprod.desc 0 f = biprod.inr ≫ biprod.snd ≫ f

Tactic:
·

Goal state after:
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f : X ⟶ Y
⊢ biprod.inl ≫ biprod.desc 0 f = biprod.inl ≫ biprod.snd ≫ f
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

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

Tactic:
·

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
f : X ⟶ Y
⊢ biprod.inr ≫ biprod.desc 0 f = biprod.inr ≫ biprod.snd ≫ f
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

Goal state before:
pp: case h₀
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.inl ≫ biprod.desc f 0 = biprod.inl ≫ biprod.fst ≫ f

pp: case h₁
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.inr ≫ biprod.desc f 0 = biprod.inr ≫ biprod.fst ≫ f

Tactic:
·

Goal state after:
case h₀
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.inl ≫ biprod.desc f 0 = biprod.inl ≫ biprod.fst ≫ f
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

Goal state before:
pp: case h₁
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.inr ≫ biprod.desc f 0 = biprod.inr ≫ biprod.fst ≫ f

Tactic:
·

Goal state after:
case h₁
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.inr ≫ biprod.desc f 0 = biprod.inr ≫ biprod.fst ≫ f
Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties

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

pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
⊢ (MorphismProperty.epimorphisms C).llp 0 → Projective P

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
⊢ Projective P → (MorphismProperty.epimorphisms C).llp 0
Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties

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

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
⊢ (MorphismProperty.epimorphisms C).llp 0 → Projective P
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: case inl
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 : Subsingleton (X ⟶ Y)
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

pp: case inr
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)
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

Tactic:
·

Goal state after:
case inl
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 : Subsingleton (X ⟶ Y)
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: case inr
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)
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

Tactic:
·

Goal state after:
case inr
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)
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1