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

Goal state before:
pp: 𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : AddCommGroup E
inst✝⁸ : NormedField 𝕝
inst✝⁷ : Module 𝕝 E
inst✝⁶ : AddCommGroup F
inst✝⁵ : NormedField 𝕝₂
inst✝⁴ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝³ : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst✝², _] ⇑((q i).comp f)
this : IsTopologicalAddGroup F
i : ι'
⊢ Tendsto (⇑(q i) ∘ ⇑f) (𝓝 0) (𝓝 0)

Tactic:
convert! (hf i).continuousAt.tendsto

Goal state after:
case e'_5
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst✝⁹ : AddCommGroup E
inst✝⁸ : NormedField 𝕝
inst✝⁷ : Module 𝕝 E
inst✝⁶ : AddCommGroup F
inst✝⁵ : NormedField 𝕝₂
inst✝⁴ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝³ : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst✝², _] ⇑((q i).comp f)
this : IsTopologicalAddGroup F
i : ι'
⊢ 0 = ((q i).comp f) 0
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 : Set E
hS : S ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
⊢ (B 0.1) 0.2 = 0

Tactic:
simp

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

Goal state before:
pp: case refine_1
𝕜 : 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 σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
f : E →SL[σ₁₂] F
⊢ (∀ (x : E), ‖x‖ ≤ 1 → ‖f x‖ ≤ 1) → ‖f‖ ≤ ‖c‖

Tactic:
hf

Goal state after:
case refine_1
𝕜 : 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 σ₁₂
A : ∀ (f : (E →SL[σ₁₂] F) × (E →SL[σ₁₂] F)), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
c : 𝕜
hc : 1 < ‖c‖
f : E →SL[σ₁₂] F
hf : ∀ (x : E), ‖x‖ ≤ 1 → ‖f x‖ ≤ 1
⊢ ‖f‖ ≤ ‖c‖
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case h
𝕜 : 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 : ι' ≃ ι
i : ι'
⊢ ((p ∘ ⇑e) i).comp LinearMap.id ≤ 1 • {e i}.sup p

Tactic:
simp

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

Goal state before:
pp: case h
𝕜 : 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 : ι' ≃ ι
i : ι
⊢ (p i).comp LinearMap.id ≤ 1 • {e.symm i}.sup (p ∘ ⇑e)

Tactic:
simp

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
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →ₛₗᵢ[σ₁₂] F
x : E
⊢ ‖f.toContinuousLinearMap x‖ ≤ 1 * ‖x‖

Tactic:
simp

Goal state after:
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
H : Type u_5
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : AddCommGroup F
inst✝¹⁴ : AddCommGroup G
inst✝¹³ : AddCommGroup H
inst✝¹² : NormedField 𝕜
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : Module 𝕜 H
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalAddGroup G
inst✝² : IsTopologicalAddGroup H
inst✝¹ : ContinuousConstSMul 𝕜 G
inst✝ : ContinuousConstSMul 𝕜 H
e : G ≃L[𝕜] H
x✝² x✝¹ : G →L[𝕜] G
x✝ : H
⊢ ((↑↑(e.arrowCongr e)).toFun (x✝² * x✝¹)) x✝ = ((↑↑(e.arrowCongr e)).toFun x✝² * (↑↑(e.arrowCongr e)).toFun x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: case inl
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
hM : ∀ (x : E), ‖f x‖ₑ ≤ ∞ * ‖x‖ₑ
⊢ ‖f‖ₑ ≤ ∞

Tactic:
simp

Goal state after:
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
H : Type u_5
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : AddCommGroup F
inst✝¹⁴ : AddCommGroup G
inst✝¹³ : AddCommGroup H
inst✝¹² : NormedField 𝕜
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : Module 𝕜 F
inst✝⁹ : Module 𝕜 G
inst✝⁸ : Module 𝕜 H
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalAddGroup G
inst✝² : IsTopologicalAddGroup H
inst✝¹ : ContinuousConstSMul 𝕜 G
inst✝ : ContinuousConstSMul 𝕜 H
e : G ≃L[𝕜] H
x✝¹ : 𝕜
x✝ : H
⊢ ((↑↑(e.arrowCongr e)).toFun ((algebraMap 𝕜 (G →L[𝕜] G)) x✝¹)) x✝ = ((algebraMap 𝕜 (H →L[𝕜] H)) x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * (‖y‖₊ * ‖f y‖₊⁻¹) < 1
hy' : ‖y‖₊ ≠ 0
hfy : ‖f y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊

Tactic:
mul_comm ‖y‖₊,

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * (‖f y‖₊⁻¹ * ‖y‖₊) < 1
hy' : ‖y‖₊ ≠ 0
hfy : ‖f y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖f x‖₊
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
G : Type u_6
inst✝ : AddMonoidWithOne M
⊢ ↑0 = fun x ↦ 0

Tactic:
simp

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst✝ : AddMonoidWithOne M
⊢ 0 = fun x ↦ 0
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
G : Type u_6
inst✝ : AddMonoidWithOne M
x✝ : ℕ
⊢ ↑(x✝ + 1) = (fun f g x ↦ (fun x1 x2 ↦ x1 + x2) (f x) (g x)) ↑x✝ fun x ↦ 1

Tactic:
simp

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l : Filter α
f g h : α → β
M : Type u_5
G : Type u_6
inst✝ : AddMonoidWithOne M
x✝ : ℕ
⊢ ↑x✝ + 1 = fun x ↦ ↑x✝ + 1
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
G : Type u_6
inst✝ : AddGroupWithOne G
x✝ : ℕ
⊢ ↑↑x✝ = ↑x✝

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : FunLike 𝓕 E F
inst✝ : RingHomIsometric σ₂₃
f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G
h : ∃ C, ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖
x y : E
z : F
⊢ ((f (x + y)).mkContinuousOfExistsBound ⋯) z =
    ((f x).mkContinuousOfExistsBound ⋯ + (f y).mkContinuousOfExistsBound ⋯) z

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
Eₗ : Type u_5
F : Type u_6
Fₗ : Type u_7
G : Type u_8
Gₗ : Type u_9
𝓕 : Type u_10
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : FunLike 𝓕 E F
inst✝ : RingHomIsometric σ₂₃
f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G
h : ∃ C, ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖
c : 𝕜
x : E
z : F
⊢ ((f (c • x)).mkContinuousOfExistsBound ⋯) z = (σ₁₃ c • (f x).mkContinuousOfExistsBound ⋯) z

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: case mpr
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen[inst✝.toTopologicalSpace] U
⊢ MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U

Tactic:
hf

Goal state after:
case mpr
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (F i) a) (⇑f) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen[inst✝.toTopologicalSpace] U
hf : MapsTo (⇑f) K U
⊢ ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
Module: Mathlib.Analysis.Normed.Operator.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁹ : SeminormedAddCommGroup E
inst✝¹⁸ : SeminormedAddCommGroup F
inst✝¹⁷ : SeminormedAddCommGroup G
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜₂ F
inst✝¹¹ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst✝¹⁰ : SeminormedAddCommGroup E'
inst✝⁹ : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst✝⁸ : NontriviallyNormedField 𝕜₁'
inst✝⁷ : NontriviallyNormedField 𝕜₂'
inst✝⁶ : NormedSpace 𝕜₁' E'
inst✝⁵ : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁴ : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst✝³ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝² : RingHomIsometric σ₂₃
inst✝¹ : RingHomIsometric σ₁₃'
inst✝ : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gF : F' →SL[σ₂'] F
x✝¹ : E'
x✝ : F'
⊢ ((f.bilinearComp 0 gF) x✝¹) x✝ = (0 x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
inst✝¹⁹ : SeminormedAddCommGroup E
inst✝¹⁸ : SeminormedAddCommGroup F
inst✝¹⁷ : SeminormedAddCommGroup G
inst✝¹⁶ : NontriviallyNormedField 𝕜
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
inst✝¹⁴ : NontriviallyNormedField 𝕜₃
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedSpace 𝕜₂ F
inst✝¹¹ : NormedSpace 𝕜₃ G
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
E' : Type u_11
F' : Type u_12
inst✝¹⁰ : SeminormedAddCommGroup E'
inst✝⁹ : SeminormedAddCommGroup F'
𝕜₁' : Type u_13
𝕜₂' : Type u_14
inst✝⁸ : NontriviallyNormedField 𝕜₁'
inst✝⁷ : NontriviallyNormedField 𝕜₂'
inst✝⁶ : NormedSpace 𝕜₁' E'
inst✝⁵ : NormedSpace 𝕜₂' F'
σ₁' : 𝕜₁' →+* 𝕜
σ₁₃' : 𝕜₁' →+* 𝕜₃
σ₂' : 𝕜₂' →+* 𝕜₂
σ₂₃' : 𝕜₂' →+* 𝕜₃
inst✝⁴ : RingHomCompTriple σ₁' σ₁₃ σ₁₃'
inst✝³ : RingHomCompTriple σ₂' σ₂₃ σ₂₃'
inst✝² : RingHomIsometric σ₂₃
inst✝¹ : RingHomIsometric σ₁₃'
inst✝ : RingHomIsometric σ₂₃'
f : E →SL[σ₁₃] F →SL[σ₂₃] G
gE : E' →SL[σ₁'] E
x✝¹ : E'
x✝ : F'
⊢ ((f.bilinearComp gE 0) x✝¹) x✝ = (0 x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, ↑(u a) ≤ b
⊢ 0 ≤ ↑b.toNNReal

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ᶠ (a : ι) in f, ↑(u a) ≥ b
⊢ 0 ≤ ↑b.toNNReal

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
inst✝ : f.NeBot
b : ℝ
hb : ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, ↑(u a_1) ≤ a) → b ≤ a
⊢ 0 ≤ ↑b.toNNReal

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
b : ℝ
hb : ∀ (a : ℝ), (∀ᶠ (a_1 : ι) in f, ↑(u a_1) ≥ a) → b ≥ a
⊢ ∀ᶠ (a : ι) in f, ↑(u a) ≥ 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
c : ℝ
⊢ ∀ᶠ (x : ℝ) in map (fun i ↦ ↑(u i)) f, (fun x1 x2 ↦ x1 ≥ x2) x 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
c r : ℝ
hr✝ : r < c
hr : r < 0
i : ι
⊢ 0 ≤ ↑(u i)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
f : Filter ι
u : ι → ℝ≥0
hf✝ : f.NeBot
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
c r : ℝ
hr✝ : r < c
hr : r < 0
i : ι
⊢ 0 ≤ ↑(u i)

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ∞
hu : u =ᶠ[f] 0
hau : (fun x ↦ a * u x) =ᶠ[f] 0
⊢ ⊥ = a * ⊥

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
ι : Type u_3
s : Finset ι
f : ι → C(α, β)
a : α
⊢ (∏ i ∈ s, f i) a = ∏ i ∈ s, (f i) a

Tactic:
simp

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

Goal state before:
pp: case mp.none
α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > ↑r, ∀ᶠ (a : α) in f, u a < y
hx : none > ↑r
⊢ ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < none

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
x✝ : Ω
⊢ x✝ ∈ ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E ↔ x✝ ∈ E

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
f : Filter α
u : α → ℝ
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
r : ℝ≥0
h : ∀ y > ↑r, ∀ᶠ (a : α) in f, ENNReal.ofReal (u a) < y
x : ℝ
hx : x > ↑r
⊢ 0 ≤ ↑r

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : f.NeBot
u : α → ℝ≥0∞
C : ℝ≥0
hf : ∀ᶠ (a : α) in f, u a ≤ ↑C
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
x : α
hx : u x ≤ ↑C
⊢ ↑C ≠ ∞

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: case zero
α : Type u_1
γ : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace γ
g : α →ₘ[μ] γ
f : α → α
hf : QuasiMeasurePreserving f μ μ
⊢ (fun x ↦ x.compQuasiMeasurePreserving f hf)^[0] g = g.compQuasiMeasurePreserving f^[0] ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Pi

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝ : Finite ι
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), ⋃ n, t i n = univ
x✝ : (i : ι) → α i
i' : ι
s : Set (α i')
hs : s ∈ C i'
⊢ x✝ i' ∈ update (fun i' ↦ iUnion (t i')) i' (⋃ x, s) i' ↔ x✝ i' ∈ ⋃ j, update (fun i' ↦ t i' j) i' s i'

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
s : Set Ω
⊢ (uniformOn s) ∅ = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
f : Filter α
u : α → ℝ≥0∞
h₁ : ∀ᶠ (a : α) in f, u a ≠ ∞
hf : f.NeBot
this : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ (u a).toReal
r : ℝ
hr : 0 ≤ r
x : ℝ
hx : ∀ᶠ (a : α) in f, (fun x1 x2 ↦ x1 ≤ x2) (u a).toReal x
hx₀ : 0 ≤ x
⊢ ¬ENNReal.ofReal x = ∞

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
hg : Continuous[inst✝¹, inst✝] g
f✝ : α →ₘ[μ] β
f : α → β
x✝ : AEStronglyMeasurable f μ
⊢ (comp g hg (mk f x✝)).toGerm = Germ.map g (mk f x✝).toGerm

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁹ : MeasurableSpace α
μ : Measure α
inst✝⁸ : TopologicalSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace β
inst✝⁵ : BorelSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : PseudoMetrizableSpace γ
inst✝² : SecondCountableTopology γ
inst✝¹ : MeasurableSpace γ
inst✝ : OpensMeasurableSpace γ
g : β → γ
hg : Measurable g
f✝ : α →ₘ[μ] β
f : α → β
x✝ : AEStronglyMeasurable f μ
⊢ (compMeasurable g hg (mk f x✝)).toGerm = Germ.map g (mk f x✝).toGerm

Tactic:
simp

Goal state after:
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 γ
g : β → γ → δ
hg : Continuous[instTopologicalSpaceProd, inst✝²] (uncurry g)
f₁✝ : α →ₘ[μ] β
f₂✝ : α →ₘ[μ] γ
f₁ : α → β
x✝¹ : AEStronglyMeasurable f₁ μ
f₂ : α → γ
x✝ : AEStronglyMeasurable f₂ μ
⊢ (comp₂ g hg (mk f₁ x✝¹) (mk f₂ x✝)).toGerm = Germ.map₂ g (mk f₁ x✝¹).toGerm (mk f₂ x✝).toGerm

Tactic:
simp

Goal state after:
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✝¹⁰ : PseudoMetrizableSpace β
inst✝⁹ : MeasurableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : PseudoMetrizableSpace γ
inst✝⁶ : SecondCountableTopologyEither β γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : PseudoMetrizableSpace δ
inst✝² : SecondCountableTopology δ
inst✝¹ : MeasurableSpace δ
inst✝ : OpensMeasurableSpace δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁✝ : α →ₘ[μ] β
f₂✝ : α →ₘ[μ] γ
f₁ : α → β
x✝¹ : AEStronglyMeasurable f₁ μ
f₂ : α → γ
x✝ : AEStronglyMeasurable f₂ μ
⊢ (comp₂Measurable g hg (mk f₁ x✝¹) (mk f₂ x✝)).toGerm = Germ.map₂ g (mk f₁ x✝¹).toGerm (mk f₂ x✝).toGerm

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝² : ConditionallyCompleteLattice β
f : α → β
inst✝¹ : Nonempty α
inst✝ : MeasurableSingletonClass α
hf : BddAbove (range f)
⊢ ∀ (a : α), Measure.count {a} ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝² : ConditionallyCompleteLattice β
f : α → β
inst✝¹ : Nonempty α
inst✝ : MeasurableSingletonClass α
hf : BddBelow (range f)
⊢ ∀ (a : α), Measure.count {a} ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: case inl.inl
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
u : Set Ω
hs ht : ∅.Finite
hst : Disjoint ∅ ∅
⊢ (uniformOn ∅) u * (uniformOn (∅ ∪ ∅)) ∅ + (uniformOn ∅) u * (uniformOn (∅ ∪ ∅)) ∅ = (uniformOn (∅ ∪ ∅)) u

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
m : MeasurableSpace α
f : α → β
⊢ ⊥ ∈ {a | ∀ᶠ (n : β) in map f (ae 0), n ≤ a}

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.EssSup

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : CompleteLattice β
inst✝ : MeasurableSingletonClass α
f : α → β
⊢ ∀ (a : α), Measure.count {a} ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
inst✝ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
s : (i : ι) → Set (α i)
⊢ piPremeasure m (univ.pi s) = ∏ i, (m i) (s i)

Tactic:
cases isEmpty_or_nonempty ι
  · simp [piPremeasure]
  rcases (pi univ s).eq_empty_or_nonempty with h | h
  · rcases univ_pi_eq_empty_iff.mp h with ⟨i, hi⟩
    have : ∃ i, m i (s i) = 0 := ⟨i, by simp [hi]⟩
    simpa [h, Finset.card_univ, zero_pow Fintype.card_ne_zero, @eq_comm _ (0 : ℝ≥0∞),
      Finset.prod_eq_zero_iff, piPremeasure]
  · simp [h, piPremeasure]

Goal state after:
Module: Mathlib.Probability.UniformOn

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s u t : Set Ω
hs : s.Finite
⊢ s = s ∩ u ∪ s ∩ uᶜ

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case nil
δ : 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)
⊢ (Measure.tprod [] μ) (Set.tprod [] s) = (List.map (fun i ↦ (μ i) (s i)) []).prod

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
b : β
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
x✝ : α
⊢ Function.const α (Classical.choose h) x✝ = Classical.choose h

Tactic:
simp

Goal state after: