case refine'_1
𝕜 : Type u_1
E : Type ?u.291143
F : Type ?u.291146
β : Type ?u.291149
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x : ι
⊢ 0 ≤ (a • f + b • g) x

case refine'_2
𝕜 : Type u_1
E : Type ?u.291143
F : Type ?u.291146
β : Type ?u.291149
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x : ι, (a • f + b • g) x = 1
𝕜 : Type u_1
E : Type ?u.291143
F : Type ?u.291146
β : Type ?u.291149
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
⊢ Convex 𝕜 (stdSimplex 𝕜 ι)
refine' fun f hf g hg a b ha hb hab => ⟨fun x => _, _⟩
no goals
case refine'_1
𝕜 : Type u_1
E : Type ?u.291143
F : Type ?u.291146
β : Type ?u.291149
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x : ι
⊢ 0 ≤ (a • f + b • g) x
apply_rules [add_nonneg, mul_nonneg, hf.1, hg.1]
case refine'_2
𝕜 : Type u_1
E : Type ?u.291143
F : Type ?u.291146
β : Type ?u.291149
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x : ι, (a • f) x + ∑ x : ι, (b • g) x = 1
case refine'_2
𝕜 : Type u_1
E : Type ?u.291143
F : Type ?u.291146
β : Type ?u.291149
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x : ι, (a • f + b • g) x = 1
erw [Finset.sum_add_distrib]
case refine'_2
𝕜 : Type u_1
E : Type ?u.291143
F : Type ?u.291146
β : Type ?u.291149
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x : ι, a • f x + ∑ x : ι, b • g x = 1
case refine'_2
𝕜 : Type u_1
E : Type ?u.291143
F : Type ?u.291146
β : Type ?u.291149
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x : ι, (a • f) x + ∑ x : ι, (b • g) x = 1
simp only [Pi.smul_apply]
case refine'_2
𝕜 : Type u_1
E : Type ?u.291143
F : Type ?u.291146
β : Type ?u.291149
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a + b = 1
case refine'_2
𝕜 : Type u_1
E : Type ?u.291143
F : Type ?u.291146
β : Type ?u.291149
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x : ι, a • f x + ∑ x : ι, b • g x = 1
rw [← Finset.smul_sum, ← Finset.smul_sum, hf.2, hg.2, smul_eq_mul,
  smul_eq_mul, mul_one, mul_one]
no goals
case refine'_2
𝕜 : Type u_1
E : Type ?u.291143
F : Type ?u.291146
β : Type ?u.291149
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a + b = 1
exact hab