mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.Completion

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 := { toFun := fun x ↦ ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }
this : Continuous fun p ↦ (inner' p.1) p.2
⊢ Continuous (uncurry (inner 𝕜))

Tactic:
rw [Completion.toInner, inner, uncurry_curry _]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 := { toFun := fun x ↦ ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }
this : Continuous fun p ↦ (inner' p.1) p.2
⊢ Continuous (⋯.extend (uncurry (inner 𝕜)))
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : a✝ ∈ closedBall 0 1
hy : b✝ ∈ closedBall 0 1
⊢ a✝ * b✝ ∈ closedBall 0 1

Tactic:
by
    rw [mem_closedBall_zero_iff] at *
    exact (norm_mul_le _ _).trans (mul_le_one₀ hx (norm_nonneg _) hy)

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

Goal state before:
pp: E : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
u : Circle
v : E
⊢ ‖↑u‖ * ‖v‖ = ‖v‖

Tactic:
norm_eq_of_mem_sphere,

Goal state after:
E : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
u : Circle
v : E
⊢ 1 * ‖v‖ = ‖v‖
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : Z.Fiber x
hx : { proj := x, snd := v } ∈ Z.proj ⁻¹' Z.baseSet i
⊢ {
      proj :=
        ({ proj := x, snd := v }.proj,
            Z.coordChange (Z.indexAt { proj := x, snd := v }.proj) i { proj := x, snd := v }.proj
              { proj := x, snd := v }.snd).1,
      snd :=
        Z.coordChange i
          (Z.indexAt
            ({ proj := x, snd := v }.proj,
                Z.coordChange (Z.indexAt { proj := x, snd := v }.proj) i { proj := x, snd := v }.proj
                  { proj := x, snd := v }.snd).1)
          ({ proj := x, snd := v }.proj,
              Z.coordChange (Z.indexAt { proj := x, snd := v }.proj) i { proj := x, snd := v }.proj
                { proj := x, snd := v }.snd).1
          ({ proj := x, snd := v }.proj,
              Z.coordChange (Z.indexAt { proj := x, snd := v }.proj) i { proj := x, snd := v }.proj
                { proj := x, snd := v }.snd).2 } =
    { proj := x, snd := v }

Tactic:
replace hx : x ∈ Z.baseSet i := hx

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : Z.Fiber x
hx : x ∈ Z.baseSet i
⊢ {
      proj :=
        ({ proj := x, snd := v }.proj,
            Z.coordChange (Z.indexAt { proj := x, snd := v }.proj) i { proj := x, snd := v }.proj
              { proj := x, snd := v }.snd).1,
      snd :=
        Z.coordChange i
          (Z.indexAt
            ({ proj := x, snd := v }.proj,
                Z.coordChange (Z.indexAt { proj := x, snd := v }.proj) i { proj := x, snd := v }.proj
                  { proj := x, snd := v }.snd).1)
          ({ proj := x, snd := v }.proj,
              Z.coordChange (Z.indexAt { proj := x, snd := v }.proj) i { proj := x, snd := v }.proj
                { proj := x, snd := v }.snd).1
          ({ proj := x, snd := v }.proj,
              Z.coordChange (Z.indexAt { proj := x, snd := v }.proj) i { proj := x, snd := v }.proj
                { proj := x, snd := v }.snd).2 } =
    { proj := x, snd := v }
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
b✝ : B
y : E b✝
T✝ : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceSubtype] fun ex ↦ ⟨T.lift ↑ex.1 ↑ex.2, ⋯⟩

Tactic:
apply Continuous.subtype_mk

Goal state after:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
b✝ : B
y : E b✝
T✝ : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦ T.lift ↑x.1 ↑x.2
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
I : Type u_3
inst✝ : TopologicalSpace I
hs : IsOpen[inst✝¹] s
hfs : IsOpen[inst✝²] (f ⁻¹' s)
x✝¹ : X
hx : x✝¹ ∈ s
h : IsEvenlyCovered (fun e ↦ f ↑e) x✝¹ I
inst : DiscreteTopology I
U : Set X
hxU : x✝¹ ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun e ↦ f ↑e) ⁻¹' U)
H : ↑((fun e ↦ f ↑e) ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑((fun e ↦ f ↑e) ⁻¹' U)), ↑(H x).1 = (fun e ↦ f ↑e) ↑x
x✝ : Nonempty I
hUs : U ⊆ s
this : Subtype.val '' (fun e ↦ f ↑e) ⁻¹' U = f ⁻¹' U
x : ↑(f ⁻¹' U)
⊢ (⋯.homeomorphImage ((fun e ↦ f ↑e) ⁻¹' U)).symm ((Homeomorph.setCongr this).symm x) = ⟨⟨↑x, ⋯⟩, ⋯⟩

Tactic:
rw [Homeomorph.symm_apply_eq]

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
hs : IsOpen[inst✝¹] s
hfs : IsOpen[inst✝²] (f ⁻¹' s)
x✝¹ : X
hx : x✝¹ ∈ s
h : IsEvenlyCovered (fun e ↦ f ↑e) x✝¹ I
inst : DiscreteTopology I
U : Set X
hxU : x✝¹ ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun e ↦ f ↑e) ⁻¹' U)
H : ↑((fun e ↦ f ↑e) ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑((fun e ↦ f ↑e) ⁻¹' U)), ↑(H x).1 = (fun e ↦ f ↑e) ↑x
x✝ : Nonempty I
hUs : U ⊆ s
this : Subtype.val '' (fun e ↦ f ↑e) ⁻¹' U = f ⁻¹' U
x : ↑(f ⁻¹' U)
⊢ (Homeomorph.setCongr this).symm x = (⋯.homeomorphImage ((fun e ↦ f ↑e) ⁻¹' U)) ⟨⟨↑x, ⋯⟩, ⋯⟩
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ (range ⇑(x.path y))ᶜ = ⇑(y.path x) '' Ioo 0 1

Tactic:
rw [range_path, ← Ioc_insert_left (by simp), image_insert_eq,
    ← path_image_Ioc_of_ne h, ← union_singleton, compl_union, compl_path_image_Ioc h,
    ← Ioo_insert_right (by simp), image_insert_eq, (y.path x).target, exp_arg,
    insert_inter_of_notMem (by simp), inter_eq_left]

Goal state after:
x y : Circle
h : x ≠ y
⊢ ⇑(y.path x) '' Ioo 0 1 ⊆ {x}ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: θ₁ θ₂ : Angle
⊢ (θ₁ + θ₂).toCircle = θ₁.toCircle * θ₂.toCircle

Tactic:
induction θ₁ using Angle.induction_on

Goal state after:
case h
θ₂ : Angle
x✝ : ℝ
⊢ (↑x✝ + θ₂).toCircle = (↑x✝).toCircle * θ₂.toCircle
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
this : ContinuousOn arg (spectrum ℂ ↑u)
y : ℂ
hy : y ∈ spectrum ℂ ↑u
hy₁ : ‖y‖ = 1
⊢ (I * ↑y.arg).re = (log y).re

Tactic:
by simp [log_re, spectrum.norm_eq_one_of_unitary u.2 hy]

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u v : ↥(unitary A)
⊢ ‖↑u - ↑v‖ = ‖(↑u * ↑(star v) - 1) * ↑v‖

Tactic:
by simp [sub_mul, mul_assoc]

Goal state after:
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✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ 0 ≤ re ⟪x, (adjoint T * T) x⟫_𝕜

Tactic:
simp only [Module.End.mul_apply, adjoint_inner_right, inner_self_eq_norm_sq_to_K]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ 0 ≤ re (↑‖T x‖ ^ 2)
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 ι
inst✝ : Nonempty ι
p : ι → P
hi : AffineIndependent k p
⊢ finrank k ↥(vectorSpan k (Set.range p)) + 1 = Fintype.card ι

Tactic:
hi.finrank_vectorSpan (tsub_add_cancel_of_le _).symm,

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 ι
inst✝ : Nonempty ι
p : ι → P
hi : AffineIndependent k p
⊢ Fintype.card ι - 1 + 1 = Fintype.card ι

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 ι
inst✝ : Nonempty ι
p : ι → P
hi : AffineIndependent k p
⊢ 1 ≤ Fintype.card ι
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
⊢ g.conjStarAlgEquiv = f.conjStarAlgEquiv ↔ ∃ α, f = α • g

Tactic:
simp_rw [StarAlgEquiv.ext_iff, LinearIsometryEquiv.ext_iff, conjStarAlgEquiv_apply,
    ← eq_toContinuousLinearMap_symm_comp, ← comp_assoc, toContinuousLinearEquiv_symm,
    eq_comp_toContinuousLinearMap_symm,
    comp_assoc, ← comp_assoc _ (f : H →L[𝕜] K), comp_coe, ← ContinuousLinearMap.mul_def,
    ← Subalgebra.mem_center_iff (R := 𝕜), Algebra.IsCentral.center_eq_bot, ← comp_coe,
    Algebra.mem_bot, Set.mem_range, Algebra.algebraMap_eq_smul_one]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
f g : H ≃ₗᵢ[𝕜] K
⊢ (∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f) ↔ ∃ α, ∀ (x : H), f x = (α • g) x
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
s : Set P
⊢ Collinear k s ↔ ∃ p₀ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀

Tactic:
by
  rcases Set.eq_empty_or_nonempty s with (rfl | ⟨⟨p₁, hp₁⟩⟩)
  · simp [collinear_empty]
  · rw [collinear_iff_of_mem hp₁]
    constructor
    · exact fun h => ⟨p₁, h⟩
    · rintro ⟨p, v, hv⟩
      use v
      intro p₂ hp₂
      rcases hv p₂ hp₂ with ⟨r, rfl⟩
      rcases hv p₁ hp₁ with ⟨r₁, rfl⟩
      use r - r₁
      simp [vadd_vadd, ← add_smul]

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

Tactic:
refine ⟨fun h ↦ affineIndependent_of_affineIndependent_collinear_ne h hcol hne2,
    fun h ↦ affineIndependent_of_affineIndependent_collinear_ne h ?_ hne1⟩
  convert! hcol using 1
  aesop

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

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f 0

Tactic:
exact memℓp_zero_iff.mpr { i : α | f i ≠ 0 }.toFinite

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

Goal state before:
pp: case refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s✝ : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
s : Finset ι
⊢ i ∉ s →
    ((∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a ↦ ∑ i ∈ s, f i a) p) →
      (∀ i_1 ∈ insert i s, Memℓp (f i_1) p) → Memℓp (fun a ↦ ∑ i ∈ insert i s, f i a) p

Tactic:
his

Goal state after:
case refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s✝ : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
⊢ ((∀ i ∈ s, Memℓp (f i) p) → Memℓp (fun a ↦ ∑ i ∈ s, f i a) p) →
    (∀ i_1 ∈ insert i s, Memℓp (f i_1) p) → Memℓp (fun a ↦ ∑ i ∈ insert i s, f i a) p
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case h
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
f : (a : α) → E a
C : ℝ
_i : Fact (1 ≤ ∞)
F : ι → ↥(lp E ∞)
hF : Bornology.IsBounded (Set.range F)
hf : Tendsto (id fun i ↦ ↑(F i)) l (𝓝 f)
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ C ∈ upperBounds (Set.range fun i ↦ ‖f i‖)

Tactic:
rintro _ ⟨a, rfl⟩

Goal state after:
case h
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
f : (a : α) → E a
C : ℝ
_i : Fact (1 ≤ ∞)
F : ι → ↥(lp E ∞)
hF : Bornology.IsBounded (Set.range F)
hf : Tendsto (id fun i ↦ ↑(F i)) l (𝓝 f)
hCF : ∀ (k : ι), ‖F k‖ ≤ C
a : α
⊢ (fun i ↦ ‖f i‖) a ≤ C
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x ↦ g x i
a₀ a : α
M : ℝ
hM : M ∈ upperBounds (Set.range fun i ↦ ‖g a₀ i‖)
⊢ Memℓp (g a) ∞

Tactic:
use ↑K * dist a a₀ + M

Goal state after:
case h
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x ↦ g x i
a₀ a : α
M : ℝ
hM : M ∈ upperBounds (Set.range fun i ↦ ‖g a₀ i‖)
⊢ ↑K * dist a a₀ + M ∈ upperBounds (Set.range fun i ↦ ‖g a i‖)
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜 E'
inst✝⁵ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : MeasurableSpace G
μ : Measure G
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
x₀ : G
h : HasCompactSupport fun t ↦ (L (f t)) (g (x₀ - t))
hf : LocallyIntegrable f μ
hg : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
⊢ ConvolutionExistsAt f g x₀ L μ

Tactic:
by
  let u := (Homeomorph.neg G).trans (Homeomorph.addRight x₀)
  let v := (Homeomorph.neg G).trans (Homeomorph.addLeft x₀)
  apply ((u.isCompact_preimage.mpr h).bddAbove_image hg.norm.continuousOn).convolutionExistsAt' L
    isClosed_closure.measurableSet subset_closure (hf.integrableOn_isCompact h)
  have A : AEStronglyMeasurable (g ∘ v)
      (μ.restrict (tsupport fun t : G => L (f t) (g (x₀ - t)))) := by
    apply (hg.comp v.continuous).continuousOn.aestronglyMeasurable_of_isCompact h
    exact (isClosed_tsupport _).measurableSet
  convert!
    ((v.continuous.measurable.measurePreserving
              (μ.restrict (tsupport fun t => L (f t) (g (x₀ - t))))).aestronglyMeasurable_comp_iff
          v.measurableEmbedding).1
      A
  ext x
  simp only [v, Homeomorph.neg, sub_eq_add_neg, val_toAddUnits_apply, Homeomorph.trans_apply,
    Equiv.neg_apply, Homeomorph.homeomorph_mk_coe, Homeomorph.coe_addLeft]

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜 E'
inst✝⁵ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : MeasurableSpace G
μ : Measure G
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
hcf : HasCompactSupport f
hf : LocallyIntegrable f μ
hg : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ t : G
ht : f t = 0
⊢ (L 0) (g (x₀ - t)) = 0

Tactic:
L.map_zero₂

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case e'_7.inr.inl
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
t : G
h : f t = 0
⊢ (L 0) (g (x - t)) = 0

Tactic:
L.map_zero₂

Goal state after:
case e'_7.inr.inl
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
t : G
h : f t = 0
⊢ 0 = 0
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x ↦ F x a) s
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (L (F' a)) x₀
hm : AEStronglyMeasurable (⇑L ∘ F') μ
hF'_int : Integrable (⇑L ∘ F') μ
key : HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), (⇑L ∘ F') a ∂μ) x₀
⊢ Integrable F' μ

Tactic:
rw [← integrable_norm_iff hm] at hF'_int

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
F' : α → E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x ↦ F x a) s
bound_integrable : Integrable bound μ
L : E →L[𝕜] 𝕜 →L[𝕜] E := (ContinuousLinearMap.smulRightL 𝕜 𝕜 E) 1
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (L (F' a)) x₀
hm : AEStronglyMeasurable (⇑L ∘ F') μ
hF'_int : Integrable (fun a ↦ ‖(⇑L ∘ F') a‖) μ
key : HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), (⇑L ∘ F') a ∂μ) x₀
⊢ Integrable F' μ
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case neg
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : SeminormedAddCommGroup G
x₀ : G
R : ℝ
hf : support f ⊆ ball 0 R
hg : ∀ x ∈ ball x₀ R, g x = g x₀
t : G
ht : f t = 0
⊢ (L 0) (g (x₀ - t)) = (L 0) (g x₀)

Tactic:
L.map_zero₂

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case refine_2
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
t : G
ht : f t = 0
⊢ (L 0) (g (x₀ - t)) = 0

Tactic:
L.map_zero₂

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 : ℝ
s : Set E
hR : R ≠ 0
e : E ≃ᵐ E := (Homeomorph.smul (Units.mk0 R hR)).toMeasurableEquiv
⊢ ∫ (y : E) in ⇑e.symm ⁻¹' s, f y ∂map (fun x ↦ R • x) μ = |(R ^ finrank ℝ E)⁻¹| • ∫ (y : E) in ⇑e.symm ⁻¹' s, f y ∂μ

Tactic:
by
    simp [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: F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
⊢ Integrable (fun x ↦ g (S • x)) μ

Tactic:
let t := ((Homeomorph.smul (isUnit_iff_ne_zero.2 hS).unit).toMeasurableEquiv : E ≃ᵐ E)

Goal state after:
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := (Homeomorph.smul ⋯.unit).toMeasurableEquiv
⊢ Integrable (fun x ↦ g (S • x)) μ
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst✝¹] w
xw : x ∈ w
y : α
⊢ y ∈ w → y ∈ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}

Tactic:
yw

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst✝¹] w
xw : x ∈ w
y : α
yw : y ∈ w
⊢ y ∈ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ∞
⊢ μ.IsEverywherePos (μ.everywherePosSubset s)

Tactic:
by
  intro x hx n hn
  rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 hn with ⟨u, u_mem, hu⟩
  have A : 0 < μ (u ∩ s) := by
    have : u ∩ s ∈ 𝓝[s] x := by rw [inter_comm]; exact inter_mem_nhdsWithin s u_mem
    exact hx.2 _ this
  have B : (u ∩ μ.everywherePosSubset s : Set α) =ᵐ[μ] (u ∩ s : Set α) :=
    ae_eq_set_inter (ae_eq_refl _) (everywherePosSubset_ae_eq_of_measure_ne_top hs h's)
  rw [← B.measure_eq] at A
  exact A.trans_le (measure_mono hu)

Goal state after: