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

Goal state before:
pp: case refine_1
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 P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) ≤ Submodule.span k ((fun x ↦ p -ᵥ x) '' s)

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
s : Set P
p : P
hp : p ∈ s
⊢ (fun x ↦ p -ᵥ x) '' s ⊆ s -ᵥ s

Tactic:
·

Goal state after:
case refine_1
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 P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) ≤ Submodule.span k ((fun x ↦ p -ᵥ x) '' s)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case refine_1
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 P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) ≤ Submodule.span k ((fun x ↦ p -ᵥ x) '' s)

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
s : Set P
p : P
hp : p ∈ s
⊢ (fun x ↦ p -ᵥ x) '' s ⊆ s -ᵥ s

Tactic:
· rw [Submodule.span_le]
    rintro v ⟨p₁, hp₁, p₂, hp₂, hv⟩
    simp_rw [← vsub_sub_vsub_cancel_left p₁ p₂ p] at hv
    rw [← hv, SetLike.mem_coe, Submodule.mem_span]
    exact fun m hm => Submodule.sub_mem _ (hm ⟨p₂, hp₂, rfl⟩) (hm ⟨p₁, hp₁, rfl⟩)

Goal state after:
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
s : Set P
p : P
hp : p ∈ s
⊢ (fun x ↦ p -ᵥ x) '' s ⊆ s -ᵥ s
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
s : Set P
p : P
hp : p ∈ s
⊢ (fun x ↦ p -ᵥ x) '' s ⊆ s -ᵥ s

Tactic:
·

Goal state after:
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
s : Set P
p : P
hp : p ∈ s
⊢ (fun x ↦ p -ᵥ x) '' s ⊆ s -ᵥ s
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case refine_1
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 P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) ≤ Submodule.span k ((fun x ↦ x -ᵥ p) '' s)

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
s : Set P
p : P
hp : p ∈ s
⊢ (fun x ↦ x -ᵥ p) '' s ⊆ s -ᵥ s

Tactic:
·

Goal state after:
case refine_1
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 P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) ≤ Submodule.span k ((fun x ↦ x -ᵥ p) '' s)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case refine_1
𝕜 : 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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ a • (f ⊔ g) x + b • (f ⊔ g) y

pp: case refine_2
𝕜 : 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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ g (a • x + b • y) ≤ a • (f ⊔ g) x + b • (f ⊔ g) y

Tactic:
·

Goal state after:
case refine_1
𝕜 : 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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ a • (f ⊔ g) x + b • (f ⊔ g) y
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
s : Set P
p : P
hp : p ∈ s
⊢ (fun x ↦ x -ᵥ p) '' s ⊆ s -ᵥ s

Tactic:
·

Goal state after:
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
s : Set P
p : P
hp : p ∈ s
⊢ (fun x ↦ x -ᵥ p) '' s ⊆ s -ᵥ s
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case refine_2
𝕜 : 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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ g (a • x + b • y) ≤ a • (f ⊔ g) x + b • (f ⊔ g) y

Tactic:
·

Goal state after:
case refine_2
𝕜 : 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 g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ g (a • x + b • y) ≤ a • (f ⊔ g) x + b • (f ⊔ g) y
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
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v) → ∃ a, ∃ (_ : a ≠ i₀), p i₀ -ᵥ p a = v

pp: case mpr
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₀ : ι
v : V
⊢ (∃ a, ∃ (_ : a ≠ i₀), p i₀ -ᵥ p a = v) → ∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v

Tactic:
·

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
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v) → ∃ a, ∃ (_ : a ≠ i₀), p i₀ -ᵥ p a = v
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case mpr
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₀ : ι
v : V
⊢ (∃ a, ∃ (_ : a ≠ i₀), p i₀ -ᵥ p a = v) → ∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v

Tactic:
·

Goal state after:
case mpr
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₀ : ι
v : V
⊢ (∃ a, ∃ (_ : a ≠ i₀), p i₀ -ᵥ p a = v) → ∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v
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
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v) → ∃ a, ∃ (_ : a ≠ i₀), p a -ᵥ p i₀ = v

pp: case mpr
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₀ : ι
v : V
⊢ (∃ a, ∃ (_ : a ≠ i₀), p a -ᵥ p i₀ = v) → ∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v

