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

Goal state before:
pp: case right
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
he : ↑s₁ ∩ ↑s₂ = ∅
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ + v₂ = p₂ -ᵥ p₁
⊢ False

Tactic:
← sub_eq_zero,

Goal state after:
case right
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
he : ↑s₁ ∩ ↑s₂ = ∅
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ + v₂ - (p₂ -ᵥ p₁) = 0
⊢ False
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
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ s ⊆ a • t

Tactic:
subset_smul_set_iff₀ (norm_pos_iff.mp <| zero_lt_one.trans_le ha)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ a⁻¹ • s ⊆ t
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst✝¹] U
h : 0 ∈ U
⊢ IsClosed[inst✝¹] (balancedCore 𝕜 U)

Tactic:
balancedCore_eq_iInter h

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst✝¹] U
h : 0 ∈ U
⊢ IsClosed[inst✝¹] (⋂ r, ⋂ (_ : 1 ≤ ‖r‖), r • U)
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ -(((1 - a) / 2) • x) + ((a - -1) / 2) • x ∈ s

Tactic:
← smul_neg

Goal state after:
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ ((1 - a) / 2) • -x + ((a - -1) / 2) • x ∈ s
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : T1Space E
inst✝¹ : RegularSpace E
inst✝ : ContinuousConstSMul 𝕜 E
a V : Set E
hV : V ∈ 𝓝 0
W : Set E
ha : Absorbs 𝕜 W a
hW₁ : W ∈ 𝓝 0
hW₂ : IsClosed[inst✝³] W
hW₃ : W ⊆ V
b : 𝕜
ha' : a ⊆ b • W
⊢ closure[inst✝³] a ⊆ b • V

Tactic:
grw [ha', closure_smul₀ b, closure_subset_iff_isClosed.mpr hW₂, hW₃]

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
⊢ ‖r‖ * f x ≤ f (r • x)

Tactic:
by_cases h : r = 0

Goal state after:
case pos
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
h : r = 0
⊢ ‖r‖ * f x ≤ f (r • x)

case neg
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
h : ¬r = 0
⊢ ‖r‖ * f x ≤ f (r • x)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case neg
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
h : ¬r = 0
⊢ ‖r‖ * f x ≤ f (r • x)

Tactic:
← mul_le_mul_iff_right₀ (inv_pos.mpr (norm_pos_iff.mpr h))

Goal state after:
case neg
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
h : ¬r = 0
⊢ ‖r‖⁻¹ * (‖r‖ * f x) ≤ ‖r‖⁻¹ * f (r • x)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case right
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
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : p -ᵥ p₁ = r • (p₂ -ᵥ p₁) + v₂
⊢ p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁

Tactic:
← sub_eq_zero,

Goal state after:
case right
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
v₂ : V
hv₂ : v₂ ∈ s.direction
r : k
hp : p -ᵥ p₁ - (r • (p₂ -ᵥ p₁) + v₂) = 0
⊢ p = r • (p₂ -ᵥ p₁) +ᵥ v₂ +ᵥ p₁
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
h : ∀ i ∈ s, (p i) x ≤ ↑a
⊢ (s.sup fun i ↦ NNReal.mk ((p i) x) ⋯) ≤ a

Tactic:
exact Finset.sup_le h

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 : AffineSubspace k P₁
⊢ map f s = ⊥ ↔ s = ⊥

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
  · rwa [← coe_eq_bot_iff, coe_map, image_eq_empty, coe_eq_bot_iff] at h
  · rw [h, map_bot]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inr
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
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' s)
h : s.Nonempty
⊢ (⨆ p, ⇑↑p) (x + y) ≤ (⨆ p, ⇑↑p) x + (⨆ p, ⇑↑p) y

Tactic:
have : Nonempty ↑s := h.coe_sort

Goal state after:
case inr
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
s : Set (Seminorm 𝕜 E)
x y : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' s)
h : s.Nonempty
this : Nonempty ↑s
⊢ (⨆ p, ⇑↑p) (x + y) ≤ (⨆ p, ⇑↑p) x + (⨆ p, ⇑↑p) y
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case mpr
ι : 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
v : V
p : ι → P
⊢ (∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) w) → v ∈ vectorSpan k (Set.range p)

Tactic:
rintro ⟨s, w, hw, rfl⟩
      exact weightedVSub_mem_vectorSpan hw p

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✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ line[k, p₃, p₄]
hp₂ : p₂ ∈ line[k, p₃, p₄]
hp₁₂ : p₁ ≠ p₂
⊢ line[k, p₁, p₂] = line[k, p₃, p₄]

Tactic:
by
  refine le_antisymm (affineSpan_pair_le_of_mem_of_mem hp₁ hp₂) ?_
  rw [← vsub_vadd p₁ p₃, vadd_left_mem_affineSpan_pair] at hp₁
  rcases hp₁ with ⟨r₁, hp₁⟩
  rw [← vsub_vadd p₂ p₃, vadd_left_mem_affineSpan_pair] at hp₂
  rcases hp₂ with ⟨r₂, hp₂⟩
  have hr₀ : r₂ - r₁ ≠ 0 := by
    rw [sub_ne_zero]
    rintro rfl
    simp_all
  have hr : (r₂ - r₁) • (p₄ -ᵥ p₃) = p₂ -ᵥ p₁ := by
    simp [sub_smul, hp₁, hp₂]
  rw [← eq_inv_smul_iff₀ hr₀] at hr
  refine affineSpan_pair_le_of_mem_of_mem ?_ ?_
  · convert! smul_vsub_vadd_mem_affineSpan_pair (-r₁ * (r₂ - r₁)⁻¹) p₁ p₂
    simp [mul_smul, ← hr, hp₁]
  · convert! smul_vsub_vadd_mem_affineSpan_pair ((1 - r₁) * (r₂ - r₁)⁻¹) p₁ p₂
    simp [mul_smul, ← hr, sub_smul, hp₁]

Goal state after:
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
s : Set V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
⊢ (fun x ↦ (x +ᵥ p₁) -ᵥ p₁) '' s \ {0} = s

Tactic:
vadd_vsub,

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 V
hs : ∀ v ∈ s, v ≠ 0
p₁ : P
⊢ (fun a ↦ a) '' s \ {0} = s
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
⊢ ∀ (p : (ι → P) × P) (v : (ι → V) × V),
    (s.weightedVSubOfPoint (v +ᵥ p).1 (v +ᵥ p).2) w =
      (∑ i ∈ s, w i • (LinearMap.proj i ∘ₗ LinearMap.fst k (ι → V) V - LinearMap.snd k (ι → V) V)) v +ᵥ
        (s.weightedVSubOfPoint p.1 p.2) w

