mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
f : (x : X) → ContDiffBump (c x)
hc : ContDiff ℝ (↑n) c
hr : ContDiff ℝ ↑n fun x ↦ (f x).rIn
hR : ContDiff ℝ ↑n fun x ↦ (f x).rOut
hg : ContDiff ℝ (↑n) g
⊢ ContDiff ℝ ↑n fun x ↦ ↑(f x) (g x)

Tactic:
rw [contDiff_iff_contDiffAt] at *

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
f : (x : X) → ContDiffBump (c x)
hc : ∀ (x : X), ContDiffAt ℝ (↑n) c x
hr : ∀ (x : X), ContDiffAt ℝ (↑n) (fun x ↦ (f x).rIn) x
hR : ∀ (x : X), ContDiffAt ℝ (↑n) (fun x ↦ (f x).rOut) x
hg : ∀ (x : X), ContDiffAt ℝ (↑n) g x
⊢ ∀ (x : X), ContDiffAt ℝ (↑n) (fun x ↦ ↑(f x) (g x)) 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
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
h : Coplanar k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 2
⊢ Coplanar k s ↔ finrank k ↥(vectorSpan k s) ≤ 2

Tactic:
← finrank_eq_rank

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
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
h : Coplanar k s ↔ ↑(finrank k ↥(vectorSpan k s)) ≤ 2
⊢ Coplanar k s ↔ finrank k ↥(vectorSpan k s) ≤ 2
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
h : Collinear k s
p : P
⊢ Coplanar k (insert p s)

Tactic:
have : FiniteDimensional k { x // x ∈ vectorSpan k s } := h.finiteDimensional_vectorSpan

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
s : Set P
h : Collinear k s
p : P
this : FiniteDimensional k ↥(vectorSpan k s)
⊢ Coplanar k (insert p s)
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ∞
f : (i : α) → E i
⊢ (if p = ∞ then BddAbove (Set.range fun i ↦ ‖f i‖) else Summable fun i ↦ ‖f i‖ ^ p.toReal) ↔
    Summable fun i ↦ ‖f i‖ ^ p.toReal

Tactic:
if_neg hp.2.ne

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ∞
f : (i : α) → E i
⊢ (Summable fun i ↦ ‖f i‖ ^ p.toReal) ↔ Summable fun i ↦ ‖f i‖ ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr.inr.inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < q.toReal
hpq : q ≤ ∞
⊢ BddAbove (Set.range fun i ↦ ‖f i‖)

Tactic:
obtain ⟨A, hA⟩ := (hfq.summable hq).tendsto_cofinite_zero.bddAbove_range_of_cofinite

Goal state after:
case inr.inr.inr.inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < q.toReal
hpq : q ≤ ∞
A : ℝ
hA : A ∈ upperBounds (Set.range fun i ↦ ‖f i‖ ^ q.toReal)
⊢ BddAbove (Set.range fun i ↦ ‖f i‖)
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)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
⊢ Summable fun i ↦ ‖(f + g) i‖ ^ p.toReal

Tactic:
let C : ℝ := if p.toReal < 1 then 1 else (2 : ℝ) ^ (p.toReal - 1)

Goal state after:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
⊢ Summable fun i ↦ ‖(f + g) i‖ ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < p.toReal
⊢ Memℓp (c • f) p

Tactic:
apply memℓp_gen
    dsimp only [Pi.smul_apply]
    have := (hf.summable hp).mul_left (↑(‖c‖₊ ^ p.toReal) : ℝ)
    simp_rw [← coe_nnnorm, ← NNReal.coe_rpow, ← NNReal.coe_mul, NNReal.summable_coe,
      ← NNReal.mul_rpow] at this ⊢
    refine NNReal.summable_of_le ?_ this
    intro i
    gcongr
    apply nnnorm_smul_le

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

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ∞
f : ↥(lp E p)
⊢ (if p = ∞ then ⨆ i, ‖↑f i‖ else (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)) =
    (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
if_neg hp.2.ne

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ∞
f : ↥(lp E p)
⊢ (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal) = (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)
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₀ : α
hga₀b : Memℓp (g a₀) ∞
a : α
⊢ Memℓp (g a) ∞

Tactic:
by
  rcases hga₀b with ⟨M, hM⟩
  use ↑K * dist a a₀ + M
  rintro - ⟨i, rfl⟩
  calc
    |g a i| = |g a i - g a₀ i + g a₀ i| := by simp
    _ ≤ |g a i - g a₀ i| + |g a₀ i| := abs_add_le _ _
    _ ≤ ↑K * dist a a₀ + M := by
        gcongr
        · exact lipschitzWith_iff_dist_le_mul.1 (hg i) a a₀
        · exact hM ⟨i, rfl⟩

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

Goal state before:
pp: case mpr
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
f : α → ↥(lp (fun x ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
⊢ (∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist (↑(f x) i) (↑(f y) i) ≤ ↑K * dist x y) →
    ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y

Tactic:
intro hgl x hx y hy

Goal state after:
case mpr
α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
f : α → ↥(lp (fun x ↦ ℝ) ∞)
s : Set α
K : ℝ≥0
hgl : ∀ (i : ι), ∀ x ∈ s, ∀ y ∈ s, dist (↑(f x) i) (↑(f y) i) ≤ ↑K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ dist (f x) (f y) ≤ ↑K * dist x y
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
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ s ⊆ t

Tactic:
have st_nonempty : (s ∩ t).Nonempty := ⟨x₀, hx₀, ⟨hx₀, hfg⟩⟩

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
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
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
st_nonempty : (s ∩ t).Nonempty
⊢ s ⊆ t
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: case refine_2
x✝ x : ℝ
hx : 1 < x
⊢ x.smoothTransition = smoothTransition 1

Tactic:
smoothTransition.one,

Goal state after:
case refine_2
x✝ x : ℝ
hx : 1 < x
⊢ x.smoothTransition = 1
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case e'_4
𝕜 : 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✝¹ : AddGroup G
inst✝ : TopologicalSpace G
hcf : HasCompactSupport f
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
x t : G
s : Set G
hx : x ∈ s
⊢ (-tsupport f + s).indicator (fun t ↦ (‖L‖ * ⨆ i, ‖f i‖) * ‖g t‖) t =
    (-tsupport f + s).indicator (fun t ↦ ‖L.flip‖ * ‖g t‖ * ⨆ i, ‖f i‖) t

Tactic:
L.opNorm_flip,

Goal state after:
case e'_4
𝕜 : 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✝¹ : AddGroup G
inst✝ : TopologicalSpace G
hcf : HasCompactSupport f
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
x t : G
s : Set G
hx : x ∈ s
⊢ (-tsupport f + s).indicator (fun t ↦ (‖L‖ * ⨆ i, ‖f i‖) * ‖g t‖) t =
    (-tsupport f + s).indicator (fun t ↦ ‖L‖ * ‖g t‖ * ⨆ i, ‖f i‖) t
Module: Mathlib.Analysis.InnerProductSpace.Calculus

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

Tactic:
ext y

Goal state after:
case e'_12
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
e_8✝ : instAddCommGroup = instRCLike.toDivisionRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ toInnerProductSpaceReal.toModule
y : F
⊢ (2 • (innerSL ℝ) x) y =
    (fderivInnerCLM ℝ (id x, id x) ∘SL (ContinuousLinearMap.id ℝ F).prod (ContinuousLinearMap.id ℝ F)) y
Module: Mathlib.Analysis.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✝¹⁰ : 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
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalAddGroup G
inst✝¹ : BorelSpace G
inst✝ : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (s ×ˢ univ)
H : ∃ p ∈ s, ∃ x, g p x ≠ 0
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun p x ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
⊢ uncurry g' = uncurry g ∘ fun w ↦ (w.1.1, w.1.2 - w.2)

Tactic:
ext y

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✝¹⁰ : 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
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalAddGroup G
inst✝¹ : BorelSpace G
inst✝ : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (s ×ˢ univ)
H : ∃ p ∈ s, ∃ x, g p x ≠ 0
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun p x ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
y : (P × G) × G
⊢ uncurry g' y = (uncurry g ∘ fun w ↦ (w.1.1, w.1.2 - w.2)) y
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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : TendstoLocallyUniformlyOn f' g' l s
hf : ∀ (n : ι), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hfg : ∀ x ∈ s, Tendsto (fun n ↦ f n x) l (𝓝 (g x))
hx : x ∈ s
h1 : s ∈ 𝓝 x
⊢ Set.univ ×ˢ s ∈ l ×ˢ 𝓝 x

Tactic:
simp only [h1, prod_mem_prod_iff, univ_mem, and_self_iff]

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

Goal state before:
pp: case e_a.e_μ.e_s
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
⊢ ⇑e.symm ⁻¹' s = R • s

Tactic:
ext y

Goal state after:
case e_a.e_μ.e_s
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
⊢ y ∈ ⇑e.symm ⁻¹' s ↔ y ∈ R • s
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case refine_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ range f ⊆ Icc 0 1

pp: case refine_4
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ f x = 1

Tactic:
· rintro t ⟨y, rfl⟩
    exact ⟨c.nonneg, c.le_one⟩

Goal state after:
case refine_4
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ f x = 1
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedSpace ℝ E'
inst✝⁴ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
μ ν : Measure ℝ
inst✝³ : SFinite μ
inst✝² : SFinite ν
inst✝¹ : μ.IsAddRightInvariant
inst✝ : NullSingletonClass ν
hf : Integrable ((Ioi 0).indicator f) ν
hg : Integrable ((Ioi 0).indicator g) μ
L : E →L[ℝ] E' →L[ℝ] F
⊢ Integrable ((Ioi 0).indicator f ⋆[L, ν] (Ioi 0).indicator g) μ

Tactic:
exact (hf.convolution_integrand L hg).integral_prod_left

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
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
K : Set G := tsupport f
K_comp : IsCompact K
L : Set G := tsupport g
L_comp : IsCompact L
M : Set G := (fun p ↦ p.1 * p.2⁻¹) '' K ×ˢ L
M_comp : IsCompact M
M'_comp : IsCompact (closure[inst✝⁹] M)
x y : G
hxy : (x, y) ∉ K ×ˢ closure[inst✝⁹] M
H : x ∈ K
⊢ g (y⁻¹ * x) = 0

Tactic:
apply image_eq_zero_of_notMem_tsupport

Goal state after:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := ⋯
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
K : Set G := ⋯
K_comp : IsCompact K
L : Set G := ⋯
L_comp : IsCompact L
M : Set G := ⋯
M_comp : IsCompact M
M'_comp : IsCompact (closure[inst✝⁹] M)
x y : G
hxy : (x, y) ∉ K ×ˢ closure[inst✝⁹] M
H : x ∈ K
⊢ y⁻¹ * x ∉ tsupport g
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
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := ⋯
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
K : Set G := ⋯
K_comp : IsCompact K
L : Set G := ⋯
L_comp : IsCompact L
M : Set G := ⋯
M_comp : IsCompact M
M'_comp : IsCompact (closure[inst✝⁹] M)
x y : G
hxy : (x, y) ∉ K ×ˢ closure[inst✝⁹] M
H : x ∈ K
⊢ y⁻¹ * x ∉ tsupport g

Tactic:
contrapose hxy

Goal state after:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
K : Set G := tsupport f
K_comp : IsCompact K
L : Set G := tsupport g
L_comp : IsCompact L
M : Set G := (fun p ↦ p.1 * p.2⁻¹) '' K ×ˢ L
M_comp : IsCompact M
M'_comp : IsCompact (closure[inst✝⁹] M)
x y : G
H : x ∈ K
hxy : y⁻¹ * x ∈ tsupport g
⊢ (x, y) ∈ K ×ˢ closure[inst✝⁹] M
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
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
K : Set G := tsupport f
K_comp : IsCompact K
L : Set G := tsupport g
L_comp : IsCompact L
M : Set G := (fun p ↦ p.1 * p.2⁻¹) '' K ×ˢ L
M_comp : IsCompact M
M'_comp : IsCompact (closure[inst✝⁹] M)
x y : G
hxy : (x, y) ∉ L ×ˢ closure[inst✝⁹] M
H : x ∈ L
⊢ f (y * x) = 0

Tactic:
apply image_eq_zero_of_notMem_tsupport

Goal state after:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := ⋯
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
K : Set G := ⋯
K_comp : IsCompact K
L : Set G := ⋯
L_comp : IsCompact L
M : Set G := ⋯
M_comp : IsCompact M
M'_comp : IsCompact (closure[inst✝⁹] M)
x y : G
hxy : (x, y) ∉ L ×ˢ closure[inst✝⁹] M
H : x ∈ L
⊢ y * x ∉ tsupport f
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
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := ⋯
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
K : Set G := ⋯
K_comp : IsCompact K
L : Set G := ⋯
L_comp : IsCompact L
M : Set G := ⋯
M_comp : IsCompact M
M'_comp : IsCompact (closure[inst✝⁹] M)
x y : G
hxy : (x, y) ∉ L ×ˢ closure[inst✝⁹] M
H : x ∈ L
⊢ y * x ∉ tsupport f

Tactic:
contrapose hxy

Goal state after:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
K : Set G := tsupport f
K_comp : IsCompact K
L : Set G := tsupport g
L_comp : IsCompact L
M : Set G := (fun p ↦ p.1 * p.2⁻¹) '' K ×ˢ L
M_comp : IsCompact M
M'_comp : IsCompact (closure[inst✝⁹] M)
x y : G
H : x ∈ L
hxy : y * x ∈ tsupport f
⊢ (x, y) ∈ L ×ˢ closure[inst✝⁹] M