awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
simp_rw :
  Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((fun (x : E) ↦ -x) '' s) : Set E)
    ((fun (x : E) ↦ -x) '' (convexHull 𝕜 : (a : Set E) → Set E) s : Set E)
⊢ Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (-s) : Set E) (-(convexHull 𝕜 : (a : Set E) → Set E) s : Set E)

Tactic:
simp_rw [← image_neg_eq_neg]

Premises used: Set.image_neg_eq_neg
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
⊢ Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((fun (x : E) ↦ -x) '' s) : Set E)
    ((fun (x : E) ↦ -x) '' (convexHull 𝕜 : (a : Set E) → Set E) s : Set E)

Tactic:
AffineMap.image_convexHull (-1) _ |>.symm

Premises used: AffineMap.image_convexHull, OfNat.ofNat, Eq.symm, Neg.neg
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
⊢ Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((fun (x : E) ↦ -x) '' s) : Set E)
    ((fun (x : E) ↦ -x) '' (convexHull 𝕜 : (a : Set E) → Set E) s : Set E)

Tactic:
exact AffineMap.image_convexHull (-1) _ |>.symm

Premises used: AffineMap.image_convexHull, OfNat.ofNat, Eq.symm, Neg.neg
-- Module: Mathlib.Analysis.Convex.Hull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
x : E
s : Set E
⊢ (convexHull 𝕜 : (a : Set E) → Set E) (x +ᵥ s) =
    HVAdd.hVAdd (β := Set E) x ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E)

Tactic:
(AffineEquiv.constVAdd 𝕜 _ x).toAffineMap.image_convexHull s |>.symm

Premises used: AffineEquiv.constVAdd, AffineEquiv.toAffineMap, AffineMap.image_convexHull, Eq.symm
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p x)
⊢ Set.Nonempty.{u_2} (α := E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s))

Tactic:
have : (convexHull 𝕜 (p '' s)).Nonempty := ⟨p x, hx⟩
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p x)
this : Set.Nonempty.{u_2} (α := E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s))
⊢ s.Nonempty

Tactic:
rw [convexHull_nonempty_iff, Set.image_nonempty] at this

Premises used: Set.image_nonempty, convexHull_nonempty_iff
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p x)
this rwa rwa₁ rwa₂ rwa₃ : s.Nonempty
⊢ x ∈ s

Tactic:
rwa [Subsingleton.mem_iff_nonempty]

Premises used: Subsingleton.mem_iff_nonempty
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
⊢ Injective p

Tactic:
fun i j hij => hc {j} i ?_

Premises used: Set.Mem, setOf, Set.singleton, Function.Injective, Singleton.singleton
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
refine :
  ∀ (i j : ι) (hij : p i = p j),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' {j}) : Set E) (p i)
⊢ Injective p

Tactic:
refine fun i j hij => hc {j} i ?_

Premises used: Singleton.singleton
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i j : ι
hij : p i = p j
rw : Membership.mem (γ := Set E) {p j} (p j)
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' {j}) : Set E) (p i)

Tactic:
rw [hij, Set.image_singleton, convexHull_singleton]

Premises used: Set.image_singleton, convexHull_singleton
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i j : ι
hij : p i = p j
⊢ Membership.mem (γ := Set E) {p j} (p j)

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 : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i j : ι
hij : p i = p j
⊢ Membership.mem (γ := Set E) {p j} (p j)

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 : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx :
  Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p ∘ (⇑f : (a : ι') → ι) '' s) : Set E)
    ((p ∘ (⇑f : (a : ι') → ι)) x)
rw : Membership.mem.{u_3, u_3} (α := ι) (γ := Set ι) ((⇑f : (a : ι') → ι) '' s) ((f : (a : ι') → ι) x : ι)
⊢ x ∈ s

Tactic:
rw [← f.injective.mem_set_image]

Premises used: Function.Embedding.injective, Function.Injective.mem_set_image
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx :
  Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p ∘ (⇑f : (a : ι') → ι) '' s) : Set E)
    ((p ∘ (⇑f : (a : ι') → ι)) x)
rwa rwa₁ rwa₂ rwa₃ :
  Membership.mem (γ := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) ((fun (x : ι') ↦ p ((f : (a : ι') → ι) x)) '' s) : Set E)
    (p ((f : (a : ι') → ι) x))
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (⇑f : (a : ι') → ι) '' s) : Set E)
    (p ((f : (a : ι') → ι) x))

Tactic:
rwa [Set.image_image]

Premises used: Set.image_image
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx :
  Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p ∘ (⇑f : (a : ι') → ι) '' s) : Set E)
    ((p ∘ (⇑f : (a : ι') → ι)) x)
⊢ Membership.mem.{u_3, u_3} (α := ι) (γ := Set ι) ((⇑f : (a : ι') → ι) '' s) ((f : (a : ι') → ι) x : ι)

Tactic:
exact hc _ _ (by rwa [Set.image_image])
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι
⊢ ConvexIndependent.{u_1, u_2, u_3} 𝕜 (E := E) fun (i : (↑s : Type u_3)) ↦ p (↑i : ι)

Tactic:
hc.comp_embedding (Embedding.subtype _)

Premises used: ConvexIndependent.comp_embedding, Function.Embedding.subtype
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : (↑(Set.range p) : Type u_2) → ι :=
  fun (x : (↑(Set.range p) : Type u_2)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : E)) ⋯
⊢ ∀ (x : (↑(Set.range p) : Type u_2)), p (f x) = (↑x : E)

Tactic:
have hf : ∀ x, p (f x) = x := fun x => x.property.choose_spec
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : (↑(Set.range p) : Type u_2) → ι :=
  fun (x : (↑(Set.range p) : Type u_2)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : E)) ⋯
hf : ∀ (x : (↑(Set.range p) : Type u_2)), p (f x) = (↑x : E)
fe : Embedding.{u_2 + 1, u_3 + 1} (↑(Set.range p) : Type u_2) ι := { toFun := f, inj' := ⋯ }
⊢ ConvexIndependent 𝕜 (ι := (↑(Set.range p) : Type u_2)) (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_2)) → ι))

Tactic:
hc.comp_embedding fe

Premises used: ConvexIndependent.comp_embedding
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : (↑(Set.range p) : Type u_2) → ι :=
  fun (x : (↑(Set.range p) : Type u_2)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : E)) ⋯
hf : ∀ (x : (↑(Set.range p) : Type u_2)), p (f x) = (↑x : E)
fe : Embedding.{u_2 + 1, u_3 + 1} (↑(Set.range p) : Type u_2) ι := { toFun := f, inj' := ⋯ }
h :
  Eq (α := { x : E // x ∈ Set.range p } → E) (Subtype.val (p := fun (x : E) ↦ x ∈ Set.range p))
    (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_2)) → ι))
⊢ ConvexIndependent.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ Set.range p })
    (Subtype.val (p := fun (x : E) ↦ x ∈ Set.range p))

Tactic:
convert! hc.comp_embedding fe

Premises used: ConvexIndependent.comp_embedding
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : (↑(Set.range p) : Type u_2) → ι :=
  fun (x : (↑(Set.range p) : Type u_2)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : E)) ⋯
hf : ∀ (x : (↑(Set.range p) : Type u_2)), p (f x) = (↑x : E)
fe : Embedding.{u_2 + 1, u_3 + 1} (↑(Set.range p) : Type u_2) ι := { toFun := f, inj' := ⋯ }
h : ∀ (x : { x : E // x ∈ Set.range p }), (↑x : E) = (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_2)) → ι)) x
⊢ Eq (α := { x : E // x ∈ Set.range p } → E) (Subtype.val (p := fun (x : E) ↦ x ∈ Set.range p))
    (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_2)) → ι))

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : (↑(Set.range p) : Type u_2) → ι :=
  fun (x : (↑(Set.range p) : Type u_2)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : E)) ⋯
hf : ∀ (x : (↑(Set.range p) : Type u_2)), p (f x) = (↑x : E)
fe : Embedding.{u_2 + 1, u_3 + 1} (↑(Set.range p) : Type u_2) ι := { toFun := f, inj' := ⋯ }
x : { x : E // x ∈ Set.range p }
h : (↑x : E) = (p ∘ f) x
h₁ : (↑x : E) = p (f x)
h₂ h₃ : (↑x : E) = (↑x : E)
⊢ (↑x : E) = (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_2)) → ι)) x

Tactic:
rw [Embedding.coeFn_mk, comp_apply, hf]

Premises used: Function.Embedding.coeFn_mk, Function.comp_apply
-- 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 t : Set E
hc : ConvexIndependent.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ t }) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
hs : s ⊆ t
⊢ ConvexIndependent.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))

Tactic:
hc.comp_embedding (s.embeddingOfSubset t hs)

Premises used: Set.Mem, ConvexIndependent.comp_embedding, Set.embeddingOfSubset
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hi : Injective p
⊢ ConvexIndependent.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ Set.range p })
      (Subtype.val (p := fun (x : E) ↦ x ∈ Set.range p)) ↔
    ConvexIndependent 𝕜 p

Tactic:
⟨fun hc =>
    hc.comp_embedding
      (⟨fun i => ⟨p i, Set.mem_range_self _⟩, fun _ _ h => hi (Subtype.mk_eq_mk.1 h)⟩ :
        ι ↪ Set.range p),
    ConvexIndependent.range⟩

Premises used: Set.mem_range_self, ConvexIndependent.comp_embedding, Function.Embedding.mk, Subtype.mk, Iff.intro, Subtype.mk_eq_mk, Iff.mp, ConvexIndependent.range
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι
i : ι
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p i) ↔ i ∈ s

Tactic:
⟨hc _ _, fun hi => subset_convexHull 𝕜 _ (Set.mem_image_of_mem p hi)⟩

Premises used: subset_convexHull, Set.mem_image_of_mem, Iff.intro, Set.image
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
⊢ ConvexIndependent 𝕜 p ↔ ∀ (i : ι) (s : Set ι), p i ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E)

Tactic:
⟨fun hc i s h => ?_, fun h s i hi => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
refine_1 :
  ∀ (hc : ConvexIndependent 𝕜 p) (i : ι) (s : Set ι)
    (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E) (p i)), False
refine_2 :
  ∀ (h : ∀ (i : ι) (s : Set ι), p i ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E)) (s : Set ι)
    (i : ι) (hi : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p i)), i ∈ s
⊢ ConvexIndependent 𝕜 p ↔ ∀ (i : ι) (s : Set ι), p i ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E)

Tactic:
refine ⟨fun hc i s h => ?_, fun h s i hi => ?_⟩
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i : ι
s : Set ι
h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E) (p i)
⊢ i ∈ s \ {i}

Tactic:
rw [hc.mem_convexHull_iff] at h

Premises used: ConvexIndependent.mem_convexHull_iff
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i : ι
s : Set ι
h : i ∈ s \ {i}
⊢ False

Tactic:
h.2 (Set.mem_singleton _)

Premises used: Set.mem_singleton, And.right
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i : ι
s : Set ι
h : i ∈ s \ {i}
⊢ False

Tactic:
exact h.2 (Set.mem_singleton _)

Premises used: Set.mem_singleton, And.right
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E)
s : Set ι
i : ι
hi : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p i)
refine_2 : ∀ (H : i ∉ s), False
⊢ i ∈ s

Tactic:
by_contra H
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E)
s : Set ι
i : ι
hi : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p i)
H : i ∉ s
⊢ False

Tactic:
h i s ?_
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E)
s : Set ι
i : ι
hi : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p i)
H : i ∉ s
refine_2 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E) (p i)
⊢ False

Tactic:
refine h i s ?_
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E)
s : Set ι
i : ι
hi : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p i)
H : i ∉ s
refine_2 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p i)
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E) (p i)

Tactic:
rw [Set.diff_singleton_eq_self H]

Premises used: Set.diff_singleton_eq_self
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E)
s : Set ι
i : ι
hi : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p i)
H : i ∉ s
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p i)

Tactic:
hi
-- Module: Mathlib.Analysis.Convex.Independent
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E)
s : Set ι
i : ι
hi : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p i)
H : i ∉ s
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p i)

Tactic:
exact hi
-- 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 :
  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
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))
⊢ 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
-- 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 : 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

Tactic:
hc { x | ↑x ∈ t } ⟨x, hxs⟩ ?_

Premises used: Set.Mem, setOf, Membership.mem, Subtype.mk
-- 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 : 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
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)
⊢ x ∈ t

Tactic:
refine hc { x | ↑x ∈ t } ⟨x, hxs⟩ ?_

Premises used: setOf, Membership.mem, Subtype.mk
-- 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 : 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
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)
⊢ 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:
rw [Subtype.coe_image_of_subset h]

Premises used: Subtype.coe_image_of_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
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) t : Set E)
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ s) x hxs) : E)

Tactic:
hxt

Premises used: Set.Mem
-- 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 : 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) t : Set E)
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ s) x hxs) : E)

Tactic:
exact hxt
-- 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)
mpr : Membership.mem (γ := Set E) ((fun (a : { x : E // x ∈ s }) ↦ (↑a : E)) '' t) (↑x : E)
⊢ x ∈ t

Tactic:
rw [← Subtype.coe_injective.mem_set_image]

Premises used: Subtype.coe_injective, Function.Injective.mem_set_image
-- 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:
hc (t.image ((↑) : s → E)) (Subtype.coe_image_subset s t) ⟨x.prop, h⟩

Premises used: Set.Mem, Subtype.coe_image_subset, Subtype.prop, And.intro, Set.image, Subtype.val