awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
⊢ ConvexIndependent.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) ↔
    ∀ t ⊆ s, s ∩ (convexHull 𝕜 : (a : Set E) → Set E) t ⊆ t
have mp : ConvexIndependent.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) →
  ∀ t ⊆ s, s ∩ (convexHull 𝕜 : (a : Set E) → Set E) t ⊆ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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 :
  ConvexIndependent.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) →
    ∀ t ⊆ s, s ∩ (convexHull 𝕜 : (a : Set E) → Set E) t ⊆ t
⊢ ConvexIndependent.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s)) ↔
    ∀ t ⊆ s, s ∩ (convexHull 𝕜 : (a : Set E) → Set E) t ⊆ t
have mpr : (∀ t ⊆ s, s ∩ (convexHull 𝕜 : (a : Set E) → Set E) t ⊆ t) →
  ConvexIndependent.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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 : ConvexIndependent.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
t : Set E
h : t ⊆ s
x : E
hxs : x ∈ s
hxt : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) t : Set E) x
⊢ x ∈ t
have mp : Membership.mem (γ := Set E)
  ((convexHull 𝕜 : (a : Set E) → Set E)
      (Set.image (α := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        {x : { x : E // x ∈ s } | (↑x : E) ∈ t}) :
    Set E)
  (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ s) x hxs) : E)
Tactic: refine hc { x | ↑x ∈ t } ⟨x, hxs⟩ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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 : ConvexIndependent.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
t : Set E
h : t ⊆ s
x : E
hxs : x ∈ s
hxt : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) t : Set E) x
⊢ Membership.mem (γ := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E)
        (Set.image (α := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
          {x : { x : E // x ∈ s } | (↑x : E) ∈ t}) :
      Set E)
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ s) x hxs) : E)
have mp : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) t : Set E)
  (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ s) x hxs) : E)
Tactic: rw [Subtype.coe_image_of_subset h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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)
⊢ x ∈ t
have mpr : Membership.mem (γ := Set E) ((fun (a : { x : E // x ∈ s }) ↦ (↑a : E)) '' t) (↑x : E)
Tactic: rw [← Subtype.coe_injective.mem_set_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : 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)
have 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)
Tactic: rw [convexIndependent_set_iff_inter_convexHull_subset]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
⊢ (∀ t ⊆ s, s ∩ (convexHull 𝕜 : (a : Set E) → Set E) t ⊆ t) ↔
    ∀ x ∈ s, x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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)
⊢ (∀ t ⊆ s, s ∩ (convexHull 𝕜 : (a : Set E) → Set E) t ⊆ t) ↔
    ∀ x ∈ s, x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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
⊢ x ∈ t
have mpr : ∀ (h : x ∉ t), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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
have 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)
Tactic: refine ⟨fun hc s x hx => hc s x ?_, fun h s x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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)
⊢ 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
have 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
Tactic: refine ⟨fun hc s x hx => hc s x ?_, fun h s x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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)
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (↑s : Set ι)) : Set E) (p x)
have 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)
Tactic: rwa [Finset.coe_image] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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
⊢ a = b
have rw : Membership.mem (γ := Finset ι) {b} a
Tactic: rw [← mem_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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
have refine : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p {b}) : Set E) : Set E) (p a)
Tactic: refine h {b} a ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p {b}) : Set E) : Set E) (p a)
have rw : Membership.mem (γ := Set E) {p b} (p b)
Tactic: rw [hab, image_singleton, coe_singleton, convexHull_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (hypothesis)
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)
⊢ x ∈ s
have hp : 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 _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (hypothesis)
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
⊢ x ∈ s
have hx₁ : 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
Cleared hypotheses: hx, hp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (hypothesis)
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
⊢ x ∈ s
have 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)
Tactic: simp_rw [Set.mem_iUnion] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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)
⊢ x ∈ s
have 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
Tactic: obtain ⟨t, ht, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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 ∈ s
have refine_2 : p x ∈ p '' s
Tactic: rw [← hp.mem_set_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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
have refine_2 : p x ∈ (↑t : Set E)
Tactic: refine ht ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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 ⋯
⊢ p x ∈ (↑t : Set E)
have rwa : ∀ (this : p x ∈ t), p x ∈ (↑t : Set E)
Tactic: rwa [mem_preimage, ← mem_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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)
⊢ p x ∈ (↑t : Set E)
have rwa₁ : ∀ (this : p x ∈ (↑t : Set E)), p x ∈ (↑t : Set E)
Tactic: rwa [mem_preimage, ← mem_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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 ∈ (↑t : Set E)
have refine_2 : x ∈ t.preimage p sorry
Tactic: suffices x ∈ t.preimage p hp.injOn by rwa [mem_preimage, ← mem_coe] at this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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 ⋯
have refine_2 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p (t.preimage p sorry)) : Set E) : Set E) (p x)
Tactic: refine h _ x ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
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)
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(image p (t.preimage p ⋯)) : Set E) : Set E) (p x)
have refine_2 : ∀ x ∈ t, x ∈ Set.range p
Tactic: rwa [t.image_preimage p hp.injOn, filter_true_of_mem]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (hypothesis)
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 μ
⊢ ∫ (x : α), f x ∂μ ∈ s
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
⊢ ∫ (x : α), f x ∂μ ∈ s
have rcases : ∀ (g : α → E) (hgm : StronglyMeasurable g) (hfg : f =ᶠ[ae μ] g), ∫ (x : α), f x ∂μ ∈ s
Tactic: rcases hfi.aestronglyMeasurable with ⟨g, hgm, hfg⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (hypothesis)
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
⊢ ∫ (x : α), f x ∂μ ∈ s
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
⊢ (range g ∩ s).Nonempty
have rcases : ∀ (x₀ : α) (h₀ : f x₀ ∈ s ∧ f x₀ = g x₀), (range g ∩ s).Nonempty
Tactic: rcases (hf.and hfg).exists with ⟨x₀, h₀⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
⊢ ∫ (x : α), f x ∂μ ∈ s
have obtain : ∀ (y₀ : E) (h₀ : y₀ ∈ range g ∩ s), ∫ (x : α), f x ∂μ ∈ s
Tactic: obtain ⟨y₀, h₀⟩ : (range g ∩ s).Nonempty := by
    rcases (hf.and hfg).exists with ⟨x₀, h₀⟩
    exact ⟨f x₀, by simp only [h₀.2, mem_range_self], h₀.1⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
⊢ ∫ (x : α), f x ∂μ ∈ s
have rw : ∫ (a : α), g a ∂μ ∈ s
Tactic: rw [integral_congr_ae hfg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
⊢ ∫ (a : α), g a ∂μ ∈ s
have rw : ∀ (hfi : Integrable g μ) (hgm : StronglyMeasurable g) (hfg : f =ᶠ[ae μ] g)
  (this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)) (y₀ : E) (h₀ : y₀ ∈ range g ∩ s), ∫ (a : α), g a ∂μ ∈ s
Tactic: rw [integrable_congr hfg] at hfi
Cleared hypotheses: hfi, hgm, hfg, this, y₀, h₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
⊢ ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
have h : ∀ (x : α) (hx : g x ∈ s), g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
Tactic: filter_upwards [hfg.rw (fun _ y => y ∈ s) hf] with x hx