awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : s = ⊥
inl : IsPreconnected.{u_4} (α := P) {y : P | False}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}

Tactic:
simp only [h, not_sOppSide_bot]

Premises used: AffineSubspace.not_sOppSide_bot
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s : Set P).Nonempty
pos : ∀ (hx : x ∈ s), IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}
neg : ∀ (hx : x ∉ s), IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s : Set P).Nonempty
hx : x ∈ s
pos : IsPreconnected.{u_4} (α := P) {y : P | False}
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}

Tactic:
simp only [hx, SOppSide, not_true, false_and, and_false]

Premises used: false_and, AffineSubspace.SOppSide, not_true, and_false
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s : Set P).Nonempty
hx : x ∉ s
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}

Tactic:
(isConnected_setOf_sOppSide hx h).isPreconnected

Premises used: IsConnected.isPreconnected, AffineSubspace.isConnected_setOf_sOppSide
-- Module: Mathlib.Analysis.Convex.Side
Goal:
V : Type u_2
P : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
h : (↑s : Set P).Nonempty
hx : x ∉ s
⊢ IsPreconnected.{u_4} (α := P) {y : P | s.SOppSide x y}

Tactic:
exact (isConnected_setOf_sOppSide hx h).isPreconnected

Premises used: IsConnected.isPreconnected, AffineSubspace.isConnected_setOf_sOppSide
-- 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
h : w₂ i = 0
⊢ False

Tactic:
simp_all
-- 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
⊢ w₂ i ≠ 0

Tactic:
have h0' : w₂ i ≠ 0 := by intro h; simp_all
-- 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
⊢ 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₂)

Tactic:
⟨?_, (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₁).not.2 h0,
    (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₂).not.2 h0'⟩

Premises used: Iff.mpr, AffineSubspace.SSameSide, Iff.not, Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iff, And.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)
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
refine :
  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₂)
⊢ 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₂)

Tactic:
refine ⟨?_, (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₁).not.2 h0,
    (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₂).not.2 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)
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)), j ≠ i

Tactic:
exists_ne _

Premises used: exists_ne
-- 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
obtain :
  ∀ (j : Fin (n + 1)) (hj : j ≠ i),
    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₂)

Tactic:
obtain ⟨j, hj⟩ : ∃ j, j ≠ i := exists_ne _

Premises used: exists_ne
-- 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
⊢ Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points j)

Tactic:
simpa using hj
-- 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
⊢ Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range (s.faceOpposite i).points)) (s.points j)

Tactic:
have hj' : s.points j ∈ affineSpan R (Set.range (s.faceOpposite i).points) := by
    simpa using hj
-- 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)
⊢ 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₂)

Tactic:
(wSameSide_iff_exists_left hj').2 (.inr ?_)

Premises used: Iff.mpr, AffineSubspace.wSameSide_iff_exists_left, Or.inr
-- 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)
refine :
  ∃ (p₂ : P),
    Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range (s.faceOpposite i).points)) p₂ ∧
      SameRay R ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁ -ᵥ s.points j)
        ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂ -ᵥ p₂)
⊢ 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₂)

Tactic:
refine (wSameSide_iff_exists_left hj').2 (.inr ?_)

Premises used: Iff.mpr, AffineSubspace.wSameSide_iff_exists_left, Or.inr
-- 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)
rw :
  ∃ (p₂ : P),
    Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range (s.faceOpposite i).points)) p₂ ∧
      SameRay R
        ((Finset.weightedVSub Finset.univ s.points : (a : Fin (n + 1) → R) → V)
          (w₁ - Pi.single (M := fun (a : Fin (n + 1)) ↦ R) j 1))
        ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂ -ᵥ p₂)
⊢ ∃ (p₂ : P),
    Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range (s.faceOpposite i).points)) p₂ ∧
      SameRay R ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₁ -ᵥ s.points j)
        ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂ -ᵥ p₂)

Tactic:
rw [← Finset.univ.affineCombination_piSingle R s.points
    (Finset.mem_univ j), Finset.affineCombination_vsub]

Premises used: Finset.affineCombination_vsub, Finset.mem_univ, Affine.Simplex.points, Finset.univ, Finset.affineCombination_piSingle
-- 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)
⊢ Eq.{u_1 + 1} (α := R) (∑ k : Fin (n + 1), w₃ k) 1

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

Premises used: Finset.mul_sum
-- 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)
⊢ Eq.{u_1 + 1} (α := R) (∑ k : Fin (n + 1), w₃ k) 1

Tactic:
have hw₃1 : ∑ k, w₃ k = 1 := by simp [w₃, hw₂, ← Finset.mul_sum, 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 :
  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
⊢ w₃ i = 0

Tactic:
simp [w₃, hj.symm, h0]

Premises used: Ne.symm
-- 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
⊢ w₃ i = 0

Tactic:
have hw₃i : w₃ i = 0 := by simp [w₃, hj.symm, 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)
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
⊢ ∃ (p₂ : P),
    Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range (s.faceOpposite i).points)) p₂ ∧
      SameRay R
        ((Finset.weightedVSub Finset.univ s.points : (a : Fin (n + 1) → R) → V)
          (w₁ - Pi.single (M := fun (a : Fin (n + 1)) ↦ R) j 1))
        ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂ -ᵥ p₂)

Tactic:
⟨Finset.univ.affineCombination R s.points w₃,
    (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₃1).2 hw₃i, ?_⟩

Premises used: Iff.mpr, Affine.Simplex.points, Finset.univ, Finset.affineCombination, Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iff, And.intro, Exists.intro, 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)
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
refine :
  SameRay R
    ((Finset.weightedVSub Finset.univ s.points : (a : Fin (n + 1) → R) → V)
      (w₁ - Pi.single (M := fun (a : Fin (n + 1)) ↦ R) j 1))
    (VSub.vsub.{u_2, u_4} (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))
⊢ ∃ (p₂ : P),
    Membership.mem (γ := AffineSubspace R P) (affineSpan R (Set.range (s.faceOpposite i).points)) p₂ ∧
      SameRay R
        ((Finset.weightedVSub Finset.univ s.points : (a : Fin (n + 1) → R) → V)
          (w₁ - Pi.single (M := fun (a : Fin (n + 1)) ↦ R) j 1))
        ((Finset.affineCombination R Finset.univ s.points : (a : Fin (n + 1) → R) → P) w₂ -ᵥ p₂)

Tactic:
refine ⟨Finset.univ.affineCombination R s.points w₃,
    (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₃1).2 hw₃i, ?_⟩
-- 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
simp :
  0 ≤ w₂ i * (w₁ i)⁻¹ ∨
    Eq.{u_2 + 1} (α := V)
      ((Finset.weightedVSub Finset.univ s.points : (a : Fin (n + 1) → R) → V)
          (w₁ - Pi.single (M := fun (a : Fin (n + 1)) ↦ R) j 1) :
        V)
      (0 : V)
⊢ SameRay R
    ((Finset.weightedVSub Finset.univ s.points : (a : Fin (n + 1) → R) → V)
      (w₁ - Pi.single (M := fun (a : Fin (n + 1)) ↦ R) j 1))
    (VSub.vsub.{u_2, u_4} (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))

Tactic:
simp only [w₃, Finset.affineCombination_vsub, sub_sub_cancel, smul_smul, map_smul,
    sameRay_smul_right_iff]

Premises used: Finset.affineCombination_vsub, smul_smul, sub_sub_cancel, sameRay_smul_right_iff, map_smul
-- 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 * (w₁ i)⁻¹
⊢ 0 ≤ w₂ i * (w₁ i)⁻¹ ∨
    Eq.{u_2 + 1} (α := V)
      ((Finset.weightedVSub Finset.univ s.points : (a : Fin (n + 1) → R) → V)
          (w₁ - Pi.single (M := fun (a : Fin (n + 1)) ↦ R) j 1) :
        V)
      (0 : V)

Tactic:
left