mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i₀ : ι
⊢ vectorSpan k (range p) = Submodule.span k (range fun i ↦ p ↑i -ᵥ p i₀)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ a • max (f x) (f y) + b • max (f x) (f y)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
j : ι
w₁ w₂ : ι → k
hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i
⊢ (s.weightedVSubOfPoint p (p j)) w₁ = (s.weightedVSubOfPoint p (p j)) w₂

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
A : Set P
inst✝ : Nonempty ↑A
x : P
hx : x ∈ affineSpan k A
c : k
u : P
hu : u ∈ affineSpan k A
v : P
hv : v ∈ affineSpan k A
w : P
hw : w ∈ affineSpan k A
⊢ ⟨u, hu⟩ ∈ affineSpan k (Subtype.val ⁻¹' A) →
    ⟨v, hv⟩ ∈ affineSpan k (Subtype.val ⁻¹' A) →
      ⟨w, hw⟩ ∈ affineSpan k (Subtype.val ⁻¹' A) → ⟨c • (u -ᵥ v) +ᵥ w, ⋯⟩ ∈ affineSpan k (Subtype.val ⁻¹' A)

Tactic:
exact AffineSubspace.smul_vsub_vadd_mem _ _

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y ≤ a • max (f x) (f y) + b • max (f x) (f y)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
A : Set P
inst✝ : Nonempty ↑A
⊢ affineSpan k (Subtype.val ⁻¹' A) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : ∑ i ∈ s, w i = 0
b₁ b₂ : P
⊢ (s.weightedVSubOfPoint p b₁) w = (s.weightedVSubOfPoint p b₂) w

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set V
p : P
h : Submodule.span k (range Subtype.val) = ⊤
⊢ affineSpan k ({p} ∪ (fun v ↦ v +ᵥ p) '' s) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
hfx : f x ≤ f (a • x + b • y)
⊢ f (a • x + b • y) ≤ f y

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
⊢ vectorSpan k {p₁, p₂} = k ∙ (p₁ -ᵥ p₂)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
⊢ vectorSpan k {p₁, p₂} = k ∙ (p₂ -ᵥ p₁)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hyz : f y ≤ f z
⊢ f z ≤ f x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
v : V
⊢ v ∈ vectorSpan k {p₁, p₂} ↔ ∃ r, r • (p₁ -ᵥ p₂) = v

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hxz : f x ≤ f z
⊢ f z ≤ f y

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
v : V
⊢ v ∈ vectorSpan k {p₁, p₂} ↔ ∃ r, r • (p₂ -ᵥ p₁) = v

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
v : V
⊢ v +ᵥ p₁ ∈ line[k, p₁, p₂] ↔ ∃ r, r • (p₂ -ᵥ p₁) = v

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hfx : f x < f (a • x + b • y)
⊢ f (a • x + b • y) < f y

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ : P
v : V
⊢ v +ᵥ p₂ ∈ line[k, p₁, p₂] ↔ ∃ r, r • (p₁ -ᵥ p₂) = v

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hyz : f y < f z
⊢ f z < f x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hxz : f x < f z
⊢ f z < f y

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p p₁ p₂ : P
h : ∃ r, r • (p₂ -ᵥ p₁) = p -ᵥ p₁
⊢ ∃ r, (AffineMap.lineMap p₁ p₂) r = p

Tactic:
obtain ⟨r, hr⟩ := h

Goal state after:
case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p p₁ p₂ : P
r : k
hr : r • (p₂ -ᵥ p₁) = p -ᵥ p₁
⊢ ∃ r, (AffineMap.lineMap p₁ p₂) r = p
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p p₁ p₂ : P
⊢ p ∈ line[k, p₁, p₂] ↔ ∃ r, (AffineMap.lineMap p₁ p₂) r = p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p p₁ p₂ : P
⊢ p ∈ line[k, p₁, p₂] ↔ ∃ r, (AffineMap.lineMap p₂ p₁) r = p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
⊢ (s.weightedVSubOfPoint p b₁) w +ᵥ b₁ = (s.weightedVSubOfPoint p b₂) w +ᵥ b₂

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ((s.erase i).weightedVSubOfPoint p (p i)) w = (s.weightedVSubOfPoint p (p i)) w

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ((insert i s).weightedVSubOfPoint p (p i)) w = (s.weightedVSubOfPoint p (p i)) w

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
w : ι → k
p : ι → P
b : P
s₁ s₂ : Finset ι
h : s₁ ⊆ s₂
⊢ (s₁.weightedVSubOfPoint p b) w = (s₂.weightedVSubOfPoint p b) ((↑s₁).indicator w)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
b : P
⊢ ((map e s₂).weightedVSubOfPoint p b) w = (s₂.weightedVSubOfPoint (p ∘ ⇑e) b) (w ∘ ⇑e)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ ConvexOn 𝕜 s (-f) ↔ ConcaveOn 𝕜 s f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ p₂ : ι → P
b : P
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) = ∑ i ∈ s, w i • (p₁ i -ᵥ b) - ∑ i ∈ s, w i • (p₂ i -ᵥ b)

Tactic:
← sum_sub_distrib,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ p₂ : ι → P
b : P
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) = ∑ x ∈ s, (w x • (p₁ x -ᵥ b) - w x • (p₂ x -ᵥ b))
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ p₂ : ι → P
b : P
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) = (s.weightedVSubOfPoint p₁ b) w - (s.weightedVSubOfPoint p₂ b) w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ ConcaveOn 𝕜 s (-f) ↔ ConvexOn 𝕜 s f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ : ι → P
p₂ b : P
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (s.weightedVSubOfPoint p₁ b) w - (∑ i ∈ s, w i) • (p₂ -ᵥ b)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₂ : ι → P
p₁ b : P
⊢ ∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = (∑ i ∈ s, w i) • (p₁ -ᵥ b) - (s.weightedVSubOfPoint p₂ b) w

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
⊢ ((s \ s₂).weightedVSubOfPoint p b) w + (s₂.weightedVSubOfPoint p b) w = (s.weightedVSubOfPoint p b) w

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
⊢ ((s \ s₂).weightedVSubOfPoint p b) w - (s₂.weightedVSubOfPoint p b) (-w) = (s.weightedVSubOfPoint p b) w

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
⊢ (((Finset.subtype pred s).weightedVSubOfPoint (fun i ↦ p ↑i) b) fun i ↦ w ↑i) =
    ({x ∈ s | pred x}.weightedVSubOfPoint p b) w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ StrictConvexOn 𝕜 s (-f) ↔ StrictConcaveOn 𝕜 s f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ StrictConcaveOn 𝕜 s (-f) ↔ StrictConvexOn 𝕜 s f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ i ∈ s, w i ≠ 0 → pred i
