Theorem: Finset.one_add_prod_le_prod_one_add (CvxLean/Lib/Math/Subadditivity.lean)

State before:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ 1 + ∏ i : n, f i ≤ ∏ i : n, (1 + f i)
Tactic:
classical
calc 1 + (∏ i, f i)
  = (∏ _a : n, 1 : ℝ) * ∏ a : n in univ \ univ, f a
    + (∏ a : n in ∅, 1) * ∏ a : n in univ \ ∅, f a := by
  { simp }
_ = ∑ x in {univ, ∅}, (∏ _a : n in x, 1 : ℝ) * ∏ a : n in univ \ x, f a := by
  { rw [Finset.sum_pair]; simp; exact Finset.univ_nonempty.ne_empty }
_ ≤ ∑ t : Finset n, (∏ _a : n in t, 1 : ℝ) * ∏ a : n in univ \ t, f a := by
  { convert @Finset.sum_le_univ_sum_of_nonneg (Finset n) ℝ _ _ _ _ _
    simp [hf, prod_nonneg] }
_ = ∏ i, (1 + f i) := by
  { rw [prod_add, powerset_univ] }
State after:
no goals

State before:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ 1 + ∏ i : n, f i ≤ ∏ i : n, (1 + f i)
Tactic:
calc 1 + (∏ i, f i)
  = (∏ _a : n, 1 : ℝ) * ∏ a : n in univ \ univ, f a
    + (∏ a : n in ∅, 1) * ∏ a : n in univ \ ∅, f a := by
  { simp }
_ = ∑ x in {univ, ∅}, (∏ _a : n in x, 1 : ℝ) * ∏ a : n in univ \ x, f a := by
  { rw [Finset.sum_pair]; simp; exact Finset.univ_nonempty.ne_empty }
_ ≤ ∑ t : Finset n, (∏ _a : n in t, 1 : ℝ) * ∏ a : n in univ \ t, f a := by
  { convert @Finset.sum_le_univ_sum_of_nonneg (Finset n) ℝ _ _ _ _ _
    simp [hf, prod_nonneg] }
_ = ∏ i, (1 + f i) := by
  { rw [prod_add, powerset_univ] }
State after:
no goals

State before:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ 1 + ∏ i : n, f i = (∏ _a : n, 1) * ∏ a ∈ univ \ univ, f a + (∏ a ∈ ∅, 1) * ∏ a ∈ univ \ ∅, f a
Tactic:
simp
State after:
no goals

State before:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ (∏ _a : n, 1) * ∏ a ∈ univ \ univ, f a + (∏ a ∈ ∅, 1) * ∏ a ∈ univ \ ∅, f a =
    ∑ x ∈ {univ, ∅}, (∏ _a ∈ x, 1) * ∏ a ∈ univ \ x, f a
Tactic:
rw [Finset.sum_pair]
State after:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ univ ≠ ∅

State before:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ univ ≠ ∅
Tactic:
simp
State after:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ ¬univ = ∅

State before:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ ¬univ = ∅
Tactic:
exact Finset.univ_nonempty.ne_empty
State after:
no goals

State before:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ ∑ x ∈ {univ, ∅}, (∏ _a ∈ x, 1) * ∏ a ∈ univ \ x, f a ≤ ∑ t : Finset n, (∏ _a ∈ t, 1) * ∏ a ∈ univ \ t, f a
Tactic:
convert @Finset.sum_le_univ_sum_of_nonneg (Finset n) ℝ _ _ _ _ _
State after:
case convert_3
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ ∀ (x : Finset n), 0 ≤ (∏ _a ∈ x, 1) * ∏ a ∈ univ \ x, f a

State before:
case convert_3
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ ∀ (x : Finset n), 0 ≤ (∏ _a ∈ x, 1) * ∏ a ∈ univ \ x, f a
Tactic:
simp [hf, prod_nonneg]
State after:
no goals

State before:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ ∑ t : Finset n, (∏ _a ∈ t, 1) * ∏ a ∈ univ \ t, f a = ∏ i : n, (1 + f i)
Tactic:
rw [prod_add, powerset_univ]
State after:
no goals