mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
h₁ : e.toPartialEquiv = e'.toPartialEquiv
h₂ : e.baseSet = e'.baseSet
⊢ e = e'

Tactic:
by
  cases e; cases e'; congr

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
this : proj (↑e.symm x) = (↑e (↑e.symm x)).1
⊢ proj (↑e.symm x) = x.1

Tactic:
rwa [← e.coe_coe, e.right_inv hx] at this

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case neg
B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
he : ¬∀ ⦃a : B⦄, a ∈ Iio d → a ∉ Ioi c
⊢ ∃ d ∈ Ioc c b, ∃ e, Icc a d ⊆ e.baseSet

Tactic:
push Not at he

Goal state after:
case neg
B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
he : ∃ a ∈ Iio d, a ∈ Ioi c
⊢ ∃ d ∈ Ioc c b, ∃ e, Icc a d ⊆ e.baseSet
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : ∀ (x : B), Nonempty (E x)
e : Pretrivialization F TotalSpace.proj
b : B
hb : b ∉ e.baseSet
y : F
⊢ e.symm b y = Classical.arbitrary (E b)

Tactic:
simp [Pretrivialization.symm, hb]

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e e' : Trivialization F proj
h₁ : e.toOpenPartialHomeomorph = e'.toOpenPartialHomeomorph
h₂ : e.baseSet = e'.baseSet
⊢ e = e'

Tactic:
by
  cases e; cases e'; congr

Goal state after:
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace F
inst✝³ : (x : B) → TopologicalSpace (E x)
inst✝² : (x : B) → Zero (E x)
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : FiberBundle F E
x : B
v : E x
⊢ extend F v x = v

Tactic:
by
  simp [extend, FiberBundle.mem_baseSet_trivializationAt' x]

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: case refine_2
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
x₁ x₂ : X
x✝² : f x₁ = f x₂
x✝¹ : x₁ ≠ x₂
x✝ : (Function.pullbackDiagonal f)ᶜ ∈ comap Subtype.val (𝓝 x₁ ×ˢ 𝓝 x₂)
t : Set (X × X)
ht : t ∈ 𝓝 x₁ ×ˢ 𝓝 x₂
t_sub : Subtype.val ⁻¹' t ⊆ (Function.pullbackDiagonal f)ᶜ
⊢ ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂

Tactic:
obtain ⟨s₁, h₁, s₂, h₂, s_sub⟩ := mem_prod_iff.mp ht
    exact ⟨s₁, h₁, s₂, h₂, disjoint_left.2 fun x h₁ h₂ ↦ @t_sub ⟨(x, x), rfl⟩ (s_sub ⟨h₁, h₂⟩) rfl⟩

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
⊢ DiscreteTopology X ↔ IsLocallyInjective fun x ↦ y

Tactic:
rw [discreteTopology_iff_singleton_mem_nhds, isLocallyInjective_iff_nhds]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
y : Y
⊢ (∀ (x : X), {x} ∈ 𝓝 x) ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, Set.InjOn (fun x ↦ y) U
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
J : Type u_4
inst✝ : TopologicalSpace J
g : I ≃ₜ J
x : X
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝²] U
hfU : IsOpen[inst✝³] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
x✝ : ↑(f ⁻¹' U)
⊢ ↑((H.trans ((Homeomorph.refl ↑U).prodCongr g)) x✝).1 = f ↑x✝

Tactic:
by simp [hH]

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
Y : Type u_4
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered (⇑g ∘ f) (g x) I
⊢ IsEvenlyCovered f x I

Tactic:
convert! h.homeomorph_comp g.symm

Goal state after:
case e'_5
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
Y : Type u_4
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered (⇑g ∘ f) (g x) I
⊢ f = ⇑g.symm ∘ ⇑g ∘ f

case e'_6
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
Y : Type u_4
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsEvenlyCovered (⇑g ∘ f) (g x) I
⊢ x = g.symm (g x)
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMapOn (⇑g ∘ f) (⇑g.symm ⁻¹' s)
⊢ IsCoveringMapOn f s

Tactic:
convert! h.homeomorph_comp g.symm

Goal state after:
case e'_5
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMapOn (⇑g ∘ f) (⇑g.symm ⁻¹' s)
⊢ f = ⇑g.symm ∘ ⇑g ∘ f

case e'_6
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMapOn (⇑g ∘ f) (⇑g.symm ⁻¹' s)
⊢ s = ⇑g.symm.symm ⁻¹' ⇑g.symm ⁻¹' s
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMap (⇑g ∘ f)
⊢ IsCoveringMap f

Tactic:
convert! h.homeomorph_comp g.symm

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMap (⇑g ∘ f)
⊢ f = ⇑g.symm ∘ ⇑g ∘ f
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
f : E → X
h : ∀ (x : E), f x ∈ s
hf : IsCoveringMap fun x ↦ ⟨f x, ⋯⟩
eq : f ⁻¹' s = Set.univ
⊢ IsOpen[inst✝¹] (f ⁻¹' s)

Tactic:
simp [eq]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ ⇑exp '' (Icc (↑x).arg (x.angleDiff y + (↑x).arg) ∪ Icc (↑y).arg (y.angleDiff x + (↑y).arg)) = univ

Tactic:
Icc_union_Icc_angleDiff_add_arg h,

Goal state after:
x y : Circle
h : x ≠ y
⊢ ⇑exp '' Icc (min (↑x).arg (↑y).arg) (min (↑x).arg (↑y).arg + 2 * π) = univ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ range ⇑(x.path y) ∩ range ⇑(y.path x) = {x, y}

Tactic:
by
  rw [← image_univ, ← image_univ, unitInterval.univ_eq_Icc, ← Ioc_insert_left (by simp),
    ← Ioo_insert_right (by simp)]
  simp_rw [image_insert_eq]
  have h : Disjoint ((x.path y) '' Ioo 0 1) ((y.path x) '' Ioo 0 1) := by
    refine (disjoint_path_image_Ioc h).mono ?_ ?_ <;> exact image_mono Ioo_subset_Ioc_self
  grind

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : z.re ≤ -1
hz_norm : ‖z‖ = 1
⊢ -1 ∈ spectrum ℂ u

Tactic:
rw [← hz_norm, ← RCLike.re_eq_complex_re, RCLike.re_le_neg_norm_iff_eq_neg_norm, hz_norm] at key

Goal state after:
case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : z = -↑1
hz_norm : ‖z‖ = 1
⊢ -1 ∈ spectrum ℂ u
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
x y : AddCircle T
⊢ (x + y).toCircle = x.toCircle * y.toCircle

Tactic:
induction x using QuotientAddGroup.induction_on

Goal state after:
case H
T : ℝ
y : AddCircle T
z✝ : ℝ
⊢ (↑z✝ + y).toCircle = toCircle ↑z✝ * y.toCircle
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
T : E →L[𝕜] E
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
⊢ Uᗮ ∈ invtSubmodule ↑T → U ∈ invtSubmodule ↑(adjoint T)

Tactic:
by simpa using orthogonal_mem_invtSubmodule (T := T.adjoint) (U := Uᗮ)

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁷ : DivisionRing k
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k V
inst✝⁴ : AffineSpace V P
V₂ : Type u_5
P₂ : Type u_6
inst✝³ : AddCommGroup V₂
inst✝² : Module k V₂
inst✝¹ : AffineSpace V₂ P₂
s : AffineSubspace k P
inst✝ : FiniteDimensional k ↥s.direction
f : P →ᵃ[k] P₂
⊢ FiniteDimensional k ↥(map f s).direction

Tactic:
rw [map_direction]
  infer_instance

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : #s = finrank k ↥sp.direction + 1
hn : s.Nonempty
hd : vectorSpan k ↑(Finset.image p s) ≤ sp.direction
⊢ vectorSpan k ↑(Finset.image p s) = sp.direction

Tactic:
exact hi.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one hd hc

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

Goal state before:
pp: case h.inr
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
p₁ p₂ p : P
hp : p = p₂
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
use 1
    simp [hp]

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: case refine_4
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p ↦ if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) ⋯
⊢ affineSpan ℝ (range fun p ↦ (lineMap q ↑p) ↑(w p)) = ⊤

Tactic:
rw [affineSpan_eq_affineSpan_lineMap_units (ht₁ hq) w, ht₃]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)

Tactic:
norm_rpow_eq_tsum hp

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) (∑' (i : α), ‖↑f i‖ ^ p.toReal)
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
x₀ : E
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
hf0 : Summable fun n ↦ f n x₀
x : E
⊢ Summable fun n ↦ f n x

Tactic:
let : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
  let _ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 _
  exact summable_of_summable_hasFDerivAt_of_isPreconnected hu isOpen_univ isPreconnected_univ
    (fun n x _ => hf n x) (fun n x _ => hf' n x) (mem_univ _) hf0 (mem_univ _)

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ f = 0 ↔ ↑f = 0

Tactic:
lp.ext_iff,

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ ↑f = ↑0 ↔ ↑f = 0
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
have hp'' : 0 < p.toReal := zero_lt_one.trans_le hp'

Goal state after:
case inr
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
C : ℝ
hC : 0 ≤ C
f : ↥(lp E p)
hf : ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal
⊢ ‖f‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
norm_rpow_eq_tsum hp

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
C : ℝ
hC : 0 ≤ C
f : ↥(lp E p)
hf : ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal
⊢ ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
hp✝ : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), ↑‖f‖₊ = ‖f‖
hLHS : HasSum (fun i ↦ ‖↑(c • f) i‖ ^ p.toReal) (‖c • f‖ ^ p.toReal)
hRHS : HasSum (fun i ↦ ‖c‖ ^ p.toReal * ‖↑f i‖ ^ p.toReal) (‖c‖ ^ p.toReal * ‖f‖ ^ p.toReal)
⊢ ‖c • f‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal

Tactic:
simp_rw [← coe_nnnorm, ← _root_.coe_nnnorm, ← NNReal.coe_rpow, ← NNReal.coe_mul,
      NNReal.hasSum_coe] at hRHS hLHS

Goal state after:
case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
hp✝ : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p)
coe_nnnorm : ∀ (f : ↥(lp E p)), ↑‖f‖₊ = ‖f‖
hRHS : HasSum (fun a ↦ ‖c‖₊ ^ p.toReal * ‖↑f a‖₊ ^ p.toReal) (‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal)
hLHS : HasSum (fun a ↦ ‖↑(c • f) a‖₊ ^ p.toReal) (‖c • f‖₊ ^ p.toReal)
⊢ ‖c • f‖₊ ^ p.toReal ≤ ‖c‖₊ ^ p.toReal * ‖f‖₊ ^ p.toReal
Module: Mathlib.Analysis.InnerProductSpace.Calculus

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
⊢ HasStrictFDerivAt (fun x ↦ re ⟪x, x⟫) (2 • (innerSL ℝ) x) x

Tactic:
convert! (hasStrictFDerivAt_id x).inner ℝ (hasStrictFDerivAt_id x)

Goal state after:
case e'_12
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
e_8✝ : instAddCommGroup = instRCLike.toDivisionRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ toInnerProductSpaceReal.toModule
⊢ 2 • (innerSL ℝ) x = fderivInnerCLM ℝ (id x, id x) ∘SL (ContinuousLinearMap.id ℝ F).prod (ContinuousLinearMap.id ℝ F)
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : TendstoLocallyUniformlyOn f' g' l s
hf : ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) (f' n x) x
hfg : ∀ x ∈ s, Tendsto (fun n ↦ f n x) l (𝓝 (g x))
hx : x ∈ s
h1 : s ∈ 𝓝 x
h2 : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2
⊢ HasDerivAt g (g' x) x

Tactic:
refine hasDerivAt_of_tendstoUniformlyOnFilter ?_ h2 (eventually_of_mem h1 hfg)

Goal state after:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : TendstoLocallyUniformlyOn f' g' l s
hf : ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) (f' n x) x
hfg : ∀ x ∈ s, Tendsto (fun n ↦ f n x) l (𝓝 (g x))
hx : x ∈ s
h1 : s ∈ 𝓝 x
h2 : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2
⊢ TendstoUniformlyOnFilter f' g' l (𝓝 x)
Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist

Goal state before:
pp: E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ (𝓝 x).HasBasis (fun r ↦ 0 < r) (ball x)

Tactic:
rw [toEuclidean.toHomeomorph.nhds_eq_comap x]
  exact Metric.nhds_basis_ball.comap _

Goal state after:
Module: Mathlib.Topology.Metrizable.Urysohn

Goal state before:
pp: case refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure[inst✝²] UV.1 ⊆ UV.2}
this✝¹ : Encodable ↑s
this✝ : TopologicalSpace ↑s := ⊥
this : DiscreteTopology ↑s
hd : ∀ (UV : ↑s), Disjoint (closure[inst✝²] (↑UV).1) (↑UV).2ᶜ
ε : ↑s → ℝ
ε01 : ∀ (UV : ↑s), ε UV ∈ Ioc 0 1
hε : Tendsto ε cofinite (𝓝 0)
f : ↑s → C(X, ℝ)
hf0 : ∀ (UV : ↑s), EqOn (⇑(f UV)) 0 (↑UV).1
hfε : ∀ (UV : ↑s), EqOn (⇑(f UV)) (fun x ↦ ε UV) (↑UV).2ᶜ
hf0ε : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 (ε UV)
hf01 : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 1
F : X → ↑s →ᵇ ℝ := fun x ↦ { toFun := fun UV ↦ (f UV) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF : ∀ (x : X) (UV : ↑s), (F x) UV = (f UV) x
x : X
⊢ 𝓝 x ≤ comap F (𝓝 (F x))

Tactic:
refine (nhds_basis_closedBall.comap _).ge_iff.2 fun δ δ0 => ?_

Goal state after:
case refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure[inst✝²] UV.1 ⊆ UV.2}
this✝¹ : Encodable ↑s
this✝ : TopologicalSpace ↑s := ⊥
this : DiscreteTopology ↑s
hd : ∀ (UV : ↑s), Disjoint (closure[inst✝²] (↑UV).1) (↑UV).2ᶜ
ε : ↑s → ℝ
ε01 : ∀ (UV : ↑s), ε UV ∈ Ioc 0 1
hε : Tendsto ε cofinite (𝓝 0)
f : ↑s → C(X, ℝ)
hf0 : ∀ (UV : ↑s), EqOn (⇑(f UV)) 0 (↑UV).1
hfε : ∀ (UV : ↑s), EqOn (⇑(f UV)) (fun x ↦ ε UV) (↑UV).2ᶜ
hf0ε : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 (ε UV)
hf01 : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 1
F : X → ↑s →ᵇ ℝ := fun x ↦ { toFun := fun UV ↦ (f UV) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF : ∀ (x : X) (UV : ↑s), (F x) UV = (f UV) x
x : X
δ : ℝ
δ0 : 0 < δ
⊢ F ⁻¹' closedBall (F x) δ ∈ 𝓝 x
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
t : Set α
t_mem : t ∈ 𝓝 x
ht : ∀ u ⊆ t, ν u = μ u
⊢ 0 < ν n

Tactic:
← inter_subset_left (s := n)

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
t : Set α
t_mem : t ∈ 𝓝 x
ht : ∀ u ⊆ t, ν u = μ u
⊢ 0 < ν (n ∩ ?m.55)

α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
t : Set α
t_mem : t ∈ 𝓝 x
ht : ∀ u ⊆ t, ν u = μ u
⊢ Set α
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: G : Type u_2
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : LocallyCompactSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst✝⁷] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
W : ℕ → Set G
W_open : ∀ (n : ℕ), IsOpen[inst✝⁷] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, μ (g • k \ k) < u n
V : ℕ → Set G := fun n ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : x ∈ ⋂ n, V n * k
v : ℕ → G
hv : ∀ (i : ℕ), v i ∈ V i
y : ℕ → G
hy : ∀ (i : ℕ), y i ∈ k
hvy : ∀ (i : ℕ), (fun x1 x2 ↦ x1 * x2) (v i) (y i) = x
z : G
zk : z ∈ k
hz : MapClusterPt z atTop y
A : ∀ (n : ℕ), μ ((x * z⁻¹) • k \ k) ≤ u n
B : μ ((x * z⁻¹) • k \ k) = 0
⊢ μ (k \ (z * x⁻¹) • k) = 0

Tactic:
have : μ ((z * x⁻¹) • (((x * z⁻¹) • k) \ k)) = 0 := by rwa [measure_smul]

Goal state after:
G : Type u_2
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : LocallyCompactSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst✝⁷] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
W : ℕ → Set G
W_open : ∀ (n : ℕ), IsOpen[inst✝⁷] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, μ (g • k \ k) < u n
V : ℕ → Set G := fun n ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : x ∈ ⋂ n, V n * k
v : ℕ → G
hv : ∀ (i : ℕ), v i ∈ V i
y : ℕ → G
hy : ∀ (i : ℕ), y i ∈ k
hvy : ∀ (i : ℕ), (fun x1 x2 ↦ x1 * x2) (v i) (y i) = x
z : G
zk : z ∈ k
hz : MapClusterPt z atTop y
A : ∀ (n : ℕ), μ ((x * z⁻¹) • k \ k) ≤ u n
B : μ ((x * z⁻¹) • k \ k) = 0
this : μ ((z * x⁻¹) • ((x * z⁻¹) • k \ k)) = 0
⊢ μ (k \ (z * x⁻¹) • k) = 0