[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : Finset.Nonempty s
hs : ∀ (i : ι), i ∈ s → p (g i)
⊢ f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
[PROOFSTEP]
refine' le_trans (Multiset.le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul _ _ _) _
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : Finset.Nonempty s
hs : ∀ (i : ι), i ∈ s → p (g i)
⊢ Multiset.map (fun i => g i) s.val ≠ ∅
[PROOFSTEP]
simp [hs_nonempty.ne_empty]
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : Finset.Nonempty s
hs : ∀ (i : ι), i ∈ s → p (g i)
⊢ ∀ (a : M), a ∈ Multiset.map (fun i => g i) s.val → p a
[PROOFSTEP]
exact Multiset.forall_mem_map_iff.mpr hs
[GOAL]
case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : Finset.Nonempty s
hs : ∀ (i : ι), i ∈ s → p (g i)
⊢ Multiset.prod (Multiset.map f (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)
[PROOFSTEP]
rw [Multiset.map_map]
[GOAL]
case refine'_3
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs_nonempty : Finset.Nonempty s
hs : ∀ (i : ι), i ∈ s → p (g i)
⊢ Multiset.prod (Multiset.map (f ∘ fun i => g i) s.val) ≤ ∏ i in s, f (g i)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_one : f 1 = 1
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs : ∀ (i : ι), i ∈ s → p (g i)
⊢ f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
[PROOFSTEP]
rcases eq_empty_or_nonempty s with (rfl | hs_nonempty)
[GOAL]
case inl
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_one : f 1 = 1
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
hs : ∀ (i : ι), i ∈ ∅ → p (g i)
⊢ f (∏ i in ∅, g i) ≤ ∏ i in ∅, f (g i)
[PROOFSTEP]
simp [h_one]
[GOAL]
case inr
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_one : f 1 = 1
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs : ∀ (i : ι), i ∈ s → p (g i)
hs_nonempty : Finset.Nonempty s
⊢ f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
[PROOFSTEP]
exact le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul g s hs_nonempty hs
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
h_one : f 1 = 1
h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y
s : Finset ι
g : ι → M
⊢ f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
[PROOFSTEP]
refine' le_trans (Multiset.le_prod_of_submultiplicative f h_one h_mul _) _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
h_one : f 1 = 1
h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y
s : Finset ι
g : ι → M
⊢ Multiset.prod (Multiset.map f (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)
[PROOFSTEP]
rw [Multiset.map_map]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
h_one : f 1 = 1
h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y
s : Finset ι
g : ι → M
⊢ Multiset.prod (Multiset.map (f ∘ fun i => g i) s.val) ≤ ∏ i in s, f (g i)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
h : ∀ (i : ι), i ∈ s → 1 ≤ f i
⊢ 1 ≤ ∏ i in s, 1
[PROOFSTEP]
rw [prod_const_one]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
h : ∀ (i : ι), i ∈ s → f i ≤ 1
⊢ ∏ i in s, 1 = 1
[PROOFSTEP]
rw [prod_const_one]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
h : s ⊆ t
hf : ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i
⊢ ∏ i in s, f i ≤ ∏ i in t, f i
[PROOFSTEP]
classical calc
  ∏ i in s, f i ≤ (∏ i in t \ s, f i) * ∏ i in s, f i :=
    le_mul_of_one_le_left' <| one_le_prod' <| by simpa only [mem_sdiff, and_imp]
  _ = ∏ i in t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
  _ = ∏ i in t, f i := by rw [sdiff_union_of_subset h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
h : s ⊆ t
hf : ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i
⊢ ∏ i in s, f i ≤ ∏ i in t, f i
[PROOFSTEP]
calc
  ∏ i in s, f i ≤ (∏ i in t \ s, f i) * ∏ i in s, f i :=
    le_mul_of_one_le_left' <| one_le_prod' <| by simpa only [mem_sdiff, and_imp]
  _ = ∏ i in t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
  _ = ∏ i in t, f i := by rw [sdiff_union_of_subset h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
h : s ⊆ t
hf : ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i
⊢ ∀ (i : ι), i ∈ t \ s → 1 ≤ f i
[PROOFSTEP]
simpa only [mem_sdiff, and_imp]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
h : s ⊆ t
hf : ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i
⊢ ∏ i in t \ s ∪ s, f i = ∏ i in t, f i
[PROOFSTEP]
rw [sdiff_union_of_subset h]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
⊢ (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
[PROOFSTEP]
classical
refine Finset.induction_on s (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.not_mem_empty _ h), fun _ ↦ rfl⟩) ?_
intro a s ha ih H
have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem
rw [prod_insert ha, mul_eq_one_iff' (H _ <| mem_insert_self _ _) (one_le_prod' this), forall_mem_insert, ih this]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
⊢ (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
[PROOFSTEP]
refine Finset.induction_on s (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.not_mem_empty _ h), fun _ ↦ rfl⟩) ?_
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s t : Finset ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ((∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)) →
        (∀ (i : ι), i ∈ insert a s → 1 ≤ f i) → (∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1)
[PROOFSTEP]
intro a s ha ih H
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s✝ t : Finset ι
a : ι
s : Finset ι
ha : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
H : ∀ (i : ι), i ∈ insert a s → 1 ≤ f i
⊢ ∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
[PROOFSTEP]
have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f g : ι → N
s✝ t : Finset ι
a : ι
s : Finset ι
ha : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
H : ∀ (i : ι), i ∈ insert a s → 1 ≤ f i
this : ∀ (i : ι), i ∈ s → 1 ≤ f i
⊢ ∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
[PROOFSTEP]
rw [prod_insert ha, mul_eq_one_iff' (H _ <| mem_insert_self _ _) (one_le_prod' this), forall_mem_insert, ih this]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f✝ g : ι → N
s✝ t s : Finset ι
f : ι → N
n : N
h : ∀ (x : ι), x ∈ s → f x ≤ n
⊢ Finset.prod s f ≤ n ^ card s
[PROOFSTEP]
refine' (Multiset.prod_le_pow_card (s.val.map f) n _).trans _
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f✝ g : ι → N
s✝ t s : Finset ι
f : ι → N
n : N
h : ∀ (x : ι), x ∈ s → f x ≤ n
⊢ ∀ (x : N), x ∈ Multiset.map f s.val → x ≤ n
[PROOFSTEP]
simpa using h
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f✝ g : ι → N
s✝ t s : Finset ι
f : ι → N
n : N
h : ∀ (x : ι), x ∈ s → f x ≤ n
⊢ n ^ ↑Multiset.card (Multiset.map f s.val) ≤ n ^ card s
[PROOFSTEP]
simp
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f✝ g : ι → N
s✝ t s : Finset ι
f : ι → N
n : N
h : ∀ (x : ι), x ∈ s → f x ≤ n
⊢ n ^ ↑Multiset.card s.val ≤ n ^ card s
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G✝ : Type u_6
k : Type u_7
R : Type u_8
G : Type u_9
inst✝ : LinearOrderedAddCommGroup G
f : ι → G
s : Finset ι
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
⊢ |∑ i in s, f i| = ∑ i in s, f i
[PROOFSTEP]
rw [abs_of_nonneg (Finset.sum_nonneg hf)]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G✝ : Type u_6
k : Type u_7
R : Type u_8
G : Type u_9
inst✝ : LinearOrderedAddCommGroup G
f : ι → G
s : Finset ι
hf : ∀ (i : ι), 0 ≤ f i
⊢ |∑ i in s, f i| = ∑ i in s, f i
[PROOFSTEP]
rw [abs_of_nonneg (Finset.sum_nonneg' hf)]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ (a : α), a ∈ s → f a ∈ t
n : ℕ
hn : ∀ (a : β), a ∈ t → card (filter (fun x => f x = a) s) ≤ n
⊢ ∑ _a in t, n = n * card t
[PROOFSTEP]
simp [mul_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ (a : α), a ∈ s → f a ∈ t
n : ℕ
hn : ∀ (a : β), a ∈ t → n ≤ card (filter (fun x => f x = a) s)
⊢ n * card t = ∑ _a in t, n
[PROOFSTEP]
simp [mul_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
Hf : ∀ (a : α), a ∈ s → f a ∈ t
n : ℕ
hn : ∀ (a : β), a ∈ t → n ≤ card (filter (fun x => f x = a) s)
⊢ ∑ a in t, card (filter (fun x => f x = a) s) = card s
[PROOFSTEP]
rw [← card_eq_sum_card_fiberwise Hf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ (a : α), a ∈ s → card (filter ((fun x x_1 => x ∈ x_1) a) B) ≤ n
⊢ ∑ t in B, card (s ∩ t) ≤ card s * n
[PROOFSTEP]
refine' le_trans _ (s.sum_le_card_nsmul _ _ h)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ (a : α), a ∈ s → card (filter ((fun x x_1 => x ∈ x_1) a) B) ≤ n
⊢ ∑ t in B, card (s ∩ t) ≤ ∑ x in s, card (filter ((fun x x_1 => x ∈ x_1) x) B)
[PROOFSTEP]
simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ (a : α), a ∈ s → card (filter ((fun x x_1 => x ∈ x_1) a) B) ≤ n
⊢ (∑ x in B, ∑ a in s, if a ∈ x then 1 else 0) ≤ ∑ x in s, ∑ a in B, if x ∈ a then 1 else 0
[PROOFSTEP]
exact sum_comm.le
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
inst✝ : Fintype α
h : ∀ (a : α), card (filter ((fun x x_1 => x ∈ x_1) a) B) ≤ n
⊢ ∑ s in B, card s = ∑ s in B, card (univ ∩ s)
[PROOFSTEP]
simp_rw [univ_inter]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ (a : α), a ∈ s → n ≤ card (filter ((fun x x_1 => x ∈ x_1) a) B)
⊢ card s * n ≤ ∑ t in B, card (s ∩ t)
[PROOFSTEP]
apply (s.card_nsmul_le_sum _ _ h).trans
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ (a : α), a ∈ s → n ≤ card (filter ((fun x x_1 => x ∈ x_1) a) B)
⊢ ∑ x in s, card (filter ((fun x x_1 => x ∈ x_1) x) B) ≤ ∑ t in B, card (s ∩ t)
[PROOFSTEP]
simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ (a : α), a ∈ s → n ≤ card (filter ((fun x x_1 => x ∈ x_1) a) B)
⊢ (∑ x in s, ∑ a in B, if x ∈ a then 1 else 0) ≤ ∑ x in B, ∑ a in s, if a ∈ x then 1 else 0
[PROOFSTEP]
exact sum_comm.le
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
inst✝ : Fintype α
h : ∀ (a : α), n ≤ card (filter ((fun x x_1 => x ∈ x_1) a) B)
⊢ ∑ s in B, card (univ ∩ s) = ∑ s in B, card s
[PROOFSTEP]
simp_rw [univ_inter]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
inst✝ : Fintype α
h : ∀ (a : α), card (filter ((fun x x_1 => x ∈ x_1) a) B) = n
⊢ ∑ s in B, card s = Fintype.card α * n
[PROOFSTEP]
simp_rw [Fintype.card, ← sum_card_inter fun a _ ↦ h a, univ_inter]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : DecidableEq α
s✝ : Finset α
B : Finset (Finset α)
n : ℕ
s : Finset ι
f : ι → Finset α
hs : Set.PairwiseDisjoint (↑s) f
hf : ∀ (i : ι), i ∈ s → Finset.Nonempty (f i)
⊢ card s ≤ card (Finset.biUnion s f)
[PROOFSTEP]
rw [card_biUnion hs, card_eq_sum_ones]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : DecidableEq α
s✝ : Finset α
B : Finset (Finset α)
n : ℕ
s : Finset ι
f : ι → Finset α
hs : Set.PairwiseDisjoint (↑s) f
hf : ∀ (i : ι), i ∈ s → Finset.Nonempty (f i)
⊢ ∑ x in s, 1 ≤ ∑ u in s, card (f u)
[PROOFSTEP]
exact sum_le_sum fun i hi ↦ (hf i hi).card_pos
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : DecidableEq α
s✝ : Finset α
B : Finset (Finset α)
n : ℕ
s : Finset ι
f : ι → Finset α
hs : Set.PairwiseDisjoint (↑s) f
⊢ card s ≤ card (Finset.biUnion s f) + card (filter (fun i => f i = ∅) s)
[PROOFSTEP]
rw [← Finset.filter_card_add_filter_neg_card_eq_card fun i ↦ f i = ∅, add_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : DecidableEq α
s✝ : Finset α
B : Finset (Finset α)
n : ℕ
s : Finset ι
f : ι → Finset α
hs : Set.PairwiseDisjoint (↑s) f
⊢ card (filter (fun a => ¬f a = ∅) s) + card (filter (fun i => f i = ∅) s) ≤
    card (Finset.biUnion s f) + card (filter (fun i => f i = ∅) s)
[PROOFSTEP]
exact
  add_le_add_right
    ((card_le_card_biUnion (hs.subset <| filter_subset _ _) fun i hi ↦
          nonempty_of_ne_empty <| (mem_filter.1 hi).2).trans <|
      card_le_of_subset <| biUnion_subset_biUnion_of_subset_left _ <| filter_subset _ _)
    _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
f : ι → M
s t : Finset ι
h : ∀ (x : ι), x ∈ s → f x ≠ 1 → x ∈ t
⊢ ∏ x in s, f x ≤ ∏ x in t, f x
[PROOFSTEP]
classical calc
  ∏ x in s, f x = (∏ x in s.filter fun x ↦ f x = 1, f x) * ∏ x in s.filter fun x ↦ f x ≠ 1, f x :=
    by
    rw [← prod_union, filter_union_filter_neg_eq]
    exact disjoint_filter.2 fun _ _ h n_h ↦ n_h h
  _ ≤ ∏ x in t, f x :=
    mul_le_of_le_one_of_le (prod_le_one' <| by simp only [mem_filter, and_imp]; exact fun _ _ ↦ le_of_eq)
      (prod_le_prod_of_subset' <| by simpa only [subset_iff, mem_filter, and_imp])
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
f : ι → M
s t : Finset ι
h : ∀ (x : ι), x ∈ s → f x ≠ 1 → x ∈ t
⊢ ∏ x in s, f x ≤ ∏ x in t, f x
[PROOFSTEP]
calc
  ∏ x in s, f x = (∏ x in s.filter fun x ↦ f x = 1, f x) * ∏ x in s.filter fun x ↦ f x ≠ 1, f x :=
    by
    rw [← prod_union, filter_union_filter_neg_eq]
    exact disjoint_filter.2 fun _ _ h n_h ↦ n_h h
  _ ≤ ∏ x in t, f x :=
    mul_le_of_le_one_of_le (prod_le_one' <| by simp only [mem_filter, and_imp]; exact fun _ _ ↦ le_of_eq)
      (prod_le_prod_of_subset' <| by simpa only [subset_iff, mem_filter, and_imp])
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
f : ι → M
s t : Finset ι
h : ∀ (x : ι), x ∈ s → f x ≠ 1 → x ∈ t
⊢ ∏ x in s, f x = (∏ x in filter (fun x => f x = 1) s, f x) * ∏ x in filter (fun x => f x ≠ 1) s, f x
[PROOFSTEP]
rw [← prod_union, filter_union_filter_neg_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
f : ι → M
s t : Finset ι
h : ∀ (x : ι), x ∈ s → f x ≠ 1 → x ∈ t
⊢ Disjoint (filter (fun x => f x = 1) s) (filter (fun x => f x ≠ 1) s)
[PROOFSTEP]
exact disjoint_filter.2 fun _ _ h n_h ↦ n_h h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
f : ι → M
s t : Finset ι
h : ∀ (x : ι), x ∈ s → f x ≠ 1 → x ∈ t
⊢ ∀ (i : ι), i ∈ filter (fun x => f x = 1) s → f i ≤ 1
[PROOFSTEP]
simp only [mem_filter, and_imp]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
f : ι → M
s t : Finset ι
h : ∀ (x : ι), x ∈ s → f x ≠ 1 → x ∈ t
⊢ ∀ (i : ι), i ∈ s → f i = 1 → f i ≤ 1
[PROOFSTEP]
exact fun _ _ ↦ le_of_eq
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedMonoid M
f : ι → M
s t : Finset ι
h : ∀ (x : ι), x ∈ s → f x ≠ 1 → x ∈ t
⊢ filter (fun x => f x ≠ 1) s ⊆ t
[PROOFSTEP]
simpa only [subset_iff, mem_filter, and_imp]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hle : ∀ (i : ι), i ∈ s → f i ≤ g i
Hlt : ∃ i, i ∈ s ∧ f i < g i
⊢ ∏ i in s, f i < ∏ i in s, g i
[PROOFSTEP]
classical
rcases Hlt with ⟨i, hi, hlt⟩
rw [← insert_erase hi, prod_insert (not_mem_erase _ _), prod_insert (not_mem_erase _ _)]
exact mul_lt_mul_of_lt_of_le hlt (prod_le_prod' fun j hj ↦ Hle j <| mem_of_mem_erase hj)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hle : ∀ (i : ι), i ∈ s → f i ≤ g i
Hlt : ∃ i, i ∈ s ∧ f i < g i
⊢ ∏ i in s, f i < ∏ i in s, g i
[PROOFSTEP]
rcases Hlt with ⟨i, hi, hlt⟩
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hle : ∀ (i : ι), i ∈ s → f i ≤ g i
i : ι
hi : i ∈ s
hlt : f i < g i
⊢ ∏ i in s, f i < ∏ i in s, g i
[PROOFSTEP]
rw [← insert_erase hi, prod_insert (not_mem_erase _ _), prod_insert (not_mem_erase _ _)]
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hle : ∀ (i : ι), i ∈ s → f i ≤ g i
i : ι
hi : i ∈ s
hlt : f i < g i
⊢ f i * ∏ x in erase s i, f x < g i * ∏ x in erase s i, g x
[PROOFSTEP]
exact mul_lt_mul_of_lt_of_le hlt (prod_le_prod' fun j hj ↦ Hle j <| mem_of_mem_erase hj)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
hs : Finset.Nonempty s
Hlt : ∀ (i : ι), i ∈ s → f i < g i
⊢ ∏ i in s, f i < ∏ i in s, g i
[PROOFSTEP]
apply prod_lt_prod'
[GOAL]
case Hle
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
hs : Finset.Nonempty s
Hlt : ∀ (i : ι), i ∈ s → f i < g i
⊢ ∀ (i : ι), i ∈ s → f i ≤ g i
[PROOFSTEP]
intro i hi
[GOAL]
case Hle
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
hs : Finset.Nonempty s
Hlt : ∀ (i : ι), i ∈ s → f i < g i
i : ι
hi : i ∈ s
⊢ f i ≤ g i
[PROOFSTEP]
apply le_of_lt (Hlt i hi)
[GOAL]
case Hlt
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
hs : Finset.Nonempty s
Hlt : ∀ (i : ι), i ∈ s → f i < g i
⊢ ∃ i, i ∈ s ∧ f i < g i
[PROOFSTEP]
cases' hs with i hi
[GOAL]
case Hlt.intro
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hlt : ∀ (i : ι), i ∈ s → f i < g i
i : ι
hi : i ∈ s
⊢ ∃ i, i ∈ s ∧ f i < g i
[PROOFSTEP]
exact ⟨i, hi, Hlt i hi⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
⊢ ∏ j in s, f j < ∏ j in t, f j
[PROOFSTEP]
classical calc
  ∏ j in s, f j < ∏ j in insert i s, f j := by
    rw [prod_insert hs]
    exact lt_mul_of_one_lt_left' (∏ j in s, f j) hlt
  _ ≤ ∏ j in t, f j := by
    apply prod_le_prod_of_subset_of_one_le'
    · simp [Finset.insert_subset_iff, h, ht]
    · intro x hx h'x
      simp only [mem_insert, not_or] at h'x
      exact hle x hx h'x.2
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
⊢ ∏ j in s, f j < ∏ j in t, f j
[PROOFSTEP]
calc
  ∏ j in s, f j < ∏ j in insert i s, f j := by
    rw [prod_insert hs]
    exact lt_mul_of_one_lt_left' (∏ j in s, f j) hlt
  _ ≤ ∏ j in t, f j := by
    apply prod_le_prod_of_subset_of_one_le'
    · simp [Finset.insert_subset_iff, h, ht]
    · intro x hx h'x
      simp only [mem_insert, not_or] at h'x
      exact hle x hx h'x.2
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
⊢ ∏ j in s, f j < ∏ j in insert i s, f j
[PROOFSTEP]
rw [prod_insert hs]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
⊢ ∏ j in s, f j < f i * ∏ x in s, f x
[PROOFSTEP]
exact lt_mul_of_one_lt_left' (∏ j in s, f j) hlt
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
⊢ ∏ j in insert i s, f j ≤ ∏ j in t, f j
[PROOFSTEP]
apply prod_le_prod_of_subset_of_one_le'
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
⊢ insert i s ⊆ t
[PROOFSTEP]
simp [Finset.insert_subset_iff, h, ht]
[GOAL]
case hf
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
⊢ ∀ (i_1 : ι), i_1 ∈ t → ¬i_1 ∈ insert i s → 1 ≤ f i_1
[PROOFSTEP]
intro x hx h'x
[GOAL]
case hf
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
x : ι
hx : x ∈ t
h'x : ¬x ∈ insert i s
⊢ 1 ≤ f x
[PROOFSTEP]
simp only [mem_insert, not_or] at h'x
[GOAL]
case hf
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : s ⊆ t
i : ι
ht : i ∈ t
hs : ¬i ∈ s
hlt : 1 < f i
hle : ∀ (j : ι), j ∈ t → ¬j ∈ s → 1 ≤ f j
x : ι
hx : x ∈ t
h'x : ¬x = i ∧ ¬x ∈ s
⊢ 1 ≤ f x
[PROOFSTEP]
exact hle x hx h'x.2
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : ∀ (i : ι), i ∈ s → 1 < f i
hs : Finset.Nonempty s
⊢ 1 ≤ ∏ i in s, 1
[PROOFSTEP]
rw [prod_const_one]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
h : ∀ (i : ι), i ∈ s → f i < 1
hs : Finset.Nonempty s
⊢ ∏ i in s, 1 ≤ 1
[PROOFSTEP]
rw [prod_const_one]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f✝ g✝ : ι → M
s t : Finset ι
f g : ι → M
h : ∀ (i : ι), i ∈ s → f i ≤ g i
⊢ ∏ i in s, f i = ∏ i in s, g i ↔ ∀ (i : ι), i ∈ s → f i = g i
[PROOFSTEP]
classical
revert h
refine
  Finset.induction_on s (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.not_mem_empty _ h), fun _ ↦ rfl⟩) fun a s ha ih H ↦ ?_
specialize ih fun i ↦ H i ∘ Finset.mem_insert_of_mem
rw [Finset.prod_insert ha, Finset.prod_insert ha, Finset.forall_mem_insert, ← ih]
exact mul_eq_mul_iff_eq_and_eq (H a (s.mem_insert_self a)) (Finset.prod_le_prod' fun i ↦ H i ∘ Finset.mem_insert_of_mem)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f✝ g✝ : ι → M
s t : Finset ι
f g : ι → M
h : ∀ (i : ι), i ∈ s → f i ≤ g i
⊢ ∏ i in s, f i = ∏ i in s, g i ↔ ∀ (i : ι), i ∈ s → f i = g i
[PROOFSTEP]
revert h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f✝ g✝ : ι → M
s t : Finset ι
f g : ι → M
⊢ (∀ (i : ι), i ∈ s → f i ≤ g i) → (∏ i in s, f i = ∏ i in s, g i ↔ ∀ (i : ι), i ∈ s → f i = g i)
[PROOFSTEP]
refine
  Finset.induction_on s (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.not_mem_empty _ h), fun _ ↦ rfl⟩) fun a s ha ih H ↦ ?_
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f✝ g✝ : ι → M
s✝ t : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → f i ≤ g i) → (∏ i in s, f i = ∏ i in s, g i ↔ ∀ (i : ι), i ∈ s → f i = g i)
H : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ ∏ i in insert a s, f i = ∏ i in insert a s, g i ↔ ∀ (i : ι), i ∈ insert a s → f i = g i
[PROOFSTEP]
specialize ih fun i ↦ H i ∘ Finset.mem_insert_of_mem
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f✝ g✝ : ι → M
s✝ t : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : ¬a ∈ s
H : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
ih : ∏ i in s, f i = ∏ i in s, g i ↔ ∀ (i : ι), i ∈ s → f i = g i
⊢ ∏ i in insert a s, f i = ∏ i in insert a s, g i ↔ ∀ (i : ι), i ∈ insert a s → f i = g i
[PROOFSTEP]
rw [Finset.prod_insert ha, Finset.prod_insert ha, Finset.forall_mem_insert, ← ih]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCancelCommMonoid M
f✝ g✝ : ι → M
s✝ t : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : ¬a ∈ s
H : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
ih : ∏ i in s, f i = ∏ i in s, g i ↔ ∀ (i : ι), i ∈ s → f i = g i
⊢ f a * ∏ x in s, f x = g a * ∏ x in s, g x ↔ f a = g a ∧ ∏ i in s, f i = ∏ i in s, g i
[PROOFSTEP]
exact mul_eq_mul_iff_eq_and_eq (H a (s.mem_insert_self a)) (Finset.prod_le_prod' fun i ↦ H i ∘ Finset.mem_insert_of_mem)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : LinearOrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hlt : ∏ i in s, f i < ∏ i in s, g i
⊢ ∃ i, i ∈ s ∧ f i < g i
[PROOFSTEP]
contrapose! Hlt with Hle
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : LinearOrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
Hle : ∀ (i : ι), i ∈ s → g i ≤ f i
⊢ ∏ i in s, g i ≤ ∏ i in s, f i
[PROOFSTEP]
exact prod_le_prod' Hle
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : LinearOrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
hs : Finset.Nonempty s
Hle : ∏ i in s, f i ≤ ∏ i in s, g i
⊢ ∃ i, i ∈ s ∧ f i ≤ g i
[PROOFSTEP]
contrapose! Hle with Hlt
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : LinearOrderedCancelCommMonoid M
f g : ι → M
s t : Finset ι
hs : Finset.Nonempty s
Hlt : ∀ (i : ι), i ∈ s → g i < f i
⊢ ∏ i in s, g i < ∏ i in s, f i
[PROOFSTEP]
exact prod_lt_prod_of_nonempty' hs Hlt
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : LinearOrderedCancelCommMonoid M
f✝ g : ι → M
s t : Finset ι
f : ι → M
h₁ : ∏ i in s, f i = 1
h₂ : ∃ i, i ∈ s ∧ f i ≠ 1
⊢ ∃ i, i ∈ s ∧ 1 < f i
[PROOFSTEP]
contrapose! h₁
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : LinearOrderedCancelCommMonoid M
f✝ g : ι → M
s t : Finset ι
f : ι → M
h₂ : ∃ i, i ∈ s ∧ f i ≠ 1
h₁ : ∀ (i : ι), i ∈ s → f i ≤ 1
⊢ ∏ i in s, f i ≠ 1
[PROOFSTEP]
obtain ⟨i, m, i_ne⟩ : ∃ i ∈ s, f i ≠ 1 := h₂
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : LinearOrderedCancelCommMonoid M
f✝ g : ι → M
s t : Finset ι
f : ι → M
h₁ : ∀ (i : ι), i ∈ s → f i ≤ 1
i : ι
m : i ∈ s
i_ne : f i ≠ 1
⊢ ∏ i in s, f i ≠ 1
[PROOFSTEP]
apply ne_of_lt
[GOAL]
case intro.intro.h
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : LinearOrderedCancelCommMonoid M
f✝ g : ι → M
s t : Finset ι
f : ι → M
h₁ : ∀ (i : ι), i ∈ s → f i ≤ 1
i : ι
m : i ∈ s
i_ne : f i ≠ 1
⊢ ∏ i in s, f i < 1
[PROOFSTEP]
calc
  ∏ j in s, f j < ∏ j in s, 1 := prod_lt_prod' h₁ ⟨i, m, (h₁ i m).lt_of_ne i_ne⟩
  _ = 1 := prod_const_one
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f g : ι → R
s t : Finset ι
h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ s → f i ≤ g i
⊢ ∏ i in s, f i ≤ ∏ i in s, g i
[PROOFSTEP]
induction' s using Finset.induction with a s has ih h
[GOAL]
case empty
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f g : ι → R
s t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s → f i ≤ g i
h0 : ∀ (i : ι), i ∈ ∅ → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ ∅ → f i ≤ g i
⊢ ∏ i in ∅, f i ≤ ∏ i in ∅, g i
[PROOFSTEP]
simp
[GOAL]
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ ∏ i in insert a s, f i ≤ ∏ i in insert a s, g i
[PROOFSTEP]
simp only [prod_insert has]
[GOAL]
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ f a * ∏ i in s, f i ≤ g a * ∏ i in s, g i
[PROOFSTEP]
apply mul_le_mul
[GOAL]
case insert.h₁
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ f a ≤ g a
[PROOFSTEP]
exact h1 a (mem_insert_self a s)
[GOAL]
case insert.h₂
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ ∏ i in s, f i ≤ ∏ i in s, g i
[PROOFSTEP]
refine ih (fun x H ↦ h0 _ ?_) (fun x H ↦ h1 _ ?_)
[GOAL]
case insert.h₂.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
x : ι
H : x ∈ s
⊢ x ∈ insert a s
[PROOFSTEP]
exact mem_insert_of_mem H
[GOAL]
case insert.h₂.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
x : ι
H : x ∈ s
⊢ x ∈ insert a s
[PROOFSTEP]
exact mem_insert_of_mem H
[GOAL]
case insert.c0
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ 0 ≤ ∏ i in s, f i
[PROOFSTEP]
apply prod_nonneg fun x H ↦ h0 x (mem_insert_of_mem H)
[GOAL]
case insert.b0
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f g : ι → R
s✝ t : Finset ι
h0✝ : ∀ (i : ι), i ∈ s✝ → 0 ≤ f i
h1✝ : ∀ (i : ι), i ∈ s✝ → f i ≤ g i
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
h0 : ∀ (i : ι), i ∈ insert a s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ insert a s → f i ≤ g i
⊢ 0 ≤ g a
[PROOFSTEP]
apply le_trans (h0 a (mem_insert_self a s)) (h1 a (mem_insert_self a s))
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f g : ι → R
s t : Finset ι
h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ s → f i ≤ 1
⊢ ∏ i in s, f i ≤ 1
[PROOFSTEP]
convert ← prod_le_prod h0 h1
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f g : ι → R
s t : Finset ι
h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i
h1 : ∀ (i : ι), i ∈ s → f i ≤ 1
⊢ ∏ i in s, 1 = 1
[PROOFSTEP]
exact Finset.prod_const_one
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ ∏ i in s, g i + ∏ i in s, h i ≤ ∏ i in s, f i
[PROOFSTEP]
simp_rw [prod_eq_mul_prod_diff_singleton hi]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ g i * ∏ i in s \ {i}, g i + h i * ∏ i in s \ {i}, h i ≤ f i * ∏ i in s \ {i}, f i
[PROOFSTEP]
refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)
[GOAL]
case refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ g i * ∏ i in s \ {i}, g i + h i * ∏ i in s \ {i}, h i ≤ (g i + h i) * ∏ i in s \ {i}, f i
[PROOFSTEP]
rw [right_distrib]
[GOAL]
case refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ g i * ∏ i in s \ {i}, g i + h i * ∏ i in s \ {i}, h i ≤ g i * ∏ i in s \ {i}, f i + h i * ∏ i in s \ {i}, f i
[PROOFSTEP]
refine add_le_add ?_ ?_
[GOAL]
case refine_1.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ g i * ∏ i in s \ {i}, g i ≤ g i * ∏ i in s \ {i}, f i
[PROOFSTEP]
refine mul_le_mul_of_nonneg_left ?_ ?_
[GOAL]
case refine_1.refine_1.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ ∏ i in s \ {i}, g i ≤ ∏ i in s \ {i}, f i
[PROOFSTEP]
refine prod_le_prod ?_ ?_
[GOAL]
case refine_1.refine_1.refine_1.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ ∀ (i_1 : ι), i_1 ∈ s \ {i} → 0 ≤ g i_1
[PROOFSTEP]
simp (config := { contextual := true }) [*]
[GOAL]
case refine_1.refine_1.refine_1.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ ∀ (i_1 : ι), i_1 ∈ s \ {i} → g i_1 ≤ f i_1
[PROOFSTEP]
simp (config := { contextual := true }) [*]
[GOAL]
case refine_1.refine_1.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ 0 ≤ g i
[PROOFSTEP]
try apply_assumption
[GOAL]
case refine_1.refine_1.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ 0 ≤ g i
[PROOFSTEP]
apply_assumption
[GOAL]
case refine_1.refine_1.refine_2.a
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ i ∈ s
[PROOFSTEP]
try assumption
[GOAL]
case refine_1.refine_1.refine_2.a
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ i ∈ s
[PROOFSTEP]
assumption
[GOAL]
case refine_1.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ h i * ∏ i in s \ {i}, h i ≤ h i * ∏ i in s \ {i}, f i
[PROOFSTEP]
refine mul_le_mul_of_nonneg_left ?_ ?_
[GOAL]
case refine_1.refine_2.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ ∏ i in s \ {i}, h i ≤ ∏ i in s \ {i}, f i
[PROOFSTEP]
refine prod_le_prod ?_ ?_
[GOAL]
case refine_1.refine_2.refine_1.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ ∀ (i_1 : ι), i_1 ∈ s \ {i} → 0 ≤ h i_1
[PROOFSTEP]
simp (config := { contextual := true }) [*]
[GOAL]
case refine_1.refine_2.refine_1.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ ∀ (i_1 : ι), i_1 ∈ s \ {i} → h i_1 ≤ f i_1
[PROOFSTEP]
simp (config := { contextual := true }) [*]
[GOAL]
case refine_1.refine_2.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ 0 ≤ h i
[PROOFSTEP]
try apply_assumption
[GOAL]
case refine_1.refine_2.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ 0 ≤ h i
[PROOFSTEP]
apply_assumption
[GOAL]
case refine_1.refine_2.refine_2.a
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ i ∈ s
[PROOFSTEP]
try assumption
[GOAL]
case refine_1.refine_2.refine_2.a
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ i ∈ s
[PROOFSTEP]
assumption
[GOAL]
case refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ 0 ≤ ∏ i in s \ {i}, f i
[PROOFSTEP]
apply prod_nonneg
[GOAL]
case refine_2.h0
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ ∀ (i_1 : ι), i_1 ∈ s \ {i} → 0 ≤ f i_1
[PROOFSTEP]
simp only [and_imp, mem_sdiff, mem_singleton]
[GOAL]
case refine_2.h0
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
⊢ ∀ (i_1 : ι), i_1 ∈ s → ¬i_1 = i → 0 ≤ f i_1
[PROOFSTEP]
intro j h1j h2j
[GOAL]
case refine_2.h0
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : OrderedCommSemiring R
f✝ g✝ : ι → R
s t : Finset ι
i : ι
f g h : ι → R
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
hh : ∀ (i : ι), i ∈ s → 0 ≤ h i
j : ι
h1j : j ∈ s
h2j : ¬j = i
⊢ 0 ≤ f j
[PROOFSTEP]
exact le_trans (hg j h1j) (hgf j h1j h2j)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
⊢ ∏ i in s, g i + ∏ i in s, h i ≤ ∏ i in s, f i
[PROOFSTEP]
classical
simp_rw [prod_eq_mul_prod_diff_singleton hi]
refine' le_trans _ (mul_le_mul_right' h2i _)
rw [right_distrib]
apply add_le_add <;> apply mul_le_mul_left' <;> apply prod_le_prod' <;>
        simp only [and_imp, mem_sdiff, mem_singleton] <;>
      intros <;>
    apply_assumption <;>
  assumption
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
⊢ ∏ i in s, g i + ∏ i in s, h i ≤ ∏ i in s, f i
[PROOFSTEP]
simp_rw [prod_eq_mul_prod_diff_singleton hi]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
⊢ g i * ∏ i in s \ {i}, g i + h i * ∏ i in s \ {i}, h i ≤ f i * ∏ i in s \ {i}, f i
[PROOFSTEP]
refine' le_trans _ (mul_le_mul_right' h2i _)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
⊢ g i * ∏ i in s \ {i}, g i + h i * ∏ i in s \ {i}, h i ≤ (g i + h i) * ∏ i in s \ {i}, f i
[PROOFSTEP]
rw [right_distrib]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
⊢ g i * ∏ i in s \ {i}, g i + h i * ∏ i in s \ {i}, h i ≤ g i * ∏ i in s \ {i}, f i + h i * ∏ i in s \ {i}, f i
[PROOFSTEP]
apply add_le_add
[GOAL]
case h₁
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
⊢ g i * ∏ i in s \ {i}, g i ≤ g i * ∏ i in s \ {i}, f i
[PROOFSTEP]
apply mul_le_mul_left'
[GOAL]
case h₂
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
⊢ h i * ∏ i in s \ {i}, h i ≤ h i * ∏ i in s \ {i}, f i
[PROOFSTEP]
apply mul_le_mul_left'
[GOAL]
case h₁.bc
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
⊢ ∏ i in s \ {i}, g i ≤ ∏ i in s \ {i}, f i
[PROOFSTEP]
apply prod_le_prod'
[GOAL]
case h₂.bc
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
⊢ ∏ i in s \ {i}, h i ≤ ∏ i in s \ {i}, f i
[PROOFSTEP]
apply prod_le_prod'
[GOAL]
case h₁.bc.h
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
⊢ ∀ (i_1 : ι), i_1 ∈ s \ {i} → g i_1 ≤ f i_1
[PROOFSTEP]
simp only [and_imp, mem_sdiff, mem_singleton]
[GOAL]
case h₂.bc.h
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
⊢ ∀ (i_1 : ι), i_1 ∈ s \ {i} → h i_1 ≤ f i_1
[PROOFSTEP]
simp only [and_imp, mem_sdiff, mem_singleton]
[GOAL]
case h₁.bc.h
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
⊢ ∀ (i_1 : ι), i_1 ∈ s → ¬i_1 = i → g i_1 ≤ f i_1
[PROOFSTEP]
intros
[GOAL]
case h₂.bc.h
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
⊢ ∀ (i_1 : ι), i_1 ∈ s → ¬i_1 = i → h i_1 ≤ f i_1
[PROOFSTEP]
intros
[GOAL]
case h₁.bc.h
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
i✝ : ι
a✝¹ : i✝ ∈ s
a✝ : ¬i✝ = i
⊢ g i✝ ≤ f i✝
[PROOFSTEP]
apply_assumption
[GOAL]
case h₂.bc.h
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
i✝ : ι
a✝¹ : i✝ ∈ s
a✝ : ¬i✝ = i
⊢ h i✝ ≤ f i✝
[PROOFSTEP]
apply_assumption
[GOAL]
case h₁.bc.h.a
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
i✝ : ι
a✝¹ : i✝ ∈ s
a✝ : ¬i✝ = i
⊢ i✝ ∈ s
[PROOFSTEP]
assumption
[GOAL]
case h₁.bc.h.a
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
i✝ : ι
a✝¹ : i✝ ∈ s
a✝ : ¬i✝ = i
⊢ i✝ ≠ i
[PROOFSTEP]
assumption
[GOAL]
case h₂.bc.h.a
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
i✝ : ι
a✝¹ : i✝ ∈ s
a✝ : ¬i✝ = i
⊢ i✝ ∈ s
[PROOFSTEP]
assumption
[GOAL]
case h₂.bc.h.a
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : CanonicallyOrderedCommSemiring R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ (j : ι), j ∈ s → j ≠ i → g j ≤ f j
hhf : ∀ (j : ι), j ∈ s → j ≠ i → h j ≤ f j
i✝ : ι
a✝¹ : i✝ ∈ s
a✝ : ¬i✝ = i
⊢ i✝ ≠ i
[PROOFSTEP]
assumption
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → WithTop M
⊢ ∑ i in s, f i = ⊤ ↔ ∃ i, i ∈ s ∧ f i = ⊤
[PROOFSTEP]
induction s using Finset.cons_induction
[GOAL]
case empty
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : AddCommMonoid M
f : ι → WithTop M
⊢ ∑ i in ∅, f i = ⊤ ↔ ∃ i, i ∈ ∅ ∧ f i = ⊤
[PROOFSTEP]
simp [*]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝ : AddCommMonoid M
f : ι → WithTop M
a✝¹ : ι
s✝ : Finset ι
h✝ : ¬a✝¹ ∈ s✝
a✝ : ∑ i in s✝, f i = ⊤ ↔ ∃ i, i ∈ s✝ ∧ f i = ⊤
⊢ ∑ i in cons a✝¹ s✝ h✝, f i = ⊤ ↔ ∃ i, i ∈ cons a✝¹ s✝ h✝ ∧ f i = ⊤
[PROOFSTEP]
simp [*]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
G : Type u_6
k : Type u_7
R : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : LT M
s : Finset ι
f : ι → WithTop M
⊢ ∑ i in s, f i < ⊤ ↔ ∀ (i : ι), i ∈ s → f i < ⊤
[PROOFSTEP]
simp only [WithTop.lt_top_iff_ne_top, ne_eq, sum_eq_top_iff, not_exists, not_and]


[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
⊢ ∀ (s : Set (Tropical R)), ¬BddAbove s → sSup s = sSup Set.univ
[PROOFSTEP]
intro s hs
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
hs : ¬BddAbove s
⊢ sSup s = sSup Set.univ
[PROOFSTEP]
have : Set.range untrop = (Set.univ : Set R) := Equiv.range_eq_univ tropEquiv.symm
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
hs : ¬BddAbove s
this : Set.range untrop = Set.univ
⊢ sSup s = sSup Set.univ
[PROOFSTEP]
simp [sSup, this]
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
hs : ¬BddAbove s
this : Set.range untrop = Set.univ
⊢ sSup (untrop '' s) = sSup Set.univ
[PROOFSTEP]
apply csSup_of_not_bddAbove
[GOAL]
case hs
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
hs : ¬BddAbove s
this : Set.range untrop = Set.univ
⊢ ¬BddAbove (untrop '' s)
[PROOFSTEP]
contrapose! hs
[GOAL]
case hs
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
this : Set.range untrop = Set.univ
hs : BddAbove (untrop '' s)
⊢ BddAbove s
[PROOFSTEP]
change BddAbove (tropOrderIso.symm '' s) at hs
[GOAL]
case hs
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
this : Set.range untrop = Set.univ
hs : BddAbove (↑(OrderIso.symm tropOrderIso) '' s)
⊢ BddAbove s
[PROOFSTEP]
exact tropOrderIso.symm.bddAbove_image.1 hs
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
⊢ ∀ (s : Set (Tropical R)), ¬BddBelow s → sInf s = sInf Set.univ
[PROOFSTEP]
intro s hs
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
hs : ¬BddBelow s
⊢ sInf s = sInf Set.univ
[PROOFSTEP]
have : Set.range untrop = (Set.univ : Set R) := Equiv.range_eq_univ tropEquiv.symm
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
hs : ¬BddBelow s
this : Set.range untrop = Set.univ
⊢ sInf s = sInf Set.univ
[PROOFSTEP]
simp [sInf, this]
[GOAL]
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
hs : ¬BddBelow s
this : Set.range untrop = Set.univ
⊢ sInf (untrop '' s) = sInf Set.univ
[PROOFSTEP]
apply csInf_of_not_bddBelow
[GOAL]
case hs
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
hs : ¬BddBelow s
this : Set.range untrop = Set.univ
⊢ ¬BddBelow (untrop '' s)
[PROOFSTEP]
contrapose! hs
[GOAL]
case hs
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
this : Set.range untrop = Set.univ
hs : BddBelow (untrop '' s)
⊢ BddBelow s
[PROOFSTEP]
change BddBelow (tropOrderIso.symm '' s) at hs
[GOAL]
case hs
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
src✝¹ : ConditionallyCompleteLattice (Tropical R) := instConditionallyCompleteLatticeTropical
src✝ : LinearOrder (Tropical R) := instLinearOrderTropical
s : Set (Tropical R)
this : Set.range untrop = Set.univ
hs : BddBelow (↑(OrderIso.symm tropOrderIso) '' s)
⊢ BddBelow s
[PROOFSTEP]
exact tropOrderIso.symm.bddBelow_image.1 hs


[GOAL]
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
L M N K : ModuleCat R
f : L ⟶ M
g : M ⟶ N
w✝ : f ≫ g = 0
h k : _root_.homology f g w✝ ⟶ K
w :
  ∀ (x : { x // x ∈ LinearMap.ker g }),
    ↑h (↑(cokernel.π (imageToKernel f g w✝)) (↑toKernelSubobject x)) =
      ↑k (↑(cokernel.π (imageToKernel f g w✝)) (↑toKernelSubobject x))
⊢ h = k
[PROOFSTEP]
refine'
  cokernel_funext fun n =>
    _
      -- porting note: as `equiv_rw` was not ported, it was replaced by `Equiv.surjective`
        -- Gosh it would be nice if `equiv_rw` could directly use an isomorphism, or an enriched `≃`.
[GOAL]
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
L M N K : ModuleCat R
f : L ⟶ M
g : M ⟶ N
w✝ : f ≫ g = 0
h k : _root_.homology f g w✝ ⟶ K
w :
  ∀ (x : { x // x ∈ LinearMap.ker g }),
    ↑h (↑(cokernel.π (imageToKernel f g w✝)) (↑toKernelSubobject x)) =
      ↑k (↑(cokernel.π (imageToKernel f g w✝)) (↑toKernelSubobject x))
n : (CategoryTheory.forget (ModuleCat R)).obj (Subobject.underlying.obj (kernelSubobject g))
⊢ ↑h (↑(cokernel.π (imageToKernel f g w✝)) n) = ↑k (↑(cokernel.π (imageToKernel f g w✝)) n)
[PROOFSTEP]
obtain ⟨n, rfl⟩ := (kernelSubobjectIso g ≪≫ ModuleCat.kernelIsoKer g).toLinearEquiv.toEquiv.symm.surjective n
[GOAL]
case intro
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
L M N K : ModuleCat R
f : L ⟶ M
g : M ⟶ N
w✝ : f ≫ g = 0
h k : _root_.homology f g w✝ ⟶ K
w :
  ∀ (x : { x // x ∈ LinearMap.ker g }),
    ↑h (↑(cokernel.π (imageToKernel f g w✝)) (↑toKernelSubobject x)) =
      ↑k (↑(cokernel.π (imageToKernel f g w✝)) (↑toKernelSubobject x))
n : ↑(of R { x // x ∈ LinearMap.ker g })
⊢ ↑h
      (↑(cokernel.π (imageToKernel f g w✝))
        (↑(LinearEquiv.toEquiv (Iso.toLinearEquiv (kernelSubobjectIso g ≪≫ kernelIsoKer g))).symm n)) =
    ↑k
      (↑(cokernel.π (imageToKernel f g w✝))
        (↑(LinearEquiv.toEquiv (Iso.toLinearEquiv (kernelSubobjectIso g ≪≫ kernelIsoKer g))).symm n))
[PROOFSTEP]
exact w n
[GOAL]
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C✝ D C : HomologicalComplex (ModuleCat R) c
i : ι
x y : ↑(Subobject.underlying.obj (cycles C i))
w : ↑(Subobject.arrow (cycles C i)) x = ↑(Subobject.arrow (cycles C i)) y
⊢ x = y
[PROOFSTEP]
apply_fun (C.cycles i).arrow using (ModuleCat.mono_iff_injective _).mp (cycles C i).arrow_mono
[GOAL]
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C✝ D C : HomologicalComplex (ModuleCat R) c
i : ι
x y : ↑(Subobject.underlying.obj (cycles C i))
w : ↑(Subobject.arrow (cycles C i)) x = ↑(Subobject.arrow (cycles C i)) y
⊢ ↑(Subobject.arrow (cycles C i)) x = ↑(Subobject.arrow (cycles C i)) y
[PROOFSTEP]
exact w
[GOAL]
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f : C ⟶ D
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑(Hom.f f i) ↑x ∈ LinearMap.ker (dFrom D i)
[PROOFSTEP]
rw [LinearMap.mem_ker, Hom.comm_from_apply, x.2, map_zero]
[GOAL]
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f : C ⟶ D
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑(cyclesMap f i) (toCycles x) =
    toCycles { val := ↑(Hom.f f i) ↑x, property := (_ : ↑(Hom.f f i) ↑x ∈ LinearMap.ker (dFrom D i)) }
[PROOFSTEP]
ext
[GOAL]
case w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f : C ⟶ D
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑(Subobject.arrow (cycles D i)) (↑(cyclesMap f i) (toCycles x)) =
    ↑(Subobject.arrow (cycles D i))
      (toCycles { val := ↑(Hom.f f i) ↑x, property := (_ : ↑(Hom.f f i) ↑x ∈ LinearMap.ker (dFrom D i)) })
[PROOFSTEP]
rw [cyclesMap_arrow_apply, toKernelSubobject_arrow, toKernelSubobject_arrow]
[GOAL]
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
⊢ (homologyFunctor (ModuleCat R) c i).map f = (homologyFunctor (ModuleCat R) c i).map g
[PROOFSTEP]
apply homology_ext
[GOAL]
case w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
⊢ ∀ (x : { x // x ∈ LinearMap.ker (dFrom C i) }),
    ↑((homologyFunctor (ModuleCat R) c i).map f)
        (↑(cokernel.π (imageToKernel (dTo C i) (dFrom C i) (_ : dTo C i ≫ dFrom C i = 0))) (↑toKernelSubobject x)) =
      ↑((homologyFunctor (ModuleCat R) c i).map g)
        (↑(cokernel.π (imageToKernel (dTo C i) (dFrom C i) (_ : dTo C i ≫ dFrom C i = 0))) (↑toKernelSubobject x))
[PROOFSTEP]
intro x
[GOAL]
case w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑((homologyFunctor (ModuleCat R) c i).map f)
      (↑(cokernel.π (imageToKernel (dTo C i) (dFrom C i) (_ : dTo C i ≫ dFrom C i = 0))) (↑toKernelSubobject x)) =
    ↑((homologyFunctor (ModuleCat R) c i).map g)
      (↑(cokernel.π (imageToKernel (dTo C i) (dFrom C i) (_ : dTo C i ≫ dFrom C i = 0))) (↑toKernelSubobject x))
[PROOFSTEP]
simp only [homologyFunctor_map]
[GOAL]
case w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑(homology.map (_ : dTo C i ≫ dFrom C i = 0) (_ : dTo D i ≫ dFrom D i = 0) (Hom.sqTo f i) (Hom.sqFrom f i)
          (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right))
      (↑(cokernel.π (imageToKernel (dTo C i) (dFrom C i) (_ : dTo C i ≫ dFrom C i = 0))) (↑toKernelSubobject x)) =
    ↑(homology.map (_ : dTo C i ≫ dFrom C i = 0) (_ : dTo D i ≫ dFrom D i = 0) (Hom.sqTo g i) (Hom.sqFrom g i)
          (_ : (Hom.sqTo g i).right = (Hom.sqTo g i).right))
      (↑(cokernel.π (imageToKernel (dTo C i) (dFrom C i) (_ : dTo C i ≫ dFrom C i = 0))) (↑toKernelSubobject x))
[PROOFSTEP]
erw [homology.π_map_apply, homology.π_map_apply]
  -- To check that two elements are equal mod boundaries, it suffices to exhibit a boundary:
[GOAL]
case w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑(homology.π (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0))
      (↑(kernelSubobjectMap (Hom.sqFrom f i)) (↑toKernelSubobject x)) =
    ↑(homology.π (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0))
      (↑(kernelSubobjectMap (Hom.sqFrom g i)) (↑toKernelSubobject x))
[PROOFSTEP]
refine'
  cokernel_π_imageSubobject_ext _ _ ((toPrev i h.hom) x.1)
    _
      -- Moreover, to check that two cycles are equal, it suffices to check their underlying elements:
[GOAL]
case w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑(kernelSubobjectMap (Hom.sqFrom f i)) (↑toKernelSubobject x) =
    ↑(kernelSubobjectMap (Hom.sqFrom g i)) (↑toKernelSubobject x) +
      ↑(imageToKernel (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0))
        (↑(factorThruImageSubobject (dTo D i)) (↑(↑(toPrev i) h.hom) ↑x))
[PROOFSTEP]
ext
[GOAL]
case w.w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑(Subobject.arrow (cycles D i)) (↑(kernelSubobjectMap (Hom.sqFrom f i)) (↑toKernelSubobject x)) =
    ↑(Subobject.arrow (cycles D i))
      (↑(kernelSubobjectMap (Hom.sqFrom g i)) (↑toKernelSubobject x) +
        ↑(imageToKernel (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0))
          (↑(factorThruImageSubobject (dTo D i)) (↑(↑(toPrev i) h.hom) ↑x)))
[PROOFSTEP]
erw [map_add, CategoryTheory.Limits.kernelSubobjectMap_arrow_apply,
  CategoryTheory.Limits.kernelSubobjectMap_arrow_apply, ModuleCat.toKernelSubobject_arrow, imageToKernel_arrow_apply,
  imageSubobject_arrow_comp_apply]
[GOAL]
case w.w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑(Hom.sqFrom f i).left ↑x = ↑(Hom.sqFrom g i).left ↑x + ↑(dTo D i) (↑(↑(toPrev i) h.hom) ↑x)
[PROOFSTEP]
rw [Hom.sqFrom_left, Hom.sqFrom_left, h.comm i, LinearMap.add_apply, LinearMap.add_apply, prevD_eq_toPrev_dTo,
  dNext_eq_dFrom_fromNext, comp_apply, comp_apply, x.2, map_zero]
[GOAL]
case w.w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ 0 + ↑(dTo D i) (↑(↑(toPrev i) h.hom) ↑x) + ↑(Hom.f g i) ↑x = ↑(Hom.f g i) ↑x + ↑(dTo D i) (↑(↑(toPrev i) h.hom) ↑x)
[PROOFSTEP]
dsimp
[GOAL]
case w.w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ 0 + ↑(dTo D i) (↑(↑(toPrev i) h.hom) ↑x) + ↑(Hom.f g i) ↑x = ↑(Hom.f g i) ↑x + ↑(dTo D i) (↑(↑(toPrev i) h.hom) ↑x)
[PROOFSTEP]
abel
[GOAL]
case w.w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ 0 + ↑(dTo D i) (↑(↑(toPrev i) h.hom) ↑x) + ↑(Hom.f g i) ↑x = ↑(Hom.f g i) ↑x + ↑(dTo D i) (↑(↑(toPrev i) h.hom) ↑x)
[PROOFSTEP]
abel