⊢ ({x ∈ s | pred x}.weightedVSubOfPoint p b) w = (s.weightedVSubOfPoint p b) w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
⊢ f 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCancelCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : Module 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
c x : E
hx : x ∈ (fun z ↦ c + z) ⁻¹' s
y : E
hy : y ∈ (fun z ↦ c + z) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCancelCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : Module 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
c : E
⊢ StrictConvexOn 𝕜 ((fun z ↦ c + z) ⁻¹' s) (f ∘ fun z ↦ z + c)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → ℝ
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul : ∀ (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x
x : E
⊢ f (-x) = f x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
c : k
⊢ (s.weightedVSubOfPoint p b) (c • w) = c • (s.weightedVSubOfPoint p b) w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCancelCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : Module 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
hf : StrictConcaveOn 𝕜 s f
c : E
⊢ StrictConcaveOn 𝕜 ((fun z ↦ c + z) ⁻¹' s) (f ∘ fun z ↦ z + c)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
⊢ (s.weightedVSub p) w = ∑ i ∈ s, w i • (p i -ᵥ Classical.choice ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
s : Set E
f : E → β
c : 𝕜
hc : 0 ≤ c
hf : ConvexOn 𝕜 s f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ c • (a • f x + b • f y) = a • c • f x + b • c • f y

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : P
h : ∑ i ∈ s, w i = 0
⊢ (s.weightedVSub fun x ↦ p) w = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_5
inst✝⁸ : Field 𝕜
inst✝⁷ : LinearOrder 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : SMul 𝕜 β
f : F → β
g : E →ᵃ[𝕜] F
s : Set F
hf : ConvexOn 𝕜 s f
x : E
hx : x ∈ ⇑g ⁻¹' s
y : E
hy : y ∈ ⇑g ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (g (a • x + b • y)) = f (a • g x + b • g y)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
w : ι → k
p : ι → P
⊢ (∅.weightedVSub p) w = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
v : V
⊢ (s.weightedVSub (v +ᵥ p)) w = (s.weightedVSub p) w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
⊢ f (r • x) = ‖r‖ * f x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
ι : Type u_4
G : Type u_6
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → V
a : G
⊢ (s.weightedVSub (a • p)) w = a • (s.weightedVSub p) w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddGroup E
inst✝ : SMul 𝕜 E
f g : Seminorm 𝕜 E
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ : ι → P
p₂ : P
h : ∑ i ∈ s, w i = 0
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (s.weightedVSub p₁) w

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝⁵ : SeminormedRing 𝕜
inst✝⁴ : AddGroup E
inst✝³ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x : E
r✝ : ℝ
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : Seminorm 𝕜 E
x✝¹ : 𝕜
x✝ : E
⊢ r • p (x✝¹ • x✝) = ‖x✝¹‖ * r • p x✝

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x✝ : E
r : ℝ
p q : Seminorm 𝕜 E
a : 𝕜
x : E
⊢ p (a • x) + q (a • x) = ‖a‖ * (p x + q x)

Tactic:
by

Goal state after: