[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedSemiring α
a b c d : α
H : 0 ≤ a
⊢ 0 ≤ a ^ 0
[PROOFSTEP]
rw [pow_zero]
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedSemiring α
a b c d : α
H : 0 ≤ a
⊢ 0 ≤ 1
[PROOFSTEP]
exact zero_le_one
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedSemiring α
a b c d : α
H : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedSemiring α
a b c d : α
H : 0 ≤ a
n : ℕ
⊢ 0 ≤ a * a ^ n
[PROOFSTEP]
exact mul_nonneg H (pow_nonneg H _)
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedSemiring α
a b c d : α
a2 : 2 ≤ a
b0 : 0 ≤ b
⊢ a + (a + a * b) ≤ a * (2 + b)
[PROOFSTEP]
rw [mul_add, mul_two, add_assoc]
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedSemiring α
a b c d : α
h : 0 < a
⊢ 0 < bit1 a
[PROOFSTEP]
nontriviality
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : OrderedSemiring α
a b c d : α
h : 0 < a
inst✝ : Nontrivial α
⊢ 0 < bit1 a
[PROOFSTEP]
exact bit1_pos h.le
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedRing α
a✝ b✝ c✝ d : α
src✝¹ : OrderedRing α := inst✝
src✝ : Semiring α := Ring.toSemiring
a b c : α
h : a ≤ b
hc : 0 ≤ c
⊢ c * a ≤ c * b
[PROOFSTEP]
simpa only [mul_sub, sub_nonneg] using OrderedRing.mul_nonneg _ _ hc (sub_nonneg.2 h)
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedRing α
a✝ b✝ c✝ d : α
src✝¹ : OrderedRing α := inst✝
src✝ : Semiring α := Ring.toSemiring
a b c : α
h : a ≤ b
hc : 0 ≤ c
⊢ a * c ≤ b * c
[PROOFSTEP]
simpa only [sub_mul, sub_nonneg] using OrderedRing.mul_nonneg _ _ (sub_nonneg.2 h) hc
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedRing α
a b c d : α
h : b ≤ a
hc : c ≤ 0
⊢ c * a ≤ c * b
[PROOFSTEP]
simpa only [neg_mul, neg_le_neg_iff] using mul_le_mul_of_nonneg_left h (neg_nonneg.2 hc)
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedRing α
a b c d : α
h : b ≤ a
hc : c ≤ 0
⊢ a * c ≤ b * c
[PROOFSTEP]
simpa only [mul_neg, neg_le_neg_iff] using mul_le_mul_of_nonneg_right h (neg_nonneg.2 hc)
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedRing α
a b c d : α
ha : a ≤ 0
hb : b ≤ 0
⊢ 0 ≤ a * b
[PROOFSTEP]
simpa only [zero_mul] using mul_le_mul_of_nonpos_right ha hb
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedRing α
a b c d : α
hb : b ≤ 0
h : a ≤ 1
⊢ b ≤ a * b
[PROOFSTEP]
simpa only [one_mul] using mul_le_mul_of_nonpos_right h hb
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedRing α
a b c d : α
hb : b ≤ 0
h : 1 ≤ a
⊢ a * b ≤ b
[PROOFSTEP]
simpa only [one_mul] using mul_le_mul_of_nonpos_right h hb
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedRing α
a b c d : α
ha : a ≤ 0
h : b ≤ 1
⊢ a ≤ a * b
[PROOFSTEP]
simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedRing α
a b c d : α
ha : a ≤ 0
h : 1 ≤ b
⊢ a * b ≤ a
[PROOFSTEP]
simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedRing α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ b = a + (b - a)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedRing α
a✝ b✝ c✝ d a b : α
x✝ : ∃ c, c ≥ 0 ∧ b = a + c
c : α
hc : c ≥ 0
h : b = a + c
⊢ a ≤ b
[PROOFSTEP]
rw [h, le_add_iff_nonneg_right]
[GOAL]
α : Type u
β : Type u_1
inst✝ : OrderedRing α
a✝ b✝ c✝ d a b : α
x✝ : ∃ c, c ≥ 0 ∧ b = a + c
c : α
hc : c ≥ 0
h : b = a + c
⊢ 0 ≤ c
[PROOFSTEP]
exact hc
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a✝ b✝ c✝ d : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
src✝ : StrictOrderedSemiring α := inst✝¹
a b c : α
hab : a ≤ b
hc : 0 ≤ c
⊢ c * a ≤ c * b
[PROOFSTEP]
obtain rfl | hab := Decidable.eq_or_lt_of_le hab
[GOAL]
case inl
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a✝ b c✝ d : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
src✝ : StrictOrderedSemiring α := inst✝¹
a c : α
hc : 0 ≤ c
hab : a ≤ a
⊢ c * a ≤ c * a
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a✝ b✝ c✝ d : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
src✝ : StrictOrderedSemiring α := inst✝¹
a b c : α
hab✝ : a ≤ b
hc : 0 ≤ c
hab : a < b
⊢ c * a ≤ c * b
[PROOFSTEP]
obtain rfl | hc := Decidable.eq_or_lt_of_le hc
[GOAL]
case inr.inl
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a✝ b✝ c d : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
src✝ : StrictOrderedSemiring α := inst✝¹
a b : α
hab✝ : a ≤ b
hab : a < b
hc : 0 ≤ 0
⊢ 0 * a ≤ 0 * b
[PROOFSTEP]
simp
[GOAL]
case inr.inr
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a✝ b✝ c✝ d : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
src✝ : StrictOrderedSemiring α := inst✝¹
a b c : α
hab✝ : a ≤ b
hc✝ : 0 ≤ c
hab : a < b
hc : 0 < c
⊢ c * a ≤ c * b
[PROOFSTEP]
exact (mul_lt_mul_of_pos_left hab hc).le
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a✝ b✝ c✝ d : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
src✝ : StrictOrderedSemiring α := inst✝¹
a b c : α
hab : a ≤ b
hc : 0 ≤ c
⊢ a * c ≤ b * c
[PROOFSTEP]
obtain rfl | hab := Decidable.eq_or_lt_of_le hab
[GOAL]
case inl
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a✝ b c✝ d : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
src✝ : StrictOrderedSemiring α := inst✝¹
a c : α
hc : 0 ≤ c
hab : a ≤ a
⊢ a * c ≤ a * c
[PROOFSTEP]
rfl
[GOAL]
case inr
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a✝ b✝ c✝ d : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
src✝ : StrictOrderedSemiring α := inst✝¹
a b c : α
hab✝ : a ≤ b
hc : 0 ≤ c
hab : a < b
⊢ a * c ≤ b * c
[PROOFSTEP]
obtain rfl | hc := Decidable.eq_or_lt_of_le hc
[GOAL]
case inr.inl
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a✝ b✝ c d : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
src✝ : StrictOrderedSemiring α := inst✝¹
a b : α
hab✝ : a ≤ b
hab : a < b
hc : 0 ≤ 0
⊢ a * 0 ≤ b * 0
[PROOFSTEP]
simp
[GOAL]
case inr.inr
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a✝ b✝ c✝ d : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
src✝ : StrictOrderedSemiring α := inst✝¹
a b c : α
hab✝ : a ≤ b
hc✝ : 0 ≤ c
hab : a < b
hc : 0 < c
⊢ a * c ≤ b * c
[PROOFSTEP]
exact (mul_lt_mul_of_pos_right hab hc).le
[GOAL]
α : Type u
β : Type u_1
inst✝ : StrictOrderedSemiring α
a b c d : α
H : 0 < a
⊢ 0 < a ^ 0
[PROOFSTEP]
nontriviality
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a b c d : α
H : 0 < a
inst✝ : Nontrivial α
⊢ 0 < a ^ 0
[PROOFSTEP]
rw [pow_zero]
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a b c d : α
H : 0 < a
inst✝ : Nontrivial α
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
α : Type u
β : Type u_1
inst✝ : StrictOrderedSemiring α
a b c d : α
H : 0 < a
n : ℕ
⊢ 0 < a ^ (n + 1)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
α : Type u
β : Type u_1
inst✝ : StrictOrderedSemiring α
a b c d : α
H : 0 < a
n : ℕ
⊢ 0 < a * a ^ n
[PROOFSTEP]
exact mul_pos H (pow_pos H _)
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a b c d : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
h1 : a < c
h2 : b < d
h3 : 0 ≤ a
h4 : 0 ≤ b
b0 : 0 = b
⊢ a * b < c * d
[PROOFSTEP]
rw [← b0, mul_zero]
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedSemiring α
a b c d : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
h1 : a < c
h2 : b < d
h3 : 0 ≤ a
h4 : 0 ≤ b
b0 : 0 = b
⊢ 0 < c * d
[PROOFSTEP]
exact mul_pos (h3.trans_lt h1) (h4.trans_lt h2)
[GOAL]
α : Type u
β : Type u_1
inst✝ : StrictOrderedSemiring α
a b c d : α
⊢ a < c → b < d → 0 ≤ a → 0 ≤ b → a * b < c * d
[PROOFSTEP]
classical exact Decidable.mul_lt_mul''
[GOAL]
α : Type u
β : Type u_1
inst✝ : StrictOrderedSemiring α
a b c d : α
⊢ a < c → b < d → 0 ≤ a → 0 ≤ b → a * b < c * d
[PROOFSTEP]
exact Decidable.mul_lt_mul''
[GOAL]
α : Type u
β : Type u_1
inst✝ : StrictOrderedSemiring α
a b c d : α
hn : 0 < a
hm : 1 < b
⊢ a < b * a
[PROOFSTEP]
convert mul_lt_mul_of_pos_right hm hn
[GOAL]
case h.e'_3
α : Type u
β : Type u_1
inst✝ : StrictOrderedSemiring α
a b c d : α
hn : 0 < a
hm : 1 < b
⊢ a = 1 * a
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u
β : Type u_1
inst✝ : StrictOrderedSemiring α
a b c d : α
hn : 0 < a
hm : 1 < b
⊢ a < a * b
[PROOFSTEP]
convert mul_lt_mul_of_pos_left hm hn
[GOAL]
case h.e'_3
α : Type u
β : Type u_1
inst✝ : StrictOrderedSemiring α
a b c d : α
hn : 0 < a
hm : 1 < b
⊢ a = a * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u
β : Type u_1
inst✝ : StrictOrderedRing α
a✝ b✝ c✝ : α
src✝¹ : StrictOrderedRing α := inst✝
src✝ : Semiring α := Ring.toSemiring
a b c : α
h : a < b
hc : 0 < c
⊢ c * a < c * b
[PROOFSTEP]
simpa only [mul_sub, sub_pos] using StrictOrderedRing.mul_pos _ _ hc (sub_pos.2 h)
[GOAL]
α : Type u
β : Type u_1
inst✝ : StrictOrderedRing α
a✝ b✝ c✝ : α
src✝¹ : StrictOrderedRing α := inst✝
src✝ : Semiring α := Ring.toSemiring
a b c : α
h : a < b
hc : 0 < c
⊢ a * c < b * c
[PROOFSTEP]
simpa only [sub_mul, sub_pos] using StrictOrderedRing.mul_pos _ _ (sub_pos.2 h) hc
[GOAL]
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedRing α
a✝ b✝ c : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
src✝¹ : StrictOrderedRing α := inst✝¹
src✝ : Semiring α := Ring.toSemiring
a b : α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b
[PROOFSTEP]
obtain ha | ha := Decidable.eq_or_lt_of_le ha
[GOAL]
case inl
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedRing α
a✝ b✝ c : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
src✝¹ : StrictOrderedRing α := inst✝¹
src✝ : Semiring α := Ring.toSemiring
a b : α
ha✝ : 0 ≤ a
hb : 0 ≤ b
ha : 0 = a
⊢ 0 ≤ a * b
[PROOFSTEP]
rw [← ha, zero_mul]
[GOAL]
case inr
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedRing α
a✝ b✝ c : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
src✝¹ : StrictOrderedRing α := inst✝¹
src✝ : Semiring α := Ring.toSemiring
a b : α
ha✝ : 0 ≤ a
hb : 0 ≤ b
ha : 0 < a
⊢ 0 ≤ a * b
[PROOFSTEP]
obtain hb | hb := Decidable.eq_or_lt_of_le hb
[GOAL]
case inr.inl
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedRing α
a✝ b✝ c : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
src✝¹ : StrictOrderedRing α := inst✝¹
src✝ : Semiring α := Ring.toSemiring
a b : α
ha✝ : 0 ≤ a
hb✝ : 0 ≤ b
ha : 0 < a
hb : 0 = b
⊢ 0 ≤ a * b
[PROOFSTEP]
rw [← hb, mul_zero]
[GOAL]
case inr.inr
α : Type u
β : Type u_1
inst✝¹ : StrictOrderedRing α
a✝ b✝ c : α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
src✝¹ : StrictOrderedRing α := inst✝¹
src✝ : Semiring α := Ring.toSemiring
a b : α
ha✝ : 0 ≤ a
hb✝ : 0 ≤ b
ha : 0 < a
hb : 0 < b
⊢ 0 ≤ a * b
[PROOFSTEP]
exact (StrictOrderedRing.mul_pos _ _ ha hb).le
[GOAL]
α : Type u
β : Type u_1
inst✝ : StrictOrderedRing α
a b c : α
h : b < a
hc : c < 0
⊢ c * a < c * b
[PROOFSTEP]
simpa only [neg_mul, neg_lt_neg_iff] using mul_lt_mul_of_pos_left h (neg_pos_of_neg hc)
[GOAL]
α : Type u
β : Type u_1
inst✝ : StrictOrderedRing α
a b c : α
h : b < a
hc : c < 0
⊢ a * c < b * c
[PROOFSTEP]
simpa only [mul_neg, neg_lt_neg_iff] using mul_lt_mul_of_pos_right h (neg_pos_of_neg hc)
[GOAL]
α : Type u
β : Type u_1
inst✝ : StrictOrderedRing α
a✝ b✝ c a b : α
ha : a < 0
hb : b < 0
⊢ 0 < a * b
[PROOFSTEP]
simpa only [zero_mul] using mul_lt_mul_of_neg_right ha hb
[GOAL]
α : Type u
β : Type u_1
inst✝ : StrictOrderedRing α
a b c : α
hb : b < 0
h : a < 1
⊢ b < a * b
[PROOFSTEP]
simpa only [one_mul] using mul_lt_mul_of_neg_right h hb
[GOAL]
α : Type u
β : Type u_1
inst✝ : StrictOrderedRing α
a b c : α
hb : b < 0
h : 1 < a
⊢ a * b < b
[PROOFSTEP]
simpa only [one_mul] using mul_lt_mul_of_neg_right h hb
[GOAL]
α : Type u
β : Type u_1
inst✝ : StrictOrderedRing α
a b c : α
ha : a < 0
h : b < 1
⊢ a < a * b
[PROOFSTEP]
simpa only [mul_one] using mul_lt_mul_of_neg_left h ha
[GOAL]
α : Type u
β : Type u_1
inst✝ : StrictOrderedRing α
a b c : α
ha : a < 0
h : 1 < b
⊢ a * b < a
[PROOFSTEP]
simpa only [mul_one] using mul_lt_mul_of_neg_left h ha
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
a b c d : α
hab : 0 ≤ a * b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
[PROOFSTEP]
refine' Decidable.or_iff_not_and_not.2 _
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
a b c d : α
hab : 0 ≤ a * b
⊢ ¬(¬(0 ≤ a ∧ 0 ≤ b) ∧ ¬(a ≤ 0 ∧ b ≤ 0))
[PROOFSTEP]
simp only [not_and, not_le]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
a b c d : α
hab : 0 ≤ a * b
⊢ (0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)
[PROOFSTEP]
intro ab nab
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
a b c d : α
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ False
[PROOFSTEP]
apply
  not_lt_of_le hab
    _
      -- Porting note: for the middle case, we used to have `rfl`, but it is now rejected.
        -- https://github.com/leanprover/std4/issues/62
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
a b c d : α
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ a * b < 0
[PROOFSTEP]
rcases lt_trichotomy 0 a with (ha | ha | ha)
[GOAL]
case inl
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
a b c d : α
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : 0 < a
⊢ a * b < 0
[PROOFSTEP]
exact mul_neg_of_pos_of_neg ha (ab ha.le)
[GOAL]
case inr.inl
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
a b c d : α
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : 0 = a
⊢ a * b < 0
[PROOFSTEP]
subst ha
[GOAL]
case inr.inl
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
b c d : α
hab : 0 ≤ 0 * b
ab : 0 ≤ 0 → b < 0
nab : 0 ≤ 0 → 0 < b
⊢ 0 * b < 0
[PROOFSTEP]
exact ((ab le_rfl).asymm (nab le_rfl)).elim
[GOAL]
case inr.inr
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
a b c d : α
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
ha : a < 0
⊢ a * b < 0
[PROOFSTEP]
exact mul_neg_of_neg_of_pos ha (nab ha.le)
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
a b c d : α
h : 0 < c
⊢ 0 ≤ c * b ↔ 0 ≤ b
[PROOFSTEP]
simpa using (mul_le_mul_left h : c * 0 ≤ c * b ↔ 0 ≤ b)
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
a b c d : α
h : 0 < c
⊢ 0 ≤ b * c ↔ 0 ≤ b
[PROOFSTEP]
simpa using (mul_le_mul_right h : 0 * c ≤ b * c ↔ 0 ≤ b)
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
a b c d : α
⊢ bit0 a ≤ bit0 b ↔ a ≤ b
[PROOFSTEP]
rw [bit0, bit0, ← two_mul, ← two_mul, mul_le_mul_left (zero_lt_two : 0 < (2 : α))]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
a b c d : α
⊢ bit0 a < bit0 b ↔ a < b
[PROOFSTEP]
rw [bit0, bit0, ← two_mul, ← two_mul, mul_lt_mul_left (zero_lt_two : 0 < (2 : α))]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
a b c d : α
⊢ 1 ≤ bit1 a ↔ 0 ≤ a
[PROOFSTEP]
rw [bit1, le_add_iff_nonneg_left, bit0, ← two_mul, zero_le_mul_left (zero_lt_two : 0 < (2 : α))]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
a b c d : α
⊢ 1 < bit1 a ↔ 0 < a
[PROOFSTEP]
rw [bit1, lt_add_iff_pos_left, bit0, ← two_mul, zero_lt_mul_left (zero_lt_two : 0 < (2 : α))]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
a b c d : α
⊢ 0 ≤ bit0 a ↔ 0 ≤ a
[PROOFSTEP]
rw [bit0, ← two_mul, zero_le_mul_left (zero_lt_two : 0 < (2 : α))]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedSemiring α
a b c d : α
⊢ 0 < bit0 a ↔ 0 < a
[PROOFSTEP]
rw [bit0, ← two_mul, zero_lt_mul_left (zero_lt_two : 0 < (2 : α))]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
src✝ : LinearOrderedRing α := inst✝
⊢ ∀ {a b : α}, a * b = 0 → a = 0 ∨ b = 0
[PROOFSTEP]
intro a b hab
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
src✝ : LinearOrderedRing α := inst✝
a b : α
hab : a * b = 0
⊢ a = 0 ∨ b = 0
[PROOFSTEP]
refine' Decidable.or_iff_not_and_not.2 fun h => _
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
src✝ : LinearOrderedRing α := inst✝
a b : α
hab : a * b = 0
h : ¬a = 0 ∧ ¬b = 0
⊢ False
[PROOFSTEP]
revert hab
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
src✝ : LinearOrderedRing α := inst✝
a b : α
h : ¬a = 0 ∧ ¬b = 0
⊢ a * b = 0 → False
[PROOFSTEP]
cases' lt_or_gt_of_ne h.1 with ha ha
[GOAL]
case inl
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
src✝ : LinearOrderedRing α := inst✝
a b : α
h : ¬a = 0 ∧ ¬b = 0
ha : a < 0
⊢ a * b = 0 → False
[PROOFSTEP]
cases' lt_or_gt_of_ne h.2 with hb hb
[GOAL]
case inr
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
src✝ : LinearOrderedRing α := inst✝
a b : α
h : ¬a = 0 ∧ ¬b = 0
ha : a > 0
⊢ a * b = 0 → False
[PROOFSTEP]
cases' lt_or_gt_of_ne h.2 with hb hb
[GOAL]
case inl.inl
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
src✝ : LinearOrderedRing α := inst✝
a b : α
h : ¬a = 0 ∧ ¬b = 0
ha : a < 0
hb : b < 0
⊢ a * b = 0 → False
case inl.inr
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
src✝ : LinearOrderedRing α := inst✝
a b : α
h : ¬a = 0 ∧ ¬b = 0
ha : a < 0
hb : b > 0
⊢ a * b = 0 → False
case inr.inl
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
src✝ : LinearOrderedRing α := inst✝
a b : α
h : ¬a = 0 ∧ ¬b = 0
ha : a > 0
hb : b < 0
⊢ a * b = 0 → False
case inr.inr
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c : α
src✝ : LinearOrderedRing α := inst✝
a b : α
h : ¬a = 0 ∧ ¬b = 0
ha : a > 0
hb : b > 0
⊢ a * b = 0 → False
[PROOFSTEP]
exacts [(mul_pos_of_neg_of_neg ha hb).ne.symm, (mul_neg_of_neg_of_pos ha hb).ne, (mul_neg_of_pos_of_neg ha hb).ne,
  (mul_pos ha hb).ne.symm]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ : α
src✝ : Nontrivial α := inferInstance
a b c : α
ha : a ≠ 0
h : a * b = a * c
⊢ b = c
[PROOFSTEP]
rw [← sub_eq_zero, ← mul_sub] at h
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ : α
src✝ : Nontrivial α := inferInstance
a b c : α
ha : a ≠ 0
h✝ : a * b = a * c
h : a * (b - c) = 0
⊢ b = c
[PROOFSTEP]
exact sub_eq_zero.1 ((eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_left ha)
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ : α
src✝ : Nontrivial α := inferInstance
a b c : α
hb : b ≠ 0
h : a * b = c * b
⊢ a = c
[PROOFSTEP]
rw [← sub_eq_zero, ← sub_mul] at h
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ : α
src✝ : Nontrivial α := inferInstance
a b c : α
hb : b ≠ 0
h✝ : a * b = c * b
h : (a - c) * b = 0
⊢ a = c
[PROOFSTEP]
exact sub_eq_zero.1 ((eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_right hb)
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
[PROOFSTEP]
rw [← neg_pos, neg_mul_eq_mul_neg, mul_pos_iff, neg_pos, neg_lt_zero]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ a b c : α
⊢ 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a
[PROOFSTEP]
iterate 3 rw [mul_nonneg_iff]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ a b c : α
⊢ 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a
[PROOFSTEP]
rw [mul_nonneg_iff]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ a b c : α
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ 0 ≤ b * c ∨ 0 ≤ c * a
[PROOFSTEP]
rw [mul_nonneg_iff]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ a b c : α
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c * a
[PROOFSTEP]
rw [mul_nonneg_iff]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ a b c : α
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
[PROOFSTEP]
have or_a := le_total 0 a
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ a b c : α
or_a : 0 ≤ a ∨ a ≤ 0
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
[PROOFSTEP]
have or_b := le_total 0 b
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ a b c : α
or_a : 0 ≤ a ∨ a ≤ 0
or_b : 0 ≤ b ∨ b ≤ 0
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
[PROOFSTEP]
have or_c := le_total 0 c
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b✝ c✝ a b c : α
or_a : 0 ≤ a ∨ a ≤ 0
or_b : 0 ≤ b ∨ b ≤ 0
or_c : 0 ≤ c ∨ c ≤ 0
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
[PROOFSTEP]
exact
  Or.elim or_c
    (fun (h0 : 0 ≤ c) =>
      Or.elim or_b
        (fun (h1 : 0 ≤ b) =>
          Or.elim or_a (fun (h2 : 0 ≤ a) => Or.inl (Or.inl ⟨h2, h1⟩))
            (fun (_ : a ≤ 0) => Or.inr (Or.inl (Or.inl ⟨h1, h0⟩))))
        (fun (h1 : b ≤ 0) =>
          Or.elim or_a (fun (h3 : 0 ≤ a) => Or.inr (Or.inr (Or.inl ⟨h0, h3⟩)))
            (fun (h3 : a ≤ 0) => Or.inl (Or.inr ⟨h3, h1⟩))))
    (fun (h0 : c ≤ 0) =>
      Or.elim or_b
        (fun (h4 : 0 ≤ b) =>
          Or.elim or_a (fun (h5 : 0 ≤ a) => Or.inl (Or.inl ⟨h5, h4⟩))
            (fun (h5 : a ≤ 0) => Or.inr (Or.inr (Or.inr ⟨h0, h5⟩))))
        (fun (h4 : b ≤ 0) =>
          Or.elim or_a (fun (_ : 0 ≤ a) => Or.inr (Or.inl (Or.inr ⟨h4, h0⟩)))
            (fun (h6 : a ≤ 0) => Or.inl (Or.inr ⟨h6, h4⟩))))
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
[PROOFSTEP]
rw [← neg_nonneg, neg_mul_eq_mul_neg, mul_nonneg_iff, neg_nonneg, neg_nonpos]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ -a ≤ a ↔ 0 ≤ a
[PROOFSTEP]
simp [neg_le_iff_add_nonneg, ← two_mul, mul_nonneg_iff, zero_le_one, (zero_lt_two' α).not_le]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ -a < a ↔ 0 < a
[PROOFSTEP]
simp [neg_lt_iff_pos_add, ← two_mul, mul_pos_iff, zero_lt_one, (zero_lt_two' α).not_lt]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ a ≤ -a ↔ - -a ≤ -a
[PROOFSTEP]
rw [neg_neg]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
⊢ a < -a ↔ - -a < -a
[PROOFSTEP]
rw [neg_neg]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
h : c * a < c * b
hc : c ≤ 0
⊢ -c * b < -c * a
[PROOFSTEP]
rwa [neg_mul, neg_mul, neg_lt_neg_iff]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
h : a * c < b * c
hc : c ≤ 0
⊢ b * -c < a * -c
[PROOFSTEP]
rwa [mul_neg, mul_neg, neg_lt_neg_iff]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ 0 < a * a ↔ a ≠ 0
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ 0 < a * a → a ≠ 0
[PROOFSTEP]
rintro h rfl
[GOAL]
case mp
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
h : 0 < 0 * 0
⊢ False
[PROOFSTEP]
rw [mul_zero] at h
[GOAL]
case mp
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a b c : α
h : 0 < 0
⊢ False
[PROOFSTEP]
exact h.false
[GOAL]
case mpr
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ a ≠ 0 → 0 < a * a
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : a ≠ 0
⊢ 0 < a * a
[PROOFSTEP]
cases' h.lt_or_lt with h h
[GOAL]
case mpr.inl
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h✝ : a ≠ 0
h : a < 0
⊢ 0 < a * a
case mpr.inr α : Type u β : Type u_1 inst✝ : LinearOrderedRing α a✝ b c a : α h✝ : a ≠ 0 h : 0 < a ⊢ 0 < a * a
[PROOFSTEP]
exacts [mul_pos_of_neg_of_neg h h, mul_pos h h]
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a b c x y : α
⊢ x * x + y * y = 0 ↔ x = 0 ∧ y = 0
[PROOFSTEP]
rw [add_eq_zero_iff', mul_self_eq_zero, mul_self_eq_zero]
[GOAL]
case ha
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a b c x y : α
⊢ 0 ≤ x * x
[PROOFSTEP]
apply mul_self_nonneg
[GOAL]
case hb
α : Type u
β : Type u_1
inst✝ : LinearOrderedRing α
a b c x y : α
⊢ 0 ≤ y * y
[PROOFSTEP]
apply mul_self_nonneg
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedCommRing α
a b✝ c✝ d b c : α
ha : 0 ≤ a
hd : 0 ≤ d
ba : b * a ≤ max d b * max c a
cd : c * d ≤ max a c * max b d
⊢ a * b ≤ max a c * max d b
[PROOFSTEP]
simpa [mul_comm, max_comm] using ba
[GOAL]
α : Type u
β : Type u_1
inst✝ : LinearOrderedCommRing α
a b✝ c✝ d b c : α
ha : 0 ≤ a
hd : 0 ≤ d
ba : b * a ≤ max d b * max c a
cd : c * d ≤ max a c * max b d
⊢ d * c ≤ max a c * max d b
[PROOFSTEP]
simpa [mul_comm, max_comm] using cd


[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
h : Exact f g
⊢ homology f g (_ : f ≫ g = 0) ≅ 0
[PROOFSTEP]
haveI := h.epi
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ homology f g (_ : f ≫ g = 0) ≅ 0
[PROOFSTEP]
exact cokernel.ofEpi _
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
h : ∃ w, Nonempty (homology f g w ≅ 0)
⊢ Exact f g
[PROOFSTEP]
obtain ⟨w, ⟨i⟩⟩ := h
[GOAL]
case intro.intro
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
i : homology f g w ≅ 0
⊢ Exact f g
[PROOFSTEP]
exact ⟨w, Preadditive.epi_of_cokernel_zero ((cancel_mono i.hom).mp (by ext))⟩
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
i : homology f g w ≅ 0
⊢ cokernel.π (imageToKernel f g w) ≫ i.hom = 0 ≫ i.hom
[PROOFSTEP]
ext
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
⊢ Exact f₂ g₂
[PROOFSTEP]
rw [Preadditive.exact_iff_homology_zero] at h ⊢
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h✝ : Exact f₁ g₁
h : ∃ w, Nonempty (homology f₁ g₁ w ≅ 0)
⊢ ∃ w, Nonempty (homology f₂ g₂ w ≅ 0)
[PROOFSTEP]
rcases h with ⟨w₁, ⟨i⟩⟩
[GOAL]
case intro.intro
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
w₁ : f₁ ≫ g₁ = 0
i : homology f₁ g₁ w₁ ≅ 0
⊢ ∃ w, Nonempty (homology f₂ g₂ w ≅ 0)
[PROOFSTEP]
suffices w₂ : f₂ ≫ g₂ = 0
[GOAL]
case intro.intro
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
w₁ : f₁ ≫ g₁ = 0
i : homology f₁ g₁ w₁ ≅ 0
w₂ : f₂ ≫ g₂ = 0
⊢ ∃ w, Nonempty (homology f₂ g₂ w ≅ 0)
case w₂
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
w₁ : f₁ ≫ g₁ = 0
i : homology f₁ g₁ w₁ ≅ 0
⊢ f₂ ≫ g₂ = 0
[PROOFSTEP]
exact ⟨w₂, ⟨(homology.mapIso w₁ w₂ α β p).symm.trans i⟩⟩
[GOAL]
case w₂
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
w₁ : f₁ ≫ g₁ = 0
i : homology f₁ g₁ w₁ ≅ 0
⊢ f₂ ≫ g₂ = 0
[PROOFSTEP]
rw [← cancel_epi α.hom.left, ← cancel_mono β.inv.right, comp_zero, zero_comp, ← w₁]
[GOAL]
case w₂
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
w₁ : f₁ ≫ g₁ = 0
i : homology f₁ g₁ w₁ ≅ 0
⊢ (α.hom.left ≫ f₂ ≫ g₂) ≫ β.inv.right = f₁ ≫ g₁
[PROOFSTEP]
have eq₁ := β.inv.w
[GOAL]
case w₂
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
w₁ : f₁ ≫ g₁ = 0
i : homology f₁ g₁ w₁ ≅ 0
eq₁ : (𝟭 V).map β.inv.left ≫ (Arrow.mk g₁).hom = (Arrow.mk g₂).hom ≫ (𝟭 V).map β.inv.right
⊢ (α.hom.left ≫ f₂ ≫ g₂) ≫ β.inv.right = f₁ ≫ g₁
[PROOFSTEP]
have eq₂ := α.hom.w
[GOAL]
case w₂
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
w₁ : f₁ ≫ g₁ = 0
i : homology f₁ g₁ w₁ ≅ 0
eq₁ : (𝟭 V).map β.inv.left ≫ (Arrow.mk g₁).hom = (Arrow.mk g₂).hom ≫ (𝟭 V).map β.inv.right
eq₂ : (𝟭 V).map α.hom.left ≫ (Arrow.mk f₂).hom = (Arrow.mk f₁).hom ≫ (𝟭 V).map α.hom.right
⊢ (α.hom.left ≫ f₂ ≫ g₂) ≫ β.inv.right = f₁ ≫ g₁
[PROOFSTEP]
dsimp at eq₁ eq₂
[GOAL]
case w₂
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
h : Exact f₁ g₁
w₁ : f₁ ≫ g₁ = 0
i : homology f₁ g₁ w₁ ≅ 0
eq₁ : β.inv.left ≫ g₁ = g₂ ≫ β.inv.right
eq₂ : α.hom.left ≫ f₂ = f₁ ≫ α.hom.right
⊢ (α.hom.left ≫ f₂ ≫ g₂) ≫ β.inv.right = f₁ ≫ g₁
[PROOFSTEP]
simp only [Category.assoc, Category.assoc, ← eq₁, reassoc_of% eq₂, p, ← reassoc_of% (Arrow.comp_left β.hom β.inv),
  β.hom_inv_id, Arrow.id_left, Category.id_comp]
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ α.symm.hom.right = β.symm.hom.left
[PROOFSTEP]
rw [← cancel_mono α.hom.right]
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ α.symm.hom.right ≫ α.hom.right = β.symm.hom.left ≫ α.hom.right
[PROOFSTEP]
simp only [Iso.symm_hom, ← Arrow.comp_right, α.inv_hom_id]
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ (𝟙 (Arrow.mk f₂)).right = β.inv.left ≫ α.hom.right
[PROOFSTEP]
simp only [p, ← Arrow.comp_left, Arrow.id_right, Arrow.id_left, Iso.inv_hom_id]
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
inst✝³ : HasZeroObject V
inst✝² : Preadditive V
inst✝¹ : HasKernels V
inst✝ : HasCokernels V
A₁ B₁ C₁ A₂ B₂ C₂ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ 𝟙 (Arrow.mk f₂).right = 𝟙 (Arrow.mk g₂).left
[PROOFSTEP]
rfl
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ f ≫ g = 0
[PROOFSTEP]
suffices Subobject.arrow (imageSubobject f) ≫ g = 0 by
  rw [← imageSubobject_arrow_comp f, Category.assoc, this, comp_zero]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
this : Subobject.arrow (imageSubobject f) ≫ g = 0
⊢ f ≫ g = 0
[PROOFSTEP]
rw [← imageSubobject_arrow_comp f, Category.assoc, this, comp_zero]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ Subobject.arrow (imageSubobject f) ≫ g = 0
[PROOFSTEP]
rw [p, kernelSubobject_arrow_comp]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ IsIso (imageToKernel f g (_ : f ≫ g = 0))
[PROOFSTEP]
refine' ⟨⟨Subobject.ofLE _ _ p.ge, _⟩⟩
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ imageToKernel f g (_ : f ≫ g = 0) ≫
        Subobject.ofLE (kernelSubobject g) (imageSubobject f) (_ : kernelSubobject g ≤ imageSubobject f) =
      𝟙 (Subobject.underlying.obj (imageSubobject f)) ∧
    Subobject.ofLE (kernelSubobject g) (imageSubobject f) (_ : kernelSubobject g ≤ imageSubobject f) ≫
        imageToKernel f g (_ : f ≫ g = 0) =
      𝟙 (Subobject.underlying.obj (kernelSubobject g))
[PROOFSTEP]
dsimp [imageToKernel]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ Subobject.ofLE (imageSubobject f) (kernelSubobject g) (_ : imageSubobject f ≤ kernelSubobject g) ≫
        Subobject.ofLE (kernelSubobject g) (imageSubobject f) (_ : kernelSubobject g ≤ imageSubobject f) =
      𝟙 (Subobject.underlying.obj (imageSubobject f)) ∧
    Subobject.ofLE (kernelSubobject g) (imageSubobject f) (_ : kernelSubobject g ≤ imageSubobject f) ≫
        Subobject.ofLE (imageSubobject f) (kernelSubobject g) (_ : imageSubobject f ≤ kernelSubobject g) =
      𝟙 (Subobject.underlying.obj (kernelSubobject g))
[PROOFSTEP]
simp only [Subobject.ofLE_comp_ofLE, Subobject.ofLE_refl]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))
[PROOFSTEP]
haveI := imageToKernel_isIso_of_image_eq_kernel f g p
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
this : IsIso (imageToKernel f g (_ : f ≫ g = 0))
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))
[PROOFSTEP]
infer_instance
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
i : B ≅ D
h : Exact f g
⊢ Exact (f ≫ i.hom) (i.inv ≫ g)
[PROOFSTEP]
refine' ⟨by simp [h.w], _⟩
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
i : B ≅ D
h : Exact f g
⊢ (f ≫ i.hom) ≫ i.inv ≫ g = 0
[PROOFSTEP]
simp [h.w]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
i : B ≅ D
h : Exact f g
⊢ Epi (imageToKernel (f ≫ i.hom) (i.inv ≫ g) (_ : (f ≫ i.hom) ≫ i.inv ≫ g = 0))
[PROOFSTEP]
rw [imageToKernel_comp_hom_inv_comp]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
i : B ≅ D
h : Exact f g
⊢ Epi ((imageSubobjectCompIso f i.hom).hom ≫ imageToKernel f g (_ : f ≫ g = 0) ≫ (kernelSubobjectIsoComp i.inv g).inv)
[PROOFSTEP]
haveI := h.epi
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
i : B ≅ D
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ Epi ((imageSubobjectCompIso f i.hom).hom ≫ imageToKernel f g (_ : f ≫ g = 0) ≫ (kernelSubobjectIsoComp i.inv g).inv)
[PROOFSTEP]
infer_instance
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
i : B ≅ D
h : Exact (f ≫ i.hom) (i.inv ≫ g)
⊢ Exact f g
[PROOFSTEP]
simpa using exact_comp_inv_hom_comp i h
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hgh : Exact g h
inst✝ : Epi f
⊢ Exact (f ≫ g) h
[PROOFSTEP]
refine' ⟨by simp [hgh.w], _⟩
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hgh : Exact g h
inst✝ : Epi f
⊢ (f ≫ g) ≫ h = 0
[PROOFSTEP]
simp [hgh.w]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hgh : Exact g h
inst✝ : Epi f
⊢ Epi (imageToKernel (f ≫ g) h (_ : (f ≫ g) ≫ h = 0))
[PROOFSTEP]
rw [imageToKernel_comp_left]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hgh : Exact g h
inst✝ : Epi f
⊢ Epi
    (Subobject.ofLE (imageSubobject (f ≫ g)) (imageSubobject g) (_ : imageSubobject (f ≫ g) ≤ imageSubobject g) ≫
      imageToKernel g h ?w)
case w
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hgh : Exact g h
inst✝ : Epi f
⊢ g ≫ h = 0
[PROOFSTEP]
haveI := hgh.epi
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hgh : Exact g h
inst✝ : Epi f
this : Epi (imageToKernel g h (_ : g ≫ h = 0))
⊢ Epi
    (Subobject.ofLE (imageSubobject (f ≫ g)) (imageSubobject g) (_ : imageSubobject (f ≫ g) ≤ imageSubobject g) ≫
      imageToKernel g h ?w)
case w
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hgh : Exact g h
inst✝ : Epi f
⊢ g ≫ h = 0
[PROOFSTEP]
infer_instance
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : IsIso f
w : Exact (f ≫ g) h
⊢ Exact g h
[PROOFSTEP]
rw [← IsIso.inv_hom_id_assoc f g]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : IsIso f
w : Exact (f ≫ g) h
⊢ Exact (inv f ≫ f ≫ g) h
[PROOFSTEP]
exact exact_epi_comp w
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hfg : Exact f g
inst✝ : Mono h
⊢ Exact f (g ≫ h)
[PROOFSTEP]
refine' ⟨by simp [hfg.w_assoc], _⟩
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hfg : Exact f g
inst✝ : Mono h
⊢ f ≫ g ≫ h = 0
[PROOFSTEP]
simp [hfg.w_assoc]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hfg : Exact f g
inst✝ : Mono h
⊢ Epi (imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0))
[PROOFSTEP]
rw [imageToKernel_comp_right f g h hfg.w]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hfg : Exact f g
inst✝ : Mono h
⊢ Epi
    (imageToKernel f g (_ : f ≫ g = 0) ≫
      Subobject.ofLE (kernelSubobject g) (kernelSubobject (g ≫ h)) (_ : kernelSubobject g ≤ kernelSubobject (g ≫ h)))
[PROOFSTEP]
haveI := hfg.epi
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
hfg : Exact f g
inst✝ : Mono h
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ Epi
    (imageToKernel f g (_ : f ≫ g = 0) ≫
      Subobject.ofLE (kernelSubobject g) (kernelSubobject (g ≫ h)) (_ : kernelSubobject g ≤ kernelSubobject (g ≫ h)))
[PROOFSTEP]
infer_instance
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
⊢ Exact f (g ≫ h) ↔ Exact f g
[PROOFSTEP]
refine' ⟨fun hfg => ⟨zero_of_comp_mono h (by rw [Category.assoc, hfg.1]), _⟩, fun h => exact_comp_mono h⟩
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
hfg : Exact f (g ≫ h)
⊢ (f ≫ g) ≫ h = 0
[PROOFSTEP]
rw [Category.assoc, hfg.1]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
hfg : Exact f (g ≫ h)
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))
[PROOFSTEP]
rw [← (Iso.eq_comp_inv _).1 (imageToKernel_comp_mono _ _ h hfg.1)]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
hfg : Exact f (g ≫ h)
⊢ Epi
    (imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0) ≫
      (Subobject.isoOfEq (kernelSubobject (g ≫ h)) (kernelSubobject g)
          (_ : kernelSubobject (g ≫ h) = kernelSubobject g)).hom)
[PROOFSTEP]
haveI := hfg.2
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
hfg : Exact f (g ≫ h)
this : Epi (imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0))
⊢ Epi
    (imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0) ≫
      (Subobject.isoOfEq (kernelSubobject (g ≫ h)) (kernelSubobject g)
          (_ : kernelSubobject (g ≫ h) = kernelSubobject g)).hom)
