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)
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∨
    w₁ i = 0 ∨ w₂ i = 0
h0 : w₁ i = 0
⊢ WOppSide (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:
exact wOppSide_of_left_mem _ ((s.affineCombination_mem_affineSpan_faceOpposite_iff hw₁).2 h0)

Premises used: Iff.mpr, AffineSubspace.wOppSide_of_left_mem, Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_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)
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∨
    w₁ i = 0 ∨ w₂ i = 0
h0 : ¬w₁ i = 0
pos :
  ∀ (h0' : w₂ i = 0),
    WOppSide (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₂)
neg :
  ∀ (h0' : ¬w₂ i = 0),
    WOppSide (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₂)
⊢ WOppSide (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:
by_cases h0' : w₂ i = 0
-- 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 :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∨
    w₁ i = 0 ∨ w₂ i = 0
h0 : ¬w₁ i = 0
h0' : w₂ i = 0
⊢ WOppSide (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:
wOppSide_of_right_mem _
          ((s.affineCombination_mem_affineSpan_faceOpposite_iff hw₂).2 h0')

Premises used: Iff.mpr, Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iff, AffineSubspace.wOppSide_of_right_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)
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∨
    w₁ i = 0 ∨ w₂ i = 0
h0 : ¬w₁ i = 0
h0' : w₂ i = 0
⊢ WOppSide (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:
exact wOppSide_of_right_mem _
          ((s.affineCombination_mem_affineSpan_faceOpposite_iff hw₂).2 h0')

Premises used: Iff.mpr, Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iff, AffineSubspace.wOppSide_of_right_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)
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∨
    w₁ i = 0 ∨ w₂ i = 0
h0 : ¬w₁ i = 0
h0' : ¬w₂ i = 0
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)

Tactic:
simp only [h0, h0', or_self, or_false] at h

Premises used: or_self, or_false
-- 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)
h0 : ¬w₁ i = 0
h0' : ¬w₂ i = 0
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
neg :
  ∀ (h' : w₁ i < 0),
    WOppSide (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₂)
neg₁ :
  ∀ (h' : 0 < w₁ i),
    WOppSide (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₂)
⊢ WOppSide (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:
rcases Ne.lt_or_gt h0 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)
h0 : ¬w₁ i = 0
h0' : ¬w₂ i = 0
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h' : w₁ i < 0
⊢ 0 < w₂ i

Tactic:
rw [sign_neg h', neg_inj, eq_comm, sign_eq_one_iff] at h

Premises used: eq_comm, sign_neg, neg_inj, 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)
h0 : ¬w₁ i = 0
h0' : ¬w₂ i = 0
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h' : w₁ i < 0
h₁ : 0 < w₂ i
⊢ w₁ i < 0

Tactic:
rw [sign_neg h', neg_inj, eq_comm, sign_eq_one_iff] at h

Premises used: eq_comm, sign_neg, neg_inj, 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)
h0 : ¬w₁ i = 0
h0' : ¬w₂ i = 0
h : 0 < w₂ i
h' : w₁ i < 0
⊢ WOppSide (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:
(s.sOppSide_affineSpan_faceOpposite_of_pos_of_neg hw₂ hw₁ h h').symm.wOppSide

Premises used: AffineSubspace.SOppSide.symm, AffineSubspace.SOppSide.wOppSide, Affine.Simplex.sOppSide_affineSpan_faceOpposite_of_pos_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)
h0 : ¬w₁ i = 0
h0' : ¬w₂ i = 0
h : 0 < w₂ i
h' : w₁ i < 0
⊢ WOppSide (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:
exact (s.sOppSide_affineSpan_faceOpposite_of_pos_of_neg hw₂ hw₁ h h').symm.wOppSide

Premises used: AffineSubspace.SOppSide.symm, AffineSubspace.SOppSide.wOppSide, Affine.Simplex.sOppSide_affineSpan_faceOpposite_of_pos_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)
h0 : ¬w₁ i = 0
h0' : ¬w₂ i = 0
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h' : 0 < w₁ i
⊢ w₂ i < 0

Tactic:
rw [sign_pos h', eq_comm, neg_eq_iff_eq_neg, sign_eq_neg_one_iff] at h

Premises used: sign_pos, neg_eq_iff_eq_neg, eq_comm, 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)
h0 : ¬w₁ i = 0
h0' : ¬w₂ i = 0
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h' : 0 < w₁ i
h₁ : w₂ i < 0
⊢ 0 < w₁ i

Tactic:
rw [sign_pos h', eq_comm, neg_eq_iff_eq_neg, sign_eq_neg_one_iff] at h

Premises used: sign_pos, neg_eq_iff_eq_neg, eq_comm, 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)
h0 : ¬w₁ i = 0
h0' : ¬w₂ i = 0
h : w₂ i < 0
h' : 0 < w₁ i
⊢ WOppSide (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:
(s.sOppSide_affineSpan_faceOpposite_of_pos_of_neg hw₁ hw₂ h' h).wOppSide

Premises used: AffineSubspace.SOppSide.wOppSide, Affine.Simplex.sOppSide_affineSpan_faceOpposite_of_pos_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)
h0 : ¬w₁ i = 0
h0' : ¬w₂ i = 0
h : w₂ i < 0
h' : 0 < w₁ i
⊢ WOppSide (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:
exact (s.sOppSide_affineSpan_faceOpposite_of_pos_of_neg hw₁ hw₂ h' h).wOppSide

Premises used: AffineSubspace.SOppSide.wOppSide, Affine.Simplex.sOppSide_affineSpan_faceOpposite_of_pos_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 : Fin (n + 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w j) 1
i : Fin (n + 1)
rw :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i) : SignType)
        ((SignType.sign : (a : R) → SignType) (Pi.single (M := fun (a : Fin (n + 1)) ↦ R) i 1 i : R) : SignType) ∧
      Ne.{u_1 + 1} (α := R) (Pi.single (M := fun (a : Fin (n + 1)) ↦ R) i 1 i : R) (0 : R) ↔
    0 < w i
⊢ SSameSide (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points i)
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w) ↔
    0 < w i

Tactic:
rw [← Finset.univ.affineCombination_piSingle R s.points (Finset.mem_univ i),
    s.sSameSide_affineSpan_faceOpposite_iff (Fintype.sum_pi_single' _ _) hw, eq_comm]

Premises used: Finset.mem_univ, Affine.Simplex.points, Finset.univ, eq_comm, Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff, Finset.affineCombination_piSingle, Fintype.sum_pi_single'
-- 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 : Fin (n + 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w j) 1
i : Fin (n + 1)
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i) : SignType)
        ((SignType.sign : (a : R) → SignType) (Pi.single (M := fun (a : Fin (n + 1)) ↦ R) i 1 i : R) : SignType) ∧
      Ne.{u_1 + 1} (α := R) (Pi.single (M := fun (a : Fin (n + 1)) ↦ R) i 1 i : R) (0 : R) ↔
    0 < w i

Tactic:
simp [sign_eq_one_iff]

Premises used: 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 : Fin (n + 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w j) 1
i : Fin (n + 1)
rw :
  SSameSide (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points i)
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w) ↔
    0 < w i
rw₁ rw₂ : 0 < w i ↔ 0 < w i
⊢ SSameSide (affineSpan R (Set.range (s.faceOpposite i).points))
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w) (s.points i) ↔
    0 < w i

Tactic:
rw [sSameSide_comm, s.sSameSide_affineSpan_faceOpposite_point_left_iff hw]

Premises used: Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_left_iff, AffineSubspace.sSameSide_comm
-- 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 : Fin (n + 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w j) 1
i : Fin (n + 1)
rw :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i) : SignType)
        (-(SignType.sign : (a : R) → SignType) (Pi.single (M := fun (a : Fin (n + 1)) ↦ R) i 1 i : R) : SignType) ∧
      Ne.{u_1 + 1} (α := R) (Pi.single (M := fun (a : Fin (n + 1)) ↦ R) i 1 i : R) (0 : R) ↔
    w i < 0
⊢ SOppSide (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points i)
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w) ↔
    w i < 0

Tactic:
rw [← Finset.univ.affineCombination_piSingle R s.points (Finset.mem_univ i),
    s.sOppSide_affineSpan_faceOpposite_iff (Fintype.sum_pi_single' _ _) hw, eq_comm,
    neg_eq_iff_eq_neg]

Premises used: Finset.mem_univ, Affine.Simplex.points, Finset.univ, neg_eq_iff_eq_neg, eq_comm, Finset.affineCombination_piSingle, Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff, Fintype.sum_pi_single'
-- 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 : Fin (n + 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w j) 1
i : Fin (n + 1)
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i) : SignType)
        (-(SignType.sign : (a : R) → SignType) (Pi.single (M := fun (a : Fin (n + 1)) ↦ R) i 1 i : R) : SignType) ∧
      Ne.{u_1 + 1} (α := R) (Pi.single (M := fun (a : Fin (n + 1)) ↦ R) i 1 i : R) (0 : R) ↔
    w i < 0

Tactic:
simp [sign_eq_neg_one_iff]

Premises used: 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 : Fin (n + 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w j) 1
i : Fin (n + 1)
rw :
  SOppSide (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points i)
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w) ↔
    w i < 0
rw₁ rw₂ : w i < 0 ↔ 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) (s.points i) ↔
    w i < 0

