mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
⊢ ∀ a ∈ s ×ˢ univ, AEStronglyMeasurable (fun a_2 ↦ (L (f a_2)) (g a.1 (a.2 - a_2))) μ

Tactic:
rintro ⟨p, x⟩ ⟨hp, -⟩

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
ε C : ℝ
εpos : 0 < ε
h₀ε : ball q₀.1 ε ⊆ s
hε : ∀ (p : P) (x : G), ‖p - q₀.1‖ < ε → ‖g' (p, x)‖ ≤ C
p : P
x : G
hp : (p, x).1 ∈ s
⊢ AEStronglyMeasurable (fun a ↦ (L (f a)) (g (p, x).1 ((p, x).2 - a))) μ
Module: Mathlib.Topology.Metrizable.Urysohn

Goal state before:
pp: 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 < δ
h_fin : {UV | δ ≤ ε UV}.Finite
UV : ↑s
x✝ : UV ∈ {UV | δ ≤ ε UV}
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist ((F x_1) UV) ((F x) UV) ≤ δ

Tactic:
exact (f UV).continuous.tendsto x (closedBall_mem_nhds _ δ0)

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

Goal state before:
pp: case succ.refine_1
𝕜 : Type u𝕜
E : Type uE
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedSpace 𝕜 E
G P : Type uP
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : NormedSpace 𝕜 G
inst✝⁶ : NormedAddCommGroup P
inst✝⁵ : NormedSpace 𝕜 P
f : G → E
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hf : LocallyIntegrable f μ
n : ℕ
ih :
  ∀ {E' F : Type uP} [inst : NormedAddCommGroup E'] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 E']
    [inst_3 : NormedSpace ℝ F] [inst_4 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'},
    (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
      ContDiffOn 𝕜 (↑↑n) (↿g) (s ×ˢ univ) → ContDiffOn 𝕜 (↑↑n) (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)
E' F : Type uP
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg :
  DifferentiableOn 𝕜 (↿g) (s ×ˢ univ) ∧
    (↑n = ⊤ → AnalyticOn 𝕜 (↿g) (s ×ˢ univ)) ∧ ContDiffOn 𝕜 (↑n) (fderiv 𝕜 ↿g) (s ×ˢ univ)
f' : P → G → P × G →L[𝕜] F := fun p a ↦ (f ⋆[precompR (P × G) L, μ] fun x ↦ fderiv 𝕜 (uncurry g) (p, x)) a
A : ∀ (q₀ : P × G), q₀.1 ∈ s → HasFDerivAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (f' q₀.1 q₀.2) q₀
⊢ DifferentiableOn 𝕜 (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)

Tactic:
rintro ⟨p, x⟩ ⟨hp, -⟩

Goal state after:
case succ.refine_1
𝕜 : Type u𝕜
E : Type uE
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedSpace 𝕜 E
G P : Type uP
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : NormedSpace 𝕜 G
inst✝⁶ : NormedAddCommGroup P
inst✝⁵ : NormedSpace 𝕜 P
f : G → E
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hf : LocallyIntegrable f μ
n : ℕ
ih :
  ∀ {E' F : Type uP} [inst : NormedAddCommGroup E'] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 E']
    [inst_3 : NormedSpace ℝ F] [inst_4 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'},
    (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
      ContDiffOn 𝕜 (↑↑n) (↿g) (s ×ˢ univ) → ContDiffOn 𝕜 (↑↑n) (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)
E' F : Type uP
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg :
  DifferentiableOn 𝕜 (↿g) (s ×ˢ univ) ∧
    (↑n = ⊤ → AnalyticOn 𝕜 (↿g) (s ×ˢ univ)) ∧ ContDiffOn 𝕜 (↑n) (fderiv 𝕜 ↿g) (s ×ˢ univ)
f' : P → G → P × G →L[𝕜] F := fun p a ↦ (f ⋆[precompR (P × G) L, μ] fun x ↦ fderiv 𝕜 (uncurry g) (p, x)) a
A : ∀ (q₀ : P × G), q₀.1 ∈ s → HasFDerivAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (f' q₀.1 q₀.2) q₀
p : P
x : G
hp : (p, x).1 ∈ s
⊢ DifferentiableWithinAt 𝕜 (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ) (p, x)
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
k : ℕ
hk : k < N
⊢ ∃ j < i,
    (closedBall (p.c (p.index j)) (p.r (p.index j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
      k = p.color j

Tactic:
← Inf_eq_N

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
k : ℕ
hk : k < sInf (univ \ A)
⊢ ∃ j < i,
    (closedBall (p.c (p.index j)) (p.r (p.index j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
      k = p.color j
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
E : Type uE
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedSpace 𝕜 E
G P : Type uP
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : NormedSpace 𝕜 G
inst✝⁶ : NormedAddCommGroup P
inst✝⁵ : NormedSpace 𝕜 P
f : G → E
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hf : LocallyIntegrable f μ
n : ℕ
ih :
  ∀ {E' F : Type uP} [inst : NormedAddCommGroup E'] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 E']
    [inst_3 : NormedSpace ℝ F] [inst_4 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'},
    (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
      ContDiffOn 𝕜 (↑↑n) (↿g) (s ×ˢ univ) → ContDiffOn 𝕜 (↑↑n) (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)
E' F : Type uP
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg :
  DifferentiableOn 𝕜 (↿g) (s ×ˢ univ) ∧
    (↑n = ⊤ → AnalyticOn 𝕜 (↿g) (s ×ˢ univ)) ∧ ContDiffOn 𝕜 (↑n) (fderiv 𝕜 ↿g) (s ×ˢ univ)
f' : P → G → P × G →L[𝕜] F := ⋯
A : ∀ (q₀ : P × G), q₀.1 ∈ s → HasFDerivAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (f' q₀.1 q₀.2) q₀
H : ContDiffOn 𝕜 (↑n) (↿f') (s ×ˢ univ)
⊢ ∀ x ∈ s ×ˢ univ, fderiv 𝕜 (fun q ↦ (f ⋆[L, μ] g q.1) q.2) x = ↿f' x

Tactic:
rintro ⟨p, x⟩ ⟨hp, -⟩

Goal state after:
𝕜 : Type u𝕜
E : Type uE
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedSpace 𝕜 E
G P : Type uP
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : NormedSpace 𝕜 G
inst✝⁶ : NormedAddCommGroup P
inst✝⁵ : NormedSpace 𝕜 P
f : G → E
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hf : LocallyIntegrable f μ
n : ℕ
ih :
  ∀ {E' F : Type uP} [inst : NormedAddCommGroup E'] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 E']
    [inst_3 : NormedSpace ℝ F] [inst_4 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'},
    (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
      ContDiffOn 𝕜 (↑↑n) (↿g) (s ×ˢ univ) → ContDiffOn 𝕜 (↑↑n) (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)
E' F : Type uP
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg :
  DifferentiableOn 𝕜 (↿g) (s ×ˢ univ) ∧
    (↑n = ⊤ → AnalyticOn 𝕜 (↿g) (s ×ˢ univ)) ∧ ContDiffOn 𝕜 (↑n) (fderiv 𝕜 ↿g) (s ×ˢ univ)
f' : P → G → P × G →L[𝕜] F := fun p a ↦ (f ⋆[precompR (P × G) L, μ] fun x ↦ fderiv 𝕜 (uncurry g) (p, x)) a
A : ∀ (q₀ : P × G), q₀.1 ∈ s → HasFDerivAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (f' q₀.1 q₀.2) q₀
H : ContDiffOn 𝕜 (↑n) (↿f') (s ×ˢ univ)
p : P
x : G
hp : (p, x).1 ∈ s
⊢ fderiv 𝕜 (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (p, x) = ↿f' (p, x)
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
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 0

Tactic:
have Bx : φ x = 0 := B _ (mem_ball_self Dpos)

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
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 0
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: case refine_3
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
f : G → E
n : ℕ∞
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ univ)
eG : Type (max uG uE' uF uP) := ⋯
this✝¹ : MeasurableSpace eG := ⋯
this✝ : BorelSpace eG
eE' : Type (max uE' uG uF uP) := ⋯
eF : Type (max uF uG uE' uP) := ⋯
eP : Type (max uP uG uE' uF) := ⋯
isoG : eG ≃L[𝕜] G := ⋯
isoE' : eE' ≃L[𝕜] E' := ⋯
isoF : eF ≃L[𝕜] F := ⋯
isoP : eP ≃L[𝕜] P := ⋯
ef : eG → E := ⋯
eμ : Measure eG := ⋯
eg : eP → eG → eE' := ⋯
eL : E →L[𝕜] eE' →L[𝕜] eF := ⋯
R : eP × eG → eF := ⋯
hek : IsCompact (⇑isoG ⁻¹' k)
hes : IsOpen[ULift.topologicalSpace] (⇑isoP ⁻¹' s)
⊢ MapsTo (⇑(isoP.prodCongr isoG)) ((⇑isoP ⁻¹' s) ×ˢ univ) (s ×ˢ univ)

Tactic:
rintro ⟨p, x⟩ ⟨hp, -⟩

Goal state after:
case refine_3
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
f : G → E
n : ℕ∞
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this✝¹ : MeasurableSpace eG := borel eG
this✝ : BorelSpace eG
eE' : Type (max uE' uG uF uP) := ULift.{max uG uF uP, uE'} E'
eF : Type (max uF uG uE' uP) := ULift.{max uG uE' uP, uF} F
eP : Type (max uP uG uE' uF) := ULift.{max uG uE' uF, uP} P
isoG : eG ≃L[𝕜] G := ContinuousLinearEquiv.ulift
isoE' : eE' ≃L[𝕜] E' := ContinuousLinearEquiv.ulift
isoF : eF ≃L[𝕜] F := ContinuousLinearEquiv.ulift
isoP : eP ≃L[𝕜] P := ContinuousLinearEquiv.ulift
ef : eG → E := f ∘ ⇑isoG
eμ : Measure eG := Measure.map (⇑isoG.symm) μ
eg : eP → eG → eE' := fun ep ex ↦ isoE'.symm (g (isoP ep) (isoG ex))
eL : E →L[𝕜] eE' →L[𝕜] eF := ↑(isoE'.arrowCongr isoF).symm ∘SL L
R : eP × eG → eF := fun q ↦ (ef ⋆[eL, eμ] eg q.1) q.2
hek : IsCompact (⇑isoG ⁻¹' k)
hes : IsOpen[ULift.topologicalSpace] (⇑isoP ⁻¹' s)
p : eP
x : eG
hp : (p, x).1 ∈ ⇑isoP ⁻¹' s
⊢ (isoP.prodCongr isoG) (p, x) ∈ s ×ˢ univ
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
f : G → E
n : ℕ∞
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ univ)
eG : Type (max uG uE' uF uP) := ⋯
this✝¹ : MeasurableSpace eG := ⋯
this✝ : BorelSpace eG
eE' : Type (max uE' uG uF uP) := ⋯
eF : Type (max uF uG uE' uP) := ⋯
eP : Type (max uP uG uE' uF) := ⋯
isoG : eG ≃L[𝕜] G := ⋯
isoE' : eE' ≃L[𝕜] E' := ⋯
isoF : eF ≃L[𝕜] F := ⋯
isoP : eP ≃L[𝕜] P := ⋯
ef : eG → E := ⋯
eμ : Measure eG := ⋯
eg : eP → eG → eE' := ⋯
eL : E →L[𝕜] eE' →L[𝕜] eF := ⋯
R : eP × eG → eF := ⋯
R_contdiff : ContDiffOn 𝕜 (↑n) R ((⇑isoP ⁻¹' s) ×ˢ univ)
⊢ MapsTo (⇑(isoP.prodCongr isoG).symm) (s ×ˢ univ) ((⇑isoP ⁻¹' s) ×ˢ univ)

Tactic:
rintro ⟨p, x⟩ ⟨hp, -⟩

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
f : G → E
n : ℕ∞
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ univ)
eG : Type (max uG uE' uF uP) := ULift.{max uE' uF uP, uG} G
this✝¹ : MeasurableSpace eG := borel eG
this✝ : BorelSpace eG
eE' : Type (max uE' uG uF uP) := ULift.{max uG uF uP, uE'} E'
eF : Type (max uF uG uE' uP) := ULift.{max uG uE' uP, uF} F
eP : Type (max uP uG uE' uF) := ULift.{max uG uE' uF, uP} P
isoG : eG ≃L[𝕜] G := ContinuousLinearEquiv.ulift
isoE' : eE' ≃L[𝕜] E' := ContinuousLinearEquiv.ulift
isoF : eF ≃L[𝕜] F := ContinuousLinearEquiv.ulift
isoP : eP ≃L[𝕜] P := ContinuousLinearEquiv.ulift
ef : eG → E := f ∘ ⇑isoG
eμ : Measure eG := Measure.map (⇑isoG.symm) μ
eg : eP → eG → eE' := fun ep ex ↦ isoE'.symm (g (isoP ep) (isoG ex))
eL : E →L[𝕜] eE' →L[𝕜] eF := ↑(isoE'.arrowCongr isoF).symm ∘SL L
R : eP × eG → eF := fun q ↦ (ef ⋆[eL, eμ] eg q.1) q.2
R_contdiff : ContDiffOn 𝕜 (↑n) R ((⇑isoP ⁻¹' s) ×ˢ univ)
p : P
x : G
hp : (p, x).1 ∈ s
⊢ (isoP.prodCongr isoG).symm (p, x) ∈ (⇑isoP ⁻¹' s) ×ˢ univ
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 j : Fin N.succ
hij : i ≠ j
⊢ (fun i j ↦
      (a.r (last N))⁻¹ * a.r i ≤
            dist ((a.r (last N))⁻¹ • (a.c i - a.c (last N))) ((a.r (last N))⁻¹ • (a.c j - a.c (last N))) ∧
          (a.r (last N))⁻¹ * a.r j ≤ τ * ((a.r (last N))⁻¹ * a.r i) ∨
        (a.r (last N))⁻¹ * a.r j ≤
            dist ((a.r (last N))⁻¹ • (a.c j - a.c (last N))) ((a.r (last N))⁻¹ • (a.c i - a.c (last N))) ∧
          (a.r (last N))⁻¹ * a.r i ≤ τ * ((a.r (last N))⁻¹ * a.r j))
    i j

Tactic:
simp (disch := positivity) only [dist_smul₀, dist_sub_right, mul_left_comm τ,
      Real.norm_of_nonneg]
    rcases a.h hij with (⟨H₁, H₂⟩ | ⟨H₁, H₂⟩) <;> [left; right] <;> constructor <;> 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✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst✝⁷] k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x ↦ x • k}
f : ℕ → G
m_max : Maximal (fun x ↦ x ∈ A) (range f)
hms : range f ⊆ s
hdj : (range f).PairwiseDisjoint fun x ↦ x • k
sm : s ⊆ ⋃ x ∈ range f, x • (k * k⁻¹)
hm : (range f).Nonempty
h'm : (range f).Countable
i j : ℕ
⊢ MeasurableSet (f j • (k * k⁻¹))

Tactic:
have : IsClosed (k • k⁻¹) := IsClosed.smul_left_of_isCompact k_closed.inv k_comp

Goal state after:
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✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst✝⁷] k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x ↦ x • k}
f : ℕ → G
m_max : Maximal (fun x ↦ x ∈ A) (range f)
hms : range f ⊆ s
hdj : (range f).PairwiseDisjoint fun x ↦ x • k
sm : s ⊆ ⋃ x ∈ range f, x • (k * k⁻¹)
hm : (range f).Nonempty
h'm : (range f).Countable
i j : ℕ
this : IsClosed[inst✝⁷] (k • k⁻¹)
⊢ MeasurableSet (f j • (k * k⁻¹))
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✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst✝⁷] k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x ↦ x • k}
f : ℕ → G
m_max : Maximal (fun x ↦ x ∈ A) (range f)
hms : range f ⊆ s
hdj : (range f).PairwiseDisjoint fun x ↦ x • k
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ y, f y • (k * k⁻¹)
⊢ s = ⋃ n, s ∩ f n • (k * k⁻¹)

Tactic:
rwa [← inter_iUnion, eq_comm, inter_eq_left]

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

Goal state before:
pp: case inl
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : a ∈ Icc a b
hc : IsMinOn g (Icc a b) a
⊢ a ∈ Ioo a b

pp: case inr
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
hac : a < c
⊢ c ∈ Ioo a b

Tactic:
· refine absurd (sub_nonneg.1 <| nonneg_of_mul_nonneg_right ?_ (sub_pos.2 hab'))
        (not_le_of_gt hma)
      have : b - a ∈ posTangentConeAt (Icc a b) a :=
        sub_mem_posTangentConeAt_of_segment_subset (segment_eq_Icc hab ▸ Subset.rfl)
      simpa only [ContinuousLinearMap.smulRight_apply, one_apply_eq_self]
        using! hc.localize.hasFDerivWithinAt_nonneg (hg a (left_mem_Icc.2 hab)) this

Goal state after:
case inr
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun x ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
hac : a < c
⊢ c ∈ Ioo a b