awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_7
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : Nontrivial 𝕜
inst_11 : SMulPosStrictMono R 𝕜
x y z : E
a b : R
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : a • x + b • y = z
⊢ 0 < HSMul.hSMul (β := 𝕜) a 1

Tactic:
zero_smul R (1 : 𝕜) ▸ smul_lt_smul_of_pos_right ‹_› zero_lt_one

Premises used: Eq.rec, smul_lt_smul_of_pos_right, zero_lt_one, zero_smul, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_7
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : Nontrivial 𝕜
inst_11 : SMulPosStrictMono R 𝕜
x y z : E
a b : R
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : a • x + b • y = z
⊢ 0 < HSMul.hSMul (β := 𝕜) a 1

Tactic:
exact zero_smul R (1 : 𝕜) ▸ smul_lt_smul_of_pos_right ‹_› zero_lt_one
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_7
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : Nontrivial 𝕜
inst_11 : SMulPosStrictMono R 𝕜
x y z : E
a b : R
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : a • x + b • y = z
⊢ 0 < HSMul.hSMul (β := 𝕜) b 1

Tactic:
zero_smul R (1 : 𝕜) ▸ smul_lt_smul_of_pos_right ‹_› zero_lt_one

Premises used: Eq.rec, smul_lt_smul_of_pos_right, zero_lt_one, zero_smul, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_7
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : Nontrivial 𝕜
inst_11 : SMulPosStrictMono R 𝕜
x y z : E
a b : R
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : a • x + b • y = z
⊢ 0 < HSMul.hSMul (β := 𝕜) b 1

Tactic:
exact zero_smul R (1 : 𝕜) ▸ smul_lt_smul_of_pos_right ‹_› zero_lt_one
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ZeroLEOneClass 𝕜
inst_6 : Nontrivial 𝕜
inst_7 : DenselyOrdered 𝕜
x z : E
h : z ∈ openSegment 𝕜 x x
a b : 𝕜
left : 0 < a
left_1 : 0 < b
hab : a + b = 1
hz : a • x + b • x = z
⊢ Membership.mem (γ := Set E) {x} z

Tactic:
simpa only [← add_smul, mem_singleton_iff, hab, one_smul, eq_comm] using hz

Premises used: eq_comm, one_smul, Set.mem_singleton_iff, add_smul
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ZeroLEOneClass 𝕜
inst_6 : Nontrivial 𝕜
inst_7 : DenselyOrdered 𝕜
x z : E
h : z = x
obtain : ∀ (a : 𝕜) (ha₀ : 0 < a) (ha₁ : a < 1), z ∈ openSegment 𝕜 x x
⊢ z ∈ openSegment 𝕜 x x

Tactic:
obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one

Premises used: zero_lt_one, OfNat.ofNat, DenselyOrdered.dense
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ZeroLEOneClass 𝕜
inst_6 : Nontrivial 𝕜
inst_7 : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ z ∈ openSegment 𝕜 x x

Tactic:
⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel _ _, ?_⟩

Premises used: Set.Mem, setOf, HSub.hSub, add_sub_cancel, And.intro, Exists.intro, openSegment, OfNat.ofNat, sub_pos_of_lt
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ZeroLEOneClass 𝕜
inst_6 : Nontrivial 𝕜
inst_7 : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
refine : a • x + (1 - a) • x = z
⊢ z ∈ openSegment 𝕜 x x

Tactic:
refine ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel _ _, ?_⟩
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ZeroLEOneClass 𝕜
inst_6 : Nontrivial 𝕜
inst_7 : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
rw : (a + (1 - a)) • x = z
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x = z
rw₂ : x = z
rw₃ rw₄ : x = x
⊢ a • x + (1 - a) • x = z

Tactic:
rw [← add_smul, add_sub_cancel, one_smul, h]

Premises used: one_smul, add_smul, add_sub_cancel
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y x_1 : E
h : x_1 ∈ [x -[𝕜] y]
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hz : a • x + b • y = x_1
⊢ (fun (θ : 𝕜) ↦ (a + b - θ) • x + θ • y) b = a • x + b • y