Tactic:
rw [sOppSide_comm, s.sOppSide_affineSpan_faceOpposite_point_left_iff hw]

Premises used: AffineSubspace.sOppSide_comm, Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_left_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 : Fin (n + 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w j) 1
i : Fin (n + 1)
rw :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i) : SignType)
        ((SignType.sign : (a : R) → SignType) (Pi.single (M := fun (a : Fin (n + 1)) ↦ R) i 1 i : R) : SignType) ∨
      Eq.{u_1 + 1} (α := R) (Pi.single (M := fun (a : Fin (n + 1)) ↦ R) i 1 i : R) (0 : R) ∨ w i = 0 ↔
    0 ≤ w i
⊢ WSameSide (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points i)
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w) ↔
    0 ≤ w i

Tactic:
rw [← Finset.univ.affineCombination_piSingle R s.points (Finset.mem_univ i),
    s.wSameSide_affineSpan_faceOpposite_iff (Fintype.sum_pi_single' _ _) hw, eq_comm]

Premises used: Finset.mem_univ, Affine.Simplex.points, Affine.Simplex.wSameSide_affineSpan_faceOpposite_iff, Finset.univ, eq_comm, Finset.affineCombination_piSingle, Fintype.sum_pi_single'
-- 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 : Fin (n + 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w j) 1
i : Fin (n + 1)
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i) : SignType)
        ((SignType.sign : (a : R) → SignType) (Pi.single (M := fun (a : Fin (n + 1)) ↦ R) i 1 i : R) : SignType) ∨
      Eq.{u_1 + 1} (α := R) (Pi.single (M := fun (a : Fin (n + 1)) ↦ R) i 1 i : R) (0 : R) ∨ w i = 0 ↔
    0 ≤ w i

