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

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
direction : Submodule k V
v : V
⊢ (∃ p₁ ∈ mk' p direction, ∃ p₂ ∈ mk' p direction, v = p₁ -ᵥ p₂) ↔ v ∈ direction

Tactic:
]

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
inst✝ : AffineSpace V P
p : P
direction : Submodule k V
v : V
⊢ (∃ p₁ ∈ mk' p direction, ∃ p₂ ∈ mk' p direction, v = p₁ -ᵥ p₂) ↔ v ∈ direction
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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 P
s₁ : AffineSubspace k P
h : s ⊆ ↑s₁
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p₁
⊢ v +ᵥ p₁ ∈ ↑s₁

Tactic:
]

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
inst✝ : AffineSpace V P
s : Set P
s₁ : AffineSubspace k P
h : s ⊆ ↑s₁
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p₁
⊢ v +ᵥ p₁ ∈ ↑s₁
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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 P
s₁ : AffineSubspace k P
h : s ⊆ ↑s₁
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ ↑s₁
hs : ∀ ⦃x : V⦄, x ∈ vectorSpan k s → x ∈ s₁.direction
⊢ v ∈ s₁.direction

Tactic:
]

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
inst✝ : AffineSpace V P
s : Set P
s₁ : AffineSubspace k P
h : s ⊆ ↑s₁
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ ↑s₁
hs : ∀ ⦃x : V⦄, x ∈ vectorSpan k s → x ∈ s₁.direction
⊢ v ∈ s₁.direction
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedRing 𝕜
inst✝ : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
⊢ ∀ ⦃x : E⦄, x ∈ {x | f x ≤ B} → ∀ ⦃y : E⦄, y ∈ {x | f x ≤ B} → [x -[𝕜] y] ⊆ {x | f x ≤ B}

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedRing 𝕜
inst✝ : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
⊢ ∀ ⦃x : E⦄, x ∈ {x | f x ≤ B} → ∀ ⦃y : E⦄, y ∈ {x | f x ≤ B} → [x -[𝕜] y] ⊆ {x | f x ≤ B}
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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 P
s₁ : AffineSubspace k P
h : s ⊆ ↑s₁
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ ↑s₁
hs : ∀ ⦃x : V⦄, x ∈ vectorSpan k s → x ∈ s₁.direction
⊢ v ∈ ↑s₁.direction

Tactic:
]

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
inst✝ : AffineSpace V P
s : Set P
s₁ : AffineSubspace k P
h : s ⊆ ↑s₁
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ ↑s₁
hs : ∀ ⦃x : V⦄, x ∈ vectorSpan k s → x ∈ s₁.direction
⊢ v ∈ ↑s₁.direction
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y a : { t // 0 ≤ t }
hxa : ↑x ≤ ↑a
hay : ↑a ≤ ↑y
⊢ a ∈ [x -[{ t // 0 ≤ t }] y]

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y a : { t // 0 ≤ t }
hxa : ↑x ≤ ↑a
hay : ↑a ≤ ↑y
⊢ a ∈ [x -[{ t // 0 ≤ t }] y]
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case a
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₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ v₁ + (p₂ -ᵥ p₄) - v₂ ∈ vectorSpan k s

Tactic:
]

Goal state after:
case a
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₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ v₁ + (p₂ -ᵥ p₄) - v₂ ∈ vectorSpan k s
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedRing 𝕜
inst✝ : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
x : E
hx : x ∈ {x | f x ≤ B}
y : E
hy : y ∈ {x | f x ≤ B}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
⊢ B ≤ B

Tactic:
]

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

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
ι : Sort u_4
s : Set (AffineSubspace k P)
c : k
p₁ p₂ p₃ : P
hp₁ : ∀ i ∈ s, p₁ ∈ ↑i
hp₂ : ∀ i ∈ s, p₂ ∈ ↑i
hp₃ : ∀ i ∈ s, p₃ ∈ ↑i
s₂ : AffineSubspace k P
hs₂ : s₂ ∈ s
⊢ c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ ↑s₂

Tactic:
]

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
ι : Sort u_4
s : Set (AffineSubspace k P)
c : k
p₁ p₂ p₃ : P
hp₁ : ∀ i ∈ s, p₁ ∈ ↑i
hp₂ : ∀ i ∈ s, p₂ ∈ ↑i
hp₃ : ∀ i ∈ s, p₃ ∈ ↑i
s₂ : AffineSubspace k P
hs₂ : s₂ ∈ s
⊢ c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ ↑s₂
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x : E
zero_mem : 0 ∈ s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ t⁻¹ • x ∈ s

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x : E
zero_mem : 0 ∈ s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ t⁻¹ • x ∈ s
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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
s₁ s₂ : AffineSubspace k P
⊢ (s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁) ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁

Tactic:
]

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

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
p : P
v : V
_hv : v ∈ ⊤
hpv : v ∈ ⊤.direction
⊢ v ∈ ⊤.direction

Tactic:
]

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
p : P
v : V
_hv : v ∈ ⊤
hpv : v ∈ ⊤.direction
⊢ v ∈ ⊤.direction
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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
contra : ∅ = univ
⊢ False

Tactic:
]

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
contra : ∅ = univ
⊢ False
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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
s : Set P
h : affineSpan k s = ⊤
⊢ s ≠ ∅

Tactic:
]

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
s : Set P
h : affineSpan k s = ⊤
⊢ s ≠ ∅
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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
h : ⊥ = ⊤
⊢ False

Tactic:
]

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
h : ⊥ = ⊤
⊢ False
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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
s : Set P
h : affineSpan k s = ⊤
⊢ ⊤ = ⊤

