awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_card : HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1 ≤ F.encard
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : (↑I : Set (Set E)) ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
obtain :
  ∀ (J : Set (Set E)),
    (↑I : Set (Set E)) ⊆ J →
      ∀ (hJ_ss : J ⊆ F) (hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1),
        (⋂₀ (↑I : Set (Set E))).Nonempty
⊢ (⋂₀ (↑I : Set (Set E))).Nonempty

Tactic:
obtain ⟨J, _, hJ_ss, hJ_card⟩ := exists_superset_subset_encard_eq hI_ss (hkt := h_card)
    (by simpa only [encard_coe_eq_coe_finsetCard, ← ENat.coe_one, ← ENat.coe_add, Nat.cast_le])

Premises used: Set.exists_superset_subset_encard_eq
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_card : HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1 ≤ F.encard
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : (↑I : Set (Set E)) ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Set (Set E)
left : (↑I : Set (Set E)) ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1
⊢ (↑I : Set (Set E)) ⊆ J

Tactic:
simpa [hI_ss]
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_card : HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1 ≤ F.encard
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : (↑I : Set (Set E)) ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Set (Set E)
left : (↑I : Set (Set E)) ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1
apply : (⋂₀ J).Nonempty
⊢ (⋂₀ (↑I : Set (Set E))).Nonempty

Tactic:
apply Set.Nonempty.mono <| sInter_mono (by simpa [hI_ss])

Premises used: Set.Nonempty.mono, Set.sInter_mono
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_card : HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1 ≤ F.encard
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : (↑I : Set (Set E)) ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Set (Set E)
left : (↑I : Set (Set E)) ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1
have : ∀ (hJ_fin : Fintype (↑J : Type u_3)), (⋂₀ J).Nonempty
⊢ (⋂₀ J).Nonempty

Tactic:
have hJ_fin : Fintype J := Finite.fintype <| finite_of_encard_eq_coe hJ_card
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_card : HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1 ≤ F.encard
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : (↑I : Set (Set E)) ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Set (Set E)
left : (↑I : Set (Set E)) ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1
hJ_fin : Fintype (↑J : Type u_3)
J' : Finset (Set E) := J.toFinset
rw : (⋂₀ (↑J.toFinset : Set (Set E))).Nonempty
⊢ (⋂₀ J).Nonempty

Tactic:
rw [← coe_toFinset J]

Premises used: Set.coe_toFinset
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_card : HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1 ≤ F.encard
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : (↑I : Set (Set E)) ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Set (Set E)
left : (↑I : Set (Set E)) ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1
hJ_fin : Fintype (↑J : Type u_3)
J' : Finset (Set E) := J.toFinset
a : (↑J' : Set (Set E)) ⊆ F
a₁ : #J' = finrank 𝕜 E + 1
⊢ (⋂₀ (↑J.toFinset : Set (Set E))).Nonempty

Tactic:
apply h_inter J'
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_card : HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1 ≤ F.encard
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : (↑I : Set (Set E)) ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Set (Set E)
left : (↑I : Set (Set E)) ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1
hJ_fin : Fintype (↑J : Type u_3)
J' : Finset (Set E) := J.toFinset
⊢ (↑J' : Set (Set E)) ⊆ F

Tactic:
simpa [J']
-- Module: Mathlib.Analysis.Convex.Radon
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
inst_6 : TopologicalSpace E
inst_7 : T2Space E
F : Set (Set E)
h_card : HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1 ≤ F.encard
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_compact : ∀ X ∈ F, IsCompact X
h_inter : ∀ (G : Finset (Set E)), (↑G : Set (Set E)) ⊆ F → #G = finrank 𝕜 E + 1 → (⋂₀ (↑G : Set (Set E))).Nonempty
I : Finset (Set E)
hI_ss : (↑I : Set (Set E)) ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Set (Set E)
left : (↑I : Set (Set E)) ⊆ J
hJ_ss : J ⊆ F
hJ_card : J.encard = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1
hJ_fin : Fintype (↑J : Type u_3)
J' : Finset (Set E) := J.toFinset
a :
  ∀ (hJ_card : (↑(#J.toFinset) : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) 1),
    let J' := J.toFinset;
    #J' = finrank 𝕜 E + 1
a₁ :
  ∀ (hJ_card : (↑(#J.toFinset) : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑(finrank 𝕜 E) : ℕ∞) (↑1 : ℕ∞)),
    let J' := J.toFinset;
    #J' = finrank 𝕜 E + 1
a₂ :
  ∀ (hJ_card : Eq (α := ℕ∞) (↑(#J.toFinset) : ℕ∞) (↑(finrank 𝕜 E + 1) : ℕ∞)),
    let J' := J.toFinset;
    #J' = finrank 𝕜 E + 1
a₃ a₄ a₅ a₆ :
  ∀ (hJ_card : #J.toFinset = finrank 𝕜 E + 1),
    let J' := J.toFinset;
    #J' = finrank 𝕜 E + 1
⊢ #J' = finrank 𝕜 E + 1

Tactic:
rwa [encard_eq_coe_toFinset_card J, ← ENat.coe_one, ← ENat.coe_add, Nat.cast_inj] at hJ_card

Premises used: ENat.coe_one, Nat.cast_inj, Set.encard_eq_coe_toFinset_card, ENat.coe_add
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x y : E
⊢ [x -[𝕜] y] = (fun (p : 𝕜 × 𝕜) ↦ p.1 • x + p.2 • y) '' {p : 𝕜 × 𝕜 | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}

Tactic:
simp only [segment, image, Prod.exists, mem_setOf_eq, and_assoc]

Premises used: Set.mem_setOf_eq, segment, and_assoc, Set.image, Prod.exists
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x y : E
⊢ openSegment 𝕜 x y = (fun (p : 𝕜 × 𝕜) ↦ p.1 • x + p.2 • y) '' {p : 𝕜 × 𝕜 | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}

Tactic:
simp only [openSegment, image, Prod.exists, mem_setOf_eq, and_assoc]

Premises used: Set.mem_setOf_eq, and_assoc, Set.image, openSegment, Prod.exists
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x y : E
⊢ [x -[𝕜] y] = [y -[𝕜] x]

Tactic:
Set.ext fun _ =>
    ⟨fun ⟨a, b, ha, hb, hab, H⟩ => ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩,
      fun ⟨a, b, ha, hb, hab, H⟩ =>
      ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩⟩

Premises used: Set.ext, _private.0.segment_symm.match_2, Membership.mem, segment, add_comm, And.intro, Iff.intro, Exists.intro, HSMul.hSMul, _private.0.segment_symm.match_1, Eq.trans
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x y : E
⊢ openSegment 𝕜 x y = openSegment 𝕜 y x

Tactic:
Set.ext fun _ =>
    ⟨fun ⟨a, b, ha, hb, hab, H⟩ => ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩,
      fun ⟨a, b, ha, hb, hab, H⟩ =>
      ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩⟩

Premises used: Set.ext, Membership.mem, _private.0.openSegment_symm.match_2, add_comm, And.intro, Iff.intro, Exists.intro, _private.0.openSegment_symm.match_1, HSMul.hSMul, openSegment, Eq.trans
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
x y : E
⊢ openSegment 𝕜 x y ⊆ [x -[𝕜] y]

Tactic:
fun _ ⟨a, b, ha, hb, hab, hz⟩ => ⟨a, b, ha.le, hb.le, hab, hz⟩

Premises used: Membership.mem, LT.lt.le, segment, Set.Subset, And.intro, Exists.intro, _private.0.openSegment_symm.match_1
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s : Set E
x y : E
⊢ [x -[𝕜] y] ⊆ s ↔ ∀ (a b : 𝕜), 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s

Tactic:
⟨fun H a b ha hb hab => H ⟨a, b, ha, hb, hab, rfl⟩, fun H _ ⟨a, b, ha, hb, hab, hz⟩ =>
    hz ▸ H a b ha hb hab⟩

Premises used: Membership.mem, Eq.rec, And.intro, Iff.intro, Exists.intro, _private.0.segment_symm.match_1, rfl
-- Module: Mathlib.Analysis.Convex.Segment
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : SMul 𝕜 E
s : Set E
x y : E
⊢ openSegment 𝕜 x y ⊆ s ↔ ∀ (a b : 𝕜), 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Tactic:
⟨fun H a b ha hb hab => H ⟨a, b, ha, hb, hab, rfl⟩, fun H _ ⟨a, b, ha, hb, hab, hz⟩ =>
    hz ▸ H a b ha hb hab⟩

Premises used: Membership.mem, Eq.rec, And.intro, Iff.intro, Exists.intro, _private.0.openSegment_symm.match_1, rfl
-- 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 : MulActionWithZero 𝕜 E
x y : E
rw : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + 0 = x
rw₁ : x + 0 = x
rw₂ rw₃ : x = x
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x

Tactic:
rw [zero_smul, one_smul, add_zero]

Premises used: one_smul, zero_smul, add_zero
-- 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 : MulActionWithZero 𝕜 E
x y : E
⊢ y ∈ [x -[𝕜] y]

Tactic:
segment_symm 𝕜 y x ▸ left_mem_segment 𝕜 y x

Premises used: left_mem_segment, segment_symm, Eq.rec
-- 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
x z : E
h : z ∈ [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 _ _ _).symm, mem_singleton_iff, hab, one_smul, eq_comm] using hz

Premises used: eq_comm, one_smul, Set.mem_singleton_iff, add_smul, Eq.symm
-- 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
x y : E
simp : [x -[𝕜] y] ⊆ insert x (insert y (openSegment 𝕜 x y))
⊢ insert x (insert y (openSegment 𝕜 x y)) = [x -[𝕜] y]

Tactic:
simp only [subset_antisymm_iff, insert_subset_iff, left_mem_segment, right_mem_segment,
    openSegment_subset_segment, true_and]

Premises used: left_mem_segment, openSegment_subset_segment, Set.insert_subset_iff, subset_antisymm_iff, right_mem_segment, true_and
-- 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
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ insert x (insert y (openSegment 𝕜 x y))

Tactic:
hb.eq_or_lt.imp ?_ fun hb' => ha.eq_or_lt.imp ?_ fun ha' => ?_

Premises used: LE.le.eq_or_lt, Set.insert, Set.Mem, setOf, Or.imp
-- 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
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_1 : 0 = b → a • x + b • y = x
refine_2 : ∀ (hb' : 0 < b), 0 = a → a • x + b • y = y
refine_3 : ∀ (hb' : 0 < b) (ha' : 0 < a), a • x + b • y ∈ openSegment 𝕜 x y
⊢ a • x + b • y ∈ insert x (insert y (openSegment 𝕜 x y))

Tactic:
refine hb.eq_or_lt.imp ?_ fun hb' => ha.eq_or_lt.imp ?_ fun ha' => ?_

Premises used: LE.le.eq_or_lt, Or.imp
-- 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
x y : E
a : 𝕜
ha : 0 ≤ a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a + 0 = 1
refine_1 : (a + 0) • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
refine_1₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
refine_1₂ : x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x
refine_1₃ : x + 0 = x
refine_1₄ refine_1₅ : x = x
⊢ a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y = x

Tactic:
rw [← add_zero a, hab, one_smul, zero_smul, add_zero]

Premises used: one_smul, zero_smul, add_zero
-- 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
x y : E
b : 𝕜
hb : 0 ≤ b
hb' : 0 < b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : 0 + b = 1
refine_2 : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + (0 + b) • y = y
refine_2₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y = y
refine_2₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + y = y
refine_2₃ : 0 + y = y
refine_2₄ refine_2₅ : y = y
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y = y

Tactic:
rw [← zero_add b, hab, one_smul, zero_smul, zero_add]

Premises used: zero_add, one_smul, zero_smul
-- 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
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
ha' : 0 < a
⊢ a • x + b • y ∈ openSegment 𝕜 x y

Tactic:
⟨a, b, ha', hb', hab, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, openSegment, rfl
-- 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
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
ha' : 0 < a
⊢ a • x + b • y ∈ openSegment 𝕜 x y

Tactic:
exact ⟨a, b, ha', hb', hab, rfl⟩
-- 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
x y z : E
hx : x ≠ z
hy : y ≠ z
hz : z ∈ [x -[𝕜] y]
⊢ z ∈ insert x (insert y (openSegment 𝕜 x y))

Tactic:
rw [← insert_endpoints_openSegment] at hz

Premises used: insert_endpoints_openSegment
-- 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
x y z : E
hx : x ≠ z
hy : y ≠ z
hz : z ∈ insert x (insert y (openSegment 𝕜 x y))
⊢ z ∈ openSegment 𝕜 x y

Tactic:
(hz.resolve_left hx.symm).resolve_left hy.symm

Premises used: Or.resolve_left, Ne.symm
-- 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
x y z : E
hx : x ≠ z
hy : y ≠ z
hz : z ∈ insert x (insert y (openSegment 𝕜 x y))
⊢ z ∈ openSegment 𝕜 x y

Tactic:
exact (hz.resolve_left hx.symm).resolve_left hy.symm

Premises used: Or.resolve_left, Ne.symm
-- 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
s : Set E
x y : E
hx : x ∈ s
hy : y ∈ s
⊢ openSegment 𝕜 x y ⊆ s ↔ [x -[𝕜] y] ⊆ s

Tactic:
simp only [← insert_endpoints_openSegment, insert_subset_iff, *, true_and]

Premises used: insert_endpoints_openSegment, Set.insert_subset_iff, true_and
-- 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 : SMulPosMono R 𝕜
x y z : E
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : a • x + b • y = z
⊢ HSMul.hSMul (β := 𝕜) a 1 + HSMul.hSMul (β := 𝕜) b 1 = 1

Tactic:
simpa [add_smul] using congr($(hab) • (1 : 𝕜))

Premises used: add_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 : SMulPosMono R 𝕜
x y z : E
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : a • x + b • y = z
⊢ HSMul.hSMul (β := 𝕜) a 1 • x + HSMul.hSMul (β := 𝕜) b 1 • y = z

Tactic:
simpa
-- 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 : SMulPosMono R 𝕜
x y z : E
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : a • x + b • y = z
refine_1 : 0 ≤ HSMul.hSMul (β := 𝕜) a 1
refine_2 : 0 ≤ HSMul.hSMul (β := 𝕜) b 1
⊢ z ∈ [x -[𝕜] y]

Tactic:
refine ⟨_, _, ?_, ?_, by simpa [add_smul] using congr($(hab) • (1 : 𝕜)), by simpa⟩
-- 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 : SMulPosMono 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_le_smul_of_nonneg_right ‹_› zero_le_one

Premises used: smul_le_smul_of_nonneg_right, Eq.rec, zero_le_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 : SMulPosMono 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_le_smul_of_nonneg_right ‹_› zero_le_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 : SMulPosMono 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_le_smul_of_nonneg_right ‹_› zero_le_one

Premises used: smul_le_smul_of_nonneg_right, Eq.rec, zero_le_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 : SMulPosMono 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_le_smul_of_nonneg_right ‹_› zero_le_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
⊢ HSMul.hSMul (β := 𝕜) a 1 + HSMul.hSMul (β := 𝕜) b 1 = 1

Tactic:
simpa [add_smul] using congr($(hab) • (1 : 𝕜))

Premises used: add_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
⊢ HSMul.hSMul (β := 𝕜) a 1 • x + HSMul.hSMul (β := 𝕜) b 1 • y = z

Tactic:
simpa
-- 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
refine_1 : 0 < HSMul.hSMul (β := 𝕜) a 1
refine_2 : 0 < HSMul.hSMul (β := 𝕜) b 1
⊢ z ∈ openSegment 𝕜 x y

Tactic:
refine ⟨_, _, ?_, ?_, by simpa [add_smul] using congr($(hab) • (1 : 𝕜)), by simpa⟩