Tactic:
simp [sign_eq_one_iff, le_iff_eq_or_lt', or_comm]

Premises used: le_iff_eq_or_lt', or_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 : Fin (n + 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w j) 1
i : Fin (n + 1)
rw :
  WSameSide (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points i)
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w) ↔
    0 ≤ w i
rw₁ rw₂ : 0 ≤ w i ↔ 0 ≤ w i
⊢ WSameSide (affineSpan R (Set.range (s.faceOpposite i).points))
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w) (s.points i) ↔
    0 ≤ w i

Tactic:
rw [wSameSide_comm, s.wSameSide_affineSpan_faceOpposite_point_left_iff hw]

Premises used: AffineSubspace.wSameSide_comm, Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_left_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 : Fin (n + 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ j : Fin (n + 1), w j) 1
i : Fin (n + 1)
rw :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i) : SignType)
        (-(SignType.sign : (a : R) → SignType) (Pi.single (M := fun (a : Fin (n + 1)) ↦ R) i 1 i : R) : SignType) ∨
      Eq.{u_1 + 1} (α := R) (Pi.single (M := fun (a : Fin (n + 1)) ↦ R) i 1 i : R) (0 : R) ∨ w i = 0 ↔
    w i ≤ 0
⊢ WOppSide (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points i)
      ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w) ↔
    w i ≤ 0

Tactic:
rw [← Finset.univ.affineCombination_piSingle R s.points (Finset.mem_univ i),
    s.wOppSide_affineSpan_faceOpposite_iff (Fintype.sum_pi_single' _ _) hw, eq_comm,
    neg_eq_iff_eq_neg]

Premises used: Finset.mem_univ, Affine.Simplex.points, Finset.univ, Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff, neg_eq_iff_eq_neg, eq_comm, Finset.affineCombination_piSingle, Fintype.sum_pi_single'