awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
e_a :
  ∑ x_1 ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) x_1 : R) (x_1 -ᵥ y) =
    s • (x -ᵥ y)
⊢ ∑ i ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i : R) (id i -ᵥ y) =
    s • (x -ᵥ y)

Tactic:
simp only [id]

Premises used: id
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
e_a :
  ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).sum fun (p : P) (w : R) ↦ w • (p -ᵥ y)) =
    s • (x -ᵥ y)
⊢ ∑ x_1 ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) x_1 : R) (x_1 -ᵥ y) =
    s • (x -ᵥ y)

Tactic:
change (Finsupp.single x s + Finsupp.single y t).sum (fun p w => w • (p -ᵥ y)) = _

Premises used: Finsupp.sum, VSub.vsub, HAdd.hAdd, HSMul.hSMul, Finsupp.single
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ∀ a ∈ Finsupp.support (Finsupp.single x s) ∪ Finsupp.support (Finsupp.single y t),
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (a -ᵥ y) = 0

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y x_1 : P
a : x_1 ∈ Finsupp.support (Finsupp.single x s) ∪ Finsupp.support (Finsupp.single y t)
b : R
⊢ ∀ (b₂ : R), (b + b₂) • (x_1 -ᵥ y) = b • (x_1 -ᵥ y) + b₂ • (x_1 -ᵥ y)

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x -ᵥ y) = 0

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (y -ᵥ y) = 0

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
e_a : s • (x -ᵥ y) + t • (y -ᵥ y) = s • (x -ᵥ y)
⊢ ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).sum fun (p : P) (w : R) ↦ w • (p -ᵥ y)) =
    s • (x -ᵥ y)

Tactic:
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)]

Premises used: Finsupp.sum_single_index, Finsupp.sum_add_index
-- Module: Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ s • (x -ᵥ y) + t • (y -ᵥ y) = s • (x -ᵥ y)

Tactic:
simp [vsub_self]

Premises used: vsub_self
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
w : StdSimplex R M
i : M
⊢ LE.le.{u} (α := R) (0 : R) ((w.weights : (a : M) → R) i : R)

Tactic:
w.nonneg i

Premises used: Convexity.StdSimplex.nonneg
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
inst_2 : Nontrivial R
total : Eq.{u + 1} (α := R) (sum 0 fun (x : M) (r : R) ↦ r) 1
⊢ False

Tactic:
simp at total
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
inst_2 : Nontrivial R
w : StdSimplex R M
⊢ w.weights.support.Nonempty

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
inst_2 : Nontrivial R
w : StdSimplex R M
⊢ Nonempty M

Tactic:
w.support_weights_nonempty.to_type

Premises used: Finset.Nonempty.to_type, Convexity.StdSimplex.support_weights_nonempty
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
f g : StdSimplex R M
mk :
  ∀ (weights : M →₀ R) (nonneg : 0 ≤ weights) (total : Eq (α := R) (weights.sum fun (x : M) (r : R) ↦ r) 1),
    { weights := weights, nonneg := nonneg, total := total : StdSimplex R M }.weights = g.weights ↔
      { weights := weights, nonneg := nonneg, total := total : StdSimplex R M } = g
⊢ f.weights = g.weights ↔ f = g

Tactic:
cases f
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
g : StdSimplex R M
weights : M →₀ R
nonneg : 0 ≤ weights
total : Eq (α := R) (weights.sum fun (x : M) (r : R) ↦ r) 1
mk :
  ∀ (weights_1 : M →₀ R) (nonneg_1 : 0 ≤ weights_1) (total_1 : Eq (α := R) (weights_1.sum fun (x : M) (r : R) ↦ r) 1),
    { weights := weights, nonneg := nonneg, total := total : StdSimplex R M }.weights =
        { weights := weights_1, nonneg := nonneg_1, total := total_1 : StdSimplex R M }.weights ↔
      { weights := weights, nonneg := nonneg, total := total : StdSimplex R M } =
        { weights := weights_1, nonneg := nonneg_1, total := total_1 }
⊢ { weights := weights, nonneg := nonneg, total := total : StdSimplex R M }.weights = g.weights ↔
    { weights := weights, nonneg := nonneg, total := total : StdSimplex R M } = g