Tactic:
·

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
ι : Type u_4
p : ι → P
i₀ : ι
v : V
⊢ (∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v) → ∃ a, ∃ (_ : a ≠ i₀), p a -ᵥ p i₀ = v
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case hb
𝕜 : 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
⊢ f x ≤ max (f x) (f y)

pp: case hb
𝕜 : 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
⊢ f y ≤ max (f x) (f y)

Tactic:
·

Goal state after:
case hb
𝕜 : 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
⊢ f x ≤ max (f x) (f y)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case mpr
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₀ : ι
v : V
⊢ (∃ a, ∃ (_ : a ≠ i₀), p a -ᵥ p i₀ = v) → ∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v

Tactic:
·

Goal state after:
case mpr
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₀ : ι
v : V
⊢ (∃ a, ∃ (_ : a ≠ i₀), p a -ᵥ p i₀ = v) → ∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case hb
𝕜 : 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
⊢ f y ≤ max (f x) (f y)

Tactic:
·

Goal state after:
case hb
𝕜 : 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
⊢ f y ≤ max (f x) (f y)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case e_f.inl
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
i : ι
h : i = j
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)

pp: case e_f.inr
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
i : ι
h : i ≠ j
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)

Tactic:
·

Goal state after:
case e_f.inl
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
i : ι
h : i = j
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case e_f.inr
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
i : ι
h : i ≠ j
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)

Tactic:
·

Goal state after:
case e_f.inr
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
i : ι
h : i ≠ j
⊢ w₁ i • (p i -ᵥ p j) = w₂ i • (p i -ᵥ p j)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case hb
𝕜 : 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
⊢ f x ≤ max (f x) (f y)

pp: case hb
𝕜 : 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
⊢ f y ≤ max (f x) (f y)

Tactic:
·

Goal state after:
case hb
𝕜 : 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
⊢ f x ≤ max (f x) (f y)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case refine_1
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
y : P
hy : y ∈ A
⊢ ⟨y, ⋯⟩ ∈ affineSpan k (Subtype.val ⁻¹' A)

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:
·

Goal state after:
case refine_1
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
y : P
hy : y ∈ A
⊢ ⟨y, ⋯⟩ ∈ affineSpan k (Subtype.val ⁻¹' A)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case hb
𝕜 : 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
⊢ f y ≤ max (f x) (f y)

Tactic:
·

Goal state after:
case hb
𝕜 : 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
⊢ f y ≤ max (f x) (f y)
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:
·

Goal state after:
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)
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
⊢ p ∈ line[k, p₁, p₂] → ∃ r, (AffineMap.lineMap p₁ p₂) r = p

pp: case mpr
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, (AffineMap.lineMap p₁ p₂) r = p) → p ∈ line[k, p₁, p₂]

Tactic:
·

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
⊢ p ∈ line[k, p₁, p₂] → ∃ r, (AffineMap.lineMap p₁ p₂) r = p
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case mp
𝕜 : 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

pp: case mpr
𝕜 : 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:
·

Goal state after:
case mp
𝕜 : 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
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case mpr
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, (AffineMap.lineMap p₁ p₂) r = p) → p ∈ line[k, p₁, p₂]

Tactic:
·

Goal state after:
case mpr
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, (AffineMap.lineMap p₁ p₂) r = p) → p ∈ line[k, p₁, p₂]
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case mpr
𝕜 : 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:
·

Goal state after:
case mpr
𝕜 : 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)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case refine_1
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₁)

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
s₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ s₁
hp₂ : p₂ ∈ s₂
⊢ s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ≤ (s₁ ⊔ s₂).direction

Tactic:
·

Goal state after:
case refine_1
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₁)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case mp
𝕜 : 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

pp: case mpr
𝕜 : 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:
·

Goal state after:
case mp
𝕜 : 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
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case mpr
𝕜 : 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:
·

Goal state after:
case mpr
𝕜 : 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)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case refine_1.inl
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₂
p₃ : P
hp₃ : p₃ ∈ ↑s₁
⊢ (fun x ↦ x -ᵥ p₁) p₃ ∈ ↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁))

pp: case refine_1.inr
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₂
p₃ : P
hp₃ : p₃ ∈ ↑s₂
⊢ (fun x ↦ x -ᵥ p₁) p₃ ∈ ↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁))

Tactic:
·

Goal state after:
case refine_1.inl
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₂
p₃ : P
hp₃ : p₃ ∈ ↑s₁
⊢ (fun x ↦ x -ᵥ p₁) p₃ ∈ ↑(s₁.direction ⊔ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁))