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

Tactic:
exact ModuleFilterBasis.continuousSMul _

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
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
V : Set E
⊢ (∃ i, (∃ i_1 r, 0 < r ∧ i = (i_1.sup p).ball 0 r) ∧ i ⊆ V) ↔ ∃ a b, 0 < b ∧ (a.sup p).ball 0 b ⊆ V

Tactic:
grind

Goal state after:
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
G : Type u_5
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
𝔖 : Set (Set E)
⊢ TopologicalSpace.induced DFunLike.coe (UniformOnFun.topologicalSpace E F 𝔖) =
    (UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.uniformSpace E F 𝔖)).toTopologicalSpace

Tactic:
rfl

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

Goal state before:
pp: case h
𝕜 : 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 : ι
r : ℝ
h✝ : r > 0 ∧ ∀ x ∈ s, (p i) x < r
⊢ ∀ ⦃x : E⦄, x ∈ s → (p i) x ≤ r

Tactic:
grind

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

Goal state before:
pp: case h
𝕜 : 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 : ι
r : ℝ
h✝ : ∀ ⦃x : E⦄, x ∈ s → (p i) x ≤ r
⊢ 1 + max r 0 > 0 ∧ ∀ x ∈ s, (p i) x < 1 + max r 0

Tactic:
grind

Goal state after:
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
G : Type u_5
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
M : Type u_6
inst✝⁵ : Monoid M
inst✝⁴ : DistribMulAction M F
inst✝³ : SMulCommClass 𝕜₂ M F
inst✝² : UniformSpace F
inst✝¹ : IsUniformAddGroup F
inst✝ : UniformContinuousConstSMul M F
𝔖 : Set (Set E)
x✝¹ : M
x✝ : E →SLᵤ[σ, 𝔖] F
⊢ (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (x✝¹ • x✝) = x✝¹ • (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) x✝

Tactic:
rfl

Goal state after:
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
ι : Type u_6
p : Filter ι
inst✝¹ : UniformSpace F
inst✝ : IsUniformAddGroup F
𝔖 : Set (Set E)
a : ι → E →SLᵤ[σ, 𝔖] F
a₀ : E →SLᵤ[σ, 𝔖] F
⊢ (∀ s ∈ 𝔖,
      TendstoUniformlyOn (⇑(UniformOnFun.toFun 𝔖) ∘ (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) ∘ a)
        ((UniformOnFun.toFun 𝔖) ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) a₀)) p s) ↔
    ∀ s ∈ 𝔖, TendstoUniformlyOn (fun x1 x2 ↦ (a x1) x2) (⇑a₀) p s

Tactic:
rfl

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
Fₗ : Type u_6
G : Type u_7
𝓕 : Type u_8
inst✝¹⁴ : SeminormedAddCommGroup E
inst✝¹³ : SeminormedAddCommGroup F
inst✝¹² : SeminormedAddCommGroup Fₗ
inst✝¹¹ : SeminormedAddCommGroup G
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜₂
inst✝⁸ : NontriviallyNormedField 𝕜₃
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : FunLike 𝓕 E F
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
ℓ : E →SL[σ₁₂] F
s : Set E
hs : Bornology.IsBounded s
M : ℝ
hM : ∀ x ∈ s, ‖x‖ ≤ M
y : F
hy : y ∈ ⇑ℓ '' s
σ : E
hσ : σ ∈ s ∧ ℓ σ = y
⊢ ‖ℓ‖ ≤ ‖ℓ‖

Tactic:
rfl

Goal state after:
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 : 𝔖₂ ⊆ 𝔖₁
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ instTopologicalSpace σ F 𝔖₁ ≤ instTopologicalSpace σ F 𝔖₂

Tactic:
simp_rw [← uniformity_toTopologicalSpace_eq]

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
𝔖₁ 𝔖₂ : Set (Set E)
inst✝¹ : TopologicalSpace F
inst✝ : IsTopologicalAddGroup F
h : 𝔖₂ ⊆ 𝔖₁
this✝ : UniformSpace F := IsTopologicalAddGroup.rightUniformSpace F
this : IsUniformAddGroup F
⊢ (instUniformSpace σ F 𝔖₁).toTopologicalSpace ≤ (instUniformSpace σ F 𝔖₂).toTopologicalSpace
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case refine_1
𝕜 : 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
s : Finset ι
⊢ ((fun s ↦ s.sup p) s).comp LinearMap.id ≤ s.sup p

Tactic:
rfl

Goal state after:
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 ≤ p i

Tactic:
rfl

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

Goal state before:
pp: case refine_1
𝕜 : 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 : ι
⊢ ((fun i ↦ (Finset.Iic i).sup p) i).comp LinearMap.id ≤ (Finset.Iic i).sup p

Tactic:
rfl

Goal state after:
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
G : Type u_5
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module 𝕜₁ E✝
inst✝¹¹ : TopologicalSpace E✝
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜₂ F✝
𝕜 : Type u_6
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
x✝³ x✝² : (i : ι) → E →Lᵤ[𝕜, 𝔖] F i
x✝¹ : E
x✝ : ι
⊢ (ContinuousLinearMap.pi (x✝³ + x✝²)) x✝¹ x✝ = (ContinuousLinearMap.pi x✝³ + ContinuousLinearMap.pi x✝²) x✝¹ x✝

Tactic:
rfl

Goal state after:
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
G : Type u_5
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module 𝕜₁ E✝
inst✝¹¹ : TopologicalSpace E✝
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜₂ F✝
𝕜 : Type u_6
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
x✝³ : 𝕜
x✝² : (i : ι) → E →Lᵤ[𝕜, 𝔖] F i
x✝¹ : E
x✝ : ι
⊢ (ContinuousLinearMap.pi (x✝³ • x✝²)) x✝¹ x✝ = ((RingHom.id 𝕜) x✝³ • ContinuousLinearMap.pi x✝²) x✝¹ x✝

Tactic:
rfl

Goal state after:
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
G : Type u_5
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module 𝕜₁ E✝
inst✝¹¹ : TopologicalSpace E✝
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜₂ F✝
𝕜 : Type u_6
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
x✝² : (i : ι) → E →Lᵤ[𝕜, 𝔖] F i
x✝¹ : ι
x✝ : E
⊢ ((fun f i ↦ ContinuousLinearMap.proj i ∘SL f) ((fun F_1 ↦ ContinuousLinearMap.pi F_1) x✝²) x✝¹) x✝ = (x✝² x✝¹) x✝

Tactic:
rfl

Goal state after:
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
G : Type u_5
inst✝¹³ : AddCommGroup E✝
inst✝¹² : Module 𝕜₁ E✝
inst✝¹¹ : TopologicalSpace E✝
inst✝¹⁰ : AddCommGroup F✝
inst✝⁹ : Module 𝕜₂ F✝
𝕜 : Type u_6
inst✝⁸ : NormedField 𝕜
E : Type u_7
ι : Type u_8
F : ι → Type u_9
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : (i : ι) → AddCommGroup (F i)
inst✝³ : (i : ι) → Module 𝕜 (F i)
inst✝² : (i : ι) → TopologicalSpace (F i)
inst✝¹ : ∀ (i : ι), IsTopologicalAddGroup (F i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)
𝔖 : Set (Set E)
this✝ : (i : ι) → UniformSpace (F i) := fun i ↦ IsTopologicalAddGroup.rightUniformSpace (F i)
this : ∀ (i : ι), IsUniformAddGroup (F i)
x✝² : E →Lᵤ[𝕜, 𝔖] (i : ι) → F i
x✝¹ : E
x✝ : ι
⊢ ((fun F_1 ↦ ContinuousLinearMap.pi F_1) ((fun f i ↦ ContinuousLinearMap.proj i ∘SL f) x✝²)) x✝¹ x✝ = x✝² x✝¹ x✝

