awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂) (t.points i₃)
w : Fin (HAdd.hAdd (α := ℕ) 2 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (2 + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R (Set.range t.points))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ r₁) :
            P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₂' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (t.points i₂) (singleton (α := P) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂ : P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hss : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₃) : SignType) (1 : SignType)
hs' :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (∑ i : Fin 3, w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hs : ∀ (i : Fin 3), 0 < w i
refine : w i₁ < 1
⊢ Membership.mem (γ := Set R) (Set.Ioo 0 1) (w i₁)

Tactic:
refine ⟨hs i₁, ?_⟩
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂) (t.points i₃)
w : Fin (HAdd.hAdd (α := ℕ) 2 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (2 + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R (Set.range t.points))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ r₁) :
            P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₂' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (t.points i₂) (singleton (α := P) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂ : P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hss : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₃) : SignType) (1 : SignType)
hs' :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (∑ i : Fin 3, w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hs : ∀ (i : Fin 3), 0 < w i
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ {i₁, i₂, i₃}, w i) 1

Tactic:
rw [hu] at hw
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂) (t.points i₃)
w : Fin (HAdd.hAdd (α := ℕ) 2 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (2 + 1), w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R (Set.range t.points))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ r₁) :
            P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₂' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (t.points i₂) (singleton (α := P) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂ : P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hss : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₃) : SignType) (1 : SignType)
hs' :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (∑ i : Fin 3, w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hs : ∀ (i : Fin 3), 0 < w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ {i₁, i₂, i₃}, w i) 1
⊢ Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R (Set.range t.points))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)

Tactic:
rw [hu] at hw
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂) (t.points i₃)
w : Fin (HAdd.hAdd (α := ℕ) 2 1) → R
hw : w i₁ + (w i₂ + w i₃) = 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R (Set.range t.points))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ r₁) :
            P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₂' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (t.points i₂) (singleton (α := P) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂ : P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hss : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₃) : SignType) (1 : SignType)
hs' :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (∑ i : Fin 3, w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hs : ∀ (i : Fin 3), 0 < w i
by_contra : ∀ (hle : ¬w i₁ < 1), False
⊢ w i₁ < 1

Tactic:
by_contra hle
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂) (t.points i₃)
w : Fin (HAdd.hAdd (α := ℕ) 2 1) → R
hw : w i₁ + (w i₂ + w i₃) = 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R (Set.range t.points))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ r₁) :
            P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₂' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (t.points i₂) (singleton (α := P) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂ : P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hss : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₃) : SignType) (1 : SignType)
hs' :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (∑ i : Fin 3, w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hs : ∀ (i : Fin 3), 0 < w i
hle : ¬w i₁ < 1
⊢ 1 ≤ w i₁

Tactic:
rw [not_lt] at hle

Premises used: not_lt
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂) (t.points i₃)
w : Fin (HAdd.hAdd (α := ℕ) 2 1) → R
hw : w i₁ + (w i₂ + w i₃) = 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R (Set.range t.points))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ r₁) :
            P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₂' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (t.points i₂) (singleton (α := P) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂ : P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hss : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₃) : SignType) (1 : SignType)
hs' :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (∑ i : Fin 3, w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hs : ∀ (i : Fin 3), 0 < w i
hle : 1 ≤ w i₁
⊢ False

Tactic:
(hle.trans_lt (lt_add_of_pos_right _ (Left.add_pos (hs i₂) (hs i₃)))).ne' hw

Premises used: lt_add_of_pos_right, LT.lt.ne', Left.add_pos, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂) (t.points i₃)
w : Fin (HAdd.hAdd (α := ℕ) 2 1) → R
hw : w i₁ + (w i₂ + w i₃) = 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R (Set.range t.points))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ r₁) :
            P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₂' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (t.points i₂) (singleton (α := P) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂ : P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hss : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₃) : SignType) (1 : SignType)
hs' :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (∑ i : Fin 3, w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hs : ∀ (i : Fin 3), 0 < w i
hle : 1 ≤ w i₁
⊢ False

Tactic:
exact (hle.trans_lt (lt_add_of_pos_right _ (Left.add_pos (hs i₂) (hs i₃)))).ne' hw

