Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: case neg.mp
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
h : P → R → V := ⋯
h_rhs :
  ∑ a ∈ (∑ d ∈ f.weights.support, f.weights d • d.weights).support,
      h a ((∑ d ∈ f.weights.support, f.weights d • d.weights) a) =
    ∑ d ∈ f.weights.support, ∑ a ∈ (f.weights d • d.weights).support, h a ((f.weights d • d.weights) a)
d : StdSimplex R P
hd : ¬f.weights d = 0
p : P
⊢ ¬d.weights p = 0 → ¬(f.weights d • d.weights) p = 0

pp: case neg.mpr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
h : P → R → V := ⋯
h_rhs :
  ∑ a ∈ (∑ d ∈ f.weights.support, f.weights d • d.weights).support,
      h a ((∑ d ∈ f.weights.support, f.weights d • d.weights) a) =
    ∑ d ∈ f.weights.support, ∑ a ∈ (f.weights d • d.weights).support, h a ((f.weights d • d.weights) a)
d : StdSimplex R P
hd : ¬f.weights d = 0
p : P
⊢ ¬(f.weights d • d.weights) p = 0 → ¬d.weights p = 0

Tactic:
· intro hp
      exact (mul_pos ((f.nonneg d).lt_of_ne' hd) ((d.nonneg p).lt_of_ne' hp)).ne'

Goal state after:
case neg.mpr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
h : P → R → V := ⋯
h_rhs :
  ∑ a ∈ (∑ d ∈ f.weights.support, f.weights d • d.weights).support,
      h a ((∑ d ∈ f.weights.support, f.weights d • d.weights) a) =
    ∑ d ∈ f.weights.support, ∑ a ∈ (f.weights d • d.weights).support, h a ((f.weights d • d.weights) a)
d : StdSimplex R P
hd : ¬f.weights d = 0
p : P
⊢ ¬(f.weights d • d.weights) p = 0 → ¬d.weights p = 0