-- Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean
theorem isUnital_rightAdd : EckmannHilton.IsUnital (· +ᵣ ·) 0

Proof state:
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
⊢ EckmannHilton.IsUnital (fun x1 x2 => rightAdd X Y x1 x2) 0

Tactic:
exact {
  left_id := fun f => by simp [h₂ f, rightAdd, biprod.lift_snd_assoc, Category.id_comp],
  right_id := fun f => by simp [h₁ f, rightAdd, biprod.lift_fst_assoc, Category.id_comp]
}

Result:
no goals

Proof state:
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:
simp only [biprod.inr_desc, BinaryBicone.inr_snd_assoc]

Result:
no goals

Proof state:
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:
intro f

Result:
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

Proof state:
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:
simp only [biprod.inr_desc, BinaryBicone.inr_fst_assoc, zero_comp]

Result:
no goals

Proof state:
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:
simp [h₁ f, rightAdd, biprod.lift_fst_assoc, Category.id_comp]

Result:
no goals

Proof state:
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

Tactic:
simp

Result:
no goals

Proof state:
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:
ext

Result:
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

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

Proof state:
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:
ext

Result:
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

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

Proof state:
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:
intro f

Result:
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

Proof state:
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:
simp [h₂ f, rightAdd, biprod.lift_snd_assoc, Category.id_comp]

Result:
no goals

Proof state:
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

Tactic:
simp

Result:
no goals