Tactic:
rfl

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
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ ↑(s.sup fun i ↦ NNReal.mk ((q i) (f x)) ⋯) = ↑(s.sup fun i ↦ NNReal.mk ((q.comp f i) x) ⋯)

Tactic:
rfl

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
l : Filter α
x✝ : l.Germ β
f : α → β
⊢ map id (Quot.mk (⇑(l.germSetoid β)) f) = id (Quot.mk (⇑(l.germSetoid β)) f)

Tactic:
rfl

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
G : Type u_6
inst✝ : Monoid M
x✝¹ x✝ : α → M
⊢ ↑(x✝¹ * x✝) = ↑x✝¹ * ↑x✝

Tactic:
rfl

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
G : Type u_6
inst✝ : Monoid M
x✝¹ : α → M
x✝ : ℕ
⊢ ↑(x✝¹ ^ x✝) = ↑x✝¹ ^ x✝

Tactic:
rfl

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
G : Type u_6
inst✝ : AddMonoidWithOne M
⊢ 0 = fun x ↦ 0

Tactic:
rfl

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
G : Type u_6
inst✝ : AddMonoidWithOne M
x✝ : ℕ
⊢ ↑x✝ + 1 = fun x ↦ ↑x✝ + 1

Tactic:
rfl

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
G : Type u_6
inst✝ : AddGroupWithOne G
x✝ : ℕ
⊢ -1 + -↑x✝ = fun x ↦ -1 + -↑x✝

Tactic:
rfl

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
⊢ CompactCoherentification.map f ∘ ⇑(CompactCoherentification.mk X) = ⇑(CompactCoherentification.mk Y) ∘ f

Tactic:
rfl

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A : Set (𝐤X)
⊢ (∀ (i : Set X),
      IsCompact i →
        IsOpen[TopologicalSpace.coinduced Subtype.val
              { IsOpen := fun s ↦ ∃ t, IsOpen[inst✝] t ∧ Subtype.val ⁻¹' t = s, isOpen_univ := ⋯, isOpen_inter := ⋯,
                isOpen_sUnion := ⋯ }]
          (⇑(CompactCoherentification.mk X) ⁻¹' A)) ↔
    ∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ ⇑(CompactCoherentification.mk X) ⁻¹' A)

Tactic:
rfl

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : 𝐤X → Y
⊢ (∀ (i : Set X),
      IsCompact i →
        Continuous[{ IsOpen := fun s ↦ ∃ t, IsOpen[inst✝¹] t ∧ Subtype.val ⁻¹' t = s, isOpen_univ := ⋯,
              isOpen_inter := ⋯, isOpen_sUnion := ⋯ },
            inst✝]
          ((f ∘ ⇑(CompactCoherentification.mk X)) ∘ Subtype.val)) ↔
    ∀ (K : Set X),
      IsCompact K →
        Continuous[instTopologicalSpaceSubtype, inst✝] (K.domRestrict (f ∘ ⇑(CompactCoherentification.mk X)))

Tactic:
rfl

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactlyCoherentSpace X
⊢ ∀ s ∈ {K | IsCompact K}, ContinuousOn (⇑(CompactCoherentification.mk X)) s

Tactic:
exact fun K hK ↦ continuousOn_isCompact_mk hK

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
A : Set X
hA : IsCompact A
f : X → Y
⊢ ContinuousOn (⇑(CompactCoherentification.mk Y) ∘ f) A ↔ ContinuousOn f A

Tactic:
simp_rw [continuousOn_iff_continuous_domRestrict]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
A : Set X
hA : IsCompact A
f : X → Y
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpace] (A.domRestrict (⇑(CompactCoherentification.mk Y) ∘ f)) ↔
    Continuous[instTopologicalSpaceSubtype, inst✝] (A.domRestrict f)
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f✝ f : C(α, β)
l : Filter C(α, β)
⊢ (∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a ↦ (id i) a) (⇑f) l K) ↔
    ∀ s ∈ {K | IsCompact K},
      TendstoUniformlyOn (⇑(UniformOnFun.toFun {K | IsCompact K}) ∘ toUniformOnFunIsCompact ∘ id)
        ((UniformOnFun.toFun {K | IsCompact K}) f.toUniformOnFunIsCompact) l s