Tactic:
cases g
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
weights : M →₀ R
nonneg : 0 ≤ weights
total : Eq (α := R) (weights.sum fun (x : M) (r : R) ↦ r) 1
weights_1 : M →₀ R
nonneg_1 : 0 ≤ weights_1
total_1 : Eq (α := R) (weights_1.sum fun (x : M) (r : R) ↦ r) 1
⊢ { weights := weights, nonneg := nonneg, total := total : StdSimplex R M }.weights =
      { weights := weights_1, nonneg := nonneg_1, total := total_1 : StdSimplex R M }.weights ↔
    { weights := weights, nonneg := nonneg, total := total : StdSimplex R M } =
      { weights := weights_1, nonneg := nonneg_1, total := total_1 }

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R_1 : Type u_1
X : Type u_2
M_1 : Type u_3
N_1 : Type u_4
P_1 : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
P : Type u_11
w : StdSimplex R M
x_1 : M
inst_2 : IsStrictOrderedRing R
x : M
⊢ LE.le (α := M →₀ R) 0 (Finsupp.single x 1)

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R_1 : Type u_1
X : Type u_2
M_1 : Type u_3
N_1 : Type u_4
P_1 : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
P : Type u_11
w : StdSimplex R M
x_1 : M
inst_2 : IsStrictOrderedRing R
x : M
⊢ Eq.{u + 1} (α := R) (sum (Finsupp.single x 1) fun (x : M) (r : R) ↦ r) 1

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
inst_2 : IsStrictOrderedRing R
x : M
nonneg : LE.le (α := M →₀ R) 0 (Finsupp.single x 1)
total : Eq.{u + 1} (α := R) (sum (Finsupp.single x 1) fun (x : M) (r : R) ↦ r) 1
⊢ { weights := Finsupp.single x 1, nonneg := nonneg, total := total : StdSimplex R M } = single x

Tactic:
rfl

Premises used: Convexity.StdSimplex.single, rfl
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst_2 : IsStrictOrderedRing R
rw : (∃ (b : R), b ≠ 0 ∧ w.weights = Finsupp.single x b) → w = single x
⊢ w.weights.support = {x} → w = single x

