awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
hc : ∀ t ⊆ s, s ∩ (convexHull 𝕜 : (a : Set E) → Set E) t ⊆ t
t : Set { x : E // x ∈ s }
x : { x : E // x ∈ s }
h :
  Membership.mem (γ := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (Subtype.val (p := fun (x : E) ↦ x ∈ s) '' t) : Set E) (↑x : E)
⊢ Membership.mem (γ := Set E) ((fun (a : { x : E // x ∈ s }) ↦ (↑a : E)) '' t) (↑x : E)

Tactic:
exact hc (t.image ((↑) : s → E)) (Subtype.coe_image_subset s t) ⟨x.prop, h⟩

Premises used: Subtype.coe_image_subset, Subtype.prop, And.intro, Set.image, Subtype.val
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
rw :
  (∀ t ⊆ s, s ∩ (convexHull 𝕜 : (a : Set E) → Set E) t ⊆ t) ↔
    ∀ x ∈ s, x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
⊢ ConvexIndependent.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) ↔
    ∀ x ∈ s, x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)

Tactic:
rw [convexIndependent_set_iff_inter_convexHull_subset]

Premises used: convexIndependent_set_iff_inter_convexHull_subset
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
mp :
  (∀ t ⊆ s, s ∩ (convexHull 𝕜 : (a : Set E) → Set E) t ⊆ t) →
    ∀ x ∈ s, x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
mpr :
  (∀ x ∈ s, x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)) →
    ∀ t ⊆ s, s ∩ (convexHull 𝕜 : (a : Set E) → Set E) t ⊆ t
⊢ (∀ t ⊆ s, s ∩ (convexHull 𝕜 : (a : Set E) → Set E) t ⊆ t) ↔
    ∀ x ∈ s, x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
hs : ∀ t ⊆ s, s ∩ (convexHull 𝕜 : (a : Set E) → Set E) t ⊆ t
x : E
hxs : x ∈ s
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E) x
⊢ False

Tactic:
(hs _ Set.diff_subset ⟨hxs, hx⟩).2 (Set.mem_singleton _)

Premises used: Set.mem_singleton, Set.diff_subset, And.right, And.intro
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
hs : ∀ t ⊆ s, s ∩ (convexHull 𝕜 : (a : Set E) → Set E) t ⊆ t
x : E
hxs : x ∈ s
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E) x
⊢ False

Tactic:
exact (hs _ Set.diff_subset ⟨hxs, hx⟩).2 (Set.mem_singleton _)

Premises used: Set.mem_singleton, Set.diff_subset, And.right, And.intro
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
hs : ∀ x ∈ s, x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
t : Set E
ht : t ⊆ s
x : E
hxs : x ∈ s
hxt : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) t : Set E) x
mpr : ∀ (h : x ∉ t), False
⊢ x ∈ t

Tactic:
by_contra h
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
hs : ∀ x ∈ s, x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
t : Set E
ht : t ⊆ s
x : E
hxs : x ∈ s
hxt : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) t : Set E) x
h : x ∉ t
⊢ False

Tactic:
hs _ hxs (convexHull_mono (Set.subset_diff_singleton ht h) hxt)

Premises used: convexHull_mono, Set.subset_diff_singleton
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
hs : ∀ x ∈ s, x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
t : Set E
ht : t ⊆ s
x : E
hxs : x ∈ s
hxt : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) t : Set E) x
h : x ∉ t
⊢ False

Tactic:
exact hs _ hxs (convexHull_mono (Set.subset_diff_singleton ht h) hxt)

Premises used: convexHull_mono, Set.subset_diff_singleton
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
⊢ ConvexIndependent 𝕜 p ↔
    ∀ (s : Finset ι) (x : ι),
      Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s

Tactic:
⟨fun hc s x hx => hc s x ?_, fun h s x hx => ?_⟩

Premises used: SetLike.coe, Iff.intro
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
refine_1 :
  ∀ (hc : ConvexIndependent 𝕜 p) (s : Finset ι) (x : ι)
    (hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x)),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (↑s : Set ι)) : Set E) (p x)
refine_2 :
  ∀
    (h :
      ∀ (s : Finset ι) (x : ι),
        Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s)
    (s : Set ι) (x : ι)
    (hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p x)), x ∈ s
⊢ ConvexIndependent 𝕜 p ↔
    ∀ (s : Finset ι) (x : ι),
      Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s

Tactic:
refine ⟨fun hc s x hx => hc s x ?_, fun h s x hx => ?_⟩
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Finset ι
x : ι
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x)
refine_1 refine_1₁ refine_1₂ refine_1₃ :
  ∀ (hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (↑s : Set ι)) : Set E) (p x)),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (↑s : Set ι)) : Set E) (p x)
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (↑s : Set ι)) : Set E) (p x)

Tactic:
rwa [Finset.coe_image] at hx

Premises used: Finset.coe_image
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p x)
a b : ι
hab : p a = p b
rw : Membership.mem (γ := Finset ι) {b} a
⊢ a = b

Tactic:
rw [← mem_singleton]

Premises used: Finset.mem_singleton
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p x)
a b : ι
hab : p a = p b
⊢ Membership.mem (γ := Finset ι) {b} a

Tactic:
h {b} a ?_

Premises used: Singleton.singleton
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p x)
a b : ι
hab : p a = p b
refine : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p {b}) : Set E) : Set E) (p a)
⊢ Membership.mem (γ := Finset ι) {b} a

Tactic:
refine h {b} a ?_

Premises used: Singleton.singleton
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p x)
a b : ι
hab : p a = p b
rw : Membership.mem (γ := Set E) {p b} (p b)
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p {b}) : Set E) : Set E) (p a)

Tactic:
rw [hab, image_singleton, coe_singleton, convexHull_singleton]

Premises used: Finset.coe_singleton, Finset.image_singleton, convexHull_singleton
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p x)
a b : ι
hab : p a = p b
⊢ Membership.mem (γ := Set E) {p b} (p b)

Tactic:
Set.mem_singleton _

Premises used: Set.mem_singleton
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p x)
a b : ι
hab : p a = p b
⊢ Membership.mem (γ := Set E) {p b} (p b)

Tactic:
exact Set.mem_singleton _

Premises used: Set.mem_singleton
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p x)
⊢ Injective p

Tactic:
have hp : Injective p := by
    rintro a b hab
    rw [← mem_singleton]
    refine h {b} a ?_
    rw [hab, image_singleton, coe_singleton, convexHull_singleton]
    exact Set.mem_singleton _
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p x)
hp : Injective p
⊢ Membership.mem (γ := Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ p '' s), (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E)) (p x)

Tactic:
rw [convexHull_eq_union_convexHull_finite_subsets] at hx

Premises used: convexHull_eq_union_convexHull_finite_subsets
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p x)
hp : Injective p
hx₁ :
  Membership.mem (γ := Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ p '' s), (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E)) (p x)
⊢ Injective p

Tactic:
rw [convexHull_eq_union_convexHull_finite_subsets] at hx

Premises used: convexHull_eq_union_convexHull_finite_subsets
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hx :
  Membership.mem (γ := Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ p '' s), (convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E)) (p x)
hp : Injective p
⊢ ∃ (i : Finset E) (_ : (↑i : Set E) ⊆ p '' s),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑i : Set E) : Set E) (p x)

Tactic:
simp_rw [Set.mem_iUnion] at hx

Premises used: Set.mem_iUnion
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hp : Injective p
hx :
  ∃ (i : Finset E) (_ : (↑i : Set E) ⊆ p '' s),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑i : Set E) : Set E) (p x)
refine_2 :
  ∀ (t : Finset E) (ht : (↑t : Set E) ⊆ p '' s)
    (hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) (p x)), x ∈ s
⊢ x ∈ s

Tactic:
obtain ⟨t, ht, hx⟩ := hx
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : (↑t : Set E) ⊆ p '' s
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) (p x)
refine_2 : p x ∈ p '' s
⊢ x ∈ s

Tactic:
rw [← hp.mem_set_image]

Premises used: Function.Injective.mem_set_image
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : (↑t : Set E) ⊆ p '' s
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) (p x)
⊢ p x ∈ p '' s

Tactic:
ht ?_
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : (↑t : Set E) ⊆ p '' s
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) (p x)
refine_2 : p x ∈ (↑t : Set E)
⊢ p x ∈ p '' s

Tactic:
refine ht ?_
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : (↑t : Set E) ⊆ p '' s
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) (p x)
this : x ∈ t.preimage p ⋯
rwa : ∀ (this : p x ∈ t), p x ∈ (↑t : Set E)
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : p x ∈ (↑t : Set E)), p x ∈ (↑t : Set E)
⊢ p x ∈ (↑t : Set E)

Tactic:
rwa [mem_preimage, ← mem_coe] at this

Premises used: Finset.mem_preimage, Finset.mem_coe
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : (↑t : Set E) ⊆ p '' s
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) (p x)
refine_2 : x ∈ t.preimage p ⋯
⊢ p x ∈ (↑t : Set E)

Tactic:
suffices x ∈ t.preimage p hp.injOn by rwa [mem_preimage, ← mem_coe] at this
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : (↑t : Set E) ⊆ p '' s
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) (p x)
⊢ x ∈ t.preimage p ⋯

Tactic:
h _ x ?_
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : (↑t : Set E) ⊆ p '' s
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) (p x)
refine_2 :
  Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p (t.preimage p ⋯)) : Set E) : Set E) (p x)
⊢ x ∈ t.preimage p ⋯

Tactic:
refine h _ x ?_
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : (↑t : Set E) ⊆ p '' s
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) (p x)
refine_2 : ∀ x ∈ t, x ∈ Set.range p
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p (t.preimage p ⋯)) : Set E) : Set E) (p x)

Tactic:
rwa [t.image_preimage p hp.injOn, filter_true_of_mem]

Premises used: Function.Injective.injOn, Finset.filter_true_of_mem, Finset.image_preimage
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : (↑t : Set E) ⊆ p '' s
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) (p x)
⊢ ∀ x ∈ t, x ∈ Set.range p

Tactic:
fun y hy => s.image_subset_range p (ht <| mem_coe.2 hy)

Premises used: Iff.mpr, Set.image_subset_range, Finset.mem_coe
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p : ι → E
h :
  ∀ (s : Finset ι) (x : ι),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p s) : Set E) : Set E) (p x) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : (↑t : Set E) ⊆ p '' s
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) (p x)
⊢ ∀ x ∈ t, x ∈ Set.range p

Tactic:
exact fun y hy => s.image_subset_range p (ht <| mem_coe.2 hy)

Premises used: Iff.mpr, Set.image_subset_range, Finset.mem_coe
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
⊢ ConvexIndependent.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ Set.extremePoints 𝕜 s })
    (Subtype.val (p := fun (x : E) ↦ x ∈ Set.extremePoints 𝕜 s))

Tactic:
convexIndependent_set_iff_notMem_convexHull_diff.2 fun _ hx h =>
    (extremePoints_convexHull_subset
          (inter_extremePoints_subset_extremePoints_of_subset
            (convexHull_min (Set.diff_subset.trans extremePoints_subset) hs) ⟨h, hx⟩)).2
      (Set.mem_singleton _)

Premises used: Iff.mpr, Set.mem_singleton, Set.diff_subset, HasSubset.Subset.trans, convexIndependent_set_iff_notMem_convexHull_diff, And.right, And.intro, extremePoints_convexHull_subset, convexHull_min, extremePoints_subset, inter_extremePoints_subset_extremePoints_of_subset
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
rcases : ∀ (g : α → E) (hgm : StronglyMeasurable g) (hfg : f =ᶠ[ae μ] g), ∫ (x : α), f x ∂μ ∈ s
⊢ ∫ (x : α), f x ∂μ ∈ s

Tactic:
rcases hfi.aestronglyMeasurable with ⟨g, hgm, hfg⟩

Premises used: MeasureTheory.Integrable.aestronglyMeasurable
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
g : α → E
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
⊢ SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)

Tactic:
haveI : SeparableSpace (range g ∩ s : Set E) :=
    (hgm.isSeparable_range.mono inter_subset_left).separableSpace