Tactic:
]

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : (convexHull 𝕜) s = ∅
⊢ s ⊆ (convexHull 𝕜) s

Tactic:
]

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : (convexHull 𝕜) s = ∅
⊢ s ⊆ (convexHull 𝕜) s
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ ¬(convexHull 𝕜) s = ∅ ↔ ¬s = ∅

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
⊢ ¬(convexHull 𝕜) s = ∅ ↔ ¬s = ∅
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h_conv : Convex 𝕜 s
⊢ (2⁻¹ + 2⁻¹) • s = s

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h_conv : Convex 𝕜 s
⊢ (2⁻¹ + 2⁻¹) • s = s
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : (convexHull 𝕜) s = {x}
⊢ s ⊆ (convexHull 𝕜) s

pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : (convexHull 𝕜) s = {x}
⊢ s.Nonempty

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : (convexHull 𝕜) s = {x}
⊢ s ⊆ (convexHull 𝕜) s

𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : (convexHull 𝕜) s = {x}
⊢ s.Nonempty
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h_conv : Convex 𝕜 s
⊢ s = s

Tactic:
]

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

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
s : Set P
hs : s.Nonempty
h : vectorSpan k s = ⊤
p : P
hp : p ∈ affineSpan k s
⊢ ⊤ = ⊤

Tactic:
]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : IsOrderedRing 𝕜
x y : E
⊢ x ∈ segment 𝕜 x y ∧ y ∈ segment 𝕜 x y

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : IsOrderedRing 𝕜
x y : E
⊢ x ∈ segment 𝕜 x y ∧ y ∈ segment 𝕜 x y
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hsx : Convex 𝕜 (s \ {x})
hx : x ∈ s \ {x}
⊢ False

Tactic:
]

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hsx : Convex 𝕜 (s \ {x})
hx : x ∈ s \ {x}
⊢ False
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hyx : y ≤ x
⊢ [y -[𝕜] x] ⊆ s

Tactic:
]

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hyx : y ≤ x
⊢ [y -[𝕜] x] ⊆ s
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∉ (convexHull 𝕜) (s \ {x})
h : s \ {x} = (convexHull 𝕜) (s \ {x})
⊢ Convex 𝕜 ((convexHull 𝕜) (s \ {x}))

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∉ (convexHull 𝕜) (s \ {x})
h : s \ {x} = (convexHull 𝕜) (s \ {x})
⊢ Convex 𝕜 ((convexHull 𝕜) (s \ {x}))
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
⊢ (fun x ↦ (x.1 • x₁ + x.2 • x₂, y)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} =
    (fun p ↦ p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
⊢ (fun x ↦ (x.1 • x₁ + x.2 • x₂, y)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} =
    (fun p ↦ p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ (convexHull 𝕜) s ⊆ ⇑f ⁻¹' (convexHull 𝕜) (⇑f '' s)

Tactic:
]

Goal state after:
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ (convexHull 𝕜) s ⊆ ⇑f ⁻¹' (convexHull 𝕜) (⇑f '' s)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
⊢ (fun x_1 ↦ (x, x_1.1 • y₁ + x_1.2 • y₂)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} =
    (fun p ↦ p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
⊢ (fun x_1 ↦ (x, x_1.1 • y₁ + x_1.2 • y₂)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} =
    (fun p ↦ p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ ⇑f '' s ⊆ (convexHull 𝕜) (⇑f '' s)

Tactic:
]

Goal state after:
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ ⇑f '' s ⊆ (convexHull 𝕜) (⇑f '' s)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case 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
s : Set P
inst✝ : Nontrivial P
hs : s.Nonempty
⊢ vectorSpan k s = ⊤ ↔ vectorSpan k s = ⊤

Tactic:
]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) s ⊆ ↑(affineSpan 𝕜 s)

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) s ⊆ ↑(affineSpan 𝕜 s)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
⊢ (fun x ↦ (x.1 • x₁ + x.2 • x₂, y)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    (fun p ↦ p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x₁ x₂ : E
y : F
⊢ (fun x ↦ (x.1 • x₁ + x.2 • x₂, y)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    (fun p ↦ p.1 • (x₁, y) + p.2 • (x₂, y)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
E : Type u_2
inst✝² : Bornology M
s₁ s₂ t₁ t₂ : Set E
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
h₁ : Absorbs M s₁ t₁
h₂ : Absorbs M s₂ t₂
x : M
hx₁ : t₁ ⊆ x • s₁
hx₂ : t₂ ⊆ x • s₂
⊢ t₁ + t₂ ⊆ x • s₁ + x • s₂

Tactic:
]

Goal state after:
M : Type u_1
E : Type u_2
inst✝² : Bornology M
s₁ s₂ t₁ t₂ : Set E
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
h₁ : Absorbs M s₁ t₁
h₂ : Absorbs M s₂ t₂
x : M
hx₁ : t₁ ⊆ x • s₁
hx₂ : t₂ ⊆ x • s₂
⊢ t₁ + t₂ ⊆ x • s₁ + x • s₂
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s : Set α
a : G₀
ha : a ≠ 0
⊢ s ⊆ univ

Tactic:
]

Goal state after:
G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s : Set α
a : G₀
ha : a ≠ 0
⊢ s ⊆ univ
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s t : Set α
c : G₀
hc : c ≠ 0
⊢ t ⊆ (fun x ↦ c⁻¹ • x) ⁻¹' s ↔ MapsTo (fun x ↦ c⁻¹ • x) t s

Tactic:
]

Goal state after:
G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s t : Set α
c : G₀
hc : c ≠ 0
⊢ t ⊆ (fun x ↦ c⁻¹ • x) ⁻¹' s ↔ MapsTo (fun x ↦ c⁻¹ • x) t s
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
⊢ (fun x_1 ↦ (x, x_1.1 • y₁ + x_1.2 • y₂)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    (fun p ↦ p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
⊢ (fun x_1 ↦ (x, x_1.1 • y₁ + x_1.2 • y₂)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    (fun p ↦ p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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
⊢ ⊥ = ⊥

Tactic:
]

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

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
Q : AffineSubspace k P
⊢ ↑Q ≠ ∅ ↔ Q ≠ ⊥

Tactic:
]

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
Q : AffineSubspace k P
⊢ ↑Q ≠ ∅ ↔ Q ≠ ⊥
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Bornology M
inst✝ : SMul M α
s t : Set α
hs : Absorbent M s
ht : t.Finite
⊢ Absorbs M s (⋃ x ∈ t, {x})

Tactic:
]

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Bornology M
inst✝ : SMul M α
s t : Set α
hs : Absorbent M s
ht : t.Finite
⊢ Absorbs M s (⋃ x ∈ t, {x})
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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
Q : AffineSubspace k P
⊢ Q = ⊥ ∨ Q ≠ ⊥

Tactic:
]

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
Q : AffineSubspace k P
⊢ Q = ⊥ ∨ Q ≠ ⊥
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
E : Type u_2
inst✝² : Bornology M
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
s₁ s₂ t : Set E
x : E
h₁ : Absorbent M s₁
h₂ : Absorbs M s₂ t
⊢ Absorbs M (s₁ + s₂) ({x} +ᵥ t)

Tactic:
]

Goal state after:
M : Type u_1
E : Type u_2
inst✝² : Bornology M
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
s₁ s₂ t : Set E
x : E
h₁ : Absorbent M s₁
h₂ : Absorbs M s₂ t
⊢ Absorbs M (s₁ + s₂) ({x} +ᵥ t)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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
ι : Sort u_4
p₁ p₂ : P
inst✝ : Subsingleton P
s : AffineSubspace k P
⊢ ↑s = ∅ ∨ ↑s = univ

Tactic:
]

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
ι : Sort u_4
p₁ p₂ : P
inst✝ : Subsingleton P
s : AffineSubspace k P
⊢ ↑s = ∅ ∨ ↑s = univ
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝⁶ : Monoid N
inst✝⁵ : SMul M N
inst✝⁴ : SMul M α
inst✝³ : MulAction N α
inst✝² : IsScalarTower M N α
inst✝¹ : Bornology M
inst✝ : Bornology N
s t : Set α
h : Absorbs N s t
hbdd : Tendsto (fun x ↦ x • 1) (cobounded M) (cobounded N)
x : M
hx : t ⊆ x • s
⊢ t ⊆ x • s

Tactic:
]

Goal state after:
M : Type u_1
N : Type u_2
α : Type u_3
inst✝⁶ : Monoid N
inst✝⁵ : SMul M N
inst✝⁴ : SMul M α
inst✝³ : MulAction N α
inst✝² : IsScalarTower M N α
inst✝¹ : Bornology M
inst✝ : Bornology N
s t : Set α
h : Absorbs N s t
hbdd : Tendsto (fun x ↦ x • 1) (cobounded M) (cobounded N)
x : M
hx : t ⊆ x • s
⊢ t ⊆ x • s