Tactic:
rfl

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
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
x✝¹ : E
x✝ : F
⊢ (f.flip.flip x✝¹) x✝ = (f x✝¹) x✝

Tactic:
rfl

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 (toUniformOnFunIsCompact ∘ fun x ↦ x.comp φ₁) inferInstance ⊓
      UniformSpace.comap (toUniformOnFunIsCompact ∘ fun x ↦ x.comp φ₂) inferInstance

Tactic:
rfl

Goal state after:
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)
S : Set α
hS : S ∈ 𝔖
⊢ ⋃ i ∈ {i | (range ⇑(φ i) ∩ S).Nonempty}, range ⇑(φ i) ∩ S = S

Tactic:
mem_ofPred,

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)
S : Set α
hS : S ∈ 𝔖
⊢ ⋃ i, ⋃ (_ : (range ⇑(φ i) ∩ S).Nonempty), range ⇑(φ i) ∩ S = S
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 (toUniformOnFunIsCompact ∘ fun x ↦ x.comp (φ i)) inferInstance

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
R : Type u_2
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsTopologicalSemiring A
k : R
a : α
⊢ (k • 1) a = k • 1

Tactic:
rfl

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ comp id ⋯ (Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝) = Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝

Tactic:
rfl

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : γ → δ
g' : β → γ
hg : Continuous[inst✝, inst✝²] g
hg' : Continuous[inst✝¹, inst✝] g'
f : α →ₘ[μ] β
a✝ : { f // AEStronglyMeasurable f μ }
⊢ comp g hg (comp g' hg' (Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝)) =
    comp (g ∘ g') ⋯ (Quot.mk (⇑(Measure.aeEqSetoid β μ)) a✝)

Tactic:
rfl

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

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

Tactic:
grind

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

Goal state before:
pp: case mk
α : Type u_1
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace γ
β : Type u_5
inst✝ : MeasurableSpace β
ν : Measure β
g : γ → δ
hg : Continuous[inst✝¹, inst✝²] g
f : β →ₘ[ν] γ
φ : α → β
hφ : Measure.QuasiMeasurePreserving φ μ ν
a✝ : { f // AEStronglyMeasurable f ν }
⊢ (comp g hg (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝)).compQuasiMeasurePreserving φ hφ =
    comp g hg (compQuasiMeasurePreserving (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝) φ hφ)

Tactic:
rfl

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₂ : α →ₘ[μ] γ
⊢ mk (uncurry g ∘ fun x ↦ (↑f₁ x, ↑f₂ x)) ⋯ = mk (fun a ↦ g (↑f₁ a) (↑f₂ a)) ⋯

Tactic:
rfl

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✝¹⁰ : 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 (uncurry g ∘ fun x ↦ (↑f₁ x, ↑f₂ x)) ⋯ = mk (fun a ↦ g (↑f₁ a) (↑f₂ a)) ⋯

Tactic:
rfl

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

Goal state before:
pp: case mk
α : Type u_1
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
β : Type u_5
inst✝ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] γ
hf : Measure.QuasiMeasurePreserving f μ ν
a✝ : { f // AEStronglyMeasurable f ν }
⊢ (compQuasiMeasurePreserving (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝) f hf).toGerm =
    (toGerm (Quot.mk (⇑(Measure.aeEqSetoid γ ν)) a✝)).compTendsto f ⋯

Tactic:
rfl

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 : Set ((i : ι) → α i)
⊢ ∏ i, (m i) ((fun a ↦ a i) '' s) = piPremeasure m s

Tactic:
rfl

Goal state after: