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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ 0 ≤ a / (a + b)

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ 0 ≤ b / (a + b)

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ 0 < a / (a + b)

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ 0 < b / (a + b)

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : CommSemiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
c : 𝕜
h : StarConvex 𝕜 (z + c • x) ((fun x ↦ z + x) '' (c • s))
⊢ StarConvex 𝕜 (z + c • x) ((fun x ↦ z + c • x) '' s)

Tactic:
rwa [← image_smul, image_image] at h

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • (y - x) ∈ s

Tactic:
by
  apply hs.segment_subset hy
  rw [segment_eq_image']
  exact mem_image_of_mem _ ⟨ht₀, ht₁⟩

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

Goal state before:
pp: case a
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ 0 ≤ a / (a + b)

Tactic:
positivity

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

Goal state before:
pp: case a
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ 0 ≤ b / (a + b)

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ (a / (a + b)) • x + (b / (a + b)) • y ∈ s

Tactic:
apply h hy
    · positivity
    · positivity
    · rw [← add_div]
      exact div_self hab.ne'

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

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

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : CommSemiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a✝ b✝ : E
ap bp : 𝕜
hap : 0 < ap
hbp : 0 < bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 < aq
hbq : 0 < bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * ap + b * aq

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : CommSemiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a✝ b✝ : E
ap bp : 𝕜
hap : 0 < ap
hbp : 0 < bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 < aq
hbq : 0 < bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * bp + b * bq

Tactic:
positivity

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

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
h : ↑s.direction = s
⊢ 0 ∈ s

Tactic:
rw [← h]

Goal state after:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
h : ↑s.direction = s
⊢ 0 ∈ ↑s.direction
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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

Tactic:
rintro ⟨p₁, hp₁, p₂, hp₂, rfl⟩

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
direction : Submodule k V
p₁ : P
hp₁ : p₁ ∈ mk' p direction
p₂ : P
hp₂ : p₂ ∈ mk' p direction
⊢ p₁ -ᵥ p₂ ∈ direction
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ ↑(vectorSpan k s) + s = ↑(affineSpan k s)

Tactic:
ext
  simp [mem_add, coe_affineSpan, spanPoints]
  grind

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
s : Set E
⊢ (convexHull 𝕜) s = ∅ ↔ s = ∅

Tactic:
constructor
  · intro h
    rw [← Set.subset_empty_iff, ← h]
    exact subset_convexHull 𝕜 _
  · rintro rfl
    exact convexHull_empty

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

Goal state before:
pp: case mpr
𝕜 : 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})
⊢ s \ {x} = (convexHull 𝕜) (s \ {x})

Tactic:
exact
    Subset.antisymm (subset_convexHull 𝕜 _) fun y hy =>
      ⟨convexHull_min sdiff_subset hs hy, by
        rintro (rfl : y = x)
        exact hx hy⟩

Goal state after:
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:
exact (h₁ x).add h₂

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ y ∈ t
⊢ (fun x ↦ a • x) y ∈ balancedCore 𝕜 s

Tactic:
rcases hy with ⟨t, ht1, ht2, hy⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
t : Set E
ht1 : Balanced 𝕜 t
ht2 : t ⊆ s
hy : y ∈ t
⊢ (fun x ↦ a • x) y ∈ balancedCore 𝕜 s
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
⊢ balancedCoreAux 𝕜 ∅ = ∅

Tactic:
simp_rw [balancedCoreAux, iInter₂_eq_empty_iff, smul_set_empty]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
⊢ ∀ (a : E), ∃ i, ∃ (_ : 1 ≤ ‖i‖), a ∉ ∅
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ x ∈ r • s

Tactic:
mem_smul_set_iff_inv_smul_mem₀ (norm_pos_iff.mp <| zero_lt_one.trans_le hr)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ r⁻¹ • x ∈ s
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hV : V ∈ 𝓝 0
hVb : Balanced 𝕜 V
n : ι
hn : ε n ≠ 0
hVS : ∀ (r : ℝ), ∃ c, r ≤ ‖c‖ ∧ ¬S ⊆ c • id V
a : 𝕜
haε : ‖(ε n)⁻¹‖ ≤ ‖a‖
haS : ¬S ⊆ a • id V
x : E
hxS : x ∈ S
hx : x ∉ a • id V
hnx : ε n • ↑⟨x, hxS⟩ ∈ V
⊢ False

Tactic:
← Set.mem_inv_smul_set_iff₀ hn

Goal state after:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
ε : ι → 𝕜
l : Filter ι
inst✝ : l.NeBot
hε : ∀ᶠ (n : ι) in l, ε n ≠ 0
S : Set E
H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Tendsto (ε • x) l (𝓝 0)
V : Set E
hV : V ∈ 𝓝 0
hVb : Balanced 𝕜 V
n : ι
hn : ε n ≠ 0
hVS : ∀ (r : ℝ), ∃ c, r ≤ ‖c‖ ∧ ¬S ⊆ c • id V
a : 𝕜
haε : ‖(ε n)⁻¹‖ ≤ ‖a‖
haS : ¬S ⊆ a • id V
x : E
hxS : x ∈ S
hx : x ∉ a • id V
hnx : ↑⟨x, hxS⟩ ∈ (ε n)⁻¹ • V
⊢ False
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕜'
inst✝⁶ : NormedAlgebra 𝕜 𝕜'
inst✝⁵ : Nontrivial 𝕜'
inst✝⁴ : Zero E
inst✝³ : TopologicalSpace E
inst✝² : SMul 𝕜 E
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : V ∈ 𝓝 0
⊢ AntilipschitzWith ‖1‖₊⁻¹ fun x ↦ x • 1

Tactic:
refine AntilipschitzWith.of_le_mul_nndist fun x y ↦ ?_

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕜'
inst✝⁶ : NormedAlgebra 𝕜 𝕜'
inst✝⁵ : Nontrivial 𝕜'
inst✝⁴ : Zero E
inst✝³ : TopologicalSpace E
inst✝² : SMul 𝕜 E
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : V ∈ 𝓝 0
x y : 𝕜
⊢ nndist x y ≤ ‖1‖₊⁻¹ * nndist (x • 1) (y • 1)
Module: Mathlib.Topology.Algebra.Equicontinuity

Goal state before:
pp: ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : TopologicalSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsTopologicalGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1
⊢ swap (DFunLike.coe ∘ F) 1 = 1

Tactic:
by dsimp [UniformFun]; ext; exact map_one _

Goal state after:
Module: Mathlib.Topology.Algebra.Equicontinuity

Goal state before:
pp: ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : UniformSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsUniformGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1
⊢ swap (DFunLike.coe ∘ F) 1 = 1

Tactic:
by dsimp [UniformFun]; ext; exact map_one _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
α : Type u_4
β : Type u_5
inst✝⁹ : Semiring 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : SMul 𝕜 E
inst✝¹ : SMul 𝕜 α
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
g : β → α
hg : StrictConvexOn 𝕜 (f '' s) g
hf : ConvexOn 𝕜 s f
hg' : MonotoneOn g (f '' s)
hf' : InjOn f s
⊢ StrictConvexOn 𝕜 s (g ∘ f)

Tactic:
refine ⟨hf.left, fun x hx y hy hxy a b ha hb hab ↦ .trans_le' (b := g (a • f x + b • f y)) ?_ ?_⟩

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
α : Type u_4
β : Type u_5
inst✝⁹ : Semiring 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : SMul 𝕜 E
inst✝¹ : SMul 𝕜 α
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
g : β → α
hg : StrictConvexOn 𝕜 (f '' s) g
hf : ConvexOn 𝕜 s f
hg' : MonotoneOn g (f '' s)
hf' : InjOn f s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ g (a • f x + b • f y) < a • (g ∘ f) x + b • (g ∘ f) y

case refine_2
𝕜 : Type u_1
E : Type u_2
α : Type u_4
β : Type u_5
inst✝⁹ : Semiring 𝕜
inst✝⁸ : PartialOrder 𝕜
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : SMul 𝕜 E
inst✝¹ : SMul 𝕜 α
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
g : β → α
hg : StrictConvexOn 𝕜 (f '' s) g
hf : ConvexOn 𝕜 s f
hg' : MonotoneOn g (f '' s)
hf' : InjOn f s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (g ∘ f) (a • x + b • y) ≤ g (a • f x + b • f y)
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : StrictConvex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ 0 < a / (a + b)

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : StrictConvex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ 0 < b / (a + b)

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht : 1 < t
⊢ t ≠ 0

Tactic:
positivity

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht : 1 < t
⊢ 0 < t⁻¹

Tactic:
positivity

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:
simp [weightedVSub_apply]

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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
⊢ p ∈ affineSpan k (insert p₂ ↑s) ↔ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
← vsub_right_mem_direction_iff_mem (mem_affineSpan k (Set.mem_insert_of_mem _ hp₁)),

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 : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
⊢ p -ᵥ p₁ ∈ (affineSpan k (insert p₂ ↑s)).direction ↔ ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ x : E
⊢ 0 ≤ p x + q (x✝ - x)

Tactic:
positivity

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
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
p q : Seminorm 𝕜 E
x i : E
⊢ 0 ≤ p i + q (0 - i)

Tactic:
positivity

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
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
hf : Function.Surjective ⇑f
h : affineSpan k s = ⊤
⊢ affineSpan k (⇑f '' s) = ⊤

Tactic:
rw [← AffineSubspace.map_span, h, map_top_of_surjective f hf]

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

Goal state before:
pp: ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
p : ι → P
hnz : ∑ i ∈ s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (Function.const ι 0) i1 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (Finset.affineCombination k s p) w1 = p i1
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)

