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 :
  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₂)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
refine_1 : False
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)

Tactic:
exfalso
-- 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 :
  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₂)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
⊢ False

Tactic:
(s.sSameSide_affineSpan_faceOpposite_of_sign_eq hw₁ hw₂ hs h0).wSameSide.not_sOppSide h

Premises used: AffineSubspace.SSameSide.wSameSide, AffineSubspace.WSameSide.not_sOppSide, Affine.Simplex.sSameSide_affineSpan_faceOpposite_of_sign_eq
-- 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 :
  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₂)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
⊢ False

Tactic:
exact (s.sSameSide_affineSpan_faceOpposite_of_sign_eq hw₁ hw₂ hs h0).wSameSide.not_sOppSide h

Premises used: AffineSubspace.SSameSide.wSameSide, AffineSubspace.WSameSide.not_sOppSide, Affine.Simplex.sSameSide_affineSpan_faceOpposite_of_sign_eq
-- 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 :
  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₂)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)

Tactic:
hs
-- 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 :
  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₂)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)

Tactic:
exact hs
-- 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
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h0 : w₁ i ≠ 0
refine_2 :
  ∀ (h' : 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₂)
refine_2₁ :
  ∀ (h' : 0 < w₁ i),
    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₂)
⊢ 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:
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)
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
    w₁ i ≠ 0
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h0 : w₁ i ≠ 0
h' : w₁ i < 0
⊢ 0 < w₂ i

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

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)
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
    w₁ i ≠ 0
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h0 : w₁ i ≠ 0
h' : w₁ i < 0
hs₁ : 0 < w₂ i
⊢ w₁ i ≠ 0

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

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)
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
    w₁ i ≠ 0
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h0 : w₁ i ≠ 0
h' : w₁ i < 0
hs₁ : 0 < w₂ i
h0₁ : w₁ i ≠ 0
⊢ w₁ i < 0

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

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)
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
    w₁ i ≠ 0
hs : 0 < w₂ i
h0 : w₁ i ≠ 0
h' : 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:
(s.sOppSide_affineSpan_faceOpposite_of_pos_of_neg hw₂ hw₁ hs h').symm

Premises used: AffineSubspace.SOppSide.symm, 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)
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
    w₁ i ≠ 0
hs : 0 < w₂ i
h0 : w₁ i ≠ 0
h' : 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:
exact (s.sOppSide_affineSpan_faceOpposite_of_pos_of_neg hw₂ hw₁ hs h').symm

Premises used: AffineSubspace.SOppSide.symm, 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)
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
    w₁ i ≠ 0
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h0 : w₁ i ≠ 0
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 hs

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)
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
    w₁ i ≠ 0
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h0 : w₁ i ≠ 0
h' : 0 < w₁ i
hs₁ : w₂ i < 0
⊢ w₁ i ≠ 0

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

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)
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
    w₁ i ≠ 0
hs :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
h0 : w₁ i ≠ 0
h' : 0 < w₁ i
hs₁ : w₂ i < 0
h0₁ : w₁ i ≠ 0
⊢ 0 < w₁ i

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

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)
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
    w₁ i ≠ 0
hs : w₂ i < 0
h0 : w₁ i ≠ 0
h' : 0 < w₁ i
⊢ 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:
s.sOppSide_affineSpan_faceOpposite_of_pos_of_neg hw₁ hw₂ h' hs

Premises used: 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)
h :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
    w₁ i ≠ 0
hs : w₂ i < 0
h0 : w₁ i ≠ 0
h' : 0 < w₁ i
⊢ 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:
exact s.sOppSide_affineSpan_faceOpposite_of_pos_of_neg hw₁ hw₂ h' hs

Premises used: 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)
⊢ WSameSide (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 ∨ w₂ i = 0

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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_1 :
  ∀
    (h :
      WSameSide (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 ∨ w₂ i = 0
refine_2 :
  ∀
    (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),
    WSameSide (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₂)
⊢ WSameSide (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 ∨ w₂ i = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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 :
  WSameSide (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₂)
pos :
  ∀ (h0 : w₁ i = 0),
    Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
        ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∨
      w₁ i = 0 ∨ w₂ i = 0
neg :
  ∀ (h0 : ¬w₁ i = 0),
    Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
        ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∨
      w₁ i = 0 ∨ w₂ i = 0
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∨
    w₁ i = 0 ∨ w₂ i = 0

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 :
  WSameSide (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₂)
h0 : w₁ i = 0
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∨
    w₁ i = 0 ∨ w₂ i = 0

Tactic:
simp [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 :
  WSameSide (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₂)
h0 : ¬w₁ i = 0
pos :
  ∀ (h0' : w₂ i = 0),
    Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
        ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∨
      w₁ i = 0 ∨ w₂ i = 0
neg :
  ∀ (h0' : ¬w₂ i = 0),
    Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
        ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∨
      w₁ i = 0 ∨ w₂ i = 0
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∨
    w₁ i = 0 ∨ w₂ i = 0

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 :
  WSameSide (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₂)
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) ∨
    w₁ i = 0 ∨ w₂ i = 0

Tactic:
simp [h0']