awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
hj' : Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points j)
w₃ : Fin (n + 1) → R := w₂ - w₂ i • (w₁ i)⁻¹ • (w₁ - Pi.single (M := fun (j : Fin (n + 1)) ↦ R) j 1)
hw₃1 : Eq.{u_1 + 1} (α := R) (∑ k : Fin (n + 1), w₃ k) 1
hw₃i : w₃ i = 0
h : ∀ (h : w₁ i < 0), 0 ≤ w₂ i * (w₁ i)⁻¹
h₁ : ∀ (h : 0 < w₁ i), 0 ≤ w₂ i * (w₁ i)⁻¹
⊢ 0 ≤ w₂ i * (w₁ i)⁻¹

Tactic:
rcases h0.lt_or_gt with h | h

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
hj' : Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points j)
w₃ : Fin (n + 1) → R := w₂ - w₂ i • (w₁ i)⁻¹ • (w₁ - Pi.single (M := fun (j : Fin (n + 1)) ↦ R) j 1)
hw₃1 : Eq.{u_1 + 1} (α := R) (∑ k : Fin (n + 1), w₃ k) 1
hw₃i : w₃ i = 0
h : w₁ i < 0
h₁ :
  ∀ (hs : w₂ i < 0) (h0 : w₁ i ≠ 0) (h0' : w₂ i ≠ 0) (j : Fin (n + 1)) (hj : j ≠ i)
    (hj' : Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points j)),
    let w₃ := w₂ - w₂ i • (w₁ i)⁻¹ • (w₁ - Pi.single (M := fun (j : Fin (n + 1)) ↦ R) j 1);
    ∀ (hw₃1 : Eq.{u_1 + 1} (α := R) (∑ k : Fin (n + 1), w₃ k) 1) (hw₃i : w₃ i = 0) (h : w₁ i < 0), 0 ≤ w₂ i * (w₁ i)⁻¹
⊢ 0 ≤ w₂ i * (w₁ i)⁻¹

Tactic:
rw [sign_neg h, eq_comm, sign_eq_neg_one_iff] at hs

Premises used: eq_comm, sign_neg, sign_eq_neg_one_iff
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs : w₂ i < 0
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
hj' : Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points j)
w₃ : Fin (n + 1) → R := w₂ - w₂ i • (w₁ i)⁻¹ • (w₁ - Pi.single (M := fun (j : Fin (n + 1)) ↦ R) j 1)
hw₃1 : Eq.{u_1 + 1} (α := R) (∑ k : Fin (n + 1), w₃ k) 1
hw₃i : w₃ i = 0
h : w₁ i < 0
⊢ 0 ≤ w₂ i * (w₁ i)⁻¹

Tactic:
(mul_pos_of_neg_of_neg hs (inv_neg''.2 h)).le

Premises used: Iff.mpr, LT.lt.le, inv_neg'', mul_pos_of_neg_of_neg
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs : w₂ i < 0
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
hj' : Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points j)
w₃ : Fin (n + 1) → R := w₂ - w₂ i • (w₁ i)⁻¹ • (w₁ - Pi.single (M := fun (j : Fin (n + 1)) ↦ R) j 1)
hw₃1 : Eq.{u_1 + 1} (α := R) (∑ k : Fin (n + 1), w₃ k) 1
hw₃i : w₃ i = 0
h : w₁ i < 0
⊢ 0 ≤ w₂ i * (w₁ i)⁻¹

Tactic:
exact (mul_pos_of_neg_of_neg hs (inv_neg''.2 h)).le

Premises used: Iff.mpr, LT.lt.le, inv_neg'', mul_pos_of_neg_of_neg
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
hj' : Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points j)
w₃ : Fin (n + 1) → R := w₂ - w₂ i • (w₁ i)⁻¹ • (w₁ - Pi.single (M := fun (j : Fin (n + 1)) ↦ R) j 1)
hw₃1 : Eq.{u_1 + 1} (α := R) (∑ k : Fin (n + 1), w₃ k) 1
hw₃i : w₃ i = 0
h : 0 < w₁ i
h₁ :
  ∀ (hs : 0 < w₂ i) (h0 : w₁ i ≠ 0) (h0' : w₂ i ≠ 0) (j : Fin (n + 1)) (hj : j ≠ i)
    (hj' : Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points j)),
    let w₃ := w₂ - w₂ i • (w₁ i)⁻¹ • (w₁ - Pi.single (M := fun (j : Fin (n + 1)) ↦ R) j 1);
    ∀ (hw₃1 : Eq.{u_1 + 1} (α := R) (∑ k : Fin (n + 1), w₃ k) 1) (hw₃i : w₃ i = 0) (h : 0 < w₁ i), 0 ≤ w₂ i * (w₁ i)⁻¹
⊢ 0 ≤ w₂ i * (w₁ i)⁻¹

Tactic:
rw [sign_pos h, eq_comm, sign_eq_one_iff] at hs

Premises used: sign_pos, eq_comm, sign_eq_one_iff
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs : 0 < w₂ i
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
hj' : Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points j)
w₃ : Fin (n + 1) → R := w₂ - w₂ i • (w₁ i)⁻¹ • (w₁ - Pi.single (M := fun (j : Fin (n + 1)) ↦ R) j 1)
hw₃1 : Eq.{u_1 + 1} (α := R) (∑ k : Fin (n + 1), w₃ k) 1
hw₃i : w₃ i = 0
h : 0 < w₁ i
⊢ 0 ≤ w₂ i * (w₁ i)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂ : (a : R) → Fin (n + 1) → R) (w₁ i / (w₁ i - w₂ i))
⊢ 0 < w₁ i - w₂ i

Tactic:
grind
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂ : (a : R) → Fin (n + 1) → R) (w₁ i / (w₁ i - w₂ i))
⊢ 0 < w₁ i - w₂ i

Tactic:
have hp : 0 < w₁ i - w₂ i := by grind
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂ : (a : R) → Fin (n + 1) → R) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
⊢ Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₃ j) 1

Tactic:
simp [w₃, lineMap_apply, Finset.sum_add_distrib, ← Finset.mul_sum, hw₁, hw₂]

Premises used: Finset.mul_sum, Finset.sum_add_distrib, AffineMap.lineMap_apply
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂ : (a : R) → Fin (n + 1) → R) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
⊢ Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₃ j) 1

Tactic:
have hw₃ : ∑ j, w₃ j = 1 := by
    simp [w₃, lineMap_apply, Finset.sum_add_distrib, ← Finset.mul_sum, hw₁, hw₂]
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂ : (a : R) → Fin (n + 1) → R) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
hw₃ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₃ j) 1
⊢ w₁ ≠ w₂

Tactic:
grind
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂ : (a : R) → Fin (n + 1) → R) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
hw₃ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₃ j) 1
⊢ w₁ i < w₁ i - w₂ i

Tactic:
grind
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂ : (a : R) → Fin (n + 1) → R) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
hw₃ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₃ j) 1
⊢ Sbtw R w₁ w₃ w₂

Tactic:
have h : Sbtw R w₁ w₃ w₂ := sbtw_lineMap_iff.2
    ⟨(by grind), div_pos hs₁ hp, (div_lt_one hp).2 (by grind)⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂ : (a : R) → Fin (n + 1) → R) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
hw₃ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₃ j) 1
h rwa rwa₁ rwa₂ rwa₃ : Sbtw R w₁ w₃ w₂
⊢ Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁ : P)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₃ : P)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂ : P)

Tactic:
rwa [s.independent.injOn_affineCombination_fintypeAffineCoords.sbtw_map_iff
     (mem_fintypeAffineCoords_iff_sum.2 hw₁) (mem_fintypeAffineCoords_iff_sum.2 hw₃)
     (mem_fintypeAffineCoords_iff_sum.2 hw₂)]

Premises used: Iff.mpr, mem_fintypeAffineCoords_iff_sum, Affine.Simplex.independent, AffineIndependent.injOn_affineCombination_fintypeAffineCoords, Set.InjOn.sbtw_map_iff
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂ : (a : R) → Fin (n + 1) → R) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
hw₃ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₃ j) 1
h : Sbtw R w₁ w₃ w₂
⊢ Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁ : P)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₃ : P)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂ : P)

Tactic:
have h' : Sbtw R (Finset.univ.affineCombination R s.points w₁)
      (Finset.univ.affineCombination R s.points w₃)
      (Finset.univ.affineCombination R s.points w₂) := by
    rwa [s.independent.injOn_affineCombination_fintypeAffineCoords.sbtw_map_iff
     (mem_fintypeAffineCoords_iff_sum.2 hw₁) (mem_fintypeAffineCoords_iff_sum.2 hw₃)
     (mem_fintypeAffineCoords_iff_sum.2 hw₂)]
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂ : (a : R) → Fin (n + 1) → R) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
hw₃ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₃ j) 1
h : Sbtw R w₁ w₃ w₂
h' :
  Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁ : P)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₃ : P)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂ : P)
⊢ SOppSide (affineSpan R (Set.range (s.faceOpposite i).points))
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂)

Tactic:
h'.sOppSide_of_notMem_of_mem
    ((s.affineCombination_mem_affineSpan_faceOpposite_iff hw₁).not.2 hs₁.ne')
    ((s.affineCombination_mem_affineSpan_faceOpposite_iff hw₃).2 ?_)

Premises used: Iff.mpr, Iff.not, LT.lt.ne', Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iff, Sbtw.sOppSide_of_notMem_of_mem
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂ : (a : R) → Fin (n + 1) → R) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
hw₃ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₃ j) 1
h : Sbtw R w₁ w₃ w₂
h' :
  Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁ : P)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₃ : P)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂ : P)
refine : w₃ i = 0
⊢ SOppSide (affineSpan R (Set.range (s.faceOpposite i).points))
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂)

Tactic:
refine h'.sOppSide_of_notMem_of_mem
    ((s.affineCombination_mem_affineSpan_faceOpposite_iff hw₁).not.2 hs₁.ne')
    ((s.affineCombination_mem_affineSpan_faceOpposite_iff hw₃).2 ?_)

Premises used: Iff.mpr, Iff.not, LT.lt.ne', Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iff, Sbtw.sOppSide_of_notMem_of_mem
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂ : (a : R) → Fin (n + 1) → R) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
hw₃ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₃ j) 1
h : Sbtw R w₁ w₃ w₂
h' :
  Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁ : P)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₃ : P)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂ : P)
simp : w₁ i / (w₁ i - w₂ i) * (w₂ i - w₁ i) + w₁ i = 0
⊢ w₃ i = 0

Tactic:
simp only [lineMap_apply, vsub_eq_sub, vadd_eq_add, Pi.add_apply, Pi.smul_apply, Pi.sub_apply,
    smul_eq_mul, w₃]

Premises used: Pi.add_apply, AffineMap.lineMap_apply, vadd_eq_add, smul_eq_mul, vsub_eq_sub, Pi.sub_apply, Pi.smul_apply
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂ : (a : R) → Fin (n + 1) → R) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
hw₃ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₃ j) 1
h : Sbtw R w₁ w₃ w₂
h' :
  Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁ : P)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₃ : P)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂ : P)
rw : -w₁ i + w₁ i = 0
⊢ w₁ i / (w₁ i - w₂ i) * (w₂ i - w₁ i) + w₁ i = 0

Tactic:
rw [← neg_sub (w₁ i) (w₂ i), mul_neg, div_mul_cancel₀ _ hp.ne']

Premises used: div_mul_cancel₀, neg_sub, LT.lt.ne', mul_neg
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
hs₁ : 0 < w₁ i
hs₂ : w₂ i < 0
w₃ : Fin (n + 1) → R := (lineMap w₁ w₂ : (a : R) → Fin (n + 1) → R) (w₁ i / (w₁ i - w₂ i))
hp : 0 < w₁ i - w₂ i
hw₃ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₃ j) 1
h : Sbtw R w₁ w₃ w₂
h' :
  Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁ : P)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₃ : P)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂ : P)
⊢ -w₁ i + w₁ i = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
⊢ SSameSide (affineSpan R (Set.range (s.faceOpposite i).points))
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁)
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂) ↔
    Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
        ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
      w₁ i ≠ 0

Tactic:
⟨fun h ↦ ?_, fun ⟨hs, h0⟩ ↦ s.sSameSide_affineSpan_faceOpposite_of_sign_eq hw₁ hw₂ hs h0⟩

Premises used: Affine.Simplex.points, _private.0.Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff.match_1, Finset.univ, AffineSubspace.SSameSide, Finset.affineCombination, Affine.Simplex.sSameSide_affineSpan_faceOpposite_of_sign_eq, affineSpan, Iff.intro, Affine.Simplex.faceOpposite, Set.range, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
refine :
  ∀
    (h :
      SSameSide (affineSpan R (Set.range (s.faceOpposite i).points))
        ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁)
        ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂)),
    Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
        ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
      w₁ i ≠ 0
⊢ SSameSide (affineSpan R (Set.range (s.faceOpposite i).points))
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁)
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂) ↔
    Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
        ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
      w₁ i ≠ 0

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨hs, h0⟩ ↦ s.sSameSide_affineSpan_faceOpposite_of_sign_eq hw₁ hw₂ hs h0⟩
-- Module: Mathlib.Analysis.Convex.Side
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
n : ℕ
inst_6 : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₁ j) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w₂ j) 1
i : Fin (n + 1)
h :
  SSameSide (affineSpan R (Set.range (s.faceOpposite i).points))
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁)
    ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂)
⊢ w₁ i ≠ 0

Tactic:
have h0 : w₁ i ≠ 0 :=
    (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₁).not.1 h.left_notMem