mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
⊢ ∀ (o : Set ↥(affineSpan 𝕜 s)),
    IsOpen[instTopologicalSpaceSubtype] o → ⟨x, ?refine_3⟩ ∈ o → (o ∩ Subtype.val ⁻¹' s).Nonempty

pp: case refine_3
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
⊢ x ∈ affineSpan 𝕜 s

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
⊢ ∀ (o : Set ↥(affineSpan 𝕜 s)),
    IsOpen[instTopologicalSpaceSubtype] o → ⟨x, ?refine_3⟩ ∈ o → (o ∩ Subtype.val ⁻¹' s).Nonempty
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case refine_3
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
⊢ x ∈ affineSpan 𝕜 s

Tactic:
·

Goal state after:
case refine_3
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
⊢ x ∈ affineSpan 𝕜 s
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
⊢ (intrinsicInterior ℝ s).Nonempty → s.Nonempty

Tactic:
nonempty_iff_ne_empty

Goal state after:
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
⊢ intrinsicInterior ℝ s ≠ ∅ → s ≠ ∅
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case inl
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : C ≤ 0
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

pp: case inr
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

Tactic:
·

Goal state after:
case inl
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : C ≤ 0
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : ¬Integrable f μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

pp: case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : Integrable f μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

Tactic:
·

Goal state after:
case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : ¬Integrable f μ
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case pos.inl
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : Integrable f μ
hμt : μ univ = ∞
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

pp: case pos.inr
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : Integrable f μ
hμt : μ univ < ∞
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C

Tactic:
·

Goal state after:
case pos.inl
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : Integrable f μ
hμt : μ univ = ∞
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case inl
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝¹ : StrictConvexSpace ℝ E
inst✝ : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
h₀ : μ = 0
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖∫ (x : α), f x ∂μ‖ < μ.real univ * C

pp: case inr
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝¹ : StrictConvexSpace ℝ E
inst✝ : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
h₀ : μ ≠ 0
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖∫ (x : α), f x ∂μ‖ < μ.real univ * C

Tactic:
·

Goal state after:
case inl
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
μ : Measure α
f : α → E
C : ℝ
inst✝¹ : StrictConvexSpace ℝ E
inst✝ : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
h₀ : μ = 0
⊢ f =ᵐ[μ] const α (⨍ (x : α), f x ∂μ) ∨ ‖∫ (x : α), f x ∂μ‖ < μ.real univ * C
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
h : P → R → V := fun x w ↦ w • (x -ᵥ b)
h_rhs :
  ∑ a ∈ (∑ d ∈ f.weights.support, f.weights d • d.weights).support,
      h a ((∑ d ∈ f.weights.support, f.weights d • d.weights) a) =
    ∑ d ∈ f.weights.support, ∑ a ∈ (f.weights d • d.weights).support, h a ((f.weights d • d.weights) a)
d : StdSimplex R P
hd : ¬f.weights d = 0
⊢ ∑ x ∈ d.weights.support, (f.weights d * d.weights x) • (x -ᵥ b) =
    ∑ a ∈ (f.weights d • d.weights).support, h a (f.weights d * d.weights a)

Tactic:
·

Goal state after:
case neg
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
h : P → R → V := fun x w ↦ w • (x -ᵥ b)
h_rhs :
  ∑ a ∈ (∑ d ∈ f.weights.support, f.weights d • d.weights).support,
      h a ((∑ d ∈ f.weights.support, f.weights d • d.weights) a) =
    ∑ d ∈ f.weights.support, ∑ a ∈ (f.weights d • d.weights).support, h a ((f.weights d • d.weights) a)
d : StdSimplex R P
hd : ¬f.weights d = 0
⊢ ∑ x ∈ d.weights.support, (f.weights d * d.weights x) • (x -ᵥ b) =
    ∑ a ∈ (f.weights d • d.weights).support, h a (f.weights d * d.weights a)
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: case inl
R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
hS : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) ∅
hS' : ∀ s ∈ ∅, IsConvexSet R s
⊢ IsConvexSet R (⋃₀ ∅)

pp: case inr
R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
S : Set (Set X)
hS : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
hS' : ∀ s ∈ S, IsConvexSet R s
hS'' : S.Nonempty
⊢ IsConvexSet R (⋃₀ S)

Tactic:
·

Goal state after:
case inl
R : Type u_3
X : Type u_5
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
hS : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) ∅
hS' : ∀ s ∈ ∅, IsConvexSet R s
⊢ IsConvexSet R (⋃₀ ∅)
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: case neg.mpr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
h : P → R → V := ⋯
h_rhs :
  ∑ a ∈ (∑ d ∈ f.weights.support, f.weights d • d.weights).support,
      h a ((∑ d ∈ f.weights.support, f.weights d • d.weights) a) =
    ∑ d ∈ f.weights.support, ∑ a ∈ (f.weights d • d.weights).support, h a ((f.weights d • d.weights) a)
d : StdSimplex R P
hd : ¬f.weights d = 0
p : P
⊢ ¬(f.weights d • d.weights) p = 0 → ¬d.weights p = 0

Tactic:
·

Goal state after:
case neg.mpr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
f : StdSimplex R (StdSimplex R P)
b : P
hL :
  (Finset.affineCombination R (StdSimplex.map convexCombination f).weights.support id)
      ⇑(StdSimplex.map convexCombination f).weights =
    ((StdSimplex.map convexCombination f).weights.support.weightedVSubOfPoint id b)
        ⇑(StdSimplex.map convexCombination f).weights +ᵥ
      b
hR :
  (Finset.affineCombination R f.join.weights.support id) ⇑f.join.weights =
    (f.join.weights.support.weightedVSubOfPoint id b) ⇑f.join.weights +ᵥ b
h : P → R → V := ⋯
h_rhs :
  ∑ a ∈ (∑ d ∈ f.weights.support, f.weights d • d.weights).support,
      h a ((∑ d ∈ f.weights.support, f.weights d • d.weights) a) =
    ∑ d ∈ f.weights.support, ∑ a ∈ (f.weights d • d.weights).support, h a ((f.weights d • d.weights) a)
d : StdSimplex R P
hd : ¬f.weights d = 0
p : P
⊢ ¬(f.weights d • d.weights) p = 0 → ¬d.weights p = 0
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: case e'_2
R : Type u_9
M : Type u_10
I : Type u_11
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : 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
a✝¹ : f.weights i ≠ 0
j : Fin (Nat.succ 0).succ
a✝ : (duple 0 1 hs ht h).weights j ≠ 0
⊢ ![e₁ i, e₂ i] j = ![e₁, e₂] j i

pp: case e'_3
R : Type u_9
M : Type u_10
I : Type u_11
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : 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
a✝ : (duple 0 1 hs ht h).weights j ≠ 0
⊢ ![iConvexComb f e₁, iConvexComb f e₂] j = iConvexComb f (![e₁, e₂] j)

Tactic:
·

Goal state after:
case e'_2
R : Type u_9
M : Type u_10
I : Type u_11
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : 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
a✝¹ : f.weights i ≠ 0
j : Fin (Nat.succ 0).succ
a✝ : (duple 0 1 hs ht h).weights j ≠ 0
⊢ ![e₁ i, e₂ i] j = ![e₁, e₂] j i
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: case e'_3
R : Type u_9
M : Type u_10
I : Type u_11
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : 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
a✝ : (duple 0 1 hs ht h).weights j ≠ 0
⊢ ![iConvexComb f e₁, iConvexComb f e₂] j = iConvexComb f (![e₁, e₂] j)

Tactic:
·

Goal state after:
case e'_3
R : Type u_9
M : Type u_10
I : Type u_11
inst✝³ : PartialOrder R
inst✝² : CommSemiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : 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
a✝ : (duple 0 1 hs ht h).weights j ≠ 0
⊢ ![iConvexComb f e₁, iConvexComb f e₂] j = iConvexComb f (![e₁, e₂] j)
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ∑ i ∈ (Finsupp.single x s + Finsupp.single y t).support, (Finsupp.single x s + Finsupp.single y t) i = 1

pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ((Finsupp.single x s + Finsupp.single y t).support.weightedVSubOfPoint id y)
        ⇑(Finsupp.single x s + Finsupp.single y t) +ᵥ
      y =
    s • (x -ᵥ y) +ᵥ y

Tactic:
·

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ∑ i ∈ (Finsupp.single x s + Finsupp.single y t).support, (Finsupp.single x s + Finsupp.single y t) i = 1
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ∑ i ∈ (Finsupp.single x s + Finsupp.single y t).support, (Finsupp.single x s + Finsupp.single y t) i =
    (Finsupp.single x s + Finsupp.single y t).sum fun x r ↦ r

pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ((Finsupp.single x s + Finsupp.single y t).sum fun x r ↦ r) = 1

Tactic:
·

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ∑ i ∈ (Finsupp.single x s + Finsupp.single y t).support, (Finsupp.single x s + Finsupp.single y t) i =
    (Finsupp.single x s + Finsupp.single y t).sum fun x r ↦ r
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: case pos
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
y : Y
hy : y ∈ w.weights.support
⊢ (mapDomain f
        { weights := onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) ⋯, nonneg := ⋯, total := ⋯ }.weights)
      y =
    w.weights y

pp: case neg
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
y : Y
hy : y ∉ w.weights.support
⊢ (mapDomain f
        { weights := onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) ⋯, nonneg := ⋯, total := ⋯ }.weights)
      y =
    w.weights y

Tactic:
·

Goal state after:
case pos
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
y : Y
hy : y ∈ w.weights.support
⊢ (mapDomain f
        { weights := onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) ⋯, nonneg := ⋯, total := ⋯ }.weights)
      y =
    w.weights y
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ((Finsupp.single x s + Finsupp.single y t).sum fun x r ↦ r) = 1

Tactic:
·

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ((Finsupp.single x s + Finsupp.single y t).sum fun x r ↦ r) = 1
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: case neg
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
y : Y
hy : y ∉ w.weights.support
⊢ (mapDomain f
        { weights := onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) ⋯, nonneg := ⋯, total := ⋯ }.weights)
      y =
    w.weights y

Tactic:
·

Goal state after:
case neg
R : Type u_3
X : Type u_5
Y : Type u_6
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
inst✝ : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : ↑w.weights.support ⊆ f '' s
u : Finset X
hus : ↑u ⊆ s
hfu : InjOn f ↑u
huw : Finset.image f u = w.weights.support
y : Y
hy : y ∉ w.weights.support
⊢ (mapDomain f
        { weights := onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) ⋯, nonneg := ⋯, total := ⋯ }.weights)
      y =
    w.weights y
Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ convexCombPair s t hs ht h x y = (AffineMap.lineMap y x) s

Tactic:
by
  simp only [convexCombPair, AddTorsor.sConvexComb_eq_affineCombination, StdSimplex.duple,
    AffineMap.lineMap_apply]
  classical
  -- Use weighted subtraction with base point y
  rw [Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ id (b := y)]
  swap
  · -- Prove sum of weights equals 1
    trans (Finsupp.single x s + Finsupp.single y t).sum fun _ r => r
    · apply Finset.sum_congr rfl
      intro i _
      simp only [Finsupp.coe_add, Pi.add_apply]
    · rw [Finsupp.sum_add_index (by simp) (by simp), Finsupp.sum_single_index (by simp),
        Finsupp.sum_single_index (by simp), h]
  -- Now simplify the weighted subtraction
  congr 1
  rw [Finset.weightedVSubOfPoint_apply]
  simp only [id]
  -- Convert to Finsupp.sum
  change (Finsupp.single x s + Finsupp.single y t).sum (fun p w => w • (p -ᵥ y)) = _
  rw [Finsupp.sum_add_index (by simp) (fun _ a b => by simp [add_smul]),
    Finsupp.sum_single_index (by simp), Finsupp.sum_single_index (by simp)]
  simp [vsub_self]

Goal state after:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: case refine_1
R : Type u_3
X : Type u_5
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
s : Set X
Y : Type u_7
inst✝ : ConvexSpace R Y
t : Set Y
hs : IsConvexSet R s
ht : IsConvexSet R t
w : StdSimplex R (X × Y)
hw : ↑w.weights.support ⊆ s ×ˢ t
⊢ ↑(StdSimplex.map Prod.fst w).weights.support ⊆ s

pp: case refine_2
R : Type u_3
X : Type u_5
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
s : Set X
Y : Type u_7
inst✝ : ConvexSpace R Y
t : Set Y
hs : IsConvexSet R s
ht : IsConvexSet R t
w : StdSimplex R (X × Y)
hw : ↑w.weights.support ⊆ s ×ˢ t
⊢ ↑(StdSimplex.map Prod.snd w).weights.support ⊆ t

Tactic:
·

Goal state after:
case refine_1
R : Type u_3
X : Type u_5
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
s : Set X
Y : Type u_7
inst✝ : ConvexSpace R Y
t : Set Y
hs : IsConvexSet R s
ht : IsConvexSet R t
w : StdSimplex R (X × Y)
hw : ↑w.weights.support ⊆ s ×ˢ t
⊢ ↑(StdSimplex.map Prod.fst w).weights.support ⊆ s
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: case refine_2
R : Type u_3
X : Type u_5
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
s : Set X
Y : Type u_7
inst✝ : ConvexSpace R Y
t : Set Y
hs : IsConvexSet R s
ht : IsConvexSet R t
w : StdSimplex R (X × Y)
hw : ↑w.weights.support ⊆ s ×ˢ t
⊢ ↑(StdSimplex.map Prod.snd w).weights.support ⊆ t

Tactic:
·

Goal state after:
case refine_2
R : Type u_3
X : Type u_5
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : ConvexSpace R X
s : Set X
Y : Type u_7
inst✝ : ConvexSpace R Y
t : Set Y
hs : IsConvexSet R s
ht : IsConvexSet R t
w : StdSimplex R (X × Y)
hw : ↑w.weights.support ⊆ s ×ˢ t
⊢ ↑(StdSimplex.map Prod.snd w).weights.support ⊆ t