mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ False

Tactic:
let w' : ι → k := Function.extend Subtype.val w 0

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
⊢ False
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
t : Finset V
h : ¬AffineIndependent k Subtype.val
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Tactic:
classical
    rw [affineIndependent_iff_of_fintype] at h
    simp only [exists_prop, not_forall] at h
    obtain ⟨w, hw, hwt, i, hi⟩ := h
    simp only [Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ w ((↑) : t → V) hw 0,
      vsub_eq_sub, Finset.weightedVSubOfPoint_apply, sub_zero] at hwt
    let f : ∀ x : V, x ∈ t → k := fun x hx => w ⟨x, hx⟩
    refine ⟨fun x => if hx : x ∈ t then f x hx else (0 : k), ?_, ?_, by use i; simp [f, hi]⟩
    on_goal 1 =>
      suffices (∑ e ∈ t, dite (e ∈ t) (fun hx => f e hx • e) fun _ => 0) = 0 by
        convert! this
        rename V => x
        by_cases hx : x ∈ t <;> simp [hx]
    all_goals
      simp only [f, Finset.sum_dite_of_true fun _ h => h, Finset.mk_coe, hwt, hw]

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

Goal state before:
pp: case insert
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
⊢ (∀ i_1 ∈ insert i t, 0 ≤ w i_1) →
    0 < ∑ i ∈ insert i t, w i → (∀ i_1 ∈ insert i t, z i_1 ∈ s) → (insert i t).centerMass w z ∈ s

Tactic:
intro h₀ hpos hmem
    have zi : z i ∈ s := hmem _ (mem_insert_self _ _)
    have hs₀ : ∀ j ∈ t, 0 ≤ w j := fun j hj => h₀ j <| mem_insert_of_mem hj
    rw [sum_insert hi] at hpos
    by_cases hsum_t : ∑ j ∈ t, w j = 0
    · have ws : ∀ j ∈ t, w j = 0 := (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t
      have wz : ∑ j ∈ t, w j • z j = 0 := sum_eq_zero fun i hi => by simp [ws i hi]
      simp only [centerMass, sum_insert hi, wz, hsum_t, add_zero]
      simp only [hsum_t, add_zero] at hpos
      rw [← mul_smul, inv_mul_cancel₀ (ne_of_gt hpos), one_smul]
      exact zi
    · rw [Finset.centerMass_insert _ _ _ hi hsum_t]
      refine convex_iff_div.1 hs zi (ht hs₀ ?_ ?_) ?_ (sum_nonneg hs₀) hpos
      · exact lt_of_le_of_ne (sum_nonneg hs₀) (Ne.symm hsum_t)
      · intro j hj
        exact hmem j (mem_insert_of_mem hj)
      · exact h₀ _ (mem_insert_self _ _)

Goal state after:
Module: Mathlib.Topology.NhdsKer

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
x y : X
⊢ x ∈ {y_1 | y_1 ⤳ y} ↔ x ⤳ y

Tactic:
mem_ofPred

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
x y : X
⊢ x ⤳ y ↔ x ⤳ y
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : AlexandrovDiscrete α
inst✝ : AlexandrovDiscrete β
s t : Set α
a : α
⊢ AlexandrovDiscrete (α × β)

Tactic:
alexandrovDiscrete_iff_nhds,

Goal state after:
ι : Sort u_1
κ : ι → Sort u_2
α : Type u_3
β : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : AlexandrovDiscrete α
inst✝ : AlexandrovDiscrete β
s t : Set α
a : α
⊢ ∀ (a : α × β), 𝓝 a = 𝓟 (nhdsKer {a})
Module: Mathlib.Topology.AlexandrovDiscrete

Goal state before:
pp: ι✝ : Sort u_1
κ : ι✝ → Sort u_2
α : Type u_3
β : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AlexandrovDiscrete α
inst✝³ : AlexandrovDiscrete β
s t : Set α
a : α
ι : Type u_5
inst✝² : Finite ι
X : ι → Type u_6
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), AlexandrovDiscrete (X i)
⊢ AlexandrovDiscrete ((i : ι) → X i)

Tactic:
alexandrovDiscrete_iff_nhds,

Goal state after:
ι✝ : Sort u_1
κ : ι✝ → Sort u_2
α : Type u_3
β : Type u_4
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AlexandrovDiscrete α
inst✝³ : AlexandrovDiscrete β
s t : Set α
a : α
ι : Type u_5
inst✝² : Finite ι
X : ι → Type u_6
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), AlexandrovDiscrete (X i)
⊢ ∀ (a : (i : ι) → X i), 𝓝 a = 𝓟 (nhdsKer {a})
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case inr.refine_1
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✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr '' pathComponentIn (inr ⁻¹' u) y ⊆ pathComponentIn u (inr y)

pp: case inr.refine_2
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✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ IsOpen[instTopologicalSpaceSum] (inr '' pathComponentIn (inr ⁻¹' u) y)

pp: case inr.refine_3
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✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr y ∈ inr '' pathComponentIn (inr ⁻¹' u) y

Tactic:
· apply IsPathConnected.subset_pathComponentIn
      · exact (isPathConnected_pathComponentIn (by exact hxu)).image continuous_inr
      · exact ⟨y, mem_pathComponentIn_self hxu, rfl⟩
      · exact (image_mono pathComponentIn_subset).trans (u.image_preimage_subset _)

Goal state after:
case inr.refine_2
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✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ IsOpen[instTopologicalSpaceSum] (inr '' pathComponentIn (inr ⁻¹' u) y)

case inr.refine_3
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✝ : LocallyPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr y ∈ inr '' pathComponentIn (inr ⁻¹' u) y
Module: Mathlib.Topology.Algebra.Module.LocallyConvex

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E

Tactic:
rw [inf_eq_iInf]

Goal state after:
𝕜 : Type u_2
E : Type u_3
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: case neg
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 : (r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹) • x ∈ U
⊢ x ∈ U

Tactic:
← smul_assoc,

Goal state after:
case neg
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 : ((r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹)) • x ∈ U
⊢ x ∈ U
Module: Mathlib.Analysis.Normed.Module.Convex

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : x = 0
⊢ IsConnected {y | SameRay ℝ x y}

pp: case neg
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ¬x = 0
⊢ IsConnected {y | SameRay ℝ x y}

Tactic:
· simpa [hx] using isConnected_univ (α := E)

Goal state after:
case neg
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ¬x = 0
⊢ IsConnected {y | SameRay ℝ x y}
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 → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ w j • p j + (w k • p k + ∑ x ∈ u, w x • p x) = c • ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • p x

Tactic:
match_scalars <;> simp [field, c]

Goal state after:
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 → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ c • ((w j / c) • f (p j) + (w k / c) • f (p k)) + ∑ x ∈ u, w x • f (p x) =
    w j • f (p j) + w k • f (p k) + ∑ x ∈ u, w x • f (p x)

Tactic:
match_scalars <;> simp [field, c]

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:
← coe_inter,

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), x ∈ (convexHull R) ↑t₁ ∧ x ∈ (convexHull R) ↑t₂ → x ∈ (convexHull R) ↑(t₁ ∩ t₂)
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
R : Type u_6
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Module R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (E →SLᵤ[σ, 𝔖] F)
h : ∀ s ∈ 𝔖, IsVonNBounded R (image2 (fun f x ↦ f x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
c : R
hc : image2 (fun f x ↦ f x) S s ⊆ c • U
hc₀ : c ≠ 0
⊢ S ⊆ c • {f | MapsTo (⇑f) s U}

Tactic:
f

Goal state after:
𝕜₁ : 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
R : Type u_6
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Module R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (E →SLᵤ[σ, 𝔖] F)
h : ∀ s ∈ 𝔖, IsVonNBounded R (image2 (fun f x ↦ f x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
c : R
hc : image2 (fun f x ↦ f x) S s ⊆ c • U
hc₀ : c ≠ 0
f : E →SLᵤ[σ, 𝔖] F
⊢ f ∈ S → f ∈ c • {f | MapsTo (⇑f) s U}
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
⊢ Tendsto (⇑B) (𝓝 0) (𝓝 0)

Tactic:
suffices ∀ s ∈ 𝔖, ∀ U ∈ 𝓝 0, ∀ᶠ (g : G) in 𝓝 0, ∀ e ∈ s, B g e ∈ U by
    simpa [UniformConvergenceCLM.nhds_zero_eq, MapsTo]

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 ∈ 𝔖, ∀ U ∈ 𝓝 0, ∀ᶠ (g : G) in 𝓝 0, ∀ e ∈ s, (B g) e ∈ U
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c : M
f✝ g✝ : l.Germ N
f g : α → N
⊢ c • (↑f + ↑g) = c • ↑f + c • ↑g

Tactic:
norm_cast
      simp [smul_add]

Goal state after:
Module: Mathlib.Order.Filter.Germ.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f✝¹ g✝¹ h : α → β
M : Type u_5
N : Type u_6
R : Type u_7
inst✝² : Monoid M
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction M N
c✝ : l.Germ M
f✝ g✝ : l.Germ N
c : α → M
f g : α → N
⊢ ↑c • (↑f + ↑g) = ↑c • ↑f + ↑c • ↑g

Tactic:
norm_cast
      simp [smul_add]

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ts : Set (TopologicalSpace E)
hts : ∀ t ∈ ts, PolynormableSpace 𝕜 E
⊢ PolynormableSpace 𝕜 E

Tactic:
rw [sInf_eq_iInf']

Goal state after:
𝕜 : Type u_2
E : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ts : Set (TopologicalSpace E)
hts : ∀ t ∈ ts, PolynormableSpace 𝕜 E
⊢ PolynormableSpace 𝕜 E
Module: Mathlib.Topology.Compactness.CompactlyCoherentSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
f : X → Y
⊢ Continuous[inst✝², instTopologicalSpace] (⇑(CompactCoherentification.mk Y) ∘ f) ↔ Continuous[inst✝², inst✝¹] f

Tactic:
rw [continuous_rng_of_compactSpace, ← Function.comp_assoc, Equiv.symm_comp_self, Function.id_comp]

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ ≪ μ[|univ]

Tactic:
rw [cond, restrict_univ]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ ≪ (μ univ)⁻¹ • μ
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
inst✝ : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
f' : α → β
hf' : Measurable f'
h : f =ᵐ[μ] f'
⊢ g.compQuasiMeasurePreserving f hf = g.compQuasiMeasurePreserving f' ⋯

Tactic:
ext
  grw [coeFn_compQuasiMeasurePreserving, coeFn_compQuasiMeasurePreserving, h]

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_2
inst✝ : DecidableEq Ω
x✝ : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet ↑s
ht : MeasurableSet ↑t
⊢ (↑(#s))⁻¹ * Measure.count (↑s ∩ ↑t) = ↑(#(s ∩ t)) / ↑(#s)

Tactic:
← coe_inter,

Goal state after:
Ω : Type u_2
inst✝ : DecidableEq Ω
x✝ : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet ↑s
ht : MeasurableSet ↑t
⊢ (↑(#s))⁻¹ * Measure.count ↑(s ∩ t) = ↑(#(s ∩ t)) / ↑(#s)
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹⁴ : MeasurableSpace α
μ : Measure α
inst✝¹³ : TopologicalSpace δ
inst✝¹² : TopologicalSpace β
inst✝¹¹ : TopologicalSpace γ
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : PseudoMetrizableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : MeasurableSpace γ
inst✝⁶ : PseudoMetrizableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : SecondCountableTopologyEither β γ
inst✝³ : MeasurableSpace δ
inst✝² : PseudoMetrizableSpace δ
inst✝¹ : OpensMeasurableSpace δ
inst✝ : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ ↑(comp₂Measurable g hg f₁ f₂) =ᵐ[μ] fun a ↦ g (↑f₁ a) (↑f₂ a)

Tactic:
rw [comp₂Measurable_eq_mk]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹⁴ : MeasurableSpace α
μ : Measure α
inst✝¹³ : TopologicalSpace δ
inst✝¹² : TopologicalSpace β
inst✝¹¹ : TopologicalSpace γ
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : PseudoMetrizableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : MeasurableSpace γ
inst✝⁶ : PseudoMetrizableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : SecondCountableTopologyEither β γ
inst✝³ : MeasurableSpace δ
inst✝² : PseudoMetrizableSpace δ
inst✝¹ : OpensMeasurableSpace δ
inst✝ : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ ↑(mk (fun a ↦ g (↑f₁ a) (↑f₂ a)) ⋯) =ᵐ[μ] fun a ↦ g (↑f₁ a) (↑f₂ a)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case cons
δ : Type u_4
X : δ → Type u_5
inst✝¹ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (X i)
a : δ
l : List δ
ih : (Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i ↦ (μ i) (s i)) l).prod
⊢ (μ a) (s a) * (Measure.tprod l μ) (Set.tprod l s) = (μ a) (s a) * (List.map (fun i ↦ (μ i) (s i)) l).prod

Tactic:
ih

Goal state after:
case cons
δ : Type u_4
X : δ → Type u_5
inst✝¹ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
s : (i : δ) → Set (X i)
a : δ
l : List δ
ih : (Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i ↦ (μ i) (s i)) l).prod
⊢ (μ a) (s a) * (List.map (fun i ↦ (μ i) (s i)) l).prod = (μ a) (s a) * (List.map (fun i ↦ (μ i) (s i)) l).prod
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: case insert
α : Type u_1
γ : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace γ
inst✝¹ : CommMonoid γ
inst✝ : ContinuousMul γ
ι : Type u_5
f : ι → α →ₘ[μ] γ
a : ι
s : Finset ι
ha : a ∉ s
ih : ↑(∏ i ∈ s, f i) =ᵐ[μ] ∏ i ∈ s, ↑(f i)
⊢ ↑(f a) * ↑(∏ i ∈ s, f i) =ᵐ[μ] ↑(f a) * ∏ i ∈ s, ↑(f i)

Tactic:
ih

Goal state after:
case insert
α : Type u_1
γ : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace γ
inst✝¹ : CommMonoid γ
inst✝ : ContinuousMul γ
ι : Type u_5
f : ι → α →ₘ[μ] γ
a : ι
s : Finset ι
ha : a ∉ s
ih : ↑(∏ i ∈ s, f i) =ᵐ[μ] ∏ i ∈ s, ↑(f i)
⊢ ↑(f a) * ∏ i ∈ s, ↑(f i) =ᵐ[μ] ↑(f a) * ∏ i ∈ s, ↑(f i)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
s : (i : ι) → Set (α i)
⊢ (Measure.pi μ) (univ.pi s) = ∏ i, (μ i) (s i)

Tactic:
by
  have : Encodable ι := Fintype.toEncodable ι
  rw [← pi'_eq_pi, pi'_pi]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov

Goal state before:
pp: case neg
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → μ {x | ‖f x‖ₑ = ∞} = 0
h : ¬ε = ∞
⊢ μ {x | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

Tactic:
have hεpow : ε ^ p.toReal ≠ 0 := (ENNReal.rpow_pos (pos_iff_ne_zero.2 hε) h).ne.symm

Goal state after:
case neg
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → μ {x | ‖f x‖ₑ = ∞} = 0
h : ¬ε = ∞
hεpow : ε ^ p.toReal ≠ 0
⊢ μ {x | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal
Module: Mathlib.MeasureTheory.Function.LpSeminorm.SMul

Goal state before:
pp: case inr
α : Type u_1
F : Type u_2
m : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
hc : c ≠ 0
⊢ eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ

Tactic:
refine le_antisymm (eLpNorm'_const_smul_le hq_pos) <| ENNReal.mul_le_of_le_div' ?_

Goal state after:
case inr
α : Type u_1
F : Type u_2
m : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
f : α → F
c : 𝕜
hq_pos : 0 < q
hc : c ≠ 0
⊢ eLpNorm' f q μ ≤ eLpNorm' (c • f) q μ / ‖c‖ₑ