awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
K : Submodule 𝕜 E
x : E
h : x ∈ (↑K : Set E)
y : E
h_1 : y ∈ (↑K : Set E)
a b : 𝕜
h_2 : 0 ≤ a
h_3 : 0 ≤ b
h_4 : a + b = 1
⊢ y ∈ K

Tactic:
assumption
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
K : Submodule 𝕜 E
⊢ StarConvex 𝕜 0 (↑K : Set E)

Tactic:
K.convex K.zero_mem

Premises used: Submodule.convex, Submodule.zero_mem
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
𝕜' : Type u_5
inst_4 : Semiring 𝕜'
σ : 𝕜' →+* 𝕜
inst_5 : RingHomSurjective σ
F' : Type u_6
inst_6 : AddCommMonoid F'
inst_7 : Module 𝕜' F'
f : F' →ₛₗ[σ] E
⊢ Convex 𝕜 (↑f.range : Set E)

Tactic:
Submodule.convex ..

Premises used: Submodule.convex
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
obtain :
  ∀ (c : R) (hc1 : Membership.mem (γ := Set R) (Ici 0) c) (hc2 : (algebraMap R A : (a : R) → A) c = a),
    a • u + b • v ∈ s
⊢ a • u + b • v ∈ s

Tactic:
obtain ⟨c, hc1, hc2⟩ := halg ha
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
obtain :
  ∀ (d : R) (hd1 : Membership.mem (γ := Set R) (Ici 0) d) (hd2 : (algebraMap R A : (a : R) → A) d = b),
    a • u + b • v ∈ s
⊢ a • u + b • v ∈ s

Tactic:
obtain ⟨d, hd1, hd2⟩ := halg hb
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
d : R
hd1 : Membership.mem (γ := Set R) (Ici 0) d
hd2 : (algebraMap R A : (a : R) → A) d = b
⊢ c • u + d • v ∈ s

Tactic:
hs hu hv hc1 hd1 _
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
d : R
hd1 : Membership.mem (γ := Set R) (Ici 0) d
hd2 : (algebraMap R A : (a : R) → A) d = b
h : a • u = c • u
h₁ : b • v = d • v
convert! : c + d = 1
⊢ a • u + b • v ∈ s

Tactic:
convert! hs hu hv hc1 hd1 _ using 2
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
d : R
hd1 : Membership.mem (γ := Set R) (Ici 0) d
hd2 : (algebraMap R A : (a : R) → A) d = b
h : HSMul.hSMul.{u_6, u_7, u_7} (α := A) ((algebraMap R A : (a : R) → A) c : A) u = c • u
h₁ h₂ : c • u = c • u
⊢ a • u = c • u

Tactic:
rw [← hc2, algebraMap_smul]

Premises used: algebraMap_smul
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
d : R
hd1 : Membership.mem (γ := Set R) (Ici 0) d
hd2 : (algebraMap R A : (a : R) → A) d = b
h : HSMul.hSMul.{u_6, u_7, u_7} (α := A) ((algebraMap R A : (a : R) → A) d : A) v = d • v
h₁ h₂ : d • v = d • v
⊢ b • v = d • v

Tactic:
rw [← hd2, algebraMap_smul]

Premises used: algebraMap_smul
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
d : R
hd1 : Membership.mem (γ := Set R) (Ici 0) d
hd2 : (algebraMap R A : (a : R) → A) d = b
rw :
  ∀ (hc1 : Membership.mem (γ := Set R) (Ici 0) c) (hc2 : (algebraMap R A : (a : R) → A) c = a) (d : R)
    (hab : Eq.{u_6 + 1} (α := A) (↑(c + d) : A) 1) (hd1 : Membership.mem (γ := Set R) (Ici 0) d)
    (hd2 : (algebraMap R A : (a : R) → A) d = b), c + d = 1
⊢ c + d = 1

Tactic:
rw [← hc2, ← hd2, ← algebraMap.coe_add] at hab

Premises used: algebraMap.coe_add
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
d : R
hab : Eq.{u_6 + 1} (α := A) (↑(c + d) : A) 1
hd1 : Membership.mem (γ := Set R) (Ici 0) d
hd2 : (algebraMap R A : (a : R) → A) d = b
⊢ c + d = 1

Tactic:
(FaithfulSMul.algebraMap_eq_one_iff R A).mp hab

Premises used: FaithfulSMul.algebraMap_eq_one_iff, Iff.mp
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
d : R
hab : Eq.{u_6 + 1} (α := A) (↑(c + d) : A) 1
hd1 : Membership.mem (γ := Set R) (Ici 0) d
hd2 : (algebraMap R A : (a : R) → A) d = b
⊢ c + d = 1

Tactic:
exact (FaithfulSMul.algebraMap_eq_one_iff R A).mp hab

Premises used: FaithfulSMul.algebraMap_eq_one_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
x y : P
r : R
⊢ Membership.mem (α := P) (↑(affineSpan R {x, y}) : Set P) ((lineMap x y : (a : R) → P) r : P)

Tactic:
lineMap_mem_affineSpan_pair _ _ _

Premises used: AffineMap.lineMap_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
x y : P
r : R
⊢ Membership.mem (α := P) (↑(affineSpan R {x, y}) : Set P) ((lineMap x y : (a : R) → P) r : P)

Tactic:
exact lineMap_mem_affineSpan_pair _ _ _

Premises used: AffineMap.lineMap_mem_affineSpan_pair
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
f : P →ᵃ[R] P'
x y : P
rw :
  Eq.{u_5 + 1} (α := Set P') ((fun (x_1 : R) ↦ (f : (a : P) → P') ((lineMap x y : (a : R) → P) x_1 : P)) '' Set.Icc 0 1)
    (Set.image.{u_1, u_5} (α := R) (⇑(f.comp (lineMap x y)) : (a : R) → P') (Set.Icc 0 1))
⊢ Eq.{u_5 + 1} (α := Set P') ((⇑f : (a : P) → P') '' affineSegment R x y : Set P')
    (affineSegment R ((f : (a : P) → P') x) ((f : (a : P) → P') y) : Set P')

Tactic:
rw [affineSegment, affineSegment, Set.image_image, ← comp_lineMap]

Premises used: affineSegment, Set.image_image, AffineMap.comp_lineMap
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
f : P →ᵃ[R] P'
x y : P
⊢ Eq.{u_5 + 1} (α := Set P') ((fun (x_1 : R) ↦ (f : (a : P) → P') ((lineMap x y : (a : R) → P) x_1 : P)) '' Set.Icc 0 1)
    (Set.image.{u_1, u_5} (α := R) (⇑(f.comp (lineMap x y)) : (a : R) → P') (Set.Icc 0 1))

Tactic:
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
x y : P
v : V
⊢ (fun (x : P) ↦ v +ᵥ x) '' affineSegment R x y = affineSegment R (v +ᵥ x) (v +ᵥ y)

Tactic:
affineSegment_image (AffineEquiv.constVAdd R P v : P →ᵃ[R] P) x y

Premises used: AffineEquiv.constVAdd, AffineEquiv.toAffineMap, affineSegment_image
-- 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
x y : V
p : P
⊢ (fun (x : V) ↦ x +ᵥ p) '' affineSegment R x y = affineSegment R (x +ᵥ p) (y +ᵥ p)

Tactic:
affineSegment_image (AffineEquiv.vaddConst R p : V →ᵃ[R] P) x y

Premises used: AffineEquiv.vaddConst, AffineEquiv.toAffineMap, affineSegment_image
-- 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
x y p : P
⊢ (fun (x : P) ↦ p -ᵥ x) '' affineSegment R x y = affineSegment R (p -ᵥ x) (p -ᵥ y)

Tactic:
affineSegment_image (AffineEquiv.constVSub R p : P →ᵃ[R] V) x y

Premises used: AffineEquiv.constVSub, AffineEquiv.toAffineMap, affineSegment_image
-- 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
x y p : P
⊢ (fun (x : P) ↦ x -ᵥ p) '' affineSegment R x y = affineSegment R (x -ᵥ p) (y -ᵥ p)

Tactic:
affineSegment_image ((AffineEquiv.vaddConst R p).symm : P →ᵃ[R] V) x y

Premises used: AffineEquiv.vaddConst, AffineEquiv.symm, AffineEquiv.toAffineMap, affineSegment_image
-- 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
x y z : P
v : V
rw : Membership.mem (γ := Set P) ((fun (x : P) ↦ v +ᵥ x) '' affineSegment R x y) (v +ᵥ z) ↔ z ∈ affineSegment R x y
rw₁ rw₂ : z ∈ affineSegment R x y ↔ z ∈ affineSegment R x y
⊢ v +ᵥ z ∈ affineSegment R (v +ᵥ x) (v +ᵥ y) ↔ z ∈ affineSegment R x y

Tactic:
rw [← affineSegment_const_vadd_image, (AddAction.injective v).mem_set_image]

Premises used: affineSegment_const_vadd_image, AddAction.injective, Function.Injective.mem_set_image
-- 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
x y z : V
p : P
rw : Membership.mem (γ := Set P) ((fun (x : V) ↦ x +ᵥ p) '' affineSegment R x y) (z +ᵥ p) ↔ z ∈ affineSegment R x y
rw₁ rw₂ : z ∈ affineSegment R x y ↔ z ∈ affineSegment R x y
⊢ z +ᵥ p ∈ affineSegment R (x +ᵥ p) (y +ᵥ p) ↔ z ∈ affineSegment R x y

Tactic:
rw [← affineSegment_vadd_const_image, (vadd_right_injective p).mem_set_image]

Premises used: affineSegment_vadd_const_image, vadd_right_injective, Function.Injective.mem_set_image
-- 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
x y z p : P
rw : Membership.mem (γ := Set V) ((fun (x : P) ↦ p -ᵥ x) '' affineSegment R x y) (p -ᵥ z) ↔ z ∈ affineSegment R x y
rw₁ rw₂ : z ∈ affineSegment R x y ↔ z ∈ affineSegment R x y
⊢ p -ᵥ z ∈ affineSegment R (p -ᵥ x) (p -ᵥ y) ↔ z ∈ affineSegment R x y

Tactic:
rw [← affineSegment_const_vsub_image, (vsub_right_injective p).mem_set_image]

Premises used: vsub_right_injective, affineSegment_const_vsub_image, Function.Injective.mem_set_image
-- 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
x y z p : P
rw : Membership.mem (γ := Set V) ((fun (x : P) ↦ x -ᵥ p) '' affineSegment R x y) (z -ᵥ p) ↔ z ∈ affineSegment R x y
rw₁ rw₂ : z ∈ affineSegment R x y ↔ z ∈ affineSegment R x y
⊢ z -ᵥ p ∈ affineSegment R (x -ᵥ p) (y -ᵥ p) ↔ z ∈ affineSegment R x y

Tactic:
rw [← affineSegment_vsub_const_image, (vsub_left_injective p).mem_set_image]

Premises used: vsub_left_injective, affineSegment_vsub_const_image, Function.Injective.mem_set_image
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : IsOrderedRing R
x y : V
rw : affineSegment R x y = Set.image.{u_1, u_2} (α := R) (⇑(lineMap x y) : (a : R) → V) (Set.Icc 0 1)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := Set V) (Set.image.{u_1, u_2} (α := R) (⇑(lineMap x y) : (a : R) → V) (Set.Icc 0 1))
    (Set.image.{u_1, u_2} (α := R) (⇑(lineMap x y) : (a : R) → V) (Set.Icc 0 1))
⊢ affineSegment R x y = segment R x y

Tactic:
rw [segment_eq_image_lineMap, affineSegment]

Premises used: affineSegment, segment_eq_image_lineMap
-- 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
x y : P
⊢ affineSegment R x y = affineSegment R y x

Tactic:
Set.ext fun z => ?_

Premises used: Set.ext
-- 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
x y : P
refine : ∀ (z : P), z ∈ affineSegment R x y ↔ z ∈ affineSegment R y x
⊢ affineSegment R x y = affineSegment R y x

Tactic:
refine Set.ext fun z => ?_

Premises used: Set.ext
-- 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
x y z : P
mp : z ∈ affineSegment R x y → z ∈ affineSegment R y x
mpr : z ∈ affineSegment R y x → z ∈ affineSegment R x y
⊢ z ∈ affineSegment R x y ↔ z ∈ affineSegment R y x

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 : AddTorsor V P
inst_5 : IsOrderedRing R
x y z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hxy : (lineMap x y : (a : R) → P) t = z
⊢ z ∈ affineSegment R y x

Tactic:
⟨1 - t, ?_, ?_⟩

Premises used: affineSegment, Set.Mem, setOf, HSub.hSub, And.intro, Exists.intro, Set.image, OfNat.ofNat
-- 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
x y z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hxy : (lineMap x y : (a : R) → P) t = z
mp : Membership.mem (γ := Set R) (Set.Icc 0 1) (1 - t)
mp₁ : (lineMap y x : (a : R) → P) (1 - t) = z
⊢ z ∈ affineSegment R y x

Tactic:
refine ⟨1 - t, ?_, ?_⟩
-- 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
x y z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hxy : (lineMap x y : (a : R) → P) t = z
mp : t ∈ Set.Icc (HSub.hSub (α := R) 1 1) (HSub.hSub (α := R) 1 0)
mp₁ : t ∈ Set.Icc 0 (HSub.hSub (α := R) 1 0)
mp₂ mp₃ mp₄ mp₅ : Membership.mem (γ := Set R) (Set.Icc 0 1) t
⊢ Membership.mem (γ := Set R) (Set.Icc 0 1) (1 - t)

Tactic:
rwa [Set.sub_mem_Icc_iff_right, sub_self, sub_zero]

Premises used: sub_self, sub_zero, Set.sub_mem_Icc_iff_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
x y z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hxy mp mp₁ mp₂ mp₃ : (lineMap x y : (a : R) → P) t = z
⊢ (lineMap y x : (a : R) → P) (1 - t) = z

Tactic:
rwa [lineMap_apply_one_sub]

Premises used: AffineMap.lineMap_apply_one_sub
-- 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
x y z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hxy : (lineMap y x : (a : R) → P) t = z
⊢ z ∈ affineSegment R x y

Tactic:
⟨1 - t, ?_, ?_⟩

Premises used: affineSegment, Set.Mem, setOf, HSub.hSub, And.intro, Exists.intro, Set.image, OfNat.ofNat
-- 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
x y z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hxy : (lineMap y x : (a : R) → P) t = z
mpr : Membership.mem (γ := Set R) (Set.Icc 0 1) (1 - t)
mpr₁ : (lineMap x y : (a : R) → P) (1 - t) = z
⊢ z ∈ affineSegment R x y

Tactic:
refine ⟨1 - t, ?_, ?_⟩
-- 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
x y z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hxy : (lineMap y x : (a : R) → P) t = z
mpr : t ∈ Set.Icc (HSub.hSub (α := R) 1 1) (HSub.hSub (α := R) 1 0)
mpr₁ : t ∈ Set.Icc 0 (HSub.hSub (α := R) 1 0)
mpr₂ mpr₃ mpr₄ mpr₅ : Membership.mem (γ := Set R) (Set.Icc 0 1) t
⊢ Membership.mem (γ := Set R) (Set.Icc 0 1) (1 - t)

Tactic:
rwa [Set.sub_mem_Icc_iff_right, sub_self, sub_zero]

Premises used: sub_self, sub_zero, Set.sub_mem_Icc_iff_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
x y z : P
t : R
ht : Membership.mem (γ := Set R) (Set.Icc 0 1) t
hxy mpr mpr₁ mpr₂ mpr₃ : (lineMap y x : (a : R) → P) t = z
⊢ (lineMap x y : (a : R) → P) (1 - t) = z

Tactic:
rwa [lineMap_apply_one_sub]

Premises used: AffineMap.lineMap_apply_one_sub
-- 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
x y : P
⊢ x ∈ affineSegment R x y

Tactic:
⟨0, Set.left_mem_Icc.2 zero_le_one, lineMap_apply_zero _ _⟩

Premises used: affineSegment, Iff.mpr, Set.Mem, setOf, AffineMap.lineMap_apply_zero, zero_le_one, Set.left_mem_Icc, And.intro, Exists.intro, Set.image, OfNat.ofNat
-- 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
x y : P
⊢ y ∈ affineSegment R x y

Tactic:
⟨1, Set.right_mem_Icc.2 zero_le_one, lineMap_apply_one _ _⟩

Premises used: affineSegment, Iff.mpr, Set.right_mem_Icc, Set.Mem, setOf, zero_le_one, AffineMap.lineMap_apply_one, And.intro, Exists.intro, Set.image, OfNat.ofNat
-- 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
x : P
simp_rw : Eq (α := Set P) (Set.image.{u_1, u_4} (α := R) (⇑(lineMap x x) : (a : R) → P) (Set.Icc 0 1)) {x}
simp_rw₁ : Eq (α := Set P) ((fun (a : R) ↦ (const R R x : (a : R) → P) a) '' Set.Icc 0 1) {x}
simp_rw₂ : Eq (α := Set P) ((fun (a : R) ↦ Function.const R x a) '' Set.Icc 0 1) {x}
simp_rw₃ : Eq (α := Set P) ((fun (a : R) ↦ x) '' Set.Icc 0 1) {x}
⊢ affineSegment R x x = {x}

Tactic:
simp_rw [affineSegment, lineMap_same, AffineMap.coe_const, Function.const,
    (Set.nonempty_Icc.mpr zero_le_one).image_const]

Premises used: affineSegment, Iff.mpr, Set.Nonempty.image_const, Set.nonempty_Icc, AffineMap.coe_const, zero_le_one, AffineMap.lineMap_same, Function.const
-- Module: Mathlib.Analysis.Convex.Between
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : IsOrderedRing R
x y z : V
rw : y ∈ segment R x z ↔ y ∈ affineSegment R x z
rw₁ rw₂ : y ∈ segment R x z ↔ y ∈ segment R x z
⊢ y ∈ segment R x z ↔ Wbtw R x y z

Tactic:
rw [Wbtw, affineSegment_eq_segment]

Premises used: Wbtw, affineSegment_eq_segment