Tactic:
rintro ⟨p, b⟩ ⟨v, b'⟩

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
v : ι → V
b' : V
⊢ (s.weightedVSubOfPoint ((v, b') +ᵥ (p, b)).1 ((v, b') +ᵥ (p, b)).2) w =
    (∑ i ∈ s, w i • (LinearMap.proj i ∘ₗ LinearMap.fst k (ι → V) V - LinearMap.snd k (ι → V) V)) (v, b') +ᵥ
      (s.weightedVSubOfPoint (p, b).1 (p, b).2) w
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
hp : AffineIndependent k p
j : ι
w : ι → kˣ
⊢ AffineIndependent k fun i ↦ (AffineMap.lineMap (p j) (p i)) ↑(w i)

Tactic:
affineIndependent_iff_linearIndependent_vsub k _ j

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
j : ι
hp : LinearIndependent k fun i ↦ p ↑i -ᵥ p j
w : ι → kˣ
⊢ LinearIndependent k fun i ↦ (AffineMap.lineMap (p j) (p ↑i)) ↑(w ↑i) -ᵥ (AffineMap.lineMap (p j) (p j)) ↑(w j)
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

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
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
r : k
hr : (s.weightedVSub p) (r • (w₁ - w₂)) = (s.weightedVSub p) w
i : ι
hi : i ∈ s
⊢ w i = r * (w₁ i - w₂ i)

Tactic:
← sub_eq_zero,

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
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
r : k
hr : (s.weightedVSub p) (r • (w₁ - w₂)) - (s.weightedVSub p) w = 0
i : ι
hi : i ∈ s
⊢ w i = r * (w₁ i - w₂ i)
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
inst✝¹ : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
inst✝ : NeZero m
h : #fs = m + 1
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
⊢ (affineCombination k univ s.points) w ∈ (s.face h).interior ↔ (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0

Tactic:
s.affineCombination_mem_interior_face_iff_mem_Ioo h hw

Goal state after:
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
inst✝¹ : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
inst✝ : NeZero m
h : #fs = m + 1
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
⊢ ((∀ i ∈ fs, w i ∈ Set.Ioo 0 1) ∧ ∀ i ∉ fs, w i = 0) ↔ (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

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
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
r : k
hr : (s.weightedVSub p) (r • (w₁ - w₂) - w) = 0
i : ι
hi : i ∈ s
hw' : ∑ j ∈ s, (r • (w₁ - w₂) - w) j = 0
hr' : (r • (w₁ - w₂) - w) i = 0
⊢ r * (w₁ i - w₂ i) = w i

Tactic:
← sub_eq_zero,

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
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
hw : ∑ i ∈ s, w i = 0
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
r : k
hr : (s.weightedVSub p) (r • (w₁ - w₂) - w) = 0
i : ι
hi : i ∈ s
hw' : ∑ j ∈ s, (r • (w₁ - w₂) - w) j = 0
hr' : (r • (w₁ - w₂) - w) i = 0
⊢ r * (w₁ i - w₂ i) - w i = 0
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case pos
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : x = y
⊢ a • x + b • y ∈ s

Tactic:
h_cases,

Goal state after:
case pos
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
h : ∀ (t : Finset E) (w : E → R), (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : x = y
⊢ a • y + b • y ∈ s
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : AlexandrovDiscrete α
inst✝ : AlexandrovDiscrete β
s t : Set α
a : α
⊢ ∀ (a : α) (b : β), 𝓟 (nhdsKer {a} ×ˢ nhdsKer {b}) = 𝓟 (nhdsKer {(a, b)})

Tactic:
nhdsKer_pair,

Goal state after:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : AlexandrovDiscrete α
inst✝ : AlexandrovDiscrete β
s t : Set α
a : α
⊢ ∀ (a : α) (b : β), True
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
t : Finset ι
p : ι → E
w : ι → R
hw₂ : ∑ i ∈ t, w i = 1
⊢ ∑ i ∈ t, w i • (p i -ᵥ 0) = ∑ i ∈ t, w i • p i

Tactic:
simp_rw [vsub_eq_sub, sub_zero]

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

Goal state before:
pp: case refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
⊢ a • (affineCombination R s v) w + b • (affineCombination R s' v) w' ∈
    {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}

Tactic:
refine ⟨s ∪ s', W, ?_, hW₁, ?_⟩

Goal state after:
case refine_2.refine_1
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
⊢ ∀ i ∈ s ∪ s', 0 ≤ W i

case refine_2.refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
⊢ (affineCombination R (s ∪ s') v) W = a • (affineCombination R s v) w + b • (affineCombination R s' v) w'
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case neg
ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PathConnectedSpace (Z i)}
i : ι
hi : i ∉ K
⊢ IsPathConnected (K.piecewise (fun i ↦ pathComponentIn (t i) (x i)) (fun x ↦ univ) i)

Tactic:
rw [piecewise_eq_of_notMem _ _ _ hi]
      have : PathConnectedSpace (Z i) := not_not.mp (not_or.1 hi).2
      exact isPathConnected_univ

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

Goal state before:
pp: case inl.refine_1
R : Type u_1
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
x : R
hl : IsBot x
inst✝ : OrderBot R
⊢ ∀ (i : R), ⊥ < i → ∃ i', (i' ∈ 𝓝 ⊥ ∧ Convex R i') ∧ id i' ⊆ Iio i

Tactic:
intros
        refine ⟨Set.Iio _, ?_, .rfl⟩
        simp_all [Iio_mem_nhds, convex_Iio]

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

Goal state before:
pp: case inr.inr.refine_1
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : OrderTopology R
x : R
hl : ∃ b, b < x
hu : ∃ b, x < b
⊢ ∀ (i : R × R), i.1 < x ∧ x < i.2 → ∃ i', (i' ∈ 𝓝 x ∧ Convex R i') ∧ id i' ⊆ Ioo i.1 i.2

Tactic:
simp only [id_eq, and_imp, Prod.forall]

Goal state after:
case inr.inr.refine_1
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : OrderTopology R
x : R
hl : ∃ b, b < x
hu : ∃ b, x < b
⊢ ∀ (a b : R), a < x → x < b → ∃ i', (i' ∈ 𝓝 x ∧ Convex R i') ∧ i' ⊆ Ioo a b
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
s t₁ t₂ : Finset E
hs : AffineIndependent R Subtype.val
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : ∑ y ∈ t₁, w₁ y = 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : ∑ y ∈ t₂, w₂ y = 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : E → R := fun x ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : ∑ i ∈ s, w i = 0
⊢ ∑ x ∈ s, w x • x = 0

Tactic:
simp only [w, sub_smul, zero_smul, ite_smul, Finset.sum_sub_distrib, ← Finset.sum_filter, h₃w₁,
      Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 ht₁, Finset.inter_eq_right.2 ht₂, h₃w₂,
      sub_self]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
⊢ f (∑ i ∈ t, w i • p i) ≠ ∑ i ∈ t, w i • f (p i) ↔ ∃ j ∈ t, p j ≠ ∑ i ∈ t, w i • p i

Tactic:
contrapose!

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : IsStrictOrderedModule 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
⊢ f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔ ∀ j ∈ t, p j = ∑ i ∈ t, w i • p i
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case pos
R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : 0 < (s.sup p) v
⊢ {x | ‖x‖ * (s.sup p) v < r} ∈ 𝓝 0

Tactic:
(lt_div_iff₀ h).symm

Goal state after:
case pos
R : Type u_1
E : Type u_6
ι : Type u_9
inst✝² : SeminormedRing R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : SeminormFamily R E ι
v : E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : 0 < (s.sup p) v
⊢ {x | ‖x‖ < r / (s.sup p) v} ∈ 𝓝 0
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ IsTopologicalAddGroup E

Tactic:
rw [hp.withSeminorms_eq]
  exact AddGroupFilterBasis.isTopologicalAddGroup _

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

Goal state before:
pp: case refine_3.refine_1
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ 𝓝 0
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
this : p.ball 0 ‖c⁻¹‖ ⊆ s
⊢ 0 < ‖c⁻¹‖

Tactic:
simpa using c_ne

Goal state after: