awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
rw :
  convexCombPair t s ht hs ⋯ (convexCombPair s' t' hs' ht' h' m₂ m₃) m₁ =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
rw₁ :
  convexCombPair t s ht hs ⋯ (convexCombPair t' s' ht' hs' ⋯ m₃ m₂) m₁ =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
rw₂ :
  convexCombPair (t * t') (t * s' + s) ⋯ ⋯ ⋯ m₃ (convexCombPair t'' s'' ht'' hs'' ⋯ m₂ m₁) =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
rw₃ :
  convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair t'' s'' ht'' hs'' ⋯ m₂ m₁) m₃ =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
⊢ convexCombPair s t hs ht h m₁ (convexCombPair s' t' hs' ht' h' m₂ m₃) =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
have rw₄ : convexCombPair (t * s' + s) (t * t') sorry sorry sorry (convexCombPair s'' t'' hs'' ht'' sorry m₁ m₂) m₃ =
  convexCombPair (t * s' + s) (t * t') sorry sorry sorry (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
Tactic: rw [convexCombPair_symm, convexCombPair_symm (x := m₂),
    convexCombPair_convexCombPair_assoc_left (hs'' := ht'') (ht'' := hs'')
      (h'' := (add_comm _ _).trans h'') (H := H),
    convexCombPair_symm, convexCombPair_symm (x := m₂)]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
⊢ (iConvexComb f fun (x : I) ↦ convexCombPair s t hs ht h (e₁ x) (e₂ x)) =
    convexCombPair s t hs ht h (iConvexComb f e₁) (iConvexComb f e₂)
have simp : (iConvexComb f fun (i : I) ↦ iConvexComb (duple 0 1 hs ht h) ![e₁ i, e₂ i]) =
  iConvexComb (duple 0 1 hs ht h) ![iConvexComb f e₁, iConvexComb f e₂]
Tactic: simp only [convexCombPair_def]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
⊢ (iConvexComb f fun (i : I) ↦ iConvexComb (duple 0 1 hs ht h) ![e₁ i, e₂ i]) =
    iConvexComb (duple 0 1 hs ht h) ![iConvexComb f e₁, iConvexComb f e₂]
have h₁ : ∀ (i : I),
  Ne.{u_9 + 1} (α := R) ((f.weights : (a : I) → R) i : R) (0 : R) →
    ∀ (j : Fin (Nat.succ 0).succ),
      Ne (α := R) ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) j : R) (0 : R) →
        ![e₁ i, e₂ i] j = ![e₁, e₂] j i
Tactic: convert (iConvexComb_comm (.duple 0 1 hs ht h) f ![e₁, e₂]).symm with i _ j _ j
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
h₁ :
  ∀ (i : I),
    Ne.{u_9 + 1} (α := R) ((f.weights : (a : I) → R) i : R) (0 : R) →
      ∀ (j : Fin (Nat.succ 0).succ),
        Ne (α := R) ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) j : R) (0 : R) →
          ![e₁ i, e₂ i] j = ![e₁, e₂] j i
⊢ (iConvexComb f fun (i : I) ↦ iConvexComb (duple 0 1 hs ht h) ![e₁ i, e₂ i]) =
    iConvexComb (duple 0 1 hs ht h) ![iConvexComb f e₁, iConvexComb f e₂]
have h₂ : ∀ (j : Fin (Nat.succ 0).succ),
  Ne (α := R) ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) j : R) (0 : R) →
    ![iConvexComb f e₁, iConvexComb f e₂] j = iConvexComb f (![e₁, e₂] j)
Tactic: convert (iConvexComb_comm (.duple 0 1 hs ht h) f ![e₁, e₂]).symm with i _ j _ j
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
i : I
h_1 : Ne.{u_9 + 1} (α := R) ((f.weights : (a : I) → R) i : R) (0 : R)
j : Fin (Nat.succ 0).succ
h_2 : Ne (α := R) ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) j : R) (0 : R)
⊢ ![e₁ i, e₂ i] j = ![e₁, e₂] j i
have h₁ : Ne (α := R)
    ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩) : R)
    (0 : R) →
  ![e₁ i, e₂ i] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ)) =
    ![e₁, e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩) i
Tactic: fin_cases j
Cleared hypotheses: j, h_2
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
i : I
h_1 : Ne.{u_9 + 1} (α := R) ((f.weights : (a : I) → R) i : R) (0 : R)
j : Fin (Nat.succ 0).succ
h_2 : Ne (α := R) ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) j : R) (0 : R)
h₁ :
  Ne (α := R)
      ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) :
        R)
      (0 : R) →
    ![e₁ i, e₂ i] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
      ![e₁, e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) i
⊢ ![e₁ i, e₂ i] j = ![e₁, e₂] j i
have h₂ : Ne (α := R)
    ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩) : R)
    (0 : R) →
  ![e₁ i, e₂ i] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ)) =
    ![e₁, e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩) i
Tactic: fin_cases j
Cleared hypotheses: j, h_2
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
j : Fin (Nat.succ 0).succ
h_1 : Ne (α := R) ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) j : R) (0 : R)
⊢ ![iConvexComb f e₁, iConvexComb f e₂] j = iConvexComb f (![e₁, e₂] j)
have h₁ : Ne (α := R)
    ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩) : R)
    (0 : R) →
  ![iConvexComb f e₁, iConvexComb f e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ)) =
    iConvexComb f (![e₁, e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩))
Tactic: fin_cases j
Cleared hypotheses: j, h_1
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
j : Fin (Nat.succ 0).succ
h_1 : Ne (α := R) ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) j : R) (0 : R)
h₁ :
  Ne (α := R)
      ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) :
        R)
      (0 : R) →
    ![iConvexComb f e₁, iConvexComb f e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
      iConvexComb f (![e₁, e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩))
⊢ ![iConvexComb f e₁, iConvexComb f e₂] j = iConvexComb f (![e₁, e₂] j)
have h₂ : Ne (α := R)
    ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩) : R)
    (0 : R) →
  ![iConvexComb f e₁, iConvexComb f e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ)) =
    iConvexComb f (![e₁, e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩))
Tactic: fin_cases j
Cleared hypotheses: j, h_1
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Module (goal)
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : SetLike F M
inst_6 : AddSubmonoidClass F M
inst_7 : SMulMemClass F R M
inst_8 : ConvexSpace R M
inst_9 : IsModuleConvexSpace R M
S : F
⊢ IsConvexSet R (↑S : Set M)
have refine : ∀ (w : StdSimplex R M) (hw : (↑w.weights.support : Set M) ⊆ (↑S : Set M)), sConvexComb w ∈ (↑S : Set M)
Tactic: refine .of_sConvexComb_mem fun w hw ↦ ?_
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Module (goal)
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : SetLike F M
inst_6 : AddSubmonoidClass F M
inst_7 : SMulMemClass F R M
inst_8 : ConvexSpace R M
inst_9 : IsModuleConvexSpace R M
S : F
w : StdSimplex R M
hw : (↑w.weights.support : Set M) ⊆ (↑S : Set M)
⊢ sConvexComb w ∈ (↑S : Set M)
have rw : (w.weights.sum fun (m : M) (r : R) ↦ r • m) ∈ (↑S : Set M)
Tactic: rw [sConvexComb_eq_sum]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Module (goal)
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : SetLike F M
inst_8 : AddSubmonoidClass F M
inst_9 : SMulMemClass F R M
inst_10 : ConvexSpace R M
inst_11 : IsModuleConvexSpace R M
S : F
w : StdSimplex.{u_2, u_3} R ↥S
⊢ sConvexComb w = w.weights.sum fun (m : ↥S) (r : R) ↦ r • m
have a : (↑(sConvexComb w) : M) = (↑(w.weights.sum fun (m : ↥S) (r : R) ↦ r • m) : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Module (goal)
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : SetLike F M
inst_8 : AddSubmonoidClass F M
inst_9 : SMulMemClass F R M
inst_10 : ConvexSpace R M
inst_11 : IsModuleConvexSpace R M
inst_12 : ConvexSpace R N
inst_13 : IsModuleConvexSpace R N
w : StdSimplex R (M × N)
⊢ sConvexComb w = w.weights.sum fun (m : M × N) (r : R) ↦ r • m
have fst : (sConvexComb w).1 = (w.weights.sum fun (m : M × N) (r : R) ↦ r • m).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Module (goal)
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : SetLike F M
inst_8 : AddSubmonoidClass F M
inst_9 : SMulMemClass F R M
inst_10 : ConvexSpace R M
inst_11 : IsModuleConvexSpace R M
inst_12 : ConvexSpace R N
inst_13 : IsModuleConvexSpace R N
w : StdSimplex R (M × N)
fst : (sConvexComb w).1 = (w.weights.sum fun (m : M × N) (r : R) ↦ r • m).1
⊢ sConvexComb w = w.weights.sum fun (m : M × N) (r : R) ↦ r • m
have snd : (sConvexComb w).2 = (w.weights.sum fun (m : M × N) (r : R) ↦ r • m).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Module (goal)
Goal:
F : Type u_1
R : Type u_2
M_1 : Type u_3
N : Type u_4
I : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M_1
inst_4 : Module R M_1
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : SetLike F M_1
inst_8 : AddSubmonoidClass F M_1
inst_9 : SMulMemClass F R M_1
inst_10 : ConvexSpace R M_1
inst_11 : IsModuleConvexSpace R M_1
ι : Type u_6
M : ι → Type u_7
inst_12 : (i : ι) → AddCommMonoid (M i)
inst_13 : (i : ι) → Module.{u_2, u_7} R (M i)
inst_14 : (i : ι) → ConvexSpace.{u_2, u_7} R (M i)
inst_15 : ∀ (i : ι), IsModuleConvexSpace.{u_2, u_7} R (M i)
w : StdSimplex R ((i : ι) → M i)
⊢ sConvexComb w = w.weights.sum fun (m : (i : ι) → M i) (r : R) ↦ r • m
have h : ∀ (x : ι), sConvexComb w x = w.weights.sum (fun (m : (i : ι) → M i) (r : R) ↦ r • m) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Module (goal)
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : SetLike F M
inst_8 : AddSubmonoidClass F M
inst_9 : SMulMemClass F R M
inst_10 : ConvexSpace R M
inst_11 : IsModuleConvexSpace R M
ι : Type u_6
w : StdSimplex R (ι →₀ M)
⊢ sConvexComb w = w.weights.sum fun (m : ι →₀ M) (r : R) ↦ r • m
have h : ∀ (a : ι),
  Eq.{u_3 + 1} (α := M) ((sConvexComb w : (a : ι) → M) a : M)
    ((w.weights.sum fun (m : ι →₀ M) (r : R) ↦ r • m : (a : ι) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Prod (goal)
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst_3 : Zero X
inst_4 : ConvexSpace R X
i : ι
w : StdSimplex R (ι →₀ X)
⊢ ι →₀ X
have refine : ∀ (a : ι),
  Ne.{u_4 + 1} (α := X) ((fun (i : ι) ↦ (iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i : X)) a) 0 →
    a ∈ w.weights.support.biUnion support
Tactic: refine .onFinset (w.weights.support.biUnion Finsupp.support) (fun i ↦ w.iConvexComb (· i)) ?_
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Prod (goal)
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst_3 : Zero X
inst_4 : ConvexSpace R X
i_1 : ι
w : StdSimplex R (ι →₀ X)
i : ι
hi : Ne.{u_4 + 1} (α := X) ((fun (i : ι) ↦ (iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i : X)) i) 0
⊢ i ∈ w.weights.support.biUnion support
have contrapose! : ∀ (hi : i ∉ w.weights.support.biUnion support),
  Eq.{u_4 + 1} (α := X) (iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) 0
Tactic: contrapose! hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Prod (goal)
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst_3 : Zero X
inst_4 : ConvexSpace R X
i : ι
w : StdSimplex R (ι →₀ X)
⊢ ι →₀ X
have refine : ∀ (a : ι),
  Ne.{u_4 + 1} (α := X) ((fun (i : ι) ↦ (iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i : X)) a) 0 →
    a ∈ w.weights.support.biUnion support
Tactic: classical
    refine .onFinset (w.weights.support.biUnion Finsupp.support) (fun i ↦ w.iConvexComb (· i)) ?_
    rintro i hi
    contrapose! hi
    simp_all
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Prod (goal)
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst_3 : Zero X
inst_4 : ConvexSpace R X
i : ι
w : StdSimplex R (ι →₀ X)
refine refine₁ :
  ∀ (i : ι)
    (hi : Ne.{u_4 + 1} (α := X) ((fun (i : ι) ↦ (iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i : X)) i) 0),
    i ∈ w.weights.support.biUnion support
⊢ ι →₀ X
have refine₂ : ∀ (i : ι) (hi : i ∉ w.weights.support.biUnion support),
  Eq.{u_4 + 1} (α := X) (iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) 0
Tactic: classical
    refine .onFinset (w.weights.support.biUnion Finsupp.support) (fun i ↦ w.iConvexComb (· i)) ?_
    rintro i hi
    contrapose! hi
    simp_all
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Prod (goal)
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst_3 : Zero X
inst_4 : ConvexSpace R X
i : ι
w : StdSimplex R (StdSimplex R (ι →₀ X))
⊢ Eq (α := ι →₀ X)
    ((fun (w : StdSimplex R (ι →₀ X)) ↦
        (onFinset (w.weights.support.biUnion support)
            (fun (i : ι) ↦ iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) ⋯ :
          ι →₀ X))
      (StdSimplex.map
        (fun (w : StdSimplex R (ι →₀ X)) ↦
          onFinset (w.weights.support.biUnion support)
            (fun (i : ι) ↦ iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) ⋯)
        w))
    ((fun (w : StdSimplex R (ι →₀ X)) ↦
        (onFinset (w.weights.support.biUnion support)
            (fun (i : ι) ↦ iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) ⋯ :
          ι →₀ X))
      (sConvexComb w))
have h : ∀ (a : ι),
  Eq.{u_4 + 1} (α := X)
    (((fun (w : StdSimplex R (ι →₀ X)) ↦
              (onFinset (w.weights.support.biUnion support)
                  (fun (i : ι) ↦ iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) sorry :
                ι →₀ X))
            (StdSimplex.map
              (fun (w : StdSimplex R (ι →₀ X)) ↦
                onFinset (w.weights.support.biUnion support)
                  (fun (i : ι) ↦ iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) sorry)
              w) :
          (a : ι) → X)
        a :
      X)
    (((fun (w : StdSimplex R (ι →₀ X)) ↦
              (onFinset (w.weights.support.biUnion support)
                  (fun (i : ι) ↦ iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) sorry :
                ι →₀ X))
            (sConvexComb w) :
          (a : ι) → X)
        a :
      X)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
Goal:
ι : Type u_1
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R ι
f : ι → X
hf : ∀ (i : ι), Ne.{u_3 + 1} (α := R) ((w.weights : (a : ι) → R) i : R) (0 : R) → f i ∈ s
⊢ iConvexComb w f ∈ s
have refine : (↑(StdSimplex.map f w).weights.support : Set X) ⊆ s
Tactic: refine hs ?_
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
Goal:
ι : Type u_1
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R ι
f : ι → X
hf : ∀ (i : ι), Ne.{u_3 + 1} (α := R) ((w.weights : (a : ι) → R) i : R) (0 : R) → f i ∈ s
⊢ (↑(StdSimplex.map f w).weights.support : Set X) ⊆ s
have grw : (↑(Finset.image f w.weights.support) : Set X) ⊆ s
Tactic: grw [StdSimplex.weights_map, mapDomain_support]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
Goal:
ι : Type u_1
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R ι
f : ι → X
hf : ∀ (i : ι), Ne.{u_3 + 1} (α := R) ((w.weights : (a : ι) → R) i : R) (0 : R) → f i ∈ s
⊢ iConvexComb w f ∈ s
have refine : (↑(StdSimplex.map f w).weights.support : Set X) ⊆ s
Tactic: classical
  refine hs ?_
  grw [StdSimplex.weights_map, mapDomain_support]
  simpa [subset_def]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
Goal:
ι : Type u_1
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R ι
f : ι → X
hf : ∀ (i : ι), Ne.{u_3 + 1} (α := R) ((w.weights : (a : ι) → R) i : R) (0 : R) → f i ∈ s
refine : (↑(StdSimplex.map f w).weights.support : Set X) ⊆ s
⊢ iConvexComb w f ∈ s
have refine₁ : (↑(Finset.image f w.weights.support) : Set X) ⊆ s
Tactic: classical
  refine hs ?_
  grw [StdSimplex.weights_map, mapDomain_support]
  simpa [subset_def]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
x y : X
hs : IsConvexSet R s
hx : x ∈ s
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ convexCombPair a b ha hb hab x y ∈ s
have refine : (↑(StdSimplex.duple x y ha hb hab).weights.support : Set X) ⊆ s
Tactic: refine hs.sConvexComb_mem ?_
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
x y : X
hs : IsConvexSet R s
hx : x ∈ s
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (↑(StdSimplex.duple x y ha hb hab).weights.support : Set X) ⊆ s
have grw : (↑({x} ∪ {y}) : Set X) ⊆ s
Tactic: grw [StdSimplex.weights_duple, support_add, support_single_subset, support_single_subset]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
x y : X
hs : IsConvexSet R s
hx : x ∈ s
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ convexCombPair a b ha hb hab x y ∈ s
have refine : (↑(StdSimplex.duple x y ha hb hab).weights.support : Set X) ⊆ s
Tactic: classical
  refine hs.sConvexComb_mem ?_
  grw [StdSimplex.weights_duple, support_add, support_single_subset, support_single_subset]
  simp [*, insert_subset_iff]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
x y : X
hs : IsConvexSet R s
hx : x ∈ s
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine : (↑(StdSimplex.duple x y ha hb hab).weights.support : Set X) ⊆ s
⊢ convexCombPair a b ha hb hab x y ∈ s
have refine₁ : (↑({x} ∪ {y}) : Set X) ⊆ s
Tactic: classical
  refine hs.sConvexComb_mem ?_
  grw [StdSimplex.weights_duple, support_add, support_single_subset, support_single_subset]
  simp [*, insert_subset_iff]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
hs : s.Subsingleton
⊢ IsConvexSet R s
have inl : ∀ (hs : Set.Subsingleton.{u_5} (α := X) ∅), IsConvexSet.{u_3, u_5} R (X := X) ∅
Tactic: obtain rfl | ⟨x, rfl⟩ := hs.eq_empty_or_singleton
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
hs : s.Subsingleton
inl : ∀ (hs : Set.Subsingleton.{u_5} (α := X) ∅), IsConvexSet.{u_3, u_5} R (X := X) ∅
⊢ IsConvexSet R s
have inr : ∀ (x : X) (hs : Set.Subsingleton (α := X) {x}), IsConvexSet R (X := X) {x}
Tactic: obtain rfl | ⟨x, rfl⟩ := hs.eq_empty_or_singleton
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
S : Set (Set X)
hS : DirectedOn (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) S
hS' : ∀ s ∈ S, IsConvexSet R s
⊢ IsConvexSet R (⋃₀ S)
have inl : ∀ (hS : DirectedOn (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) ∅)
  (hS' : ∀ (s : Set X), Membership.mem (γ := Set (Set X)) ∅ s → IsConvexSet R s),
  IsConvexSet.{u_3, u_5} R (X := X) (⋃₀ ∅)
Tactic: obtain rfl | hS'' := S.eq_empty_or_nonempty
Cleared hypotheses: S, hS, hS'
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
S : Set (Set X)
hS : DirectedOn (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) S
hS' : ∀ s ∈ S, IsConvexSet R s
inl :
  ∀ (hS : DirectedOn (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) ∅)
    (hS' : ∀ (s : Set X), Membership.mem (γ := Set (Set X)) ∅ s → IsConvexSet R s),
    IsConvexSet.{u_3, u_5} R (X := X) (⋃₀ ∅)
⊢ IsConvexSet R (⋃₀ S)
have inr : ∀ (hS'' : S.Nonempty), IsConvexSet R (⋃₀ S)
Tactic: obtain rfl | hS'' := S.eq_empty_or_nonempty