Tactic:
have hv : s.affineCombination k p w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction := by
      rw [direction_affineSpan, ← hw1s, Finset.affineCombination_vsub]
      apply weightedVSub_mem_vectorSpan
      simp [Pi.sub_apply, h, hw1]

Goal state after:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
p : ι → P
hnz : ∑ i ∈ s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (Function.const ι 0) i1 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (Finset.affineCombination k s p) w1 = p i1
hv : (Finset.affineCombination k s p) w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

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
inst✝ : Fintype ι
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i, (↑s).indicator w i = 0
hs : (univ.weightedVSub p) ((↑s).indicator w) = 0
i : ι
hi : i ∈ s
h : (↑s).indicator w i = 0
⊢ w i = 0

Tactic:
simpa [hi] using h

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

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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x ↦ x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ g i = 0

Tactic:
hfg

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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
hg : ∑ i ∈ s, g i • (p ↑i -ᵥ p i1) = 0
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x ↦ x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
⊢ f ↑i = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

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
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x ↦ x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι ∈ s2, f ι = 0
f2 : ι → V := fun x ↦ f x • (p x -ᵥ p i1)
hf2def : f2 = fun x ↦ f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x ↦ g x • (p ↑x -ᵥ p i1)
hg : s.sum g2 = 0
x : { x // x ≠ i1 }
⊢ f ↑x • (p ↑x -ᵥ p i1) = g x • (p ↑x -ᵥ p i1)

Tactic:
hfg

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
ι : Type u_4
p : ι → P
i1 : ι
h : AffineIndependent k p
s : Finset { x // x ≠ i1 }
g : { x // x ≠ i1 } → k
i : { x // x ≠ i1 }
hi : i ∈ s
f : ι → k := fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
hfdef : f = fun x ↦ if hx : x = i1 then -∑ y ∈ s, g y else g ⟨x, hx⟩
s2 : Finset ι := insert i1 (map (Embedding.subtype fun x ↦ x ≠ i1) s)
hfg : ∀ (x : { x // x ≠ i1 }), g x = f ↑x
hf : ∑ ι ∈ s2, f ι = 0
f2 : ι → V := fun x ↦ f x • (p x -ᵥ p i1)
hf2def : f2 = fun x ↦ f x • (p x -ᵥ p i1)
g2 : { x // x ≠ i1 } → V := fun x ↦ g x • (p ↑x -ᵥ p i1)
hg : s.sum g2 = 0
x : { x // x ≠ i1 }
⊢ f ↑x • (p ↑x -ᵥ p i1) = f ↑x • (p ↑x -ᵥ p i1)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : p x ≠ 0
⊢ 0 < p x / ε

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : p x ≠ 0
xεpos : 0 < p x / ε
n : ℤ
hn : p x / ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
⊢ 0 < ‖c‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
q : Seminorm 𝕜 E
ε : ℝ
C : ℝ≥0
ε_pos : 0 < ε
c : 𝕜
hc : 1 < ‖c‖
hf : ∀ (x : E), (∀ i ∈ s, (p i) x < ε) → ∀ j ∈ s, ε / ‖c‖ ≤ (p j) x → q x ≤ (C • p j) x
x : E
hx : ∃ j ∈ s, (p j) x ≠ 0
⊢ q x ≤ (C • s.sup p) x

Tactic:
by
  rcases hx with ⟨j, hj, hjx⟩
  have : (s.sup p) x ≠ 0 :=
    ne_of_gt ((hjx.symm.lt_of_le <| apply_nonneg _ _).trans_le (le_finset_sup_apply hj))
  refine (s.sup p).bound_of_shell_smul q ε_pos hc (fun y hle hlt ↦ ?_) this
  rcases exists_apply_eq_finset_sup p ⟨j, hj⟩ y with ⟨i, hi, hiy⟩
  rw [smul_apply, hiy]
  exact hf y (fun k hk ↦ (le_finset_sup_apply hk).trans_lt hlt) i hi (hiy ▸ hle)

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

Goal state before:
pp: x y : ℝ
h : x < y
⊢ ⇑(Path.segment x y) '' Ico 0 1 = Ico x y

Tactic:
simp_rw [Path.segment_apply, ← image_image _ Subtype.val (Ico 0 1)]
  simp only [lineMap_apply, vsub_eq_sub, smul_eq_mul, vadd_eq_add, image_subtype_val_Ico,
    Icc.coe_zero, Icc.coe_one]
  convert! image_affine_Ico (sub_pos_of_lt h) x 0 1 using 2 <;> ring

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : PartialOrder k
s : Simplex k P 0
⊢ s.interior = ∅

Tactic:
ext p
  simp only [Simplex.interior, Simplex.setInterior, Nat.reduceAdd, univ_unique, Fin.default_eq_zero,
    Fin.isValue, sum_singleton, Set.mem_Ioo, Set.mem_ofPred_eq, Set.mem_empty_iff_false, iff_false,
    not_exists, not_and]
  intro w h hi
  simpa [h] using hi 0

Goal state after: