awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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 - w₂ i) * (w₂ i - w₁ i) + w₁ i = 0
have rw : -w₁ i + w₁ i = 0
Tactic: rw [← neg_sub (w₁ i) (w₂ i), mul_neg, div_mul_cancel₀ _ hp.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
have 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
Tactic: refine ⟨fun h ↦ ?_, fun ⟨hs, h0⟩ ↦ s.sSameSide_affineSpan_faceOpposite_of_sign_eq hw₁ hw₂ hs h0⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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₂)
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
    w₁ i ≠ 0
have h0 : w₁ i ≠ 0
Tactic: have h0 : w₁ i ≠ 0 :=
    (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₁).not.1 h.left_notMem
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂)
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
have refine : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
  ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
Tactic: refine ⟨?_, h0⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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₂)
h0 : w₁ i ≠ 0
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
have h0' : w₂ i ≠ 0
Tactic: have h0' : w₂ i ≠ 0 :=
    (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₂).not.1 h.right_notMem
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂)
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)
have inl : ∀
  (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: rcases sign_eq_sign_or_eq_neg h0 h0' with hs | hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
inl :
  ∀
    (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)
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
have inr : ∀
  (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: rcases sign_eq_sign_or_eq_neg h0 h0' with hs | hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂)
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)
have inr : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂)
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
have inr : ∀ (h' : w₁ i < 0), False
Tactic: rcases Ne.lt_or_gt h0 with h' | h'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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₂)
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)
inr : ∀ (h' : w₁ i < 0), False
⊢ False
have inr₁ : ∀ (h' : 0 < w₁ i), False
Tactic: rcases Ne.lt_or_gt h0 with h' | h'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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₂)
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)
h' : w₁ i < 0
⊢ False
have hs₁ : 0 < w₂ i
Tactic: rw [sign_neg h', neg_inj, eq_comm, sign_eq_one_iff] at hs
Cleared hypotheses: hs, h'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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₂)
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)
h' : 0 < w₁ i
⊢ False
have hs₁ : w₂ i < 0
Tactic: rw [sign_pos h', eq_comm, neg_eq_iff_eq_neg, sign_eq_neg_one_iff] at hs
Cleared hypotheses: hs, h'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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)
⊢ 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₂) ↔
    Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
        (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
      w₁ i ≠ 0
have refine_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₂)),
  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⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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 :
      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₂)),
    Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
        (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
      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₂) ↔
    Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
        (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
      w₁ i ≠ 0
have refine_2 : 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),
    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 ⟨fun h ↦ ?_, fun ⟨hs, h0⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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₂)
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
    w₁ i ≠ 0
have h0 : w₁ i ≠ 0
Tactic: have h0 : w₁ i ≠ 0 :=
      (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₁).not.1 h.left_notMem
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
      (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType) ∧
    w₁ i ≠ 0
have refine_1 : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
  (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
Tactic: refine ⟨?_, h0⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (hypothesis)
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
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
have h0' : w₂ i ≠ 0
Tactic: have h0' : w₂ i ≠ 0 :=
      (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₂).not.1 h.right_notMem
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
have refine_1 : ∀
  (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: rcases sign_eq_sign_or_eq_neg h0 h0' with hs | hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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
refine_1 :
  ∀
    (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)
⊢ Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w₁ i) : SignType)
    (-(SignType.sign : (a : R) → SignType) (w₂ i) : SignType)
have refine_1₁ : ∀
  (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: rcases sign_eq_sign_or_eq_neg h0 h0' with hs | hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.Side (goal)
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)
have refine_1 : False
Tactic: exfalso