Premises used: lt_add_of_pos_right, LT.lt.ne', Left.add_pos, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂) (t.points i₃)
w : Fin (HAdd.hAdd (α := ℕ) 2 1) → R
hw : w i₁ + ∑ x ∈ {i₂, i₃}, w x = 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R (Set.range t.points))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ r₁) :
            P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₂' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (t.points i₂) (singleton (α := P) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂ : P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hss : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₃) : SignType) (1 : SignType)
hs' :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (∑ i : Fin 3, w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hs : ∀ (i : Fin 3), 0 < w i
⊢ i₂ ∉ {i₃}

Tactic:
simpa using h₂₃
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AddTorsor V P
inst_6 : IsTorsionFree R V
t : Affine.Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
hu : Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}
r₁ : R
hr₁0 : 0 < r₁
hr₁1 : r₁ < 1
h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃) : (a : R) → P) r₁) (t.points i₃)
r₂ : R
hr₂0 : 0 < r₂
hr₂1 : r₂ < 1
h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂) (t.points i₃)
w : Fin (HAdd.hAdd (α := ℕ) 2 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ {i₁, i₂, i₃}, w i) 1
hp :
  Membership.mem (α := P) (γ := AffineSubspace R P) (affineSpan R (Set.range t.points))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P)
        ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
            (Pi.single (M := fun (a : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ R) i₁ 1) :
          P)
        (singleton (α := P)
          ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P)
              (Finset.affineCombinationLineMapWeights i₂ i₃ r₁) :
            P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₂' :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (t.points i₂) (singleton (α := P) ((lineMap (t.points i₁) (t.points i₃) : (a : R) → P) r₂ : P))))
    ((Finset.affineCombination R Finset.univ t.points : (a : Fin (2 + 1) → R) → P) w : P)
h₁s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₂) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
h₂s :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₁) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hss : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (w i₃) : SignType) (1 : SignType)
hs' :
  Eq (α := SignType) ((SignType.sign : (a : R) → SignType) (∑ i : Fin 3, w i) : SignType)
    ((SignType.sign : (a : R) → SignType) (w i₃) : SignType)
hs : ∀ (i : Fin 3), 0 < w i
⊢ i₁ ∉ {i₂, i₃}

Tactic:
simpa [not_or] using ⟨h₁₂, h₁₃⟩

Premises used: not_or
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y z : R
hxz_1 : x ≤ z
hxz : x = z
inl : ∀ (hxz : x ≤ x), Wbtw R x y x ↔ x ≤ y ∧ y ≤ x
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

Tactic:
subst hxz
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y : R
hxz : x ≤ x
inl : Wbtw R x y x ↔ x = y
inl₁ : y = x ↔ x = y
inl₂ inl₃ : x = y ↔ x = y
⊢ Wbtw R x y x ↔ x ≤ y ∧ y ≤ x

Tactic:
rw [← le_antisymm_iff, wbtw_self_iff, eq_comm]

Premises used: eq_comm, wbtw_self_iff, le_antisymm_iff
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y z : R
hxz_1 : x ≤ z
hxz : x < z
⊢ 0 < z - x

Tactic:
have hxz' : 0 < z - x := sub_pos.mpr hxz
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y z : R
hxz_1 : x ≤ z
hxz : x < z
hxz' : 0 < z - x
r : R := (y - x) / (z - x)
⊢ y = r * (z - x) + x

Tactic:
simp [r, hxz'.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y z : R
hxz_1 : x ≤ z
hxz : x < z
hxz' : 0 < z - x
r : R := (y - x) / (z - x)
⊢ y = r * (z - x) + x

Tactic:
have hy : y = r * (z - x) + x := by simp [r, hxz'.ne']
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x y z : R
hxz_1 : x ≤ z
hxz : x < z
hxz' : 0 < z - x
r : R := (y - x) / (z - x)
hy : y = r * (z - x) + x
⊢ Wbtw R x y z ↔ x ≤ y ∧ y ≤ z

Tactic:
simp [hy, wbtw_mul_sub_add_iff, mul_nonneg_iff_of_pos_right hxz', ← le_sub_iff_add_le,
      mul_le_iff_le_one_left hxz', hxz.ne]

Premises used: mul_nonneg_iff_of_pos_right, le_sub_iff_add_le, wbtw_mul_sub_add_iff, mul_le_iff_le_one_left, LT.lt.ne