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 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y : P
r : R
rw :
  x ≠ y →
    (Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
        (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioo 0 1))
        ((lineMap x y : (a : R) → P) r : P) ↔
      Membership.mem (γ := Set R) (Set.Ioo 0 1) r)
⊢ Sbtw R x ((lineMap x y : (a : R) → P) r) y ↔ x ≠ y ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r

Tactic:
rw [sbtw_iff_mem_image_Ioo_and_ne, and_comm, and_congr_right]

Premises used: sbtw_iff_mem_image_Ioo_and_ne, and_comm, and_congr_right
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
x y : P
r : R
hxy : x ≠ y
rw rw₁ : Membership.mem (γ := Set R) (Set.Ioo 0 1) r ↔ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
⊢ Membership.mem.{u_4, u_4} (α := P) (γ := Set P)
      (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x y) : (a : R) → P) (Set.Ioo 0 1)) ((lineMap x y : (a : R) → P) r : P) ↔
    Membership.mem (γ := Set R) (Set.Ioo 0 1) r

Tactic:
rw [(lineMap_injective R hxy).mem_set_image]

Premises used: AffineMap.lineMap_injective, Function.Injective.mem_set_image
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : IsDomain R
x y r : R
⊢ Wbtw R x (r * (y - x) + x) y ↔ x = y ∨ Membership.mem (γ := Set R) (Set.Icc 0 1) r

Tactic:
wbtw_lineMap_iff

Premises used: wbtw_lineMap_iff
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : IsDomain R
x y r : R
⊢ Sbtw R x (r * (y - x) + x) y ↔ x ≠ y ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r

Tactic:
sbtw_lineMap_iff

Premises used: sbtw_lineMap_iff
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y z : P
h₁ : Wbtw R w y z
h₂ : Sbtw R w x y
⊢ Sbtw R w x z

Tactic:
⟨h₁.trans_left h₂.wbtw, h₂.ne_left, ?_⟩

Premises used: Sbtw.ne_left, And.intro, Sbtw.wbtw, Wbtw.trans_left, Sbtw
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y z : P
h₁ : Wbtw R w y z
h₂ : Sbtw R w x y
refine : x ≠ z
⊢ Sbtw R w x z

Tactic:
refine ⟨h₁.trans_left h₂.wbtw, h₂.ne_left, ?_⟩
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y : P
h₂ : Sbtw R w x y
h₁ : Wbtw R w y x
⊢ False

Tactic:
h₂.right_ne ((wbtw_swap_right_iff R w).1 ⟨h₁, h₂.wbtw⟩)

Premises used: Sbtw.right_ne, wbtw_swap_right_iff, And.intro, Sbtw.wbtw, Iff.mp
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y : P
h₂ : Sbtw R w x y
h₁ : Wbtw R w y x
⊢ False

Tactic:
exact h₂.right_ne ((wbtw_swap_right_iff R w).1 ⟨h₁, h₂.wbtw⟩)

Premises used: Sbtw.right_ne, wbtw_swap_right_iff, And.intro, Sbtw.wbtw, Iff.mp
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y z : P
h₁ : Wbtw R w x z
h₂ : Sbtw R x y z
⊢ Wbtw R z x w

Tactic:
rw [wbtw_comm] at *

Premises used: wbtw_comm
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y z : P
h₁ : Wbtw R w x z
h₂ : Sbtw R x y z
h₃ : Wbtw R z x w
⊢ Sbtw R x y z

Tactic:
rw [wbtw_comm] at *

Premises used: wbtw_comm
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y z : P
h₁ : Wbtw R z x w
h₂ : Sbtw R x y z
rw : ∀ (h₂ : Sbtw R z y x), Sbtw R z y w
⊢ Sbtw R w y z

Tactic:
rw [sbtw_comm] at *

Premises used: sbtw_comm
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y z : P
h₁ : Wbtw R z x w
h₂ : Sbtw R z y x
⊢ Sbtw R z y w

Tactic:
h₁.trans_sbtw_left h₂

Premises used: Wbtw.trans_sbtw_left
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y z : P
h₁ : Wbtw R z x w
h₂ : Sbtw R z y x
⊢ Sbtw R z y w

Tactic:
exact h₁.trans_sbtw_left h₂

Premises used: Wbtw.trans_sbtw_left
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y z : P
h₁ : Sbtw R w y z
h₂ : Sbtw R w x y
⊢ Sbtw R w x z

Tactic:
h₁.wbtw.trans_sbtw_left h₂

Premises used: Sbtw.wbtw, Wbtw.trans_sbtw_left
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y z : P
h₁ : Sbtw R w x z
h₂ : Sbtw R x y z
⊢ Sbtw R w y z

Tactic:
h₁.wbtw.trans_sbtw_right h₂

Premises used: Wbtw.trans_sbtw_right, Sbtw.wbtw
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y : P
h₂ : Wbtw R w x y
h₁ : Wbtw R w y x
h : y ≠ x
⊢ False

Tactic:
h (h₁.swap_right_iff.1 h₂)

Premises used: Wbtw.swap_right_iff, Iff.mp
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y : P
h₂ : Wbtw R w x y
h₁ : Wbtw R w y x
h : y ≠ x
⊢ False

Tactic:
exact h (h₁.swap_right_iff.1 h₂)

Premises used: Wbtw.swap_right_iff, Iff.mp
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x z : P
h₁ : Wbtw R w x z
h : w ≠ x
h₂ : Wbtw R x w z
⊢ False

Tactic:
h (h₁.swap_left_iff.1 h₂)

Premises used: Wbtw.swap_left_iff, Iff.mp
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x z : P
h₁ : Wbtw R w x z
h : w ≠ x
h₂ : Wbtw R x w z
⊢ False

Tactic:
exact h (h₁.swap_left_iff.1 h₂)

Premises used: Wbtw.swap_left_iff, Iff.mp
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y z : P
h₁ : Sbtw R w y z
h₂ : Wbtw R w x y
⊢ x ≠ z

Tactic:
h₁.wbtw.trans_left_ne h₂ h₁.ne_right

Premises used: Wbtw.trans_left_ne, Sbtw.wbtw, Sbtw.ne_right
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
w x y z : P
h₁ : Sbtw R w x z
h₂ : Wbtw R x y z
⊢ w ≠ y

Tactic:
h₁.wbtw.trans_right_ne h₂ h₁.left_ne

Premises used: Wbtw.trans_right_ne, Sbtw.wbtw, Sbtw.left_ne
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
h :
  Membership.mem (α := P) (γ := AffineSubspace R P)
    (affineSpan R
      (insert (α := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
        (singleton (α := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P))))
    ((Finset.affineCombination R s p : (a : ι → R) → P) w : P)
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
rw :
  ∀ (h : ∃ (r : R), ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i) {i : ι} (his : i ∈ s) (hs : Sbtw R (w₁ i) (w i) (w₂ i)),
    Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
      ((Finset.affineCombination R s p : (a : ι → R) → P) w : P)
      ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P)
⊢ Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P)

Tactic:
rw [affineCombination_mem_affineSpan_pair ha hw hw₁ hw₂] at h

Premises used: affineCombination_mem_affineSpan_pair
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
h : ∃ (r : R), ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
rcases :
  ∀ (r : R) (hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i),
    Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
      ((Finset.affineCombination R s p : (a : ι → R) → P) w : P)
      ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P)
⊢ Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P)

Tactic:
rcases h with ⟨r, hr⟩
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
r : R
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r

Tactic:
rw [hr i his, sbtw_mul_sub_add_iff] at hs

Premises used: sbtw_mul_sub_add_iff
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
hs : Sbtw R (w₁ i) (w i) (w₂ i)
r : R
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
hs₁ : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
⊢ ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i

Tactic:
rw [hr i his, sbtw_mul_sub_add_iff] at hs

Premises used: sbtw_mul_sub_add_iff
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i

Tactic:
change ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i at hr

Premises used: HSub.hSub, HAdd.hAdd, HSMul.hSMul
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
rw :
  Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) (r • (w₂ - w₁) + w₁) : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P)
⊢ Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P)

Tactic:
rw [s.affineCombination_congr hr fun _ _ => rfl]

Premises used: Finset.affineCombination_congr, rfl
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
rw : Ne.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
⊢ Sbtw.{u_1, u_2, u_4} R (P := P) ((Finset.affineCombination R s p : (a : ι → R) → P) w₁ : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) (r • (w₂ - w₁) + w₁) : P)
    ((Finset.affineCombination R s p : (a : ι → R) → P) w₂ : P)

Tactic:
rw [← s.weightedVSub_vadd_affineCombination, s.weightedVSub_const_smul,
    ← s.affineCombination_vsub, ← lineMap_apply, sbtw_lineMap_iff, and_iff_left hs.2,
    ← @vsub_ne_zero V, s.affineCombination_vsub]

Premises used: Finset.affineCombination_vsub, vsub_ne_zero, and_iff_left, Finset.weightedVSub_const_smul, AffineMap.lineMap_apply, And.right, Finset.weightedVSub_vadd_affineCombination, sbtw_lineMap_iff
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
simp_rw : Eq.{u_1 + 1} (α := R) (∑ x ∈ s, (w₁ x - w₂ x)) 0
simp_rw₁ : HSub.hSub (α := R) (∑ x ∈ s, w₁ x) (∑ x ∈ s, w₂ x) = 0
simp_rw₂ : HSub.hSub (α := R) 1 (∑ x ∈ s, w₂ x) = 0
simp_rw₃ : HSub.hSub (α := R) 1 1 = 0
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (w₁ - w₂) i) 0

Tactic:
simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, hw₁, hw₂, sub_self]

Premises used: sub_self, Finset.sum_sub_distrib, Pi.sub_apply
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (w₁ - w₂) i) 0

Tactic:
have hw₁w₂ : (∑ i ∈ s, (w₁ - w₂) i) = 0 := by
    simp_rw [Pi.sub_apply, Finset.sum_sub_distrib, hw₁, hw₂, sub_self]
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
hw₁w₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (w₁ - w₂) i) 0
⊢ False

Tactic:
hs.1 ?_

Premises used: And.left
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
hw₁w₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (w₁ - w₂) i) 0
refine : w₁ i = w₂ i
⊢ False

Tactic:
refine hs.1 ?_

Premises used: And.left
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
hw₁w₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (w₁ - w₂) i) 0
⊢ (w₁ - w₂) i = 0

Tactic:
have ha' := ha s (w₁ - w₂) hw₁w₂ hz i his
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : IsOrderedRing R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ Membership.mem (γ := Set R) (Set.Ioo 0 1) r
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
hz : Eq.{u_2 + 1} (α := V) ((s.weightedVSub p : (a : ι → R) → V) (w₁ - w₂) : V) (0 : V)
hw₁w₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (w₁ - w₂) i) 0
ha' : (w₁ - w₂) i = 0
rwa : ∀ (ha' : w₁ i - w₂ i = 0), w₁ i = w₂ i
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (ha' : w₁ i = w₂ i), w₁ i = w₂ i
⊢ w₁ i = w₂ i

Tactic:
rwa [Pi.sub_apply, sub_eq_zero] at ha'

Premises used: sub_eq_zero, Pi.sub_apply
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
h : ∀ (p : P), p ∈ s.closedInterior ↔ p ∈ affineSegment R (s.points 0) (s.points 1)
⊢ s.closedInterior = affineSegment R (s.points 0) (s.points 1)

Tactic:
ext p
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
p : P
h : p ∈ s.closedInterior → p ∈ affineSegment R (s.points 0) (s.points 1)
h₁ : p ∈ affineSegment R (s.points 0) (s.points 1) → p ∈ s.closedInterior
⊢ p ∈ s.closedInterior ↔ p ∈ affineSegment R (s.points 0) (s.points 1)

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (1 + 1), w i) 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Icc 0 1) (w i)
⊢ w 0 + w 1 = 1

Tactic:
rw [Fin.sum_univ_two] at hw

Premises used: Fin.sum_univ_two
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
P : Type u_4
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AffineSpace V P
inst_5 : IsOrderedRing R
s : Simplex R P 1
w : Fin (HAdd.hAdd (α := ℕ) 1 1) → R
hw : Eq.{u_1 + 1} (α := R) (∑ i : Fin (1 + 1), w i) 1
h01 : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Icc 0 1) (w i)
hw₁ : w 0 + w 1 = 1
⊢ ∀ (i : Fin (HAdd.hAdd (α := ℕ) 1 1)), Membership.mem (γ := Set R) (Set.Icc 0 1) (w i)

Tactic:
rw [Fin.sum_univ_two] at hw

Premises used: Fin.sum_univ_two