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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝¹³ : Ring 𝕜
inst✝¹² : LinearOrder 𝕜
inst✝¹¹ : IsStrictOrderedRing 𝕜
inst✝¹⁰ : DenselyOrdered 𝕜
inst✝⁹ : PseudoMetricSpace 𝕜
inst✝⁸ : OrderTopology 𝕜
inst✝⁷ : ProperSpace 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ closure (openSegment 𝕜 x y) = [x -[𝕜] y]

Tactic:
segment_eq_image,

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝¹³ : Ring 𝕜
inst✝¹² : LinearOrder 𝕜
inst✝¹¹ : IsStrictOrderedRing 𝕜
inst✝¹⁰ : DenselyOrdered 𝕜
inst✝⁹ : PseudoMetricSpace 𝕜
inst✝⁸ : OrderTopology 𝕜
inst✝⁷ : ProperSpace 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ closure (openSegment 𝕜 x y) = (fun θ ↦ (1 - θ) • x + θ • y) '' Icc 0 1
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝¹³ : Ring 𝕜
inst✝¹² : LinearOrder 𝕜
inst✝¹¹ : IsStrictOrderedRing 𝕜
inst✝¹⁰ : DenselyOrdered 𝕜
inst✝⁹ : PseudoMetricSpace 𝕜
inst✝⁸ : OrderTopology 𝕜
inst✝⁷ : ProperSpace 𝕜
inst✝⁶ : CompactIccSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ Continuous fun θ ↦ (1 - θ) • x + θ • y

Tactic:
by fun_prop

Goal state after:
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
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : (if h : HasFiniteSupport ((fun i ↦ w i) ∘ PLift.down) then ∑ i ∈ Finite.toFinset h, w i.down else 0) = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
H : ¬HasFiniteSupport (w ∘ PLift.down)
⊢ False

Tactic:
dif_neg H

Goal state after:
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : 0 = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
H : ¬HasFiniteSupport (w ∘ PLift.down)
⊢ False
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inr
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
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h ⋯)) k V := Basis.extend h
hsvi : LinearIndependent (ι := ↑(LinearIndepOn.extend h ⋯)) k ⇑bsv
hsvt : Submodule.span k (Set.range ⇑bsv) = ⊤
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤

Tactic:
rw [Basis.coe_extend] at hsvi hsvt

Goal state after:
case inr
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
hp₁ : p₁ ∈ s
bsv : Basis (↑(LinearIndepOn.extend h ⋯)) k V := Basis.extend h
hsvi : LinearIndependent (ι := ↑(LinearIndepOn.extend h ⋯)) k Subtype.val
hsvt : Submodule.span k (Set.range Subtype.val) = ⊤
⊢ ∃ t, s ⊆ t ∧ (AffineIndependent k fun p ↦ ↑p) ∧ affineSpan k t = ⊤
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
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:
· use hsvi
      exact affineSpan_singleton_union_vadd_eq_top_of_span_eq_top p₁ hsvt

Goal state after:
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
inst✝ : LocallyPathConnectedSpace X
⊢ LocallyConnectedSpace X

Tactic:
refine ⟨forall_imp (fun x h ↦ ⟨fun s ↦ ?_⟩) isOpen_isPathConnected_basis⟩
  refine ⟨fun hs ↦ ?_, fun ⟨u, ⟨hu, hxu, _⟩, hus⟩ ↦ mem_nhds_iff.mpr ⟨u, hus, hu, hxu⟩⟩
  let ⟨u, ⟨hu, hxu, hu'⟩, hus⟩ := (h.mem_iff' s).mp hs
  exact ⟨u, ⟨hu, hxu, hu'.isConnected⟩, hus⟩

Goal state after:
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
⊢ (affineCombination R t p) w = t.centerMass w p

Tactic:
rw [affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ w _ hw₂ (0 : E),
    Finset.weightedVSubOfPoint_apply, vadd_eq_add, add_zero, t.centerMass_eq_of_sum_1 _ hw₂]
  simp_rw [vsub_eq_sub, sub_zero]

Goal state after:
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y✝ z : X
ι : Type u_3
F : Set X
inst✝¹ : LocallyPathConnectedSpace X
inst✝ : AlexandrovDiscrete X
x y : X
hy : y ⤳ x
⊢ JoinedIn (nhdsKer {x}) y x

Tactic:
apply hy.joinedIn <;> rewrite [mem_nhdsKer_singleton] <;> [assumption; rfl]

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✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing 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 = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
r : k
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ SignType.sign (r * (w₂ i - 0)) = SignType.sign (r * (w₂ j - 0))

Tactic:
sub_zero,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing 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 = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
r : k
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ SignType.sign (r * w₂ i) = SignType.sign (r * (w₂ j - 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✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing 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 = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
r : k
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ SignType.sign (r * w₂ i) = SignType.sign (r * (w₂ j - 0))

Tactic:
sub_zero,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing 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 = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i j : ι
hi : i ∈ s
hj : j ∈ s
hi0 : w₁ i = 0
hj0 : w₁ j = 0
hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)
r : k
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ SignType.sign (r * w₂ i) = SignType.sign (r * w₂ j)
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
⊢ closedBall x r = closedBall (x + 0) r

Tactic:
add_zero

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
⊢ closedBall x r = closedBall x r
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ¬x = 0
⊢ ContinuousOn (fun r ↦ r • x) (Ici 0)

Tactic:
by fun_prop

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : x ≠ 0
⊢ ContinuousOn (fun r ↦ r • x) (Ioi 0)

Tactic:
by fun_prop

Goal state after:
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, (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ ∑ y ∈ t₁ ∩ t₂, w y = 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x

Tactic:
let w (x : E) : R := (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0

Goal state after:
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
⊢ ∃ w, (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ ∑ y ∈ t₁ ∩ t₂, w y = 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
Module: Mathlib.Analysis.Convex.Jensen

Goal state before:
pp: case h₀
𝕜 : 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
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
⊢ ∀ i ∈ {x ∈ t | w x ≠ 0}, 0 < w i

pp: case h₁
𝕜 : 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
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
⊢ ∑ i ∈ t with w i ≠ 0, w i = 1

pp: case hmem
𝕜 : 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
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
⊢ ∀ i ∈ {x ∈ t | w x ≠ 0}, p i ∈ s

Tactic:
· simp +contextual [(h₀ _ _).lt_iff_ne']

Goal state after:
case h₁
𝕜 : 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
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
⊢ ∑ i ∈ t with w i ≠ 0, w i = 1

case hmem
𝕜 : 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
hw : ∀ i ∈ t, w i • p i ≠ 0 → w i ≠ 0
hw' : ∀ i ∈ t, w i • f (p i) ≠ 0 → w i ≠ 0
⊢ ∀ i ∈ {x ∈ t | w x ≠ 0}, p i ∈ s
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case pos
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : x ≠ 0
⊢ ∃ V ∈ p.addGroupFilterBasis.sets, V ⊆ (s.sup p).ball 0 (r / ‖x‖)

Tactic:
use (s.sup p).ball 0 (r / ‖x‖)

Goal state after:
case h
𝕜 : Type u_2
F : Type u_7
ι : Type u_9
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
p : SeminormFamily 𝕜 F ι
x : 𝕜
U : Set F
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : x ≠ 0
⊢ (s.sup p).ball 0 (r / ‖x‖) ∈ p.addGroupFilterBasis.sets ∧ (s.sup p).ball 0 (r / ‖x‖) ⊆ (s.sup p).ball 0 (r / ‖x‖)
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_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
H : ∀ (i : ι'), ∃ s C, ∀ (x : E), (q i) (f x) ≤ C * (s.sup p) x
⊢ IsBounded p q f

Tactic:
IsBounded

Goal state after:
𝕜 : 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
H : ∀ (i : ι'), ∃ s C, ∀ (x : E), (q i) (f x) ≤ C * (s.sup p) x
⊢ ∀ (i : ι'), ∃ s C, (q i).comp f ≤ C • s.sup p
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
x : E
this✝ : IsTopologicalAddGroup E
sr : Finset ι × ℝ
this : (sr.1.sup p).ball (x + 0) sr.2 = x +ᵥ (sr.1.sup p).ball 0 sr.2
⊢ (sr.1.sup p).ball x sr.2 = (fun x_1 ↦ x + x_1) '' (sr.1.sup p).ball 0 sr.2

Tactic:
add_zero

Goal state after:
𝕜 : 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
x : E
this✝ : IsTopologicalAddGroup E
sr : Finset ι × ℝ
this : (sr.1.sup p).ball x sr.2 = x +ᵥ (sr.1.sup p).ball 0 sr.2
⊢ (sr.1.sup p).ball x sr.2 = (fun x_1 ↦ x + x_1) '' (sr.1.sup p).ball 0 sr.2
Module: Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM

Goal state before:
pp: 𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜₂ F
𝕜₁ : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup G
𝕜₃ : Type u_7
inst✝⁸ : NormedField 𝕜₃
inst✝⁷ : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst✝⁶ : RingHomSurjective τ
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousConstSMul 𝕜₂ F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] E →SLᵤ[σ, 𝔖] F
hB : Continuous[instTopologicalSpaceProd, inst✝⁵] fun p ↦ (B p.1) p.2
⊢ ∀ s ∈ 𝔖, ∀ U ∈ 𝓝 0, ∀ᶠ (g : G) in 𝓝 0, ∀ e ∈ s, (B g) e ∈ U

Tactic:
intro S hS U hU

Goal state after:
𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₂
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜₂ F
𝕜₁ : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜₁
σ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup G
𝕜₃ : Type u_7
inst✝⁸ : NormedField 𝕜₃
inst✝⁷ : Module 𝕜₃ G
τ : 𝕜₃ →+* 𝕜₂
inst✝⁶ : RingHomSurjective τ
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousConstSMul 𝕜₂ F
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
𝔖 : Set (Set E)
h𝔖 : ∀ s ∈ 𝔖, IsVonNBounded 𝕜₁ s
B : G →ₛₗ[τ] E →SLᵤ[σ, 𝔖] F
hB : Continuous[instTopologicalSpaceProd, inst✝⁵] fun p ↦ (B p.1) p.2
S : Set E
hS : S ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
⊢ ∀ᶠ (g : G) in 𝓝 0, ∀ e ∈ S, (B g) e ∈ U
Module: Mathlib.Analysis.Normed.Operator.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
x : E
hx : ‖x‖ ≠ 0
⊢ ‖f x‖ ≤ C * ‖x‖

Tactic:
have H₁ : ‖algebraMap _ 𝕜 ‖x‖⁻¹ • x‖ = 1 := by simp [norm_smul, inv_mul_cancel₀ hx]

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : NormedAlgebra ℝ 𝕜
f : E →SL[σ₁₂] F
C : ℝ
hC : 0 ≤ C
hf : ∀ (x : E), ‖x‖ = 1 → ‖f x‖ ≤ C
x : E
hx : ‖x‖ ≠ 0
H₁ : ‖(algebraMap ℝ 𝕜) ‖x‖⁻¹ • x‖ = 1
⊢ ‖f x‖ ≤ C * ‖x‖
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: case right
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen[instTopologicalSpaceProd] V
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed[instTopologicalSpaceProd] W
hWU : W ⊆ V
s : Set α := ⋯
hnhds : s ∈ 𝓝[K] x
hcomp : IsCompact s
hmaps : MapsTo (⇑f) s (ball (f x) V)
⊢ ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, (fun i a ↦ (F i) a) n y) ∈ U

Tactic:
refine (h s hcomp _ (isOpen_ball _ hVo) hmaps).mono fun g hg y hy ↦ ?_

Goal state after:
case right
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β), IsOpen[inst✝.toTopologicalSpace] U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen[instTopologicalSpaceProd] V
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed[instTopologicalSpaceProd] W
hWU : W ⊆ V
s : Set α := K ∩ ⇑f ⁻¹' ball (f x) W
hnhds : s ∈ 𝓝[K] x
hcomp : IsCompact s
hmaps : MapsTo (⇑f) s (ball (f x) V)
g : ι
hg : MapsTo (⇑(F g)) s (ball (f x) V)
y : α
hy : y ∈ s
⊢ (f y, (fun i a ↦ (F i) a) g y) ∈ U
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
Eₗ : Type u_5
Fₗ : Type u_7
Gₗ : Type u_9
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : SeminormedAddCommGroup Fₗ
inst✝⁵ : SeminormedAddCommGroup Gₗ
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜 Eₗ
inst✝¹ : NormedSpace 𝕜 Fₗ
inst✝ : NormedSpace 𝕜 Gₗ
L : E →L[𝕜] Fₗ →L[𝕜] Gₗ
⊢ ‖(precompR Eₗ L.flip).flip‖ ≤ ‖L‖

Tactic:
opNorm_flip,

Goal state after:
𝕜 : Type u_1
E : Type u_4
Eₗ : Type u_5
Fₗ : Type u_7
Gₗ : Type u_9
inst✝⁸ : SeminormedAddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : SeminormedAddCommGroup Fₗ
inst✝⁵ : SeminormedAddCommGroup Gₗ
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜 Eₗ
inst✝¹ : NormedSpace 𝕜 Fₗ
inst✝ : NormedSpace 𝕜 Gₗ
L : E →L[𝕜] Fₗ →L[𝕜] Gₗ
⊢ ‖precompR Eₗ L.flip‖ ≤ ‖L‖
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace C(α, β)
f : α → β
s : Set α
⊢ IsComplete {g | EqOn (⇑g) f s}

Tactic:
by
  classical
  intro l hlc hlf
  rcases CompleteSpace.complete hlc with ⟨f', hf'⟩
  have := hlc.1
  have H₁ : ∀ x ∈ s, Inseparable (f x) (f' x) := fun x hx ↦ by
    refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')
    refine tendsto_const_nhds.congr' <| .filter_mono ?_ hlf
    exact fun _ h ↦ (h hx).symm
  have H₂ (x) : Inseparable (s.piecewise f f' x) (f' x) := by
    by_cases hx : x ∈ s <;> simp [hx, H₁, Inseparable.refl]
  set g : C(α, β) :=
    ⟨s.piecewise f f', (continuous_congr_of_inseparable H₂).mpr <| map_continuous f'⟩
  refine ⟨g, Set.piecewise_eqOn _ _ _, hf'.trans_eq ?_⟩
  rwa [eq_comm, ← Inseparable, ← inseparable_coe, inseparable_pi]

Goal state after:
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case mpr.inr
ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb₀ : 0 ≤ b
hb : ∀ (x : ℝ) (hx : 0 ≤ x), (∀ᶠ (a : ι) in f, ↑(NNReal.mk x hx) ≤ ↑(u a)) → ↑(NNReal.mk x hx) ≤ ↑(NNReal.mk b hb₀)
x : ℝ
hx : ∀ᶠ (a : ι) in f, ↑(u a) ≥ x
hx₀ : 0 ≤ x
⊢ b ≥ x

Tactic:
exact hb _ hx₀ hx

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: case hs
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ MeasurableSet (i ⁻¹' s ∩ t)

Tactic:
exact ht

Goal state after:
case hs
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ MeasurableSet (i ⁻¹' s ∩ t)
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: case hs
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ MeasurableSet (i ⁻¹' s)

Tactic:
exact ht

Goal state after:
case hs
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ MeasurableSet (i ⁻¹' s)
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: case hs
Ω : Type u_1
Ω' : Type u_2
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s : Set Ω
i : Ω' → Ω
hi : MeasurableEmbedding i
hs : MeasurableSet s
t : Set Ω'
ht : MeasurableSet t
hi' : μ (range i)ᶜ = 0
⊢ MeasurableSet t

Tactic:
exact ht

Goal state after: