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

Goal state before:
pp: case left
this : (fun x ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
⊢ x ∈ {x | x < 1} → (fun x ↦ x * (1 + x)⁻¹) ((fun x ↦ x * (1 - x)⁻¹) x) = x

Tactic:
(hx : x < 1)

Goal state after:
case left
this : (fun x ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
⊢ (fun x ↦ x * (1 + x)⁻¹) ((fun x ↦ x * (1 - x)⁻¹) x) = x
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: case right
this : (fun x ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
⊢ x ∈ {x | x < 1} → (fun x ↦ x * (1 - x)⁻¹) ((fun x ↦ x * (1 + x)⁻¹) x) = x

Tactic:
(hx : x < 1)

Goal state after:
case right
this : (fun x ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹
x : ℝ≥0
hx : x < 1
⊢ (fun x ↦ x * (1 - x)⁻¹) ((fun x ↦ x * (1 + x)⁻¹) x) = x
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ↑(Finset.univ.sup fun b ↦ ‖fun j ↦ A b j‖₊) = ↑(Finset.univ.sup fun i ↦ Finset.univ.sup fun j ↦ ‖A i j‖₊)

Tactic:
Pi.nnnorm_def

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

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
⊢ ‖fun i j ↦ diagonal v i j‖₊ = ‖v‖₊

Tactic:
Pi.nnnorm_def

Goal state after:
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
⊢ (Finset.univ.sup fun b ↦ Finset.univ.sup fun b_1 ↦ ‖diagonal v b b_1‖₊) = Finset.univ.sup fun b ↦ ‖v b‖₊
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: m : Type u_3
α : Type u_5
ι : Type u_7
inst✝² : Fintype m
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ (Finset.univ.sup fun i ↦ ∑ j, ‖replicateCol ι v i j‖₊) = ‖v‖₊

Tactic:
Pi.nnnorm_def

Goal state after:
m : Type u_3
α : Type u_5
ι : Type u_7
inst✝² : Fintype m
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ (Finset.univ.sup fun i ↦ ∑ j, ‖replicateCol ι v i j‖₊) = Finset.univ.sup fun b ↦ ‖v b‖₊
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
⊢ (Finset.univ.sup fun i ↦ ∑ j, ‖diagonal v i j‖₊) = ‖v‖₊

Tactic:
Pi.nnnorm_def

Goal state after:
m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
⊢ (Finset.univ.sup fun i ↦ ∑ j, ‖diagonal v i j‖₊) = Finset.univ.sup fun b ↦ ‖v b‖₊
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
x✝² x✝¹ x✝ : f.PreGNS
⊢ f (star (f.ofPreGNS (x✝² + x✝¹)) * f.ofPreGNS x✝) =
    f (star (f.ofPreGNS x✝²) * f.ofPreGNS x✝) + f (star (f.ofPreGNS x✝¹) * f.ofPreGNS x✝)

Tactic:
rw [map_add, star_add, add_mul, map_add]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a : A
x : f.PreGNS
⊢ star (f.ofPreGNS x) * star a * (a * f.ofPreGNS x) ≤ ‖a‖ ^ 2 • star (f.ofPreGNS x) * f.ofPreGNS x

Tactic:
rw [← mul_assoc, mul_assoc _ (star a), sq, ← CStarRing.norm_star_mul_self (x := a),
        smul_mul_assoc]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a : A
x : f.PreGNS
⊢ star (f.ofPreGNS x) * (star a * a) * f.ofPreGNS x ≤ ‖star a * a‖ • (star (f.ofPreGNS x) * f.ofPreGNS x)
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: case ih
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
x✝¹ x✝ : A
c : f.PreGNS
⊢ (f.leftMulMapPreGNS (x✝¹ + x✝)).completion ↑c =
    ((f.leftMulMapPreGNS x✝¹).completion + (f.leftMulMapPreGNS x✝).completion) ↑c

Tactic:
| ih c =>

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: case ih
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
x✝¹ x✝ : A
c : f.PreGNS
⊢ (f.leftMulMapPreGNS (x✝¹ * x✝)).completion ↑c =
    ((f.leftMulMapPreGNS x✝¹).completion * (f.leftMulMapPreGNS x✝).completion) ↑c

Tactic:
| ih c =>

Goal state after:
Module: Mathlib.Data.Bundle

Goal state before:
pp: case h₂
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ proj ⁻¹' {b} ⊆ range (mk b)

Tactic:
· rintro ⟨_, x⟩ rfl
    exact ⟨x, rfl⟩

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
X : Type u_5
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ ContinuousAt (↑e.toOpenPartialHomeomorph ∘ f) x

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
X : Type u_5
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ f ⁻¹' e.source ∈ 𝓝 x

Tactic:
· exact hf

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ f ⁻¹' e.source ∈ 𝓝 x
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
hgf : IsLocalHomeomorphOn (g ∘ f) s
hf : IsLocalHomeomorphOn f s
x : X
hx : x ∈ s
⊢ ∃ e, f x ∈ e.source ∧ Set.EqOn g (↑e) e.source

Tactic:
obtain ⟨f, hxf, rfl⟩ := hf x hx

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
⊢ ∃ e, ↑f x ∈ e.source ∧ Set.EqOn g (↑e) e.source
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsLocalHomeomorph f
⊢ DiscreteTopology ↑(f '' Set.univ) ↔ DiscreteTopology ↑Set.univ

Tactic:
exact h.isLocalHomeomorphOn.discreteTopology_image_iff isOpen_univ

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
⊢ f x ∈ (hf.localInverseAt x).source

Tactic:
by
  rw [← congrFun (hf.localInverseAt_symm x)]
  exact (hf.localInverseAt x).map_target hf.self_mem_localInverseAt_target

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
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
e : E
he : e ∈ f ⁻¹' V
⊢ inv (idx e ⋯) ⋯ = e

Tactic:
exact inj _ (inv_U _ he) (idx_U e he) (f_inv _ _)

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
h : ‖x‖ = 1
⊢ normalize x = x

Tactic:
by
  simp [normalize, h]

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

Goal state before:
pp: case h.right
A : Type u_1
inst✝ : CStarAlgebra A
x : A
x✝¹ : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
x✝ : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
u₁ : ↥(unitary A) := ⋯
u₂ : ↥(unitary A) := ⋯
this : x = ‖x‖ • 2⁻¹ • (↑u₁ + ↑(star u₁) + I • (↑u₂ + ↑(star u₂)))
⊢ ∀ (i : Fin 4), ‖![↑‖x‖ * 2⁻¹, ↑‖x‖ * 2⁻¹, ↑‖x‖ * 2⁻¹ * I, ↑‖x‖ * 2⁻¹ * I] i‖ ≤ ‖x‖ / 2

Tactic:
· intro i
      fin_cases i
      all_goals simp [div_eq_mul_inv]

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✝ : Fintype ι
p : ι → P
n : ℕ
hc : #Finset.univ = n + 1
i₁ : ι
⊢ finrank k ↥(Submodule.span k (Set.range fun i ↦ p ↑i -ᵥ p i₁)) = Fintype.card { x // x ≠ i₁ } ↔
    finrank k ↥(Submodule.span k (Set.range fun i ↦ p ↑i -ᵥ p i₁)) = n

Tactic:
Fintype.subtype_card

Goal state after:
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✝ : Fintype ι
p : ι → P
n : ℕ
hc : #Finset.univ = n + 1
i₁ : ι
⊢ finrank k ↥(Submodule.span k (Set.range fun i ↦ p ↑i -ᵥ p i₁)) = #{x | x ≠ i₁} ↔
    finrank k ↥(Submodule.span k (Set.range fun i ↦ p ↑i -ᵥ p i₁)) = n
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✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ AffineIndependent k p ↔ finrank k ↥(vectorSpan k (Set.range p)) = n

Tactic:
have hn : Nonempty ι := by simp [← Fintype.card_pos_iff, hc]
  obtain ⟨i₁⟩ := hn
  rw [affineIndependent_iff_linearIndependent_vsub _ _ i₁,
    linearIndependent_iff_card_eq_finrank_span, eq_comm,
    vectorSpan_range_eq_span_range_vsub_right_ne k p i₁, Set.finrank]
  rw [← Finset.card_univ] at hc
  rw [Fintype.subtype_card]
  simp [Finset.filter_ne', Finset.card_erase_of_mem, hc]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ (↑n)⁻¹ • (s.centroid -ᵥ s.points i) +ᵥ s.centroid ∈ line[k, s.points i, s.centroid]

Tactic:
have h : (n : k)⁻¹ • (s.centroid -ᵥ s.points i) = (-1 / n : k) • (s.points i -ᵥ s.centroid)
        := by
      rw [← neg_vsub_eq_vsub_rev]
      have : -(s.points i -ᵥ s.centroid) = (-1 : k) • (s.points i -ᵥ s.centroid) := by simp
      rw [this, smul_smul]
      congr 1
      rw [mul_neg_one, inv_eq_one_div, neg_div]

Goal state after:
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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
h : (↑n)⁻¹ • (s.centroid -ᵥ s.points i) = (-1 / ↑n) • (s.points i -ᵥ s.centroid)
⊢ (↑n)⁻¹ • (s.centroid -ᵥ s.points i) +ᵥ s.centroid ∈ line[k, s.points i, s.centroid]
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case h₁
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Summable fun i ↦ ‖g i‖ ^ p.toReal
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hp : 0 < p.toReal
i : α
⊢ ‖f i‖ ≤ ‖g i‖

Tactic:
exact hfg i

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg0 : Summable fun n ↦ g n y₀
y : 𝕜
⊢ Summable fun n ↦ g n y

Tactic:
by
  exact summable_of_summable_hasDerivAt_of_isPreconnected hu isOpen_univ isPreconnected_univ
    (fun n x _ => hg n x) (fun n x _ => hg' n x) (mem_univ _) hg0 (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)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : (fun i ↦ ‖↑f i‖ ^ p.toReal) = 0
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
i : α
⊢ ↑f i = 0 ∧ p.toReal ≠ 0

Tactic:
simpa [Real.rpow_eq_zero_iff_of_nonneg (norm_nonneg (f i))] using! congr_fun hf i

Goal state after:
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this :
  TendstoUniformlyOnFilter (fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0 (l ×ˢ l) (𝓝 x) ∧
    TendstoUniformlyOnFilter (fun n x_1 ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x)
⊢ TendstoUniformlyOnFilter (fun n z ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l) (𝓝 x)

Tactic:
have := this.1.neg.add this.2.neg
    rw [neg_zero, add_zero] at this
    apply this.congr (.of_forall (fun x ↦ by simp; abel))

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)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
⊢ ‖∑ i ∈ s, lp.single p i (f i)‖ ^ p.toReal = ∑ i ∈ s, ‖f i‖ ^ p.toReal

Tactic:
refine (hasSum_norm hp (∑ i ∈ s, lp.single p i (f i))).unique ?_

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
⊢ HasSum (fun i ↦ ‖↑(∑ i ∈ s, lp.single p i (f i)) i‖ ^ p.toReal) (∑ i ∈ s, ‖f i‖ ^ p.toReal)
Module: Mathlib.Analysis.Calculus.FDeriv.WithLp

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Finite ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
⊢ DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun x ↦ (f x).ofLp i) t

Tactic:
by
  have := Fintype.ofFinite ι
  rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiableOn_iff, differentiableOn_pi]
  rfl

Goal state after:
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx✝ : x✝ ∈ s
hfg : Cauchy (map (fun n ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n ↦ f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
x : E
hx : x ∈ t
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
⊢ ∃ ε > 0, Metric.ball x ε ⊆ t

Tactic:
exact ⟨ε, εpos, A x ε hx hε⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: case hmono
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
⊢ ∀ ⦃s t : Set α⦄, s ⊆ t → μ t = 0 → μ s = 0

Tactic:
exact fun s t hst ht ↦ measure_mono_null hst ht

Goal state after:
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
⊢ x ∈ k

Tactic:
obtain ⟨z, zk, hz⟩ : ∃ z ∈ k, MapClusterPt z atTop y := hk.exists_mapClusterPt (by simp [hy])

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
⊢ x ∈ k
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case hbc
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n✝ : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := ⋯
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := ⋯
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
n : ℕ
R : ℕ → ℝ
hR : ∀ (i : ℕ) (x : E), ‖iteratedFDeriv ℝ i (fun x ↦ g n x) x‖ ≤ R i
M : ℝ := ⋯
δnpos : 0 < δ n
IR : ∀ i ≤ n, R i ≤ M
i : ℕ
hi : i ≤ n
x : E
⊢ ‖iteratedFDeriv ℝ i (g n) x‖ ≤ M

Tactic:
exact (hR i x).trans (IR i hi)

Goal state after:
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
B' : ∀ y ∈ ball x D, φ y = φ x
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1

Tactic:
rw [convolution_eq_right' _ (le_of_eq (w_support E Dpos)) B']

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
B' : ∀ y ∈ ball x D, φ y = φ x
⊢ ∫ (t : E), ((lsmul ℝ ℝ) (w D t)) (φ x) ∂μ = 1
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∉ ball 0 (1 + D)
B : ∀ y ∈ ball x D, φ y = 0
Bx : φ x = 0
B' : ∀ y ∈ ball x D, φ y = φ x
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 0

Tactic:
rw [convolution_eq_right' _ (le_of_eq (w_support E Dpos)) B']

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∉ ball 0 (1 + D)
B : ∀ y ∈ ball x D, φ y = 0
Bx : φ x = 0
B' : ∀ y ∈ ball x D, φ y = φ x
⊢ ∫ (t : E), ((lsmul ℝ ℝ) (w D t)) (φ x) ∂μ = 0
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c j‖
ah : Pairwise fun i j ↦ a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
C : a.r j ≤ 4
⊢ (1 - δ / 4) * (τ * a.r i) ≤ 1 * a.r i

Tactic:
by rw [← mul_assoc]; gcongr

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: G : Type u_1
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : Group G
inst✝⁸ : IsTopologicalGroup G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : LocallyCompactSpace G
μ' μ : Measure G
inst✝⁴ : μ.IsHaarMeasure
inst✝³ : IsFiniteMeasureOnCompacts μ'
inst✝² : μ'.IsMulLeftInvariant
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : μ'.InnerRegularCompactLTTop
s✝ : Set G
hs✝ : μ s✝ ≠ ∞
h's✝ : μ' s✝ ≠ ∞
c : ℝ≥0 := μ'.haarScalarFactor μ
s : Set G
s_meas : MeasurableSet s
hs : μ s < ∞
h's : μ' s < ∞
⊢ (c • μ) s ≠ ∞

Tactic:
simp [ENNReal.mul_eq_top, hs.ne]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace 𝕜 D
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ∞ω
f : D → E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 D
⊢ ContDiff 𝕜 (n + 1) f ↔
    Differentiable 𝕜 f ∧ (n = ω → AnalyticOnNhd 𝕜 f Set.univ) ∧ ∀ (y : D), ContDiff 𝕜 n fun x ↦ (fderiv 𝕜 f x) y

Tactic:
contDiff_succ_iff_fderiv,

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : NormedSpace 𝕜 D
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ∞ω
f : D → E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 D
⊢ Differentiable 𝕜 f ∧ (n = ω → AnalyticOnNhd 𝕜 f Set.univ) ∧ ContDiff 𝕜 n (fderiv 𝕜 f) ↔
    Differentiable 𝕜 f ∧ (n = ω → AnalyticOnNhd 𝕜 f Set.univ) ∧ ∀ (y : D), ContDiff 𝕜 n fun x ↦ (fderiv 𝕜 f x) y