Tactic:
rw [support_eq_singleton']

Premises used: Finsupp.support_eq_singleton'
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst_2 : IsStrictOrderedRing R
a : R
ha : a ≠ 0
hwa : w.weights = Finsupp.single x a
a₁ : w.weights = weights (single x)
⊢ w = single x

Tactic:
ext : 1
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst_2 : IsStrictOrderedRing R
a : R
ha : a ≠ 0
hwa : w.weights = Finsupp.single x a
a₁ : Eq (α := M →₀ R) (Finsupp.single x a) (Finsupp.single x 1)
⊢ w.weights = weights (single x)

Tactic:
simp only [hwa, weights_single]

Premises used: Convexity.StdSimplex.weights_single
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst_2 : IsStrictOrderedRing R
a : R
ha : a ≠ 0
hwa : w.weights = Finsupp.single x a
a₁ : a = 1
⊢ Eq (α := M →₀ R) (Finsupp.single x a) (Finsupp.single x 1)

Tactic:
congr
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst_2 : IsStrictOrderedRing R
a : R
ha : a ≠ 0
hwa : w.weights = Finsupp.single x a
⊢ a = 1

Tactic:
simpa [hwa] using w.total

Premises used: Convexity.StdSimplex.total
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst_2 : IsStrictOrderedRing R
rw rw₁ rw₂ : (∃ (b : R), b ≠ 0 ∧ w.weights = Finsupp.single x b) → w = single x
rw₃ : ∀ (a : R) (ha : a ≠ 0) (hwa : w.weights = Finsupp.single x a), w = single x
a : ∀ (a : R) (ha : a ≠ 0) (hwa : w.weights = Finsupp.single x a), w.weights = weights (single x)
a₁ :
  ∀ (a : R) (ha : a ≠ 0) (hwa : w.weights = Finsupp.single x a),
    Eq (α := M →₀ R) (Finsupp.single x a) (Finsupp.single x 1)
a₂ : ∀ (a : R) (ha : a ≠ 0) (hwa : w.weights = Finsupp.single x a), a = 1
⊢ w.weights.support = {x} → w = single x

Tactic:
classical
    rw [support_eq_singleton']
    rintro ⟨a, ha, hwa⟩
    ext : 1
    simp only [hwa, weights_single]
    congr
    simpa [hwa] using w.total

Premises used: Convexity.StdSimplex.weights_single, Convexity.StdSimplex.total, Finsupp.support_eq_singleton'
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
x : M
inst_2 : IsStrictOrderedRing R
⊢ support.{u_9, u} (M := R) (weights (single x)) = {x}

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R_1 : Type u_1
X : Type u_2
M_1 : Type u_3
N_1 : Type u_4
P_1 : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
P : Type u_11
w : StdSimplex R M
x_1 : M
inst_2 : IsStrictOrderedRing R
x y : M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
⊢ LE.le (α := M →₀ R) 0 (Finsupp.single x s)

Tactic:
simpa
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R_1 : Type u_1
X : Type u_2
M_1 : Type u_3
N_1 : Type u_4
P_1 : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
P : Type u_11
w : StdSimplex R M
x_1 : M
inst_2 : IsStrictOrderedRing R
x y : M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
⊢ LE.le (α := M →₀ R) 0 (Finsupp.single y t)

Tactic:
simpa
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R_1 : Type u_1
X : Type u_2
M_1 : Type u_3
N_1 : Type u_4
P_1 : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
P : Type u_11
w : StdSimplex R M
x_1 : M
inst_2 : IsStrictOrderedRing R
x y : M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
⊢ Eq (α := R) ((HAdd.hAdd (α := M →₀ R) (Finsupp.single x s) (Finsupp.single y t)).sum fun (x : M) (r : R) ↦ r) 1

Tactic:
simpa [sum_add_index]

Premises used: Finsupp.sum_add_index
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R_1 : Type u_1
X : Type u_2
M_1 : Type u_3
N_1 : Type u_4
P_1 : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
P : Type u_11
w : StdSimplex R M
x_1 : M
inst_2 : IsStrictOrderedRing R
x y : M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
⊢ Eq (α := R) ((HAdd.hAdd (α := M →₀ R) (Finsupp.single x s) (Finsupp.single y t)).sum fun (x : M) (r : R) ↦ r) 1

Tactic:
classical simpa [sum_add_index]

Premises used: Finsupp.sum_add_index
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R_1 : Type u_1
X : Type u_2
M_1 : Type u_3
N_1 : Type u_4
P_1 : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M_2 : Type u_9
N_2 : Type u_10
P : Type u_11
w : StdSimplex R M_2
x : M_2
inst_2 : IsStrictOrderedRing R
M : Type v
N : Type w
g : M → N
f : StdSimplex R M
⊢ Eq (α := R) ((mapDomain g f.weights).sum fun (x : N) (r : R) ↦ r) 1

Tactic:
simp [sum_mapDomain_index]

Premises used: Finsupp.sum_mapDomain_index
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
inst_2 : IsStrictOrderedRing R
f : StdSimplex R M
x : N
a :
  ∀ (a : N),
    Eq.{u + 1} (α := R) ((weights (map (fun (x_1 : M) ↦ x) f) : (a : N) → R) a : R)
      ((weights (single x) : (a : N) → R) a : R)
⊢ map (fun (x_1 : M) ↦ x) f = single x

Tactic:
ext a
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
inst_2 : IsStrictOrderedRing R
f : StdSimplex R M
x a : N
pos :
  x = a →
    Eq.{u + 1} (α := R) ((weights (map (fun (x_1 : M) ↦ x) f) : (a : N) → R) a : R)
      ((weights (single x) : (a : N) → R) a : R)
neg :
  ¬x = a →
    Eq.{u + 1} (α := R) ((weights (map (fun (x_1 : M) ↦ x) f) : (a : N) → R) a : R)
      ((weights (single x) : (a : N) → R) a : R)
⊢ Eq.{u + 1} (α := R) ((weights (map (fun (x_1 : M) ↦ x) f) : (a : N) → R) a : R)
    ((weights (single x) : (a : N) → R) a : R)

Tactic:
by_cases x = a
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
inst_2 : IsStrictOrderedRing R
f : StdSimplex R M
x a : N
h : x = a
⊢ Eq.{u + 1} (α := R) ((weights (map (fun (x_1 : M) ↦ x) f) : (a : N) → R) a : R)
    ((weights (single x) : (a : N) → R) a : R)

Tactic:
simp [*, mapDomain]

Premises used: Finsupp.mapDomain
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
inst_2 : IsStrictOrderedRing R
f : StdSimplex R M
x a : N
h : ¬x = a
⊢ Eq.{u + 1} (α := R) ((weights (map (fun (x_1 : M) ↦ x) f) : (a : N) → R) a : R)
    ((weights (single x) : (a : N) → R) a : R)

Tactic:
simp [*, mapDomain]

Premises used: Finsupp.mapDomain
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
inst_2 : IsStrictOrderedRing R
x : M
f : M → N
a :
  ∀ (a : N),
    Eq.{u + 1} (α := R) ((weights (map f (single x)) : (a : N) → R) a : R)
      ((weights (single (f x)) : (a : N) → R) a : R)
⊢ Eq (α := StdSimplex R N) (map f (single x)) (single (f x))

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
inst_2 : IsStrictOrderedRing R
x : M
f : M → N
a : N
⊢ Eq.{u + 1} (α := R) ((weights (map f (single x)) : (a : N) → R) a : R) ((weights (single (f x)) : (a : N) → R) a : R)

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
inst_2 : IsStrictOrderedRing R
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : M
f : M → N
a :
  ∀ (a : N),
    Eq.{u + 1} (α := R) (((map f (duple x y hs ht h)).weights : (a : N) → R) a : R)
      (((duple (f x) (f y) hs ht h).weights : (a : N) → R) a : R)
⊢ map f (duple x y hs ht h) = duple (f x) (f y) hs ht h

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
inst_2 : IsStrictOrderedRing R
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : M
f : M → N
a : N
⊢ Eq.{u + 1} (α := R) (((map f (duple x y hs ht h)).weights : (a : N) → R) a : R)
    (((duple (f x) (f y) hs ht h).weights : (a : N) → R) a : R)

Tactic:
simp [mapDomain_add]

Premises used: Finsupp.mapDomain_add
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
inst_2 : IsStrictOrderedRing R
f : StdSimplex R M
a : ∀ (a : M), Eq.{u + 1} (α := R) (((map id f).weights : (a : M) → R) a : R) ((f.weights : (a : M) → R) a : R)
⊢ map id f = f

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
inst_2 : IsStrictOrderedRing R
f : StdSimplex R M
a : M
⊢ Eq.{u + 1} (α := R) (((map id f).weights : (a : M) → R) a : R) ((f.weights : (a : M) → R) a : R)

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
P : Type u_11
inst_2 : IsStrictOrderedRing R
f : StdSimplex R M
g₁ : M → N
g₂ : N → P
a :
  ∀ (a : P),
    Eq.{u + 1} (α := R) (((map (g₂ ∘ g₁) f).weights : (a : P) → R) a : R)
      (((map g₂ (map g₁ f)).weights : (a : P) → R) a : R)
⊢ map (g₂ ∘ g₁) f = map g₂ (map g₁ f)

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
P : Type u_11
inst_2 : IsStrictOrderedRing R
f : StdSimplex R M
g₁ : M → N
g₂ : N → P
a : P
⊢ Eq.{u + 1} (α := R) (((map (g₂ ∘ g₁) f).weights : (a : P) → R) a : R)
    (((map g₂ (map g₁ f)).weights : (a : P) → R) a : R)

Tactic:
simp [mapDomain_comp]

Premises used: Finsupp.mapDomain_comp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
P : Type u_11
inst_2 : IsStrictOrderedRing R
f : StdSimplex R M
g₁ : M → N
g₂ : N → P
⊢ map g₂ (map g₁ f) = map (fun (x : M) ↦ g₂ (g₁ x)) f

Tactic:
(map_comp ..).symm

Premises used: Convexity.StdSimplex.map_comp, Eq.symm
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R_1 : Type u_1
X : Type u_2
M_1 : Type u_3
N_1 : Type u_4
P_1 : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
P : Type u_11
w : StdSimplex R M
x : M
inst_2 : IsStrictOrderedRing R
f : StdSimplex R (StdSimplex R M)
⊢ Eq.{u + 1} (α := R) (sum (f.weights.sum fun (d : StdSimplex R M) (r : R) ↦ r • d.weights) fun (x : M) (r : R) ↦ r) 1

Tactic:
simp [sum_sum_index, sum_smul_index, ← mul_sum]

Premises used: Finsupp.sum_smul_index, Finsupp.mul_sum, Finsupp.sum_sum_index
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
inst_2 : IsStrictOrderedRing R
f : StdSimplex R (StdSimplex R (StdSimplex R M))
a : f.join.join.weights = weights (join (map (fun (x : StdSimplex R (StdSimplex R M)) ↦ x.join) f))
⊢ f.join.join = join (map (fun (x : StdSimplex R (StdSimplex R M)) ↦ x.join) f)

Tactic:
ext1
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
inst_2 : IsStrictOrderedRing R
f : StdSimplex R (StdSimplex R (StdSimplex R M))
⊢ f.join.join.weights = weights (join (map (fun (x : StdSimplex R (StdSimplex R M)) ↦ x.join) f))

Tactic:
simp [mapDomain, add_smul, sum_sum_index, sum_smul_index, smul_sum, mul_smul]

Premises used: Finsupp.sum_smul_index, Finsupp.mapDomain, add_smul, Finsupp.smul_sum, SemigroupAction.mul_smul, Finsupp.sum_sum_index
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
inst_2 : IsStrictOrderedRing R
f : StdSimplex R (StdSimplex R M)
g : M → N
a : (map g f.join).weights = weights (join (map (fun (x : StdSimplex R M) ↦ map g x) f))
⊢ map g f.join = join (map (fun (x : StdSimplex R M) ↦ map g x) f)

Tactic:
ext1
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
inst_2 : IsStrictOrderedRing R
f : StdSimplex R (StdSimplex R M)
g : M → N
⊢ (map g f.join).weights = weights (join (map (fun (x : StdSimplex R M) ↦ map g x) f))

Tactic:
simp [mapDomain, add_smul, sum_sum_index, sum_smul_index, smul_sum]

Premises used: Finsupp.sum_smul_index, Finsupp.mapDomain, add_smul, Finsupp.smul_sum, Finsupp.sum_sum_index
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
inst_2 : IsStrictOrderedRing R
x : StdSimplex R M
a : ∀ (a : M), Eq.{u + 1} (α := R) (((join (single x)).weights : (a : M) → R) a : R) ((x.weights : (a : M) → R) a : R)
⊢ join (single x) = x

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
inst_2 : IsStrictOrderedRing R
x : StdSimplex R M
a : M
⊢ Eq.{u + 1} (α := R) (((join (single x)).weights : (a : M) → R) a : R) ((x.weights : (a : M) → R) a : R)

Tactic:
simp [join, ← mk_single]

Premises used: Convexity.StdSimplex.mk_single, Convexity.StdSimplex.join
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
X : Type u_2
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
w : StdSimplex K X
p : X → Prop
inst_3 : DecidablePred p
⊢ ∀ i ∈ (filter p w.weights).support, LE.le.{u_8} (α := K) (0 : K) ((filter p w.weights : (a : X) → K) i : K)

Tactic:
simp [filter_apply, apply_ite]

Premises used: apply_ite, Finsupp.filter_apply
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
X : Type u_2
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
w : StdSimplex K X
p : X → Prop
inst_3 : DecidablePred p
hp : ∃ (a : X), p a ∧ Ne.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) a : K) (0 : K)
⊢ ∀ i ∈ (filter p w.weights).support, LT.lt.{u_8} (α := K) (0 : K) ((filter p w.weights : (a : X) → K) i : K)

Tactic:
simp +contextual [lt_iff_le_and_ne, eq_comm]

Premises used: lt_iff_le_and_ne, eq_comm
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
X : Type u_2
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
w : StdSimplex K X
p : X → Prop
inst_3 : DecidablePred p
hp : ∃ (a : X), p a ∧ Ne.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) a : K) (0 : K)
⊢ filter p w.weights ≠ 0

Tactic:
simpa [ne_iff, filter_apply]

Premises used: Finsupp.filter_apply, Finsupp.ne_iff