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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
x✝ : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : ↑a ∈ Icc 0 1
hb01 : ↑b ∈ Icc 0 1
⊢ t • (↑e * (1 - ↑a) * ↑e) ≤ t • (↑e * (1 - ↑a) * ↑e) + s • (↑e * (1 - ↑b) * ↑e)

Tactic:
refine le_add_of_nonneg_right <| smul_nonneg h0s.le ?_

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
he : IsStarProjection e
a : A
ha : 0 ≤ a
ha1 : ‖a‖ ≤ 1
b : A
hb : 0 ≤ b
hb1 : ‖b‖ ≤ 1
x✝ : e ∈ openSegment ℝ a b
t s : ℝ
h0t : 0 < t
h0s : 0 < s
hts : t + s = 1
hlin : t • a + s • b = e
ha01 : ↑a ∈ Icc 0 1
hb01 : ↑b ∈ Icc 0 1
⊢ 0 ≤ ↑e * (1 - ↑b) * ↑e
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case hs
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e e' : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
z : Z
⊢ z ∈ ((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)).source ↔ z ∈ (e.symm.trans e').source

Tactic:
· simp_rw [OpenPartialHomeomorph.trans_source, e.lift_openEmbedding_symm_source, e.symm_source,
      e.lift_openEmbedding_symm, e'.lift_openEmbedding_source]
    refine ⟨fun ⟨hx, ⟨y, hy, hxy⟩⟩ ↦ ⟨hx, ?_⟩, fun ⟨hx, hx'⟩ ↦ ⟨hx, mem_image_of_mem f hx'⟩⟩
    rw [mem_preimage]; rw [comp_apply] at hxy
    exact (hf.injective hxy) ▸ hy

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 : Trivialization F proj
x : Z
ex : x ∈ e.source
⊢ map (Prod.fst ∘ ↑e) (𝓝 x) = 𝓝 (↑e x).1

Tactic:
← map_map,

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
e : Trivialization F proj
x : Z
ex : x ∈ e.source
⊢ map Prod.fst (map (↑e) (𝓝 x)) = 𝓝 (↑e x).1
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case inl
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
e : (x : ↑s) → Trivialization (F x) f
h : ∀ (x : ↑s), ↑x ∈ (e x).baseSet
h✝ : IsEmpty E
⊢ IsCoveringMapOn f s

Tactic:
exact .of_isEmpty _ _

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : RCLike 𝕜
p : A → Prop
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : ContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
⊢ cfc exp a = exp a

Tactic:
by
  conv_rhs => rw [← cfc_id 𝕜 a ha, cfc_apply id a ha]
  have h := cfcHom_continuous (R := 𝕜) ha
  have _ : ContinuousOn exp (spectrum 𝕜 a) := exp_continuous.continuousOn
  let +nondep : Algebra ℚ A := .restrictScalars ℚ 𝕜 A
  simp_rw [← map_exp _ h, cfc_apply exp a ha]
  congr 1
  ext
  simp [exp_continuousMap_eq]

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

Goal state before:
pp: z : ℝ
⊢ z + 2 * π = z + ↑1 * (2 * π)

Tactic:
Int.cast_one,

Goal state after:
z : ℝ
⊢ z + 2 * π = z + 1 * (2 * π)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
⊢ exp (log a) = a

Tactic:
by
  have ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0 := by grind
  rw [← real_exp_eq_normedSpace_exp .log, log, ← cfc_comp' Real.exp Real.log a (by fun_prop)]
  conv_rhs => rw [← cfc_id (R := ℝ) a]
  refine cfc_congr fun x hx => ?_
  grind [Real.exp_log]

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

Goal state before:
pp: z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : |(↑z).arg| < π / ↑n
h2 : |(n • ↑(↑z).arg).toReal| < s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ (↑(↑z).arg).toReal ∈ Ioo (-π / ↑n) (π / ↑n)

Tactic:
neg_div,

Goal state after:
z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : |(↑z).arg| < π / ↑n
h2 : |(n • ↑(↑z).arg).toReal| < s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ (↑(↑z).arg).toReal ∈ Ioo (-(π / ↑n)) (π / ↑n)
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
⊢ ‖↑(expUnitary x) - 1‖ < 2

Tactic:
← sq_lt_sq₀ (by positivity) (by positivity),

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
⊢ ‖↑(expUnitary x) - 1‖ ^ 2 < 2 ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
⊢ Continuous fun x ↦ ↑(↑x).arg

Tactic:
by
    rw [continuous_iff_continuousAt]
    intro x
    exact (continuousAt_arg_coe_angle x.coe_ne_zero).comp continuousAt_subtype_val

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

Goal state before:
pp: case h
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : t ∈ Set.Icc 0 1
hu : ‖↑u - 1‖ < 2
key : ‖t • argSelfAdjoint u‖ ≤ ‖argSelfAdjoint u‖
⊢ Real.cos ‖argSelfAdjoint u‖ ≤ Real.cos ‖t • argSelfAdjoint u‖

Tactic:
exact Real.cos_le_cos_of_nonneg_of_le_pi (by positivity) (norm_argSelfAdjoint_le_pi u) key

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
⊢ ‖↑(expUnitary x) - 1‖ < 2

Tactic:
← sq_lt_sq₀ (by positivity) (by positivity),

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
⊢ ‖↑(expUnitary x) - 1‖ ^ 2 < 2 ^ 2
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
⊢ span ℂ ↑(unitary A) = ⊤

Tactic:
rw [eq_top_iff]
  rintro x -
  obtain ⟨u, c, rfl, h⟩ := CStarAlgebra.exists_sum_four_unitary x
  exact sum_mem fun i _ ↦ smul_mem _ _ (subset_span (u i).2)

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

Goal state before:
pp: case mp
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
⊢ finrank k ↥(vectorSpan k (Set.range p)) = n → n ≤ finrank k ↥(vectorSpan k (Set.range p))

Tactic:
rintro rfl
    rfl

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✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
⊢ affineSpan k (Set.range p) = ⊤ ↔ Fintype.card ι = finrank k V + 1

Tactic:
constructor
  · intro h_tot
    let n := Fintype.card ι - 1
    have hn : Fintype.card ι = n + 1 :=
      (Nat.succ_pred_eq_of_pos (card_pos_of_affineSpan_eq_top k V P h_tot)).symm
    rw [hn, ← finrank_top, ← (vectorSpan_eq_top_of_affineSpan_eq_top k V P) h_tot,
      ← hi.finrank_vectorSpan hn]
  · intro hc
    rw [← finrank_top, ← direction_top k V P] at hc
    exact hi.affineSpan_eq_of_le_of_card_eq_finrank_add_one le_top hc

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

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
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k {p₂, p₃, p}
hne : p₂ ≠ p
⊢ AffineIndependent k ![p₁, p₂, p]

Tactic:
rw [affineIndependent_iff_not_collinear_set]

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
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k {p₂, p₃, p}
hne : p₂ ≠ p
⊢ ¬Collinear k {p₁, p₂, p}
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr.inr.inr.inr.refine_1
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i ↦ ‖f i‖ ^ q.toReal
⊢ {i | 1 ≤ ‖f i‖}.Finite

Tactic:
have H : { x : α | 1 ≤ ‖f x‖ ^ q.toReal }.Finite := by
        simpa using hf'.tendsto_cofinite_zero.eventually_lt_const (by simp)

Goal state after:
case inr.inr.inr.inr.inr.refine_1
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i ↦ ‖f i‖ ^ q.toReal
H : {x | 1 ≤ ‖f x‖ ^ q.toReal}.Finite
⊢ {i | 1 ≤ ‖f i‖}.Finite
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
hp' : 1 / p.toReal ≠ 0
⊢ (∑' (i : α), ‖↑0 i‖ ^ p.toReal) ^ (1 / p.toReal) = 0

Tactic:
simpa [Real.zero_rpow hp.ne'] using Real.zero_rpow hp'

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

Goal state before:
pp: I : Type u_5
B : I → Type u_6
inst✝¹ : (i : I) → NormedRing (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
⊢ 1 ∈ upperBounds (Set.range fun i ↦ ‖1 i‖)

Tactic:
by rintro i ⟨i, rfl⟩; exact norm_one.le

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
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝³ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this✝² : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this✝¹ : l.NeBot
hr : 0 < r
this✝ :
  TendstoUniformlyOn (fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0 (l ×ˢ l) (Metric.ball x r) ∧
    TendstoUniformlyOn (fun n x_1 ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (Metric.ball x r)
this :
  TendstoUniformlyOn ((-fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) + -fun n x_1 ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
    (Metric.ball x r)
⊢ TendstoUniformlyOn (fun n z ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l) (Metric.ball x r)

Tactic:
refine this.congr ?_

Goal state after:
ι : 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
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝³ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this✝² : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this✝¹ : l.NeBot
hr : 0 < r
this✝ :
  TendstoUniformlyOn (fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0 (l ×ˢ l) (Metric.ball x r) ∧
    TendstoUniformlyOn (fun n x_1 ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (Metric.ball x r)
this :
  TendstoUniformlyOn ((-fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) + -fun n x_1 ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
    (Metric.ball x r)
⊢ ∀ᶠ (n : ι × ι) in l ×ˢ l,
    Set.EqOn (((-fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) + -fun n x_1 ↦ f n.1 x - f n.2 x) n)
      (fun z ↦ -f n.1 z + f n.2 z) (Metric.ball x r)
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hfg' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < ε
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x,
    dist (0 n.2) (-((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x)) + (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε

Tactic:
obtain ⟨q, hqpos, hqε⟩ := exists_pos_rat_lt hε

Goal state after:
ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hfg' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < ε
ε : ℝ
hε : ε > 0
q : ℚ
hqpos : 0 < q
hqε : ↑q < ε
⊢ ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x,
    dist (0 n.2) (-((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x)) + (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε
Module: Mathlib.Analysis.InnerProductSpace.Calculus

Goal state before:
pp: n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : ‖y‖ < 1
⊢ 0 < 1 - ‖y‖ ^ 2

Tactic:
← _root_.abs_one,

Goal state after:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : ‖y‖ < |1|
⊢ 0 < 1 - ‖y‖ ^ 2
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
x₀ : H
s : Set H
inst✝ : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : H → ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_int : IntervalIntegrable (F x₀) μ a b
h_bound :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, ‖F' x_1 x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), ∀ x_1 ∈ s, HasFDerivAt (fun x_2 ↦ F x_2 x) (F' x_1 x) x_1) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), ∀ x_1 ∈ s, HasFDerivAt (fun x_2 ↦ F x_2 x) (F' x_1 x) x_1
hF'_meas :
  AEStronglyMeasurable (F' x₀) (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable (F' x₀) (μ.restrict (Set.Ioc b a))
hF_meas :
  (∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc a b))) ∧
    ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc b a))
⊢ HasFDerivAt (fun x ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀

Tactic:
exact
    (hasFDerivAt_integral_of_dominated_of_fderiv_le hs hF_meas.1 hF_int.1 hF'_meas.1 h_bound.1
          bound_integrable.1 h_diff.1).sub
      (hasFDerivAt_integral_of_dominated_of_fderiv_le hs hF_meas.2 hF_int.2 hF'_meas.2 h_bound.2
        bound_integrable.2 h_diff.2)

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

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
R : ℝ
⊢ ∫ (x : E), f (R • x) ∂μ = |(R ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ

Tactic:
by
  by_cases hF : CompleteSpace F; swap
  · simp [integral, hF]
  rcases eq_or_ne R 0 with (rfl | hR)
  · simp only [zero_smul, integral_const]
    rcases Nat.eq_zero_or_pos (finrank ℝ E) with (hE | hE)
    · have : Subsingleton E := finrank_zero_iff.1 hE
      have : f = fun _ => f 0 := by ext x; rw [Subsingleton.elim x 0]
      conv_rhs => rw [this]
      simp only [hE, pow_zero, inv_one, abs_one, one_smul, integral_const]
    · have : Nontrivial E := finrank_pos_iff.1 hE
      simp [zero_pow hE.ne', measure_univ_of_isAddLeftInvariant, measureReal_def]
  · calc
      (∫ x, f (R • x) ∂μ) = ∫ y, f y ∂Measure.map (fun x => R • x) μ :=
        (integral_map_equiv (Homeomorph.smul (isUnit_iff_ne_zero.2 hR).unit).toMeasurableEquiv
            f).symm
      _ = |(R ^ finrank ℝ E)⁻¹| • ∫ x, f x ∂μ := by
        simp only [map_addHaar_smul μ hR, integral_smul_measure, ENNReal.toReal_ofReal, abs_nonneg]

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

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
R : ℝ
hR : 0 ≤ R
⊢ |R ^ finrank ℝ E| • ∫ (x : E), f x ∂μ = R ^ finrank ℝ E • ∫ (x : E), f x ∂μ

Tactic:
abs_of_nonneg (pow_nonneg hR _)

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
R : ℝ
hR : 0 ≤ R
⊢ R ^ finrank ℝ E • ∫ (x : E), f x ∂μ = R ^ finrank ℝ E • ∫ (x : E), f x ∂μ
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : SecondCountableTopology G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : SFinite μ
inst✝¹ : NormedSpace ℝ E'
inst✝ : CompleteSpace E'
ι : Type u_1
g : ι → G → E'
l : Filter ι
x₀ : G
z₀ : E'
φ : ι → G → ℝ
k : ι → G
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : G), 0 ≤ φ i x
hiφ : ∀ᶠ (i : ι) in l, ∫ (x : G), φ i x ∂μ = 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ t ∈ 𝓝 0, ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ pa,
      (∀ᶠ (i : ι) in l, pa i) ∧ ∃ ε_1 > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : G⦄, dist x x₀ < ε_1 → dist (uncurry g (i, x)) z₀ < ε
ε : ℝ
hε : ε > 0
h2ε : 0 < ε / 3
p : ι → Prop
hp : ∀ᶠ (i : ι) in l, p i
δ : ℝ
hδ : δ > 0
hgδ : ∀ ⦃i : ι⦄, p i → ∀ ⦃x : G⦄, dist x x₀ < δ → dist (g i x) z₀ < ε / 3
h2k : ∀ᶠ (x : ι) in l, dist (k x) x₀ < δ / 2
h2φ : ∀ᶠ (x : ι) in l, support (φ x) ⊆ ball 0 (δ / 2)
i : ι
hpi : p i
hki : dist (k i) x₀ < δ / 2
hφi : support (φ i) ⊆ ball 0 (δ / 2)
hnφi : ∀ (x : G), 0 ≤ φ i x
hiφi : ∫ (x : G), φ i x ∂μ = 1
hmgi : AEStronglyMeasurable (g i) μ
hgi : dist (g i (k i)) z₀ < ε / 3
x' : G
⊢ x' ∈ ball (k i) (δ / 2) → dist (g i x') (g i (k i)) ≤ ε / 3 + ε / 3

Tactic:
hx'

Goal state after:
G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : SecondCountableTopology G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : SFinite μ
inst✝¹ : NormedSpace ℝ E'
inst✝ : CompleteSpace E'
ι : Type u_1
g : ι → G → E'
l : Filter ι
x₀ : G
z₀ : E'
φ : ι → G → ℝ
k : ι → G
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : G), 0 ≤ φ i x
hiφ : ∀ᶠ (i : ι) in l, ∫ (x : G), φ i x ∂μ = 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ t ∈ 𝓝 0, ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ pa,
      (∀ᶠ (i : ι) in l, pa i) ∧ ∃ ε_1 > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : G⦄, dist x x₀ < ε_1 → dist (uncurry g (i, x)) z₀ < ε
ε : ℝ
hε : ε > 0
h2ε : 0 < ε / 3
p : ι → Prop
hp : ∀ᶠ (i : ι) in l, p i
δ : ℝ
hδ : δ > 0
hgδ : ∀ ⦃i : ι⦄, p i → ∀ ⦃x : G⦄, dist x x₀ < δ → dist (g i x) z₀ < ε / 3
h2k : ∀ᶠ (x : ι) in l, dist (k x) x₀ < δ / 2
h2φ : ∀ᶠ (x : ι) in l, support (φ x) ⊆ ball 0 (δ / 2)
i : ι
hpi : p i
hki : dist (k i) x₀ < δ / 2
hφi : support (φ i) ⊆ ball 0 (δ / 2)
hnφi : ∀ (x : G), 0 ≤ φ i x
hiφi : ∫ (x : G), φ i x ∂μ = 1
hmgi : AEStronglyMeasurable (g i) μ
hgi : dist (g i (k i)) z₀ < ε / 3
x' : G
hx' : x' ∈ ball (k i) (δ / 2)
⊢ dist (g i x') (g i (k i)) ≤ ε / 3 + ε / 3
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: 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) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
⊢ ∃ T, T.Countable ∧ ⋃ f ∈ T, support ↑f = s

Tactic:
have : ⋃ f : ι, (f : E → ℝ).support = s := by
      refine Subset.antisymm (iUnion_subset fun f => f.2.1) ?_
      intro x hx
      rcases exists_contDiff_tsupport_subset (hs.mem_nhds hx) with ⟨f, hf⟩
      let g : ι := ⟨f, (subset_tsupport f).trans hf.1, hf.2.1, hf.2.2.1, hf.2.2.2.1⟩
      have : x ∈ support (g : E → ℝ) := by
        simp only [g, hf.2.2.2.2, mem_support, Ne, one_ne_zero, not_false_iff]
      exact mem_iUnion_of_mem _ this
    simp_rw [← this]
    apply isOpen_iUnion_countable
    rintro ⟨f, hf⟩
    exact hf.2.2.1.continuous.isOpen_support

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

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ (∫ (x : E), ↑f x ∂μ)⁻¹ • ∫ (x : E), ↑f x ∂μ = 1

Tactic:
exact inv_mul_cancel₀ f.integral_pos.ne'

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

Goal state before:
pp: case hd
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
x : E
⊢ 0 < μ.real (closedBall c f.rIn)

Tactic:
exact ENNReal.toReal_pos (measure_closedBall_pos _ _ f.rIn_pos).ne' measure_closedBall_lt_top.ne

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 : ℝ
Dpos : 0 < D
⊢ HasCompactSupport (w D)

Tactic:
rw [hasCompactSupport_def, w_support E Dpos, closure_ball (0 : E) Dpos.ne']

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
⊢ IsCompact (closedBall 0 D)
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin (N + 1)
hi : i < last N
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N)) ∧
    (a.r (last N))⁻¹ * a.r (last N) ≤ (a.r (last N))⁻¹ * (τ * a.r i)

Tactic:
have ⟨H₁, H₂⟩ := a.hlast i hi

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin (N + 1)
hi : i < last N
H₁ : a.r i ≤ dist (a.c i) (a.c (last N))
H₂ : a.r (last N) ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N)) ∧
    (a.r (last N))⁻¹ * a.r (last N) ≤ (a.r (last N))⁻¹ * (τ * a.r i)