Tactic:
simp only [add_sub_cancel_right]

Premises used: add_sub_cancel_right
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y x_1 : E
h : x_1 ∈ openSegment 𝕜 x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = x_1
⊢ (fun (θ : 𝕜) ↦ (a + b - θ) • x + θ • y) b = a • x + b • y

Tactic:
simp only [add_sub_cancel_right]

Premises used: add_sub_cancel_right
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
⊢ [x -[𝕜] y] = (fun (θ : 𝕜) ↦ (1 - θ) • x + θ • y) '' Icc 0 1

Tactic:
segment_eq_image 𝕜 x y

Premises used: segment_eq_image
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
h : ∀ (a : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) a → x + a • (y - x) = (1 - a) • x + a • y
⊢ [x -[𝕜] y] = (fun (θ : 𝕜) ↦ x + θ • (y - x)) '' Icc 0 1

Tactic:
convert! segment_eq_image 𝕜 x y using 2

Premises used: segment_eq_image
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
a : 𝕜
h_1 : Membership.mem (γ := Set 𝕜) (Icc 0 1) a
h : x + (a • y - a • x) = x - a • x + a • y
⊢ x + a • (y - x) = (1 - a) • x + a • y

Tactic:
simp only [smul_sub, sub_smul, one_smul]

Premises used: sub_smul, one_smul, smul_sub
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
a : 𝕜
h : Membership.mem (γ := Set 𝕜) (Icc 0 1) a
⊢ x + (a • y - a • x) = x - a • x + a • y

Tactic:
abel
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
⊢ openSegment 𝕜 x y = (fun (θ : 𝕜) ↦ (1 - θ) • x + θ • y) '' Ioo 0 1

Tactic:
openSegment_eq_image 𝕜 x y

Premises used: openSegment_eq_image
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
h : ∀ (a : 𝕜), Membership.mem (γ := Set 𝕜) (Ioo 0 1) a → x + a • (y - x) = (1 - a) • x + a • y
⊢ openSegment 𝕜 x y = (fun (θ : 𝕜) ↦ x + θ • (y - x)) '' Ioo 0 1

Tactic:
convert! openSegment_eq_image 𝕜 x y using 2

Premises used: openSegment_eq_image
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
a : 𝕜
h_1 : Membership.mem (γ := Set 𝕜) (Ioo 0 1) a
h : x + (a • y - a • x) = x - a • x + a • y
⊢ x + a • (y - x) = (1 - a) • x + a • y

Tactic:
simp only [smul_sub, sub_smul, one_smul]

Premises used: sub_smul, one_smul, smul_sub
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
a : 𝕜
h : Membership.mem (γ := Set 𝕜) (Ioo 0 1) a
⊢ x + (a • y - a • x) = x - a • x + a • y

Tactic:
abel
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
h : ∀ (a : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) a → (AffineMap.lineMap x y : (a : 𝕜) → E) a = (1 - a) • x + a • y
⊢ [x -[𝕜] y] = image.{u_1, u_2} (α := 𝕜) (⇑(AffineMap.lineMap x y) : (a : 𝕜) → E) (Icc 0 1)

Tactic:
convert! segment_eq_image 𝕜 x y using 2

Premises used: segment_eq_image
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
a : 𝕜
h : Membership.mem (γ := Set 𝕜) (Icc 0 1) a
⊢ (AffineMap.lineMap x y : (a : 𝕜) → E) a = (1 - a) • x + a • y

Tactic:
AffineMap.lineMap_apply_module _ _ _

Premises used: AffineMap.lineMap_apply_module
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
a : 𝕜
h : Membership.mem (γ := Set 𝕜) (Icc 0 1) a
⊢ (AffineMap.lineMap x y : (a : 𝕜) → E) a = (1 - a) • x + a • y

Tactic:
exact AffineMap.lineMap_apply_module _ _ _

Premises used: AffineMap.lineMap_apply_module
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
h : ∀ (a : 𝕜), Membership.mem (γ := Set 𝕜) (Ioo 0 1) a → (AffineMap.lineMap x y : (a : 𝕜) → E) a = (1 - a) • x + a • y
⊢ openSegment 𝕜 x y = image.{u_1, u_2} (α := 𝕜) (⇑(AffineMap.lineMap x y) : (a : 𝕜) → E) (Ioo 0 1)

Tactic:
convert! openSegment_eq_image 𝕜 x y using 2

Premises used: openSegment_eq_image
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
a : 𝕜
h : Membership.mem (γ := Set 𝕜) (Ioo 0 1) a
⊢ (AffineMap.lineMap x y : (a : 𝕜) → E) a = (1 - a) • x + a • y

Tactic:
AffineMap.lineMap_apply_module _ _ _

Premises used: AffineMap.lineMap_apply_module
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
a : 𝕜
h : Membership.mem (γ := Set 𝕜) (Ioo 0 1) a
⊢ (AffineMap.lineMap x y : (a : 𝕜) → E) a = (1 - a) • x + a • y

Tactic:
exact AffineMap.lineMap_apply_module _ _ _

Premises used: AffineMap.lineMap_apply_module
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a b : E
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Ioo 0 1) t
⊢ Membership.mem (α := E) (openSegment 𝕜 a b) ((AffineMap.lineMap a b : (a : 𝕜) → E) t : E)

Tactic:
openSegment_eq_image_lineMap 𝕜 a b ▸ mem_image_of_mem _ ht

Premises used: Eq.rec, openSegment_eq_image_lineMap, Set.mem_image_of_mem, Eq.symm
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a b : E
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Icc 0 1) t
⊢ Membership.mem (α := E) [a -[𝕜] b] ((AffineMap.lineMap a b : (a : 𝕜) → E) t : E)

Tactic:
segment_eq_image_lineMap 𝕜 a b ▸ mem_image_of_mem _ ht

Premises used: Eq.rec, Set.mem_image_of_mem, segment_eq_image_lineMap, Eq.symm
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 E
inst_6 : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
simp_rw :
  Membership.mem (γ := Set F)
      (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F)
        (image.{u_1, u_2} (α := 𝕜) (⇑(AffineMap.lineMap a b) : (a : 𝕜) → E) (Icc 0 1)))
      x ↔
    Membership.mem (γ := Set F)
      (image.{u_1, u_3} (α := 𝕜)
        (⇑(AffineMap.lineMap ((f : (a : E) → F) a) ((f : (a : E) → F) b) : 𝕜 →ᵃ[𝕜] F) : (a : 𝕜) → F) (Icc 0 1))
      x
simp_rw₁ :
  (∃ (x_1 : E),
      (∃ (x : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x ∧ (AffineMap.lineMap a b : (a : 𝕜) → E) x = x_1) ∧
        (f : (a : E) → F) x_1 = x) ↔
    ∃ (x_1 : 𝕜),
      Membership.mem (γ := Set 𝕜) (Icc 0 1) x_1 ∧
        ((AffineMap.lineMap ((f : (a : E) → F) a) ((f : (a : E) → F) b) : 𝕜 →ᵃ[𝕜] F) : (a : 𝕜) → F) x_1 = x
simp_rw₂ :
  (∃ (a_1 : 𝕜),
      Membership.mem (γ := Set 𝕜) (Icc 0 1) a_1 ∧
        (f : (a : E) → F) ((AffineMap.lineMap a b : (a : 𝕜) → E) a_1 : E) = x) ↔
    ∃ (x_1 : 𝕜),
      Membership.mem (γ := Set 𝕜) (Icc 0 1) x_1 ∧
        ((AffineMap.lineMap ((f : (a : E) → F) a) ((f : (a : E) → F) b) : 𝕜 →ᵃ[𝕜] F) : (a : 𝕜) → F) x_1 = x
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' [a -[𝕜] b]) x ↔
    Membership.mem (γ := Set F) ([(f : (a : E) → F) a -[𝕜] (f : (a : E) → F) b] : Set F) x

Tactic:
simp_rw [segment_eq_image_lineMap, mem_image, exists_exists_and_eq_and, AffineMap.apply_lineMap]

Premises used: AffineMap.apply_lineMap, Set.mem_image, exists_exists_and_eq_and, segment_eq_image_lineMap
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
G : Type u_4
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup G
inst_5 : Module 𝕜 E
inst_6 : AddTorsor G E
inst_7 : VAddCommClass G E E
a : G
b c : E
⊢ a +ᵥ [b -[𝕜] c] = [a +ᵥ b -[𝕜] a +ᵥ c]

Tactic:
#adaptation_note /-- Prior to https://github.com/leanprover/lean4/pull/12286/
  we didn't need this `let` statement. -/
  let : AddTorsor E E := addGroupIsAddTorsor E
  image_segment 𝕜 ⟨_, LinearMap.id, fun _ _ => vadd_comm _ _ _⟩ b c

Premises used: LinearMap.id, AffineMap.mk, VAddCommClass.vadd_comm, addGroupIsAddTorsor, HVAdd.hVAdd, image_segment
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
G : Type u_4
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : AddCommGroup G
inst_5 : Module 𝕜 E
inst_6 : AddTorsor G E
inst_7 : VAddCommClass G E E
a : G
b c : E
⊢ a +ᵥ openSegment 𝕜 b c = openSegment 𝕜 (a +ᵥ b) (a +ᵥ c)

Tactic:
#adaptation_note /-- Prior to https://github.com/leanprover/lean4/pull/12286/
  we didn't need this `let` statement. -/
  let : AddTorsor E E := addGroupIsAddTorsor E
  image_openSegment 𝕜 ⟨_, LinearMap.id, fun _ _ => vadd_comm _ _ _⟩ b c

Premises used: LinearMap.id, AffineMap.mk, VAddCommClass.vadd_comm, image_openSegment, addGroupIsAddTorsor, HVAdd.hVAdd
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a x b c : E
simp_rw : a +ᵥ x ∈ [a +ᵥ b -[𝕜] a +ᵥ c] ↔ x ∈ [b -[𝕜] c]
simp_rw₁ : a +ᵥ x ∈ a +ᵥ [b -[𝕜] c] ↔ x ∈ [b -[𝕜] c]
⊢ a + x ∈ [a + b -[𝕜] a + c] ↔ x ∈ [b -[𝕜] c]

Tactic:
simp_rw [← vadd_eq_add, ← vadd_segment, vadd_mem_vadd_set_iff]

Premises used: Set.vadd_mem_vadd_set_iff, vadd_segment, vadd_eq_add
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a x b c : E
simp_rw : a +ᵥ x ∈ openSegment 𝕜 (a +ᵥ b) (a +ᵥ c) ↔ x ∈ openSegment 𝕜 b c
simp_rw₁ : a +ᵥ x ∈ a +ᵥ openSegment 𝕜 b c ↔ x ∈ openSegment 𝕜 b c
⊢ a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c

Tactic:
simp_rw [← vadd_eq_add, ← vadd_openSegment, vadd_mem_vadd_set_iff]

Premises used: Set.vadd_mem_vadd_set_iff, vadd_openSegment, vadd_eq_add
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a b c : E
⊢ (fun (x : E) ↦ a + x) ⁻¹' [a + b -[𝕜] a + c] = [b -[𝕜] c]

Tactic:
Set.ext fun _ => mem_segment_translate 𝕜 a

Premises used: Set.ext, mem_segment_translate
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a b c : E
⊢ (fun (x : E) ↦ a + x) ⁻¹' openSegment 𝕜 (a + b) (a + c) = openSegment 𝕜 b c

Tactic:
Set.ext fun _ => mem_openSegment_translate 𝕜 a

Premises used: Set.ext, mem_openSegment_translate
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
z : E
this : ∀ (hzt : z ∈ [c -[𝕜] x]) (hzs : z ∈ [c -[𝕜] y]), Membership.mem (γ := Set E) {c} z
⊢ z ∈ [c -[𝕜] x] ∩ [c -[𝕜] y] → Membership.mem (γ := Set E) {c} z

Tactic:
⟨hzt, hzs⟩
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
z : E
hzt : z ∈ [c -[𝕜] x]
hzs : z ∈ [c -[𝕜] y]
⊢ ∃ (x_1 : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x_1 ∧ (1 - x_1) • c + x_1 • x = z

Tactic:
rw [segment_eq_image, mem_image] at hzt hzs

Premises used: Set.mem_image, segment_eq_image
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
z : E
hzt : z ∈ [c -[𝕜] x]
hzs : z ∈ [c -[𝕜] y]
hzt₁ : ∃ (x_1 : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x_1 ∧ (1 - x_1) • c + x_1 • x = z
⊢ ∃ (x : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x ∧ (1 - x) • c + x • y = z

Tactic:
rw [segment_eq_image, mem_image] at hzt hzs

Premises used: Set.mem_image, segment_eq_image
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
z : E
hzt : ∃ (x_1 : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x_1 ∧ (1 - x_1) • c + x_1 • x = z
hzs : ∃ (x : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x ∧ (1 - x) • c + x • y = z
rcases :
  ∀ (p : 𝕜) (p0 : 0 ≤ p) (p1 : p ≤ 1)
    (hzs : ∃ (x_1 : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x_1 ∧ (1 - x_1) • c + x_1 • y = (1 - p) • c + p • x),
    Membership.mem (γ := Set E) {c} ((1 - p) • c + p • x)
⊢ Membership.mem (γ := Set E) {c} z

Tactic:
rcases hzt with ⟨p, ⟨p0, p1⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
hzs : ∃ (x_1 : 𝕜), Membership.mem (γ := Set 𝕜) (Icc 0 1) x_1 ∧ (1 - x_1) • c + x_1 • y = (1 - p) • c + p • x
rcases :
  ∀ (q : 𝕜) (H : (1 - q) • c + q • y = (1 - p) • c + p • x) (q0 : 0 ≤ q) (q1 : q ≤ 1),
    Membership.mem (γ := Set E) {c} ((1 - p) • c + p • x)
⊢ Membership.mem (γ := Set E) {c} ((1 - p) • c + p • x)

Tactic:
rcases hzs with ⟨q, ⟨q0, q1⟩, H⟩
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + q • y = (1 - p) • c + p • x
q0 : 0 ≤ q
q1 : q ≤ 1
⊢ x = x - c + c

Tactic:
abel
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + q • y = (1 - p) • c + p • x
q0 : 0 ≤ q
q1 : q ≤ 1
⊢ x = x - c + c

Tactic:
have Hx : x = (x - c) + c := by abel
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + q • y = (1 - p) • c + p • x
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
⊢ y = y - c + c

Tactic:
abel
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + q • y = (1 - p) • c + p • x
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
⊢ y = y - c + c

Tactic:
have Hy : y = (y - c) + c := by abel
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + q • y = (1 - p) • c + p • x
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
⊢ (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)

Tactic:
rw [Hx, Hy, smul_add, smul_add] at H

Premises used: smul_add
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + q • y = (1 - p) • c + p • x
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
H₁ : (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)
⊢ 0 ≤ q

Tactic:
rw [Hx, Hy, smul_add, smul_add] at H

Premises used: smul_add
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + q • y = (1 - p) • c + p • x
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
H₁ : (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)
q0₁ : 0 ≤ q
⊢ q ≤ 1

Tactic:
rw [Hx, Hy, smul_add, smul_add] at H

Premises used: smul_add
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + q • y = (1 - p) • c + p • x
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
H₁ : (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)
q0₁ : 0 ≤ q
q1₁ : q ≤ 1
⊢ x = x - c + c

Tactic:
rw [Hx, Hy, smul_add, smul_add] at H

Premises used: smul_add
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + q • y = (1 - p) • c + p • x
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
H₁ : (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)
q0₁ : 0 ≤ q
q1₁ : q ≤ 1
Hx₁ : x = x - c + c
⊢ y = y - c + c

Tactic:
rw [Hx, Hy, smul_add, smul_add] at H

Premises used: smul_add