[PROOFSTEP]
infer_instance
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ Exact (Subobject.arrow (kernelSubobject f)) f
[PROOFSTEP]
refine' ⟨by simp, _⟩
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ Subobject.arrow (kernelSubobject f) ≫ f = 0
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ Epi (imageToKernel (Subobject.arrow (kernelSubobject f)) f (_ : Subobject.arrow (kernelSubobject f) ≫ f = 0))
[PROOFSTEP]
refine' @IsIso.epi_of_iso _ _ _ _ _ ?_
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ IsIso (imageToKernel (Subobject.arrow (kernelSubobject f)) f (_ : Subobject.arrow (kernelSubobject f) ≫ f = 0))
[PROOFSTEP]
exact ⟨⟨factorThruImageSubobject _, by aesop_cat, by aesop_cat⟩⟩
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ imageToKernel (Subobject.arrow (kernelSubobject f)) f (_ : Subobject.arrow (kernelSubobject f) ≫ f = 0) ≫
      factorThruImageSubobject (Subobject.arrow (kernelSubobject f)) =
    𝟙 (Subobject.underlying.obj (imageSubobject (Subobject.arrow (kernelSubobject f))))
[PROOFSTEP]
aesop_cat
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ factorThruImageSubobject (Subobject.arrow (kernelSubobject f)) ≫
      imageToKernel (Subobject.arrow (kernelSubobject f)) f (_ : Subobject.arrow (kernelSubobject f) ≫ f = 0) =
    𝟙 (Subobject.underlying.obj (kernelSubobject f))
[PROOFSTEP]
aesop_cat
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ Exact (kernel.ι f) f
[PROOFSTEP]
rw [← kernelSubobject_arrow', exact_iso_comp]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
⊢ Exact (Subobject.arrow (kernelSubobject f)) f
[PROOFSTEP]
exact exact_kernelSubobject_arrow
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact f g
⊢ Epi (factorThruKernelSubobject g f (_ : f ≫ g = 0))
[PROOFSTEP]
rw [← factorThruImageSubobject_comp_imageToKernel]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact f g
⊢ Epi (factorThruImageSubobject f ≫ imageToKernel f g (_ : f ≫ g = 0))
[PROOFSTEP]
haveI := h.epi
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ Epi (factorThruImageSubobject f ≫ imageToKernel f g (_ : f ≫ g = 0))
[PROOFSTEP]
apply epi_comp
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact f g
⊢ Epi (kernel.lift g f (_ : f ≫ g = 0))
[PROOFSTEP]
rw [← factorThruKernelSubobject_comp_kernelSubobjectIso]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact f g
⊢ Epi (factorThruKernelSubobject g f (_ : f ≫ g = 0) ≫ (kernelSubobjectIso g).hom)
[PROOFSTEP]
haveI := h.epi_factorThruKernelSubobject
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact f g
this : Epi (factorThruKernelSubobject g f (_ : f ≫ g = 0))
⊢ Epi (factorThruKernelSubobject g f (_ : f ≫ g = 0) ≫ (kernelSubobjectIso g).hom)
[PROOFSTEP]
apply epi_comp
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact 0 g
⊢ Subobject.arrow (kernelSubobject g) = 0
[PROOFSTEP]
haveI := h.epi
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact 0 g
this : Epi (imageToKernel 0 g (_ : 0 ≫ g = 0))
⊢ Subobject.arrow (kernelSubobject g) = 0
[PROOFSTEP]
rw [← cancel_epi (imageToKernel (0 : A ⟶ B) g h.w), ← cancel_epi (factorThruImageSubobject (0 : A ⟶ B))]
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact 0 g
this : Epi (imageToKernel 0 g (_ : 0 ≫ g = 0))
⊢ factorThruImageSubobject 0 ≫ imageToKernel 0 g (_ : 0 ≫ g = 0) ≫ Subobject.arrow (kernelSubobject g) =
    factorThruImageSubobject 0 ≫ imageToKernel 0 g (_ : 0 ≫ g = 0) ≫ 0
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact 0 g
⊢ kernel.ι g = 0
[PROOFSTEP]
rw [← kernelSubobject_arrow']
[GOAL]
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝¹ : HasZeroMorphisms V
inst✝ : HasEqualizers V
h : Exact 0 g
⊢ (kernelSubobjectIso g).inv ≫ Subobject.arrow (kernelSubobject g) = 0
[PROOFSTEP]
simp [kernelSubobject_arrow_eq_zero_of_exact_zero_left A h]
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝³ : HasZeroMorphisms V
inst✝² : HasEqualizers V
inst✝¹ : HasZeroObject V
inst✝ : Mono g
⊢ 0 ≫ g = 0
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
h : Exact f g
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
suffices Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0 by
  rw [← kernelSubobject_arrow', Category.assoc, this, comp_zero]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
h : Exact f g
this : Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
rw [← kernelSubobject_arrow', Category.assoc, this, comp_zero]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
h : Exact f g
⊢ Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0
[PROOFSTEP]
haveI := h.epi
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0
[PROOFSTEP]
apply zero_of_epi_comp (imageToKernel f g h.w) _
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ imageToKernel f g (_ : f ≫ g = 0) ≫ Subobject.arrow (kernelSubobject g) ≫ cokernel.π f = 0
[PROOFSTEP]
rw [imageToKernel_arrow_assoc, ← imageSubobject_arrow, Category.assoc, ← Iso.eq_inv_comp]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
h : Exact f g
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ image.ι f ≫ cokernel.π f = (imageSubobjectIso f).inv ≫ 0
[PROOFSTEP]
aesop_cat
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
h : Exact f g
X Y : V
ι : X ⟶ B
hι : ι ≫ g = 0
π : B ⟶ Y
hπ : f ≫ π = 0
⊢ ι ≫ π = 0
[PROOFSTEP]
rw [← kernel.lift_ι _ _ hι, ← cokernel.π_desc _ _ hπ, Category.assoc, kernel_comp_cokernel_assoc _ _ h, zero_comp,
  comp_zero]
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B C✝ D : V
f✝ : A✝ ⟶ B
g✝ : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
f : A ⟶ 0
g : 0 ⟶ C
⊢ Exact f g
[PROOFSTEP]
obtain rfl : f = 0 := by ext
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B C✝ D : V
f✝ : A✝ ⟶ B
g✝ : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
f : A ⟶ 0
g : 0 ⟶ C
⊢ f = 0
[PROOFSTEP]
ext
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B C✝ D : V
f : A✝ ⟶ B
g✝ : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
g : 0 ⟶ C
⊢ Exact 0 g
[PROOFSTEP]
obtain rfl : g = 0 := by ext
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B C✝ D : V
f : A✝ ⟶ B
g✝ : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
g : 0 ⟶ C
⊢ g = 0
[PROOFSTEP]
ext
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B C✝ D : V
f : A✝ ⟶ B
g : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
⊢ Exact 0 0
[PROOFSTEP]
fconstructor
[GOAL]
case w
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B C✝ D : V
f : A✝ ⟶ B
g : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
⊢ 0 ≫ 0 = 0
[PROOFSTEP]
simp
[GOAL]
case epi
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B C✝ D : V
f : A✝ ⟶ B
g : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
⊢ Epi (imageToKernel 0 0 (_ : 0 ≫ 0 = 0))
[PROOFSTEP]
exact imageToKernel_epi_of_zero_of_mono 0
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A B✝ C✝ D : V
f✝ : A ⟶ B✝
g : B✝ ⟶ C✝
h✝ : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasKernels V
B C : V
f : B ⟶ C
h : Exact 0 f
⊢ Epi 0
[PROOFSTEP]
simpa using h.epi
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
⊢ Epi f
[PROOFSTEP]
have e₁ := h.epi
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (imageToKernel f 0 (_ : f ≫ 0 = 0))
⊢ Epi f
[PROOFSTEP]
rw [imageToKernel_zero_right] at e₁
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
⊢ Epi f
[PROOFSTEP]
have e₂ : Epi (((imageSubobject f).arrow ≫ inv (kernelSubobject 0).arrow) ≫ (kernelSubobject 0).arrow) :=
  @epi_comp _ _ _ _ _ _ e₁ _ _
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
e₂ :
  Epi
    ((Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0))) ≫
      Subobject.arrow (kernelSubobject 0))
⊢ Epi f
[PROOFSTEP]
rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id] at e₂
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
e₂ : Epi (Subobject.arrow (imageSubobject f))
⊢ Epi f
[PROOFSTEP]
rw [← imageSubobject_arrow] at e₂
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
e₂ : Epi ((imageSubobjectIso f).hom ≫ image.ι f)
⊢ Epi f
[PROOFSTEP]
haveI : Epi (image.ι f) := epi_of_epi (imageSubobjectIso f).hom (image.ι f)
[GOAL]
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasImages V
A✝ B✝ C D : V
f✝ : A✝ ⟶ B✝
g : B✝ ⟶ C
h✝ : C ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : Preadditive V
inst✝ : HasEqualizers V
A B : V
f : A ⟶ B
h : Exact f 0
e₁ : Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
e₂ : Epi ((imageSubobjectIso f).hom ≫ image.ι f)
this : Epi (image.ι f)
⊢ Epi f
[PROOFSTEP]
apply epi_of_epi_image


[GOAL]
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
x y : G₁ × G₂
⊢ x ∣ y ↔ x.fst ∣ y.fst ∧ x.snd ∣ y.snd
[PROOFSTEP]
cases x
[GOAL]
case mk
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
y : G₁ × G₂
fst✝ : G₁
snd✝ : G₂
⊢ (fst✝, snd✝) ∣ y ↔ (fst✝, snd✝).fst ∣ y.fst ∧ (fst✝, snd✝).snd ∣ y.snd
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
G₁ : Type u_1
G₂ : Type u_2
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
fst✝¹ : G₁
snd✝¹ : G₂
fst✝ : G₁
snd✝ : G₂
⊢ (fst✝¹, snd✝¹) ∣ (fst✝, snd✝) ↔ (fst✝¹, snd✝¹).fst ∣ (fst✝, snd✝).fst ∧ (fst✝¹, snd✝¹).snd ∣ (fst✝, snd✝).snd
[PROOFSTEP]
simp only [dvd_def, Prod.exists, Prod.mk_mul_mk, Prod.mk.injEq, exists_and_left, exists_and_right, and_self, true_and]


[GOAL]
α : Type u_1
inst✝ : Monoid α
a b : α
h : a = b
⊢ a ∣ b
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
a b c✝ c : α
h : c * a = b
⊢ a * ?m.8269 c h = b
[PROOFSTEP]
rw [mul_comm] at h
[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
a b c✝ c : α
h✝ : c * a = b
h : a * c = b
⊢ a * ?m.8269 c h✝ = b
[PROOFSTEP]
apply h
[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
a b c : α
⊢ (∃ c, b = c * a) → a ∣ b
[PROOFSTEP]
rintro ⟨c, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : CommSemigroup α
a c✝ c : α
⊢ a ∣ c * a
[PROOFSTEP]
exact ⟨c, mul_comm _ _⟩
[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
a b c✝ : α
h : a ∣ b
c : α
⊢ a ∣ c * b
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
a b c✝ : α
h : a ∣ b
c : α
⊢ a ∣ b * c
[PROOFSTEP]
exact h.mul_right _
[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
a✝ b c✝ a c e f : α
⊢ a * e * (c * f) = a * c * (e * f)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
a b c : α
h : a * b ∣ c
d : α
ceq : c = a * b * d
⊢ b * (a * d) = c
[PROOFSTEP]
simp [ceq]
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a✝ b✝ a b : α
h : a ∣ b
⊢ a ^ 0 ∣ b ^ 0
[PROOFSTEP]
rw [pow_zero, pow_zero]
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a✝ b✝ a b : α
h : a ∣ b
n : ℕ
⊢ a ^ (n + 1) ∣ b ^ (n + 1)
[PROOFSTEP]
rw [pow_succ, pow_succ]
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a✝ b✝ a b : α
h : a ∣ b
n : ℕ
⊢ a * a ^ n ∣ b * b ^ n
[PROOFSTEP]
exact mul_dvd_mul h (pow_dvd_pow_of_dvd h n)


[GOAL]
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
⊢ a = ↑u * (↑u⁻¹ * a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
x✝ : a ∣ b * ↑u
c : α
Eq : b * ↑u = a * c
⊢ b = a * (c * ↑u⁻¹)
[PROOFSTEP]
rw [← mul_assoc, ← Eq, Units.mul_inv_cancel_right]
[GOAL]
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
h : a ∣ b
⊢ a * ↑u * ↑u⁻¹ = a
[PROOFSTEP]
rw [mul_assoc, u.mul_inv, mul_one]
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ ↑u * b ↔ a ∣ b
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ b * ↑u ↔ a ∣ b
[PROOFSTEP]
apply dvd_mul_right
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ ↑u * a ∣ b ↔ a ∣ b
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a * ↑u ∣ b ↔ a ∣ b
[PROOFSTEP]
apply mul_right_dvd
[GOAL]
α : Type u_1
inst✝ : Monoid α
a b u : α
hu : IsUnit u
⊢ u ∣ a
[PROOFSTEP]
rcases hu with ⟨u, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
⊢ ↑u ∣ a
[PROOFSTEP]
apply Units.coe_dvd
[GOAL]
α : Type u_1
inst✝ : Monoid α
a b u : α
hu : IsUnit u
⊢ a ∣ b * u ↔ a ∣ b
[PROOFSTEP]
rcases hu with ⟨u, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
⊢ a ∣ b * ↑u ↔ a ∣ b
[PROOFSTEP]
apply Units.dvd_mul_right
[GOAL]
α : Type u_1
inst✝ : Monoid α
a b u : α
hu : IsUnit u
⊢ a * u ∣ b ↔ a ∣ b
[PROOFSTEP]
rcases hu with ⟨u, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
⊢ a * ↑u ∣ b ↔ a ∣ b
[PROOFSTEP]
apply Units.mul_right_dvd
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a b u : α
hu : IsUnit u
⊢ a ∣ u * b ↔ a ∣ b
[PROOFSTEP]
rcases hu with ⟨u, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ ↑u * b ↔ a ∣ b
[PROOFSTEP]
apply Units.dvd_mul_left
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
a b u : α
hu : IsUnit u
⊢ u * a ∣ b ↔ a ∣ b
[PROOFSTEP]
rcases hu with ⟨u, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ ↑u * a ∣ b ↔ a ∣ b
[PROOFSTEP]
apply Units.mul_left_dvd
[GOAL]
α : Type u_1
inst✝ : CommMonoid α
x : α
x✝ : x ∣ 1
y : α
h : 1 = x * y
⊢ y * x = 1
[PROOFSTEP]
rw [h, mul_comm]


[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A✝ B✝ C✝ A' B' C' : 𝒜
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
χ : C ⟶ B
φ : B ⟶ A
hfg : f ≫ g = 0
H : φ ≫ f + g ≫ χ = 𝟙 B
⊢ Epi (imageToKernel f g hfg)
[PROOFSTEP]
set ψ : (kernelSubobject g : 𝒜) ⟶ imageSubobject f := Subobject.arrow _ ≫ φ ≫ factorThruImageSubobject f
[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A✝ B✝ C✝ A' B' C' : 𝒜
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
χ : C ⟶ B
φ : B ⟶ A
hfg : f ≫ g = 0
H : φ ≫ f + g ≫ χ = 𝟙 B
ψ : Subobject.underlying.obj (kernelSubobject g) ⟶ Subobject.underlying.obj (imageSubobject f) :=
  Subobject.arrow (kernelSubobject g) ≫ φ ≫ factorThruImageSubobject f
⊢ Epi (imageToKernel f g hfg)
[PROOFSTEP]
suffices : ψ ≫ imageToKernel f g hfg = 𝟙 _
[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A✝ B✝ C✝ A' B' C' : 𝒜
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
χ : C ⟶ B
φ : B ⟶ A
hfg : f ≫ g = 0
H : φ ≫ f + g ≫ χ = 𝟙 B
ψ : Subobject.underlying.obj (kernelSubobject g) ⟶ Subobject.underlying.obj (imageSubobject f) :=
  Subobject.arrow (kernelSubobject g) ≫ φ ≫ factorThruImageSubobject f
this : ψ ≫ imageToKernel f g hfg = 𝟙 (Subobject.underlying.obj (kernelSubobject g))
⊢ Epi (imageToKernel f g hfg)
[PROOFSTEP]
exact epi_of_epi_fac this
[GOAL]
case this
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A✝ B✝ C✝ A' B' C' : 𝒜
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
χ : C ⟶ B
φ : B ⟶ A
hfg : f ≫ g = 0
H : φ ≫ f + g ≫ χ = 𝟙 B
ψ : Subobject.underlying.obj (kernelSubobject g) ⟶ Subobject.underlying.obj (imageSubobject f) :=
  Subobject.arrow (kernelSubobject g) ≫ φ ≫ factorThruImageSubobject f
⊢ ψ ≫ imageToKernel f g hfg = 𝟙 (Subobject.underlying.obj (kernelSubobject g))
[PROOFSTEP]
rw [← cancel_mono (Subobject.arrow _)]
[GOAL]
case this
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A✝ B✝ C✝ A' B' C' : 𝒜
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
χ : C ⟶ B
φ : B ⟶ A
hfg : f ≫ g = 0
H : φ ≫ f + g ≫ χ = 𝟙 B
ψ : Subobject.underlying.obj (kernelSubobject g) ⟶ Subobject.underlying.obj (imageSubobject f) :=
  Subobject.arrow (kernelSubobject g) ≫ φ ≫ factorThruImageSubobject f
⊢ (ψ ≫ imageToKernel f g hfg) ≫ Subobject.arrow (kernelSubobject g) =
    𝟙 (Subobject.underlying.obj (kernelSubobject g)) ≫ Subobject.arrow (kernelSubobject g)
[PROOFSTEP]
simp only [imageToKernel_arrow, imageSubobject_arrow_comp, Category.id_comp, Category.assoc]
[GOAL]
case this
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A✝ B✝ C✝ A' B' C' : 𝒜
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
χ : C ⟶ B
φ : B ⟶ A
hfg : f ≫ g = 0
H : φ ≫ f + g ≫ χ = 𝟙 B
ψ : Subobject.underlying.obj (kernelSubobject g) ⟶ Subobject.underlying.obj (imageSubobject f) :=
  Subobject.arrow (kernelSubobject g) ≫ φ ≫ factorThruImageSubobject f
⊢ Subobject.arrow (kernelSubobject g) ≫ φ ≫ f = Subobject.arrow (kernelSubobject g)
[PROOFSTEP]
calc
  (kernelSubobject g).arrow ≫ φ ≫ f = (kernelSubobject g).arrow ≫ 𝟙 B :=
    by
    rw [← H, Preadditive.comp_add]
    simp only [add_zero, zero_comp, kernelSubobject_arrow_comp_assoc]
  _ = (kernelSubobject g).arrow := Category.comp_id _
[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A✝ B✝ C✝ A' B' C' : 𝒜
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
χ : C ⟶ B
φ : B ⟶ A
hfg : f ≫ g = 0
H : φ ≫ f + g ≫ χ = 𝟙 B
ψ : Subobject.underlying.obj (kernelSubobject g) ⟶ Subobject.underlying.obj (imageSubobject f) :=
  Subobject.arrow (kernelSubobject g) ≫ φ ≫ factorThruImageSubobject f
⊢ Subobject.arrow (kernelSubobject g) ≫ φ ≫ f = Subobject.arrow (kernelSubobject g) ≫ 𝟙 B
[PROOFSTEP]
rw [← H, Preadditive.comp_add]
[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A✝ B✝ C✝ A' B' C' : 𝒜
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
χ : C ⟶ B
φ : B ⟶ A
hfg : f ≫ g = 0
H : φ ≫ f + g ≫ χ = 𝟙 B
ψ : Subobject.underlying.obj (kernelSubobject g) ⟶ Subobject.underlying.obj (imageSubobject f) :=
  Subobject.arrow (kernelSubobject g) ≫ φ ≫ factorThruImageSubobject f
⊢ Subobject.arrow (kernelSubobject g) ≫ φ ≫ f =
    Subobject.arrow (kernelSubobject g) ≫ φ ≫ f + Subobject.arrow (kernelSubobject g) ≫ g ≫ χ
[PROOFSTEP]
simp only [add_zero, zero_comp, kernelSubobject_arrow_comp_assoc]
[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
h : Split f g
⊢ Exact f g
[PROOFSTEP]
obtain ⟨φ, χ, -, -, h1, -, h2⟩ := h
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
φ : B ⟶ A
χ : C ⟶ B
h1 : f ≫ g = 0
h2 : φ ≫ f + g ≫ χ = 𝟙 B
⊢ Exact f g
[PROOFSTEP]
exact exact_of_split h1 h2
[GOAL]
𝒜✝ : Type u_1
inst✝⁸ : Category.{?u.22622, u_1} 𝒜✝
A✝ B✝ C✝ A' B' C' : 𝒜✝
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁷ : Preadditive 𝒜✝
inst✝⁶ : HasKernels 𝒜✝
inst✝⁵ : HasImages 𝒜✝
𝒜 : Type u_2
ℬ : Type u_3
inst✝⁴ : Category.{u_4, u_2} 𝒜
inst✝³ : Preadditive 𝒜
inst✝² : Category.{u_5, u_3} ℬ
inst✝¹ : Preadditive ℬ
F : 𝒜 ⥤ ℬ
inst✝ : Functor.Additive F
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
h : Split f g
⊢ Split (F.map f) (F.map g)
[PROOFSTEP]
obtain ⟨φ, χ, h1, h2, h3, h4, h5⟩ := h
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
𝒜✝ : Type u_1
inst✝⁸ : Category.{?u.22622, u_1} 𝒜✝
A✝ B✝ C✝ A' B' C' : 𝒜✝
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁷ : Preadditive 𝒜✝
inst✝⁶ : HasKernels 𝒜✝
inst✝⁵ : HasImages 𝒜✝
𝒜 : Type u_2
ℬ : Type u_3
inst✝⁴ : Category.{u_4, u_2} 𝒜
inst✝³ : Preadditive 𝒜
inst✝² : Category.{u_5, u_3} ℬ
inst✝¹ : Preadditive ℬ
F : 𝒜 ⥤ ℬ
inst✝ : Functor.Additive F
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
φ : B ⟶ A
χ : C ⟶ B
h1 : f ≫ φ = 𝟙 A
h2 : χ ≫ g = 𝟙 C
h3 : f ≫ g = 0
h4 : χ ≫ φ = 0
h5 : φ ≫ f + g ≫ χ = 𝟙 B
⊢ Split (F.map f) (F.map g)
[PROOFSTEP]
refine ⟨⟨F.map φ, F.map χ, ?_⟩⟩
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
𝒜✝ : Type u_1
inst✝⁸ : Category.{?u.22622, u_1} 𝒜✝
A✝ B✝ C✝ A' B' C' : 𝒜✝
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁷ : Preadditive 𝒜✝
inst✝⁶ : HasKernels 𝒜✝
inst✝⁵ : HasImages 𝒜✝
𝒜 : Type u_2
ℬ : Type u_3
inst✝⁴ : Category.{u_4, u_2} 𝒜
inst✝³ : Preadditive 𝒜
inst✝² : Category.{u_5, u_3} ℬ
inst✝¹ : Preadditive ℬ
F : 𝒜 ⥤ ℬ
inst✝ : Functor.Additive F
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
φ : B ⟶ A
χ : C ⟶ B
h1 : f ≫ φ = 𝟙 A
h2 : χ ≫ g = 𝟙 C
h3 : f ≫ g = 0
h4 : χ ≫ φ = 0
h5 : φ ≫ f + g ≫ χ = 𝟙 B
⊢ F.map f ≫ F.map φ = 𝟙 (F.obj A) ∧
    F.map χ ≫ F.map g = 𝟙 (F.obj C) ∧
      F.map f ≫ F.map g = 0 ∧ F.map χ ≫ F.map φ = 0 ∧ F.map φ ≫ F.map f + F.map g ≫ F.map χ = 𝟙 (F.obj B)
[PROOFSTEP]
simp only [← F.map_comp, ← F.map_id]
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
𝒜✝ : Type u_1
inst✝⁸ : Category.{?u.22622, u_1} 𝒜✝
A✝ B✝ C✝ A' B' C' : 𝒜✝
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁷ : Preadditive 𝒜✝
inst✝⁶ : HasKernels 𝒜✝
inst✝⁵ : HasImages 𝒜✝
𝒜 : Type u_2
ℬ : Type u_3
inst✝⁴ : Category.{u_4, u_2} 𝒜
inst✝³ : Preadditive 𝒜
inst✝² : Category.{u_5, u_3} ℬ
inst✝¹ : Preadditive ℬ
F : 𝒜 ⥤ ℬ
inst✝ : Functor.Additive F
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
φ : B ⟶ A
χ : C ⟶ B
h1 : f ≫ φ = 𝟙 A
h2 : χ ≫ g = 𝟙 C
h3 : f ≫ g = 0
h4 : χ ≫ φ = 0
h5 : φ ≫ f + g ≫ χ = 𝟙 B
⊢ F.map (f ≫ φ) = F.map (𝟙 A) ∧
    F.map (χ ≫ g) = F.map (𝟙 C) ∧ F.map (f ≫ g) = 0 ∧ F.map (χ ≫ φ) = 0 ∧ F.map (φ ≫ f) + F.map (g ≫ χ) = F.map (𝟙 B)
[PROOFSTEP]
rw [← F.map_add]
  -- porting note: `simp only` fails to use this lemma
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
𝒜✝ : Type u_1
inst✝⁸ : Category.{?u.22622, u_1} 𝒜✝
A✝ B✝ C✝ A' B' C' : 𝒜✝
f✝ : A✝ ⟶ B✝
g✝ : B✝ ⟶ C✝
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁷ : Preadditive 𝒜✝
inst✝⁶ : HasKernels 𝒜✝
inst✝⁵ : HasImages 𝒜✝
𝒜 : Type u_2
ℬ : Type u_3
inst✝⁴ : Category.{u_4, u_2} 𝒜
inst✝³ : Preadditive 𝒜
inst✝² : Category.{u_5, u_3} ℬ
inst✝¹ : Preadditive ℬ
F : 𝒜 ⥤ ℬ
inst✝ : Functor.Additive F
A B C : 𝒜
f : A ⟶ B
g : B ⟶ C
φ : B ⟶ A
χ : C ⟶ B
h1 : f ≫ φ = 𝟙 A
h2 : χ ≫ g = 𝟙 C
h3 : f ≫ g = 0
h4 : χ ≫ φ = 0
h5 : φ ≫ f + g ≫ χ = 𝟙 B
⊢ F.map (f ≫ φ) = F.map (𝟙 A) ∧
    F.map (χ ≫ g) = F.map (𝟙 C) ∧ F.map (f ≫ g) = 0 ∧ F.map (χ ≫ φ) = 0 ∧ F.map (φ ≫ f + g ≫ χ) = F.map (𝟙 B)
[PROOFSTEP]
simp only [F.map_zero, *, true_and]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ biprod.inl ≫ h.iso.inv = f
[PROOFSTEP]
rw [Iso.comp_inv_eq, h.comp_iso_eq_inl]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ h.iso.inv ≫ g = biprod.snd
[PROOFSTEP]
rw [Iso.inv_comp_eq, h.iso_comp_snd_eq]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ section h ≫ g = 𝟙 C
[PROOFSTEP]
simp [Splitting.section]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ f ≫ retraction h = 𝟙 A
[PROOFSTEP]
simp [retraction]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ section h ≫ retraction h = 0
[PROOFSTEP]
delta Splitting.section retraction
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ (biprod.inr ≫ h.iso.inv) ≫ h.iso.hom ≫ biprod.fst = 0
[PROOFSTEP]
simp
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{?u.48802, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ f ≫ retraction h = 𝟙 A
[PROOFSTEP]
simp
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{?u.49754, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ section h ≫ g = 𝟙 C
[PROOFSTEP]
simp
[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{?u.54404, u_1} 𝒜
A B C A' B' C' : 𝒜
f✝ : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : HasZeroMorphisms 𝒜
inst✝¹ : HasBinaryBiproducts 𝒜
h : Splitting f✝ g
X Y Z : 𝒜
f : X ⟶ Y
inst✝ : IsIso f
hZ : IsZero Z
⊢ f ≫ ((asIso f).symm ≪≫ isoBiprodZero hZ).hom = biprod.inl
[PROOFSTEP]
simp [hZ.eq_of_tgt _ 0]
[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{?u.54404, u_1} 𝒜
A B C A' B' C' : 𝒜
f✝ : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : HasZeroMorphisms 𝒜
inst✝¹ : HasBinaryBiproducts 𝒜
h : Splitting f✝ g
X Y Z : 𝒜
f : X ⟶ Y
inst✝ : IsIso f
hZ : IsZero Z
⊢ ((asIso f).symm ≪≫ isoBiprodZero hZ).hom ≫ biprod.snd = 0
[PROOFSTEP]
simp
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{?u.60340, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ Mono (section h)
[PROOFSTEP]
delta Splitting.section
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{?u.60340, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ Mono (biprod.inr ≫ h.iso.inv)
[PROOFSTEP]
infer_instance
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{?u.61269, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ Epi (retraction h)
[PROOFSTEP]
delta retraction
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{?u.61269, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : HasZeroMorphisms 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ Epi (h.iso.hom ≫ biprod.fst)
[PROOFSTEP]
apply epi_comp
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ retraction h ≫ f + g ≫ section h = 𝟙 B
[PROOFSTEP]
delta Splitting.section retraction
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ (h.iso.hom ≫ biprod.fst) ≫ f + g ≫ biprod.inr ≫ h.iso.inv = 𝟙 B
[PROOFSTEP]
rw [← cancel_mono h.iso.hom, ← cancel_epi h.iso.inv]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ h.iso.inv ≫ ((h.iso.hom ≫ biprod.fst) ≫ f + g ≫ biprod.inr ≫ h.iso.inv) ≫ h.iso.hom = h.iso.inv ≫ 𝟙 B ≫ h.iso.hom
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp, Category.assoc, Iso.inv_hom_id_assoc, Iso.inv_hom_id,
  Limits.biprod.total, Preadditive.comp_add, Preadditive.add_comp, Splitting.comp_iso_eq_inl,
  Splitting.iso_comp_eq_snd_assoc]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h✝ h h' : Splitting f g
⊢ section h' ≫ retraction h = -section h ≫ retraction h'
[PROOFSTEP]
haveI := h.mono
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h✝ h h' : Splitting f g
this : Mono f
⊢ section h' ≫ retraction h = -section h ≫ retraction h'
[PROOFSTEP]
rw [← cancel_mono f]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h✝ h h' : Splitting f g
this : Mono f
⊢ (section h' ≫ retraction h) ≫ f = (-section h ≫ retraction h') ≫ f
[PROOFSTEP]
simp [retraction_ι_eq_id_sub]
[GOAL]
𝒜 : Type u_1
inst✝² : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝¹ : Preadditive 𝒜
inst✝ : HasBinaryBiproducts 𝒜
h : Splitting f g
⊢ f ≫ g = 0
[PROOFSTEP]
rw [← h.inl_comp_iso_eq, Category.assoc, h.iso_comp_eq_snd, biprod.inl_snd]
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ Exact f g
[PROOFSTEP]
rw [exact_iff_exact_of_iso f g (biprod.inl : A ⟶ A ⊞ C) (biprod.snd : A ⊞ C ⟶ C) _ _ _]
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ Exact biprod.inl biprod.snd
[PROOFSTEP]
exact exact_inl_snd _ _
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ Arrow.mk f ≅ Arrow.mk biprod.inl
[PROOFSTEP]
refine Arrow.isoMk (Iso.refl _) h.iso ?_
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ (Iso.refl (Arrow.mk f).left).hom ≫ (Arrow.mk biprod.inl).hom = (Arrow.mk f).hom ≫ h.iso.hom
[PROOFSTEP]
simp only [Iso.refl_hom, Arrow.mk_hom, Category.id_comp, comp_iso_eq_inl]
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ biprod.inl = biprod.inl
[PROOFSTEP]
rfl
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ Arrow.mk g ≅ Arrow.mk biprod.snd
[PROOFSTEP]
refine Arrow.isoMk h.iso (Iso.refl _) ?_
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ h.iso.hom ≫ (Arrow.mk biprod.snd).hom = (Arrow.mk g).hom ≫ (Iso.refl (Arrow.mk g).right).hom
[PROOFSTEP]
dsimp
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ h.iso.hom ≫ biprod.snd = g ≫ 𝟙 C
[PROOFSTEP]
simp
[GOAL]
𝒜 : Type u_1
inst✝⁶ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ (Arrow.isoMk (Iso.refl (Arrow.mk f).left) h.iso).hom.right =
    (Arrow.isoMk h.iso (Iso.refl (Arrow.mk g).right)).hom.left
[PROOFSTEP]
rfl


[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p in antidiagonal (n + 1), f p = f (0, n + 1) * ∏ p in antidiagonal n, f (p.fst + 1, p.snd)
[PROOFSTEP]
rw [antidiagonal_succ, prod_cons, prod_map]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1) *
      ∏ x in antidiagonal n,
        f
          (↑(Function.Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Function.Embedding.refl ℕ))
            x) =
    f (0, n + 1) * ∏ p in antidiagonal n, f (p.fst + 1, p.snd)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p in antidiagonal n, f (Prod.swap p) = ∏ p in antidiagonal n, f p
[PROOFSTEP]
conv_lhs => rw [← map_swap_antidiagonal, Finset.prod_map]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
| ∏ p in antidiagonal n, f (Prod.swap p)
[PROOFSTEP]
rw [← map_swap_antidiagonal, Finset.prod_map]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
| ∏ p in antidiagonal n, f (Prod.swap p)
[PROOFSTEP]
rw [← map_swap_antidiagonal, Finset.prod_map]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
| ∏ p in antidiagonal n, f (Prod.swap p)
[PROOFSTEP]
rw [← map_swap_antidiagonal, Finset.prod_map]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p in antidiagonal (n + 1), f p = f (n + 1, 0) * ∏ p in antidiagonal n, f (p.fst, p.snd + 1)
[PROOFSTEP]
rw [← prod_antidiagonal_swap, prod_antidiagonal_succ, ← prod_antidiagonal_swap]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → M
⊢ f (Prod.swap (0, n + 1)) * ∏ p in antidiagonal n, f (Prod.swap ((Prod.swap p).fst + 1, (Prod.swap p).snd)) =
    f (n + 1, 0) * ∏ p in antidiagonal n, f (p.fst, p.snd + 1)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : AddCommMonoid N
n : ℕ
f : ℕ × ℕ → ℕ → M
p : ℕ × ℕ
hp : p ∈ antidiagonal n
⊢ f p n = f p (p.fst + p.snd)
[PROOFSTEP]
rw [Nat.mem_antidiagonal.1 hp]


[GOAL]
α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : Option α → M
s : Finset α
⊢ ∏ x in ↑insertNone s, f x = f none * ∏ x in s, f (some x)
[PROOFSTEP]
simp [insertNone]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ ∏ x in ↑eraseNone s, f x = ∏ x in s, Option.elim' 1 f x
[PROOFSTEP]
classical calc
  ∏ x in eraseNone s, f x = ∏ x in (eraseNone s).map Embedding.some, Option.elim' 1 f x :=
    (prod_map (eraseNone s) Embedding.some <| Option.elim' 1 f).symm
  _ = ∏ x in s.erase none, Option.elim' 1 f x := by rw [map_some_eraseNone]
  _ = ∏ x in s, Option.elim' 1 f x := prod_erase _ rfl
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ ∏ x in ↑eraseNone s, f x = ∏ x in s, Option.elim' 1 f x
[PROOFSTEP]
calc
  ∏ x in eraseNone s, f x = ∏ x in (eraseNone s).map Embedding.some, Option.elim' 1 f x :=
    (prod_map (eraseNone s) Embedding.some <| Option.elim' 1 f).symm
  _ = ∏ x in s.erase none, Option.elim' 1 f x := by rw [map_some_eraseNone]
  _ = ∏ x in s, Option.elim' 1 f x := prod_erase _ rfl
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ ∏ x in map Embedding.some (↑eraseNone s), Option.elim' 1 f x = ∏ x in erase s none, Option.elim' 1 f x
[PROOFSTEP]
rw [map_some_eraseNone]