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

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
e : E
r : ℝ
hr : 0 < r
⊢ (⨆ i, p i).closedBall e r = ⋂ i, (p i).closedBall e r

Tactic:
cases isEmpty_or_nonempty ι
  · rw [iSup_of_empty', iInter_of_empty, Seminorm.sSup_empty]
    exact closedBall_bot _ hr
  · ext x
    have := Seminorm.bddAbove_range_iff.mp hp (x - e)
    simp only [mem_closedBall, mem_iInter, Seminorm.iSup_apply hp, ciSup_le_iff this]

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
ι' : Type u_5
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent k (p ∘ ⇑e)
this : p = p ∘ ⇑e ∘ ⇑e.symm.toEmbedding
⊢ AffineIndependent k p

Tactic:
rw [this]

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
ι' : Type u_5
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent k (p ∘ ⇑e)
this : p = p ∘ ⇑e ∘ ⇑e.symm.toEmbedding
⊢ AffineIndependent k (p ∘ ⇑e ∘ ⇑e.symm.toEmbedding)
Module: Mathlib.Topology.Algebra.Monoid.FunOnFinite

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
X : Type u_2
Y : Type u_3
inst✝¹ : Finite X
inst✝ : Finite Y
f : X → Y
⊢ Continuous (map f)

Tactic:
have := Fintype.ofFinite X
  refine continuous_pi (fun y ↦ ?_)
  simp only [FunOnFinite.map_apply_apply]
  exact continuous_finsetSum _ (fun _ _ ↦ continuous_apply _)

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

Goal state before:
pp: case e_a.e_a
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
i : ι
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
ha : i ∉ t
hw : ∑ j ∈ t, w j ≠ 0
⊢ (w i + ∑ i ∈ t, w i)⁻¹ = (∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹ / (w i + ∑ i ∈ t, w i)

Tactic:
mul_inv_cancel₀ hw,

Goal state after:
case e_a.e_a
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝³ : Field R
inst✝² : AddCommGroup E
inst✝¹ : Module R E
i : ι
t : Finset ι
w : ι → R
z : ι → E
inst✝ : DecidableEq ι
ha : i ∉ t
hw : ∑ j ∈ t, w j ≠ 0
⊢ (w i + ∑ i ∈ t, w i)⁻¹ = 1 / (w i + ∑ i ∈ t, w i)
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹² : AddCommGroup V
inst✝¹¹ : TopologicalSpace V
inst✝¹⁰ : AddTorsor V P
inst✝⁹ : TopologicalSpace P
inst✝⁸ : IsTopologicalAddTorsor P
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : AddTorsor W Q
inst✝⁴ : TopologicalSpace Q
inst✝³ : IsTopologicalAddTorsor Q
inst✝² : Ring R
inst✝¹ : Module R V
inst✝ : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
this : ⇑f.linear = ⇑(Homeomorph.vaddConst (f default)).symm ∘ ⇑f ∘ ⇑(Homeomorph.vaddConst default)
⊢ Continuous ⇑f.linear ↔ Continuous ⇑f

Tactic:
rw [this]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹² : AddCommGroup V
inst✝¹¹ : TopologicalSpace V
inst✝¹⁰ : AddTorsor V P
inst✝⁹ : TopologicalSpace P
inst✝⁸ : IsTopologicalAddTorsor P
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : AddTorsor W Q
inst✝⁴ : TopologicalSpace Q
inst✝³ : IsTopologicalAddTorsor Q
inst✝² : Ring R
inst✝¹ : Module R V
inst✝ : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
this : ⇑f.linear = ⇑(Homeomorph.vaddConst (f default)).symm ∘ ⇑f ∘ ⇑(Homeomorph.vaddConst default)
⊢ Continuous (⇑(Homeomorph.vaddConst (f default)).symm ∘ ⇑f ∘ ⇑(Homeomorph.vaddConst default)) ↔ Continuous ⇑f
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' _ _)]

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✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
⊢ ∀ (i_1 : Fin (n + 1)), Pi.single i 1 i_1 ∈ Set.Icc 0 1
Module: Mathlib.Topology.Algebra.Affine

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹² : AddCommGroup V
inst✝¹¹ : TopologicalSpace V
inst✝¹⁰ : AddTorsor V P
inst✝⁹ : TopologicalSpace P
inst✝⁸ : IsTopologicalAddTorsor P
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : AddTorsor W Q
inst✝⁴ : TopologicalSpace Q
inst✝³ : IsTopologicalAddTorsor Q
inst✝² : Ring R
inst✝¹ : Module R V
inst✝ : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
this : ⇑f.linear = ⇑(Homeomorph.vaddConst (f default)).symm ∘ ⇑f ∘ ⇑(Homeomorph.vaddConst default)
⊢ IsOpenMap ⇑f.linear ↔ IsOpenMap ⇑f

Tactic:
rw [this]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹² : AddCommGroup V
inst✝¹¹ : TopologicalSpace V
inst✝¹⁰ : AddTorsor V P
inst✝⁹ : TopologicalSpace P
inst✝⁸ : IsTopologicalAddTorsor P
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : AddTorsor W Q
inst✝⁴ : TopologicalSpace Q
inst✝³ : IsTopologicalAddTorsor Q
inst✝² : Ring R
inst✝¹ : Module R V
inst✝ : Module R W
f : P →ᵃ[R] Q
inhabited_h : Inhabited P
this : ⇑f.linear = ⇑(Homeomorph.vaddConst (f default)).symm ∘ ⇑f ∘ ⇑(Homeomorph.vaddConst default)
⊢ IsOpenMap (⇑(Homeomorph.vaddConst (f default)).symm ∘ ⇑f ∘ ⇑(Homeomorph.vaddConst default)) ↔ IsOpenMap ⇑f
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: case pos
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
ws : ∀ j ∈ t, w j = 0
⊢ (insert i t).centerMass w z ∈ s

Tactic:
have wz : ∑ j ∈ t, w j • z j = 0 := sum_eq_zero fun i hi => by simp [ws i hi]

Goal state after:
case pos
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
ws : ∀ j ∈ t, w j = 0
wz : ∑ j ∈ t, w j • z j = 0
⊢ (insert i t).centerMass w z ∈ s
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
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
x✝ : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
⊢ ∑ i ∈ s, (w - w₁) i = 0

Tactic:
simp_all only [Pi.sub_apply, Finset.sum_sub_distrib, sub_self]

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

Goal state before:
pp: case inr.refine_2.hd
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
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = vectorSpan k s
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
this : Submodule.span k b = Submodule.span k (insert 0 b)
⊢ insert ((Equiv.vaddConst p).symm p) (⇑(Equiv.vaddConst p).symm '' ⇑(Equiv.vaddConst p) '' b) = insert 0 b

Tactic:
← Set.image_comp

Goal state after:
case inr.refine_2.hd
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
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = vectorSpan k s
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
this : Submodule.span k b = Submodule.span k (insert 0 b)
⊢ insert ((Equiv.vaddConst p).symm p) (⇑(Equiv.vaddConst p).symm ∘ ⇑(Equiv.vaddConst p) '' b) = insert 0 b
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : 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₂]

Goal state after:
R : Type u_1
E : Type u_3
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
t : Finset ι
p : ι → E
w : ι → R
hw₂ : ∑ i ∈ t, w i = 1
⊢ ∑ i ∈ t, w i • (p i -ᵥ 0) = ∑ i ∈ t, w i • p i
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 : ∑ i ∈ s, wm i = 0
⊢ wm i = -1

Tactic:
simp [wm, his.2]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : Tendsto y f (𝓝 x)
hz : Tendsto z f (𝓝 x)
hr✝ : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
p : α → Prop
hp : ∀ᶠ (i : α) in f, p i
δ : ℝ
hδ : δ > 0
hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2
⊢ ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v

Tactic:
Metric.tendsto_nhds

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (y x_1) x < ε
hz : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (z x_1) x < ε
hr✝ : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
p : α → Prop
hp : ∀ᶠ (i : α) in f, p i
δ : ℝ
hδ : δ > 0
hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2
⊢ ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v
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 : Set E
⊢ (convexHull R) ((fun x ↦ x.1 + x.2) '' s ×ˢ t) = (fun x ↦ x.1 + x.2) '' (convexHull R) s ×ˢ (convexHull R) t

Tactic:
← IsLinearMap.isLinearMap_add.image_convexHull,

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 : Set E
⊢ (fun x ↦ x.1 + x.2) '' (convexHull R) (s ×ˢ t) = (fun x ↦ x.1 + x.2) '' (convexHull R) s ×ˢ (convexHull R) t
Module: Mathlib.Analysis.Convex.Jensen

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

Tactic:
exact h_eq.not_gt <| hf.map_sum_lt h₀ h₁ hmem this

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), x ∈ (convexHull R) ↑t₁ ∧ x ∈ (convexHull R) ↑t₂ → x ∈ (convexHull R) ↑(t₁ ∩ t₂)

Tactic:
mem_convexHull'

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

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

Tactic:
by rw [H _ hi]

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_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
i : ι'
hi : i ∈ s'
⊢ (fₛ i).sup p ≤ (s'.biUnion fₛ).sup p

Tactic:
exact Finset.sup_mono (Finset.subset_biUnion_of_mem fₛ hi)

Goal state after:
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
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ t = ⨅ i, PseudoMetricSpace.toUniformSpace.toTopologicalSpace

Tactic:
p.withSeminorms_iff_nhds_eq_iInf,

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
t : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0) ↔ t = ⨅ i, PseudoMetricSpace.toUniformSpace.toTopologicalSpace
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
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
𝔖 : Set (Set E)
⊢ instTopologicalSpace σ F 𝔖 =
    TopologicalSpace.induced (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.topologicalSpace E F 𝔖)

Tactic:
rw [instTopologicalSpace]
  congr
  exact IsUniformAddGroup.rightUniformSpace_eq

Goal state after:
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
u : UniformSpace E
inst✝ : IsUniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ u = ⨅ i, PseudoMetricSpace.toUniformSpace

Tactic:
p.withSeminorms_iff_nhds_eq_iInf,

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
u : UniformSpace E
inst✝ : IsUniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0) ↔ u = ⨅ i, PseudoMetricSpace.toUniformSpace
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_3.refine_2.inr
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
t : Set E
ht : t ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).toFilterBasis
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = (w.sup fun x ↦ p).ball 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
⊢ t ∈ 𝓝 0

Tactic:
rw [this]

Goal state after:
case refine_3.refine_2.inr
𝕜 : Type u_2
E : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : p.ball 0 1 ∈ 𝓝 0
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : s ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).filter
t : Set E
ht : t ∈ (SeminormFamily.moduleFilterBasis fun x ↦ p).toFilterBasis
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = (w.sup fun x ↦ p).ball 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
⊢ p.ball 0 r ∈ 𝓝 0
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
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
𝔖₁ 𝔖₂ : Set (Set E)
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
⊢ instTopologicalSpace σ F 𝔖₁ ≤ instTopologicalSpace σ F 𝔖₂

Tactic:
let := IsTopologicalAddGroup.rightUniformSpace F
  have : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  simp_rw [← uniformity_toTopologicalSpace_eq]
  exact UniformSpace.toTopologicalSpace_mono (uniformSpace_mono σ F h)

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
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‖
⊢ ‖f‖ = a

Tactic:
by
  obtain ⟨x, hx⟩ := exists_norm_ne_zero E
  replace hx : 0 < ‖x‖ := lt_of_le_of_ne' (norm_nonneg _) hx
  have ha : 0 ≤ a := by simpa only [hf, hx, mul_nonneg_iff_of_pos_right] using norm_nonneg (f x)
  apply le_antisymm (f.opNorm_le_bound ha fun y => le_of_eq (hf y))
  simpa only [hf, hx, mul_le_mul_iff_left₀] using f.le_opNorm x

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 ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
⊢ WithSeminorms (p ∘ ⇑e)

Tactic:
refine hp.congr ?_ ?_ <;>
  intro i <;>
  [use {e i}, 1; use {e.symm i}, 1] <;>
  simp

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) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ ⇑φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ ⇑φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover' : ∀ S ∈ 𝔖, S ⊆ range ⇑φ₁ ∪ range ⇑φ₂
⊢ inferInstance =
    UniformSpace.comap (fun x ↦ x.comp φ₁) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp φ₂) inferInstance

Tactic:
replaceTopology_eq,

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) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ ⇑φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover' : ∀ S ∈ 𝔖, S ⊆ range ⇑φ₁ ∪ range ⇑φ₂
⊢ inferInstance =
    UniformSpace.comap (fun x ↦ x.comp φ₁) inferInstance ⊓ UniformSpace.comap (fun x ↦ x.comp φ₂) inferInstance
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i ↦ range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i ↦ {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
h_cover' : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range ⇑(φ i)
⊢ inferInstance = ⨅ i, UniformSpace.comap (fun x ↦ x.comp (φ i)) inferInstance

Tactic:
replaceTopology_eq,

Goal state after:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i ↦ range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i ↦ {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x ↦ ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
h_cover' : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range ⇑(φ i)
⊢ inferInstance = ⨅ i, UniformSpace.comap (fun x ↦ x.comp (φ i)) inferInstance
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
r : C(α, R)
x : α
⊢ (r • 0) x = 0 x

Tactic:
exact smul_zero _

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

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : TopologicalSpace R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : ContinuousSMul R M
inst✝¹ : IsTopologicalSemiring R
inst✝ : ContinuousAdd M
r : C(α, R)
⊢ r • 0 = 0

Tactic:
by ext x; exact smul_zero _

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case pos
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ω ∈ t
⊢ Measure.count ({ω} ∩ t) = 1

pp: case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ω ∉ t
⊢ Measure.count ({ω} ∩ t) = 0

Tactic:
· rw [(by simpa : ({ω} : Set Ω) ∩ t = {ω}), Measure.count_singleton]

Goal state after:
case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst✝ : Decidable (ω ∈ t)
h✝ : ω ∉ t
⊢ Measure.count ({ω} ∩ t) = 0