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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i0 : ι
⊢ vectorSpan k (range p) = Submodule.span k (range fun i ↦ p i -ᵥ p i0)

Tactic:
rw [vectorSpan_eq_span_vsub_set_right k (Set.mem_range_self i0), ← Set.range_comp]

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
i0 : ι
⊢ Submodule.span k (range ((fun x ↦ x -ᵥ p i0) ∘ p)) = Submodule.span k (range fun i ↦ p i -ᵥ p i0)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
hconv : Convex 𝕜 s
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ f (a • x + b • y)

Tactic:
exact h hx hy ha hb hab

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
⊢ ⨆ i, ↑i 0 = 0

Tactic:
← @Real.iSup_const_zero s

Goal state after:
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)
h : BddAbove (DFunLike.coe '' s)
⊢ ⨆ i, ↑i 0 = ⨆ x, 0
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 ι
V₂ : Type u_6
P₂ : Type u_7
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : s.sum w = 1
f : P →ᵃ[k] P₂
b : P
b₂ : P₂
⊢ f ((s.weightedVSubOfPoint p b) w +ᵥ b) = (s.weightedVSubOfPoint (⇑f ∘ p) b₂) w +ᵥ b₂

Tactic:
←
    s.weightedVSubOfPoint_vadd_eq_of_sum_eq_one w (f ∘ p) hw (f b) b₂

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 ι
V₂ : Type u_6
P₂ : Type u_7
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
p : ι → P
w : ι → k
hw : s.sum w = 1
f : P →ᵃ[k] P₂
b : P
b₂ : P₂
⊢ f ((s.weightedVSubOfPoint p b) w +ᵥ b) = (s.weightedVSubOfPoint (⇑f ∘ p) (f b)) w +ᵥ f b
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 ≠ 0
⊢ ∑ i, centroidWeightsIndicator k s i = 1

Tactic:
rw [sum_centroidWeightsIndicator]
  exact s.sum_centroidWeights_eq_one_of_card_ne_zero k h

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

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

Tactic:
Set.range_eq_empty,

Goal state after:
case mp.inl
ι : 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
hι : IsEmpty ι
⊢ v ∈ vectorSpan k ∅ → ∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) 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
ha : AffineIndependent k p
f : ↑(Set.range p) → ι := fun x ↦ Exists.choose ⋯
⊢ AffineIndependent k fun x ↦ ↑x

Tactic:
have hf : ∀ x, p (f x) = x := fun x => x.property.choose_spec

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
ha : AffineIndependent k p
f : ↑(Set.range p) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
⊢ AffineIndependent k fun x ↦ ↑x
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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s1 s2 : Set ι
hd : Disjoint s1 s2
⊢ Disjoint ↑(affineSpan k (p '' s1)) ↑(affineSpan k (p '' s2))

Tactic:
by
  refine Set.disjoint_left.2 fun p0 hp0s1 hp0s2 => ?_
  obtain ⟨i, hi⟩ := ha.exists_mem_inter_of_exists_mem_inter_affineSpan hp0s1 hp0s2
  exact Set.disjoint_iff.1 hd hi

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
i j : ι
hij : i ≠ j
⊢ 1 ≤ Metric.diam (stdSimplex ℝ ι)

Tactic:
show (1 : ℝ) = dist (Pi.single i 1 : ι → ℝ) (Pi.single j 1) by
    simp [dist_single_single i j (1 : ℝ) 1 hij, Real.dist_eq]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
i j : ι
hij : i ≠ j
⊢ dist (Pi.single i 1) (Pi.single j 1) ≤ Metric.diam (stdSimplex ℝ ι)
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
i j : ι
hij : i ≠ j
⊢ 1 ≤ Metric.diam (stdSimplex ℝ ι)

Tactic:
classical
  rw [show (1 : ℝ) = dist (Pi.single i 1 : ι → ℝ) (Pi.single j 1) by
    simp [dist_single_single i j (1 : ℝ) 1 hij, Real.dist_eq]]
  exact Metric.dist_le_diam_of_mem (bounded_stdSimplex _)
    (single_mem_stdSimplex _ _) (single_mem_stdSimplex _ _)

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
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : j ∈ s₁
hne : j ≠ i
he : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
fs : Finset ↑s₂
w : ↑s₂ → k
hw : ∑ i ∈ fs, w i = 0
hs : p i -ᵥ p j = (fs.weightedVSub fun x ↦ p ↑x) w
w' : ι → k := extend Subtype.val w 0
hw' : ∑ t ∈ map (Embedding.subtype fun x ↦ x ∈ s₂) fs, w' t = 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun x ↦ x ∈ s₂) fs).weightedVSub p) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun x ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun x ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun x ↦ x ∈ s₂) fs)).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p) w''
⊢ ∑ t ∈ fs', w'' t = 0

Tactic:
rw [← hw']

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
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : j ∈ s₁
hne : j ≠ i
he : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
fs : Finset ↑s₂
w : ↑s₂ → k
hw : ∑ i ∈ fs, w i = 0
hs : p i -ᵥ p j = (fs.weightedVSub fun x ↦ p ↑x) w
w' : ι → k := extend Subtype.val w 0
hw' : ∑ t ∈ map (Embedding.subtype fun x ↦ x ∈ s₂) fs, w' t = 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun x ↦ x ∈ s₂) fs).weightedVSub p) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun x ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun x ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun x ↦ x ∈ s₂) fs)).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p) w''
⊢ ∑ t ∈ fs', w'' t = ∑ t ∈ map (Embedding.subtype fun x ↦ x ∈ s₂) fs, w' t
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✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
⊢ s.points i ∈ s.closedInterior

Tactic:
rw [← Finset.univ.affineCombination_piSingle k s.points (Finset.mem_univ i),
    affineCombination_mem_closedInterior_iff (Fintype.sum_pi_single' _ _)]
  intro j
  obtain rfl | hj := eq_or_ne j i <;> simp_all

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

Goal state before:
pp: R : Type u_1
W : Type u_4
Q : Type u_5
inst✝⁸ : AddCommGroup W
inst✝⁷ : TopologicalSpace W
inst✝⁶ : AddTorsor W Q
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : IsTopologicalAddTorsor Q
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : Module R W
inst✝ : ContinuousSMul R W
x : Q
s : Set Q
y : Q
hy : y ∈ interior s
cont : Continuous[inst✝², inst✝⁵] fun δ ↦ (homothety x δ) y
⊢ ∀ᶠ (δ : R) in 𝓝 1, (homothety x δ) y ∈ s

Tactic:
filter_upwards [cont.tendsto' 1 y (by simp) |>.eventually (isOpen_interior.eventually_mem hy)]
    with _ h using interior_subset h

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k V
inst✝⁴ : AffineSpace V P
inst✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
h : ∃ i, w i ≤ 0 ∨ 1 ≤ w i
⊢ ∃ j, w j = 0

Tactic:
obtain ⟨i, hi | hi⟩ := h

Goal state after:
case inl
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✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
i : Fin (n + 1)
hi : w i ≤ 0
⊢ ∃ j, w j = 0

case inr
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✝³ : LinearOrder k
inst✝² : IsOrderedAddMonoid k
inst✝¹ : ZeroLEOneClass k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1
hp' : (affineCombination k univ s.points) w ∈ ↑(affineSpan k (Set.range s.points))
i : Fin (n + 1)
hi : 1 ≤ w i
⊢ ∃ j, w j = 0
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ 𝓝ˢ (nhdsKer s) = 𝓝ˢ s

Tactic:
refine le_antisymm ((hasBasis_nhdsSet _).ge_iff.2 ?_) (nhdsSet_mono subset_nhdsKer)

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ ∀ (i' : Set X), IsOpen[inst✝] i' ∧ s ⊆ i' → i' ∈ 𝓝ˢ (nhdsKer s)
Module: Mathlib.Analysis.Convex.Topology

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a b : 𝕜
has : a ∈ closure[inst✝¹] s
hbs : b ∈ closure[inst✝¹] s
⊢ Ioo a b ⊆ s

Tactic:
by
  cases subsingleton_or_nontrivial s with
  | inl hs_sub =>
    simp only [subsingleton_coe] at hs_sub
    simp [hs_sub.closure has hbs]
  | inr h' =>
    simp only [nontrivial_coe_sort] at h'
    calc Ioo a b
    _ = interior (Ioo a b) := interior_Ioo.symm
    _ ⊆ interior (openSegment 𝕜 a b) := interior_mono <| Ioo_subset_openSegment
    _ ⊆ interior (closure s) := interior_mono <| hs.closure.openSegment_subset has hbs
    _ = interior s := hs.interior_closure_eq_interior_of_nonempty_interior <|
      hs.nontrivial_iff_nonempty_interior.1 h'
    _ ⊆ s := interior_subset

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

Goal state before:
pp: case intro.inr
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
s : Set ι
t : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)
val✝ : Fintype ι
this :
  ∀ {s : Set ι} {t : (i : ι) → Set (E i)},
    (∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)) → s = Set.univ → x ∈ (convexHull 𝕜) (s.pi t)
hs : ¬s = Set.univ
⊢ x ∈ (convexHull 𝕜) (s.pi t)

Tactic:
← pi_univ_ite

Goal state after:
case intro.inr
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
s : Set ι
t : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)
val✝ : Fintype ι
this :
  ∀ {s : Set ι} {t : (i : ι) → Set (E i)},
    (∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)) → s = Set.univ → x ∈ (convexHull 𝕜) (s.pi t)
