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

Goal state before:
pp: case e'_6
R : Type u_5
inst✝⁹ : CommSemiring R
A : Type u_6
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
M : Type u_7
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module A M
inst✝⁴ : Module R M
inst✝³ : IsScalarTower R A M
inst✝² : PartialOrder R
inst✝¹ : PartialOrder A
inst✝ : FaithfulSMul R A
s : Set M
halg : Ici 0 ⊆ ⇑(algebraMap R A) '' Ici 0
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : c ∈ Ici 0
hc2 : (algebraMap R A) c = a
d : R
hd1 : d ∈ Ici 0
hd2 : (algebraMap R A) d = b
⊢ b • v = d • v

Tactic:
← hd2,

Goal state after:
case e'_6
R : Type u_5
inst✝⁹ : CommSemiring R
A : Type u_6
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
M : Type u_7
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module A M
inst✝⁴ : Module R M
inst✝³ : IsScalarTower R A M
inst✝² : PartialOrder R
inst✝¹ : PartialOrder A
inst✝ : FaithfulSMul R A
s : Set M
halg : Ici 0 ⊆ ⇑(algebraMap R A) '' Ici 0
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : c ∈ Ici 0
hc2 : (algebraMap R A) c = a
d : R
hd1 : d ∈ Ici 0
hd2 : (algebraMap R A) d = b
⊢ (algebraMap R A) d • v = d • v
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: R : Type u_5
inst✝⁹ : CommSemiring R
A : Type u_6
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
M : Type u_7
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module A M
inst✝⁴ : Module R M
inst✝³ : IsScalarTower R A M
inst✝² : PartialOrder R
inst✝¹ : PartialOrder A
inst✝ : FaithfulSMul R A
s : Set M
halg : Ici 0 ⊆ ⇑(algebraMap R A) '' Ici 0
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
c : R
hab : (algebraMap R A) c + b = 1
hc1 : c ∈ Ici 0
hc2 : (algebraMap R A) c = a
d : R
hd1 : d ∈ Ici 0
hd2 : (algebraMap R A) d = b
⊢ c + d = 1

Tactic:
← hd2,

Goal state after:
R : Type u_5
inst✝⁹ : CommSemiring R
A : Type u_6
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
M : Type u_7
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module A M
inst✝⁴ : Module R M
inst✝³ : IsScalarTower R A M
inst✝² : PartialOrder R
inst✝¹ : PartialOrder A
inst✝ : FaithfulSMul R A
s : Set M
halg : Ici 0 ⊆ ⇑(algebraMap R A) '' Ici 0
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
c : R
hc1 : c ∈ Ici 0
hc2 : (algebraMap R A) c = a
d : R
hab : (algebraMap R A) c + (algebraMap R A) d = 1
hd1 : d ∈ Ici 0
hd2 : (algebraMap R A) d = b
⊢ c + d = 1
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
a : 𝕜
ha : 1 ≤ ‖a‖
ha' : 0 < ‖a‖
⊢ IsClosed[inst✝¹] (a • U)

Tactic:
norm_pos_iff

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
a : 𝕜
ha : 1 ≤ ‖a‖
ha' : a ≠ 0
⊢ IsClosed[inst✝¹] (a • U)
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
S : Type u_7
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
V : S
hV : Absorbent 𝕜 ↑V
x : E
c : 𝕜
hc : c • x ∈ ↑V
hc' : c ∈ {0}ᶜ
⊢ x ∈ ↑V

Tactic:
rw [← inv_smul_smul₀ hc' x]

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
S : Type u_7
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
V : S
hV : Absorbent 𝕜 ↑V
x : E
c : 𝕜
hc : c • x ∈ ↑V
hc' : c ∈ {0}ᶜ
⊢ c⁻¹ • c • x ∈ ↑V
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
⊢ ↑(Submodule.span k (insert 0 s)) ⊆ ↑(affineSpan k (insert 0 s))

Tactic:
← vectorSpan_add_self,

Goal state after:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ ↑(Submodule.span k (insert 0 s)) ⊆ ↑(vectorSpan k (insert 0 s)) + insert 0 s
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 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 : ConvexOn 𝕜 (f '' s) g
hf : StrictConvexOn 𝕜 s f
hg' : StrictMonoOn g (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

Tactic:
exact hg.right (mem_image_of_mem f hx) (mem_image_of_mem f hy) ha.le hb.le hab

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
⊢ Convex 𝕜 {p | p.1 ∈ s ∧ f p.1 ≤ p.2}

Tactic:
rintro ⟨x, r⟩ ⟨hx, hr⟩ ⟨y, t⟩ ⟨hy, ht⟩ a b ha hb hab

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x : E
r : β
hx : (x, r).1 ∈ s
hr : f (x, r).1 ≤ (x, r).2
y : E
t : β
hy : (y, t).1 ∈ s
ht : f (y, t).1 ≤ (y, t).2
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (x, r) + b • (y, t) ∈ {p | p.1 ∈ s ∧ f p.1 ≤ p.2}
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ ConvexOn 𝕜 s f ↔
    Convex 𝕜 s ∧ s.Pairwise fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
rw [convexOn_iff_forall_pos]

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ (Convex 𝕜 s ∧
      ∀ ⦃x : E⦄,
        x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y) ↔
    Convex 𝕜 s ∧ s.Pairwise fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
Module: Mathlib.Analysis.Convex.Function

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

Tactic:
by
      gcongr
      · apply le_max_left
      · apply le_max_right

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

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

Tactic:
by
      gcongr
      · apply le_max_left
      · apply le_max_right

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ i ∈ s, w i ≠ 0 → pred i
i : ι
hi : i ∈ s
hne : w i • (p i -ᵥ b) ≠ 0
hw : w i = 0
⊢ False

Tactic:
simp [hw] at hne

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

Goal state before:
pp: case refine_2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
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:
refine sup_le (sup_direction_le _ _) ?_

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
p : ι → P
⊢ (s.weightedVSub p) w₁ +ᵥ (affineCombination k s p) w₂ = (affineCombination k s p) (w₁ + w₂)

Tactic:
← vadd_eq_add,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
p : ι → P
⊢ (s.weightedVSub p) w₁ +ᵥ (affineCombination k s p) w₂ = (affineCombination k s p) (w₁ +ᵥ w₂)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConcaveOn 𝕜 univ ⇑f
⊢ ConvexOn 𝕜 univ ⇑f.symm

Tactic:
refine ⟨convex_univ, fun x _ y _ a b ha hb hab => ?_⟩
  obtain ⟨x', hx''⟩ := f.surjective.exists.mp ⟨x, rfl⟩
  obtain ⟨y', hy''⟩ := f.surjective.exists.mp ⟨y, rfl⟩
  simp only [hx'', hy'', OrderIso.symm_apply_apply]
  rw [← f.le_iff_le, OrderIso.apply_symm_apply]
  exact hf.2 (by simp : x' ∈ univ) (by simp : y' ∈ univ) ha hb hab

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : ConvexOn 𝕜 univ ⇑f
⊢ ConcaveOn 𝕜 univ ⇑f.symm

Tactic:
refine ⟨convex_univ, fun x _ y _ a b ha hb hab => ?_⟩
  obtain ⟨x', hx''⟩ := f.surjective.exists.mp ⟨x, rfl⟩
  obtain ⟨y', hy''⟩ := f.surjective.exists.mp ⟨y, rfl⟩
  simp only [hx'', hy'', OrderIso.symm_apply_apply]
  rw [← f.le_iff_le, OrderIso.apply_symm_apply]
  exact hf.2 (by simp : x' ∈ univ) (by simp : y' ∈ univ) ha hb hab

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

Goal state before:
pp: k : Type u_6
V : Type u_7
P : Type u_8
inst✝⁴ : CommRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_9
inst✝ : DecidableEq ι
s : Finset ι
p : ι → P
w : ι → k
i : ι
hi : i ∈ s
r : k
⊢ (AffineMap.homothety (p i) r) ((affineCombination k s p) w) =
    (affineCombination k s p) ((AffineMap.lineMap (Pi.single i 1) w) r)

Tactic:
rw [AffineMap.homothety_eq_lineMap, ← Finset.lineMap_affineCombination,
    Finset.affineCombination_piSingle _ _ _ hi]

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

Goal state before:
pp: k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : s.Nonempty
⊢ ∑ i ∈ s, centroidWeights k s i = 1

Tactic:
exact s.sum_centroidWeights_eq_one_of_nonempty k h

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ p.ball x r ↔ y ∈ {x_1 | x_1 ∈ univ ∧ (⇑p ∘ fun z ↦ z + -x) x_1 < r}

Tactic:
sep_univ,

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : SMul ℝ 𝕜
inst✝³ : NormSMulClass ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ p.ball x r ↔ y ∈ {x_1 | (⇑p ∘ fun z ↦ z + -x) x_1 < r}
Module: Mathlib.Analysis.Convex.PathConnected

Goal state before:
pp: case h
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
x y : E
s : Set E
h : [x -[ℝ] y] ⊆ s
⊢ ∀ (t : ↑I), (Path.segment x y) t ∈ s

Tactic:
← range_subset_iff,

Goal state after:
case h
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
x y : E
s : Set E
h : [x -[ℝ] y] ⊆ s
⊢ range ⇑(Path.segment x y) ⊆ s
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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
hs : p i ∈ affineSpan k (p '' s)
h : (s ∩ {i}).Nonempty
⊢ i ∈ s

Tactic:
Set.inter_singleton_nonempty

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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
hs : p i ∈ affineSpan k (p '' s)
h : i ∈ s
⊢ i ∈ s
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: S : Type u_1
inst✝⁶ : Semiring S
inst✝⁵ : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : Fintype X
inst✝³ : Fintype Y
inst✝² : Fintype Z
inst✝¹ : IsOrderedRing S
inst✝ : Subsingleton X
s t : ↑(stdSimplex S X)
i : X
⊢ s i = t i

Tactic:
have (u : stdSimplex S X) : u i = 1 := by
      rw [← sum_eq_one u, Finset.sum_eq_single i _ (by simp)]
      intro j _ hj
      exact (hj (Subsingleton.elim j i)).elim

Goal state after:
S : Type u_1
inst✝⁶ : Semiring S
inst✝⁵ : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : Fintype X
inst✝³ : Fintype Y
inst✝² : Fintype Z
inst✝¹ : IsOrderedRing S
inst✝ : Subsingleton X
s t : ↑(stdSimplex S X)
i : X
this : ∀ (u : ↑(stdSimplex S X)), u i = 1
⊢ s i = t i
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
| nhdsKer (univ.pi s)

Tactic:
← biUnion_of_singleton (univ.pi s),

Goal state after:
ι : Type u_3
X : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
| nhdsKer (⋃ x ∈ univ.pi s, {x})
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
hs' : (interior s).Nonempty
⊢ interior (closure s) = interior s

Tactic:
by
  refine subset_antisymm ?_ (interior_mono subset_closure)
  intro y hy
  rcases hs' with ⟨x, hx⟩
  have h := AffineMap.lineMap_apply_one (k := 𝕜) x y
  obtain ⟨t, ht1, ht⟩ := AffineMap.lineMap_continuous.tendsto' _ _ h |>.eventually_mem
    (mem_interior_iff_mem_nhds.1 hy) |>.exists_gt
  apply hs.openSegment_interior_closure_subset_interior hx ht
  nth_rw 1 [← AffineMap.lineMap_apply_zero (k := 𝕜) x y, ← image_openSegment]
  exact ⟨1, Ioo_subset_openSegment ⟨zero_lt_one, ht1⟩, h⟩

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

Goal state before:
pp: F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
this : (convexHull ℝ) (sphere 0 r) = closedBall 0 r
⊢ (convexHull ℝ) (sphere (x + 0) r) = closedBall (x + 0) r

Tactic:
← vadd_eq_add,

Goal state after:
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
this : (convexHull ℝ) (sphere 0 r) = closedBall 0 r
⊢ (convexHull ℝ) (sphere (x +ᵥ 0) r) = closedBall (x +ᵥ 0) r
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Nontrivial F
x : F
r : ℝ
hr : 0 ≤ r
⊢ (convexHull ℝ) (sphere x r) = closedBall x r

Tactic:
suffices convexHull ℝ (sphere (0 : F) r) = closedBall 0 r by
    rw [← add_zero x, ← vadd_eq_add, ← vadd_sphere, convexHull_vadd,
      this, vadd_closedBall_zero, vadd_eq_add, add_zero]
  refine subset_antisymm (convexHull_min sphere_subset_closedBall (convex_closedBall 0 r))
    (fun x h ↦ mem_convexHull_iff.mpr fun U hU_sub hU ↦ ?_)
  have zero_mem : (0 : F) ∈ U := by
    have _ : Invertible (2 : ℝ) := by use 2⁻¹ <;> grind
    obtain ⟨z, hz⟩ := NormedSpace.sphere_nonempty (E := F).mpr hr
    rw [← midpoint_self_neg (R := ℝ) (x := z)]
    exact Convex.midpoint_mem hU (hU_sub hz) <| hU_sub (by simp_all)
  by_cases hr₀ : r = 0
  · simp_all
  by_cases x_zero : x = 0
  · rwa [x_zero]
  set z := (r * ‖x‖⁻¹) • x with hz_def
  have hr₁ : r⁻¹ * ‖x‖ ≤ 1 := by
    simp only [mem_closedBall, dist_zero_right] at h
    grw [h, inv_mul_le_one]
  have hz : z ∈ U := by
    apply hU_sub
    simp_all [norm_smul]
  have := StarConvex.smul_mem (hU.starConvex zero_mem) hz (by positivity) hr₁
  rwa [hz_def, ← smul_assoc, smul_eq_mul, ← mul_assoc, mul_comm, mul_comm r⁻¹, mul_assoc _ r⁻¹,
    inv_mul_cancel₀ hr₀, mul_one, inv_mul_cancel₀ (by simp_all), one_smul] at this

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

Goal state before:
pp: case h
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁷ : SeminormedRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : SeminormedRing 𝕜₂
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
ι : Type u_11
inst✝ : Nonempty ι
p : Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
h : ∀ (i : ι'), ∃ C, (q i).comp f ≤ C • p
i : ι'
⊢ ∃ C, (q i).comp f ≤ C • {Classical.arbitrary ι}.sup fun x ↦ p

Tactic:
simp only [h, Finset.sup_singleton]

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

Goal state before:
pp: case mp
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r) → ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r

Tactic:
intro hI

Goal state after:
case mp
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hI : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
⊢ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : FunLike 𝓕 E F
inst✝¹ : SemilinearMapClass 𝓕 σ₁₂ E F
inst✝ : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ball x r ⊆ Set.range ⇑f
⊢ ball 0 r ⊆ Set.range ⇑f

Tactic:
← LinearMap.coe_coe

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
𝓕 : Type u_8
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : FunLike 𝓕 E F
inst✝¹ : SemilinearMapClass 𝓕 σ₁₂ E F
inst✝ : RingHomSurjective σ₁₂
f : 𝓕
x : F
r : ℝ
hr : 0 < r
h : ball x r ⊆ Set.range ⇑f
⊢ ball 0 r ⊆ Set.range ⇑↑f
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ Seminorm.IsBounded p q LinearMap.id

Tactic:
by assumption

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
ι' : Type u_10
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
q : SeminormFamily 𝕜 E ι'
hpq : Seminorm.IsBounded p q LinearMap.id
hqp : Seminorm.IsBounded q p LinearMap.id
⊢ Seminorm.IsBounded q p LinearMap.id

Tactic:
by assumption

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NNNorm

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : DenselyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
h✝ : Nontrivial E
this : NormedSpace ℝ E
ub : ℝ≥0
hub : ub < ‖f‖₊
x : E
hx : ‖x‖₊ = 1
hxf : ub < ‖f x‖₊
⊢ x ∈ sphere 0 1

Tactic:
by simpa using! congrArg NNReal.toReal hx

Goal state after:
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly (fun i a ↦ (F i) a) (⇑f) p
K : Set α
hK : IsCompact K
⊢ TendstoLocallyUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K

Tactic:
exact h.tendstoLocallyUniformlyOn

Goal state after:
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝³ : TopologicalSpace α
inst✝² : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst✝¹ : TopologicalSpace δ₁
inst✝ : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap ⇑φ₁
h_proper₂ : IsProperMap ⇑φ₂
h_cover : range ⇑φ₁ ∪ range ⇑φ₂ = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K | IsCompact K}
h_image₁ : MapsTo (fun x ↦ ⇑φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ ⇑φ₂ '' x) 𝔗₂ 𝔖
⊢ inferInstance =
    UniformSpace.comap (fun x ↦ x.comp φ₁) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp φ₂) inferInstance

Tactic:
have h_preimage₁ : MapsTo (φ₁ ⁻¹' ·) 𝔖 𝔗₁ := fun K ↦ h_proper₁.isCompact_preimage

Goal state after:
α : Type u₁
β : Type u₂
inst✝³ : TopologicalSpace α
inst✝² : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst✝¹ : TopologicalSpace δ₁
inst✝ : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap ⇑φ₁
h_proper₂ : IsProperMap ⇑φ₂
h_cover : range ⇑φ₁ ∪ range ⇑φ₂ = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K | IsCompact K}
h_image₁ : MapsTo (fun x ↦ ⇑φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ ⇑φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ ⇑φ₁ ⁻¹' x) 𝔖 𝔗₁
⊢ inferInstance =
    UniformSpace.comap (fun x ↦ x.comp φ₁) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp φ₂) inferInstance