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

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

Tactic:
smul_comm c,

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
s : Set E
f : E → β
c : 𝕜
hc : 0 ≤ c
hf : ConvexOn 𝕜 s f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • c • f x + c • b • f y = a • c • f x + b • c • f y
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
⊢ (affineCombination k s p).linear (w₁ -ᵥ w₂) = (s.weightedVSub p) (w₁ - w₂)

Tactic:
affineCombination_linear,

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₁ -ᵥ w₂) = (s.weightedVSub p) (w₁ - w₂)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inr
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
⊢ p x < ‖k‖ * r → ∃ y ∈ p.ball 0 r, k • y = x

Tactic:
refine fun hx => ⟨k⁻¹ • x, ?_, ?_⟩

Goal state after:
case inr.refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
hx : p x < ‖k‖ * r
⊢ k⁻¹ • x ∈ p.ball 0 r

case inr.refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : k ≠ 0
x : E
hx : p x < ‖k‖ * r
⊢ k • k⁻¹ • x = x
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
⊢ p x ≤ ‖k‖ * r → ∃ y ∈ p.closedBall 0 r, k • y = x

Tactic:
refine fun hx => ⟨k⁻¹ • x, ?_, ?_⟩

Goal state after:
case refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : p x ≤ ‖k‖ * r
⊢ k⁻¹ • x ∈ p.closedBall 0 r

case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
k : 𝕜
r : ℝ
hk : 0 < ‖k‖
x : E
hx : p x ≤ ‖k‖ * r
⊢ k • k⁻¹ • x = x
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
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
h₁ : (insert j s).sum w' = 1
⊢ (s.weightedVSubOfPoint p (p j)) w +ᵥ p j ∈ affineSpan k (Set.range p)

Tactic:
have hww : ∀ i, i ≠ j → w i = w' i := by
        intro i hij
        simp [w', hij]

Goal state after:
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
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
h₁ : (insert j s).sum w' = 1
hww : ∀ (i : ι), i ≠ j → w i = w' i
⊢ (s.weightedVSubOfPoint p (p j)) w +ᵥ p j ∈ affineSpan k (Set.range p)
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ s.points '' Set.range ⇑(fs.orderEmbOfFin h) = s.points '' ↑fs

Tactic:
Finset.range_orderEmbOfFin

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_5
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ s.points '' ↑fs = s.points '' ↑fs
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
i : Fin (n + 1)
h : w i = 0
hk : Nontrivial k
⊢ ∀ i_1 ∈ univ, i_1 ∉ {i}ᶜ → w i_1 = 0

Tactic:
by simpa using h

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

Goal state before:
pp: case refine_1
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
I : Set k
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (m + 1) → k
hw : ∑ i, w i = 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
x✝ : (affineCombination k univ (s.reindex e).points) w ∈ Simplex.setInterior I (s.reindex e)
hw' : ∑ i, (w ∘ ⇑e) i = 1
⊢ (affineCombination k univ s.points) (w ∘ ⇑e) ∈ Simplex.setInterior I s

Tactic:
affineCombination_mem_setInterior_iff hw'

Goal state after:
case refine_1
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
I : Set k
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (m + 1) → k
hw : ∑ i, w i = 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
x✝ : (affineCombination k univ (s.reindex e).points) w ∈ Simplex.setInterior I (s.reindex e)
hw' : ∑ i, (w ∘ ⇑e) i = 1
⊢ ∀ (i : Fin (n + 1)), (w ∘ ⇑e) i ∈ I
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case refine_2
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
I : Set k
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
x✝ : (affineCombination k univ s.points) w ∈ Simplex.setInterior I s
hw' : ∑ i, (w ∘ ⇑e.symm) i = 1
⊢ (affineCombination k univ (s.reindex e).points) (w ∘ ⇑e.symm) ∈ Simplex.setInterior I (s.reindex e)

Tactic:
affineCombination_mem_setInterior_iff hw'

Goal state after:
case refine_2
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
I : Set k
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
x✝ : (affineCombination k univ s.points) w ∈ Simplex.setInterior I s
hw' : ∑ i, (w ∘ ⇑e.symm) i = 1
⊢ ∀ (i : Fin (m + 1)), (w ∘ ⇑e.symm) i ∈ I
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case mp
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✝ : ZeroLEOneClass k
s : Simplex k P 0
w : Fin 1 → k
h0 : w 0 = 1
hi : ∀ (i : Fin 1), 0 ≤ w i ∧ w i ≤ 1
⊢ (affineCombination k {0} s.points) w = s.points 0

Tactic:
simp [affineCombination_apply, h0]

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

Goal state before:
pp: case refine_1
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
I : Set k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
w' : Fin (m + 1) → k
hi : (affineCombination k univ (s.face h).points) w' ∈ Simplex.setInterior I (s.face h)
hw' : ∑ i, w' i = 1
he : (affineCombination k univ s.points) w = (affineCombination k univ (s.face h).points) w'
⊢ (∀ i ∈ fs, w i ∈ I) ∧ ∀ i ∉ fs, w i = 0

Tactic:
affineCombination_mem_setInterior_iff hw'

Goal state after:
case refine_1
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
I : Set k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
w' : Fin (m + 1) → k
hi : ∀ (i : Fin (m + 1)), w' i ∈ I
hw' : ∑ i, w' i = 1
he : (affineCombination k univ s.points) w = (affineCombination k univ (s.face h).points) w'
⊢ (∀ i ∈ fs, w i ∈ I) ∧ ∀ i ∉ fs, w i = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w₁ w₂ : V → k
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i
⊢ ∀ i ∈ s, w₁ i = w₂ i

Tactic:
refine fun i hi => sub_eq_zero.1 (hp.eq_zero_of_sum_eq_zero_subtype (w := w₁ - w₂) ?_ ?_ _ hi)

Goal state after:
case refine_1
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w₁ w₂ : V → k
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i
i : V
hi : i ∈ s
⊢ ∑ x ∈ s, (w₁ - w₂) x = 0

case refine_2
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w₁ w₂ : V → k
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i
i : V
hi : i ∈ s
⊢ ∑ x ∈ s, (w₁ - w₂) x • x = 0
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:
rw [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.Analysis.Convex.Combination

Goal state before:
pp: case neg.refine_3
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
s : Set E
t✝ : Finset ι
w : ι → R
z : ι → E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬∑ j ∈ t, w j = 0
⊢ 0 ≤ w i

Tactic:
exact h₀ _ (mem_insert_self _ _)

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
x : X
⊢ nhdsKer {x} = (𝓝 x).ker

Tactic:
simp [nhdsKer]

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

Goal state before:
pp: case inr.refine_1
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
s : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
h : LinearIndepOn k id ((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : AffineIndependent k fun p ↦ ↑p
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p ↦ p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
h0 : ∀ v ∈ h.extend ⋯, v ≠ 0
⊢ s ⊆ {p₁} ∪ (fun v ↦ v +ᵥ p₁) '' h.extend ⋯

pp: case inr.refine_2
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
s : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
h : LinearIndepOn k id ((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : AffineIndependent k fun p ↦ ↑p
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p ↦ p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
h0 : ∀ v ∈ h.extend ⋯, v ≠ 0
⊢ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k ({p₁} ∪ (fun v ↦ v +ᵥ p₁) '' h.extend ⋯) = ⊤

Tactic:
· refine Set.Subset.trans ?_ (Set.union_subset_union_right _ (Set.image_mono hsv))
      simp [Set.image_image]

Goal state after:
case inr.refine_2
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
s : Set P
p₁ : P
h✝ : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))) ↦ ↑v
h : LinearIndepOn k id ((fun p ↦ p -ᵥ p₁) '' (s \ {p₁}))
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h✝ ⋯)) k V := Basis.extend h✝
hsvi : AffineIndependent k fun p ↦ ↑p
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
hsv : (fun p ↦ p -ᵥ p₁) '' (s \ {p₁}) ⊆ h.extend ⋯
h0 : ∀ v ∈ h.extend ⋯, v ≠ 0
⊢ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k ({p₁} ∪ (fun v ↦ v +ᵥ p₁) '' h.extend ⋯) = ⊤
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

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
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x ↦ p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x ↦ x ≠ i) s
p' : { y // y ≠ i } → P := fun x ↦ p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : (s.weightedVSub p) wm = 0
hwm : ∑ x ∈ s with x ≠ i, wm x + ∑ x ∈ s with ¬x ≠ i, wm x = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x ↦ wm ↑x
⊢ ∑ x ∈ s with x ≠ i, wm x = 1

Tactic:
simpa only [not_not, Finset.filter_eq' _ i, if_pos his.1, sum_singleton, hwmi,
          add_neg_eq_zero] using hwm

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 r) = closedBall x r

Tactic:
rw [← add_zero x, ← vadd_eq_add, ← vadd_sphere, convexHull_vadd,
      this, vadd_closedBall_zero, vadd_eq_add, add_zero]

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
x : F
h : x ∈ closedBall 0 r
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
x✝ : Invertible 2
z : F
hz : z ∈ sphere 0 r
⊢ -z ∈ sphere 0 r

Tactic:
by simp_all

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
x : F
h : x ∈ closedBall 0 r
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (‖x‖⁻¹ * ‖x‖) • x ∈ U
⊢ ‖x‖ ≠ 0

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Topology.Algebra.SeparationQuotient.Section

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup E
inst✝³ : Module K E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul K E
f : SeparationQuotient E →ₗ[K] E
hf : ↑(mkCLM K E) ∘ₗ f = LinearMap.id
⊢ ∃ f, mkCLM K E ∘SL f = ContinuousLinearMap.id K (SeparationQuotient E)

Tactic:
replace hf : mk ∘ f = id := congr_arg DFunLike.coe hf

Goal state after:
K : Type u_1
E : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup E
inst✝³ : Module K E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul K E
f : SeparationQuotient E →ₗ[K] E
hf : mk ∘ ⇑f = id
⊢ ∃ f, mkCLM K E ∘SL f = ContinuousLinearMap.id K (SeparationQuotient E)
Module: Mathlib.Topology.Algebra.Module.UniformConvergence

Goal state before:
pp: case hsmul_left
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup H
inst✝⁸ : Module 𝕜 H
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this✝ : IsTopologicalAddGroup H
hb : (𝓝 0).HasBasis (fun x ↦ x ∈ 𝓝 0) fun V ↦ {u | ∀ (x : α), φ u x ∈ V}
c : 𝕜
U : Set E
hU : U ∈ 𝓝 0
this : Tendsto (fun x ↦ c • x) (𝓝 0) (𝓝 0)
⊢ ∃ j ∈ 𝓝 0, Set.MapsTo (fun x ↦ c • x) {u | ∀ (x : α), φ u x ∈ j} {u | ∀ (x : α), φ u x ∈ U}

Tactic:
refine ⟨_, this hU, fun u hu x ↦ ?_⟩

Goal state after:
case hsmul_left
𝕜 : Type u_1
α : Type u_2
E : Type u_3
H : Type u_4
hom : Type u_5
inst✝¹⁰ : NormedField 𝕜
inst✝⁹ : AddCommGroup H
inst✝⁸ : Module 𝕜 H
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : UniformSpace E
inst✝³ : IsUniformAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : FunLike hom H (α → E)
inst✝ : LinearMapClass hom 𝕜 H (α → E)
φ : hom
hφ : IsInducing (⇑ofFun ∘ ⇑φ)
h : ∀ (u : H), Bornology.IsVonNBounded 𝕜 (Set.range (φ u))
this✝ : IsTopologicalAddGroup H
hb : (𝓝 0).HasBasis (fun x ↦ x ∈ 𝓝 0) fun V ↦ {u | ∀ (x : α), φ u x ∈ V}
c : 𝕜
U : Set E
hU : U ∈ 𝓝 0
this : Tendsto (fun x ↦ c • x) (𝓝 0) (𝓝 0)
u : H
hu : u ∈ {u | ∀ (x : α), φ u x ∈ (fun x ↦ c • x) ⁻¹' U}
x : α
⊢ φ ((fun x ↦ c • x) u) x ∈ U
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_9
ι' : Type u_10
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : s'.Nonempty
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
⊢ ∑ x ∈ s', (pullback f) (q x) ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p

Tactic:
pullback_apply

Goal state after:
case h
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
ι' : Type u_10
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p : ι → Seminorm 𝕜 E
q : ι' → Seminorm 𝕜₂ F
f : E →ₛₗ[σ₁₂] F
s' : Finset ι'
h✝ : s'.Nonempty
fₛ : ι' → Finset ι
fC : ι' → ℝ≥0
hf : ∀ (i : ι'), (q i).comp f ≤ fC i • (fₛ i).sup p
hs : ∀ i ∈ s', (q i).comp f ≤ s'.sup fC • (s'.biUnion fₛ).sup p
⊢ ∑ x ∈ s', (q x).comp f ≤ (s'.card • s'.sup fC) • (s'.biUnion fₛ).sup p
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
𝔖 : Set (Set E)
⊢ IsUniformAddGroup (E →SLᵤ[σ, 𝔖] F)

Tactic:
let φ : (E →SLᵤ[σ, 𝔖] F) →+ E →ᵤ[𝔖] F :=
    ⟨⟨(DFunLike.coe : (E →SLᵤ[σ, 𝔖] F) → E →ᵤ[𝔖] F), rfl⟩, fun _ _ => rfl⟩

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
𝔖 : Set (Set E)
φ : (E →SLᵤ[σ, 𝔖] F) →+ E →ᵤ[𝔖] F := { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }
⊢ IsUniformAddGroup (E →SLᵤ[σ, 𝔖] F)
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
⊢ Function.Surjective ⇑f → ball x r ⊆ Set.range ⇑f

Tactic:
by simp_all

Goal state after:
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
⊢ Function.Surjective ⇑f → closedBall x r ⊆ Set.range ⇑f

Tactic:
by simp_all

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
F' : Type u_9
𝓕' : Type u_10
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
inst✝³ : Nontrivial F'
τ : 𝕜 →+* ℝ
inst✝² : FunLike 𝓕' E F'
inst✝¹ : SemilinearMapClass 𝓕' τ E F'
inst✝ : RingHomSurjective τ
f : 𝓕'
x : F'
r : ℝ
hr : 0 < r
⊢ Function.Surjective ⇑f → sphere x r ⊆ Set.range ⇑f

Tactic:
by simp_all

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

Goal state before:
pp: 𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
κ : Type u_11
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
x✝¹ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
x✝ : UniformEquicontinuous (DFunLike.coe ∘ f)
H : UniformEquicontinuous (DFunLike.coe ∘ f) := x✝
this : ∀ᶠ (x : E) in 𝓝 0, ∀ (k : κ), (q i) ((f k) x) ≤ 1
bdd : BddAbove (Set.range fun k ↦ (q i).comp (f k))
⊢ BddAbove (Set.range fun k ↦ (q i).comp (f k)) ∧ Continuous[inst✝².toTopologicalSpace, _] ⇑(⨆ i_1, (q i).comp (f i_1))

Tactic:
refine ⟨bdd, Seminorm.continuous' (r := 1) ?_⟩

Goal state after:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
κ : Type u_11
q : SeminormFamily 𝕜₂ F ι'
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
f : κ → E →ₛₗ[σ₁₂] F
i : ι'
x✝¹ : SeminormedAddCommGroup F := (q i).toSeminormedAddCommGroup
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
x✝ : UniformEquicontinuous (DFunLike.coe ∘ f)
H : UniformEquicontinuous (DFunLike.coe ∘ f) := x✝
this : ∀ᶠ (x : E) in 𝓝 0, ∀ (k : κ), (q i) ((f k) x) ≤ 1
bdd : BddAbove (Set.range fun k ↦ (q i).comp (f k))
⊢ (⨆ i_1, (q i).comp (f i_1)).closedBall 0 1 ∈ 𝓝 0