hs : ¬s = Set.univ
⊢ x ∈ (convexHull 𝕜) (Set.univ.pi fun i ↦ if i ∈ s then t i else Set.univ)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 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 ι
U : Set E
hU : U ∈ p.basisSets
⊢ ∃ V ∈ p.basisSets, V + V ⊆ U

Tactic:
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩

Goal state after:
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 ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ p.basisSets, V + V ⊆ U
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 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 ι
U : Set E
hU' : U ∈ p.basisSets
⊢ ∃ V ∈ p.basisSets, V ⊆ (fun x ↦ -x) ⁻¹' U

Tactic:
by
  rcases p.basisSets_iff.mp hU' with ⟨s, r, _, hU⟩
  rw [hU, neg_preimage, neg_ball (s.sup p), neg_zero]
  exact ⟨U, hU', Eq.subset hU⟩

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

Goal state before:
pp: 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
⊢ ∀ᶠ (x : R) in 𝓝 0, x • v ∈ U

Tactic:
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩

Goal state after:
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
⊢ ∀ᶠ (x : R) in 𝓝 0, x • v ∈ U
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 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 ι
U : Set E
hU : U ∈ p.basisSets
⊢ ∃ V ∈ 𝓝 0, ∃ W ∈ p.addGroupFilterBasis.sets, V • W ⊆ U

Tactic:
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩

Goal state after:
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 ι
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ V ∈ 𝓝 0, ∃ W ∈ p.addGroupFilterBasis.sets, V • W ⊆ U
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : 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
⊢ ∃ V ∈ p.addGroupFilterBasis.sets, V ⊆ (fun y ↦ x • y) ⁻¹' U

Tactic:
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩

Goal state after:
𝕜 : 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
⊢ ∃ V ∈ p.addGroupFilterBasis.sets, V ⊆ (fun y ↦ x • y) ⁻¹' U
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case mpr
𝕜 : 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 : ι'
⊢ ∃ s C, (q i).comp f ≤ C • s.sup fun x ↦ p

Tactic:
use {Classical.arbitrary ι}

Goal state after:
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
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
h : ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0
this : IsTopologicalAddGroup E
x : E
hx : x ≠ 0
i : ι
pi_nonzero : (p i) x ≠ 0
⊢ 0 ∉ ({i}.sup p).ball x ((p i) x)

Tactic:
Finset.sup_singleton,

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
h : ∀ (x : E), x ≠ 0 → ∃ i, (p i) x ≠ 0
this : IsTopologicalAddGroup E
x : E
hx : x ≠ 0
i : ι
pi_nonzero : (p i) x ≠ 0
⊢ 0 ∉ (p i).ball x ((p i) x)
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: 𝕜 : 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
⊢ IsVonNBounded 𝕜 s ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Tactic:
hp.hasBasis.isVonNBounded_iff

Goal state after:
𝕜 : 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 ∈ p.basisSets, Absorbs 𝕜 (id i) s) ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ 1 • {{i}}.sup fun s ↦ s.sup p

Tactic:
Finset.sup_singleton,

Goal state after:
case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ 1 • {i}.sup p
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ 1 • {i}.sup p

Tactic:
Finset.sup_singleton,

Goal state after:
case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ 1 • p i
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ 1 • {i}.sup fun i ↦ (Finset.Iic i).sup p

Tactic:
Finset.sup_singleton,

Goal state after:
case refine_2
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
hp : WithSeminorms p
i : ι
⊢ (p i).comp LinearMap.id ≤ 1 • (Finset.Iic i).sup p
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✝ : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
x : E
hx : 0 < ‖x‖
ha : 0 ≤ a
⊢ ‖f‖ = a

Tactic:
apply le_antisymm (f.opNorm_le_bound ha fun y => le_of_eq (hf y))

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✝ : NontrivialTopology E
f : E →SL[σ₁₂] F
a : ℝ
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
x : E
hx : 0 < ‖x‖
ha : 0 ≤ a
⊢ a ≤ ‖f‖
Module: Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
S : Type u_5
inst✝²² : NormedField 𝕜
inst✝²¹ : Semiring S
inst✝²⁰ : AddCommGroup E
inst✝¹⁹ : Module 𝕜 E
inst✝¹⁸ : TopologicalSpace E
inst✝¹⁷ : IsTopologicalAddGroup E
inst✝¹⁶ : ContinuousConstSMul 𝕜 E
inst✝¹⁵ : AddCommGroup F
inst✝¹⁴ : Module 𝕜 F
inst✝¹³ : TopologicalSpace F
inst✝¹² : IsTopologicalAddGroup F
inst✝¹¹ : ContinuousConstSMul 𝕜 F
inst✝¹⁰ : AddCommGroup G
inst✝⁹ : Module 𝕜 G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : IsTopologicalAddGroup G
inst✝⁶ : ContinuousConstSMul 𝕜 G
inst✝⁵ : Module S G
inst✝⁴ : SMulCommClass 𝕜 S G
inst✝³ : ContinuousConstSMul S G
inst✝² : Module S F
inst✝¹ : SMulCommClass 𝕜 S F
inst✝ : ContinuousConstSMul S F
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace] (↑(prodₗ S)).toFun

Tactic:
by
    change Continuous fun x => .id 𝕜 _ ∘L prodₗ S x
    simp_rw [← coprod_inl_inr]
    exact (((inl 𝕜 F G).postcomp E).coprod ((inr 𝕜 F G).postcomp E)).continuous

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
h :
  ∀ (s : Set X),
    (∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] (f : K → X),
        Continuous[_, inst✝] f → IsOpen (f ⁻¹' s)) →
      IsOpen[inst✝] s
A : Set X
hA : ∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ A)
K : Type u
x✝¹ : TopologicalSpace K
x✝ : CompactSpace K
f : K → X
hf : Continuous[x✝¹, inst✝] f
⊢ IsOpen[x✝¹] (f ⁻¹' A)

Tactic:
specialize hA (range f) (isCompact_range hf)

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
h :
  ∀ (s : Set X),
    (∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] (f : K → X),
        Continuous[_, inst✝] f → IsOpen (f ⁻¹' s)) →
      IsOpen[inst✝] s
A : Set X
K : Type u
x✝¹ : TopologicalSpace K
x✝ : CompactSpace K
f : K → X
hA : IsOpen[instTopologicalSpaceSubtype] (range f ↓∩ A)
hf : Continuous[x✝¹, inst✝] f
⊢ IsOpen[x✝¹] (f ⁻¹' A)
Module: Mathlib.Order.Filter.ENNReal

Goal state before:
pp: case pos
α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ∞
ha₀ : a = 0
⊢ liminf (fun x ↦ ⊥) f = ⊥

Tactic:
apply liminf_const

Goal state after: