mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
p : P
this : ∑ i, (s.points i -ᵥ p) = ∑ i, (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid))
h : (n + 1) • (p -ᵥ s.centroid) = 0
h' : (↑n + 1) • (p -ᵥ s.centroid) = 0
⊢ p -ᵥ s.centroid = 0

Tactic:
rw [smul_eq_zero_iff_right (by norm_cast)] at h'

Goal state after:
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
p : P
this : ∑ i, (s.points i -ᵥ p) = ∑ i, (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid))
h : (n + 1) • (p -ᵥ s.centroid) = 0
h' : p -ᵥ s.centroid = 0
⊢ p -ᵥ s.centroid = 0
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✝ : DecidableEq P
p : ι → P
s : Finset ι
n : ℕ
hc : #s = n + 1
⊢ s.Nonempty

Tactic:
← Finset.card_pos,

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✝ : DecidableEq P
p : ι → P
s : Finset ι
n : ℕ
hc : #s = n + 1
⊢ 0 < #s
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: case neg.inl
𝕜 : 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
x✝ : ∃ y, y • 1 = ↑(↑g).symm ∘SL ↑↑f
y : 𝕜
h : y • 1 = ↑(↑g).symm ∘SL ↑↑f
hy : y ≠ 0
hfg : ↑↑f = y • ↑↑g
hgf : ↑↑g = star y • ↑↑f
this : (starRingEnd 𝕜) y * y = 1
⊢ ∃ α, ∀ (x : H), f x = (α • g) x

Tactic:
exact ⟨⟨y, by simp [Unitary.mem_iff, this, mul_comm y]⟩, fun x ↦ congr($hfg x)⟩

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

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

Tactic:
faceOppositeCentroid_eq_smul_vsub_vadd_point

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ (↑n)⁻¹ • (s.centroid -ᵥ s.points i) +ᵥ s.centroid ∈ line[k, s.points i, s.centroid]
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✝¹ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : #s = finrank k ↥sp.direction + 1
⊢ s.Nonempty

Tactic:
← Finset.card_pos,

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✝¹ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k ↑(Finset.image p s) ≤ sp
hc : #s = finrank k ↥sp.direction + 1
⊢ 0 < #s
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : x ∈ closedBall c f.rIn
⊢ ↑f x = 1

Tactic:
apply ContDiffBumpBase.eq_one _ _ f.one_lt_rOut_div_rIn
  simpa only [norm_smul, Real.norm_eq_abs, abs_inv, abs_of_nonneg f.rIn_pos.le, ← div_eq_inv_mul,
    div_le_one f.rIn_pos] using mem_closedBall_iff_norm.1 hx

Goal state after:
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
F : Type u_6
inst✝⁴ : MeasurableSpace G
inst✝³ : NormedAddCommGroup F
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
f : G → F
s : Set G
hf : IntegrableOn f s μ
this : s⁻¹ = ⇑(MeasurableEquiv.inv G) ⁻¹' s
⊢ Integrable f ((map (⇑(MeasurableEquiv.inv G)) μ).restrict s)

Tactic:
simpa using! hf

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

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : HasContDiffBump E
c : E
f : ContDiffBump c
inst✝ : FiniteDimensional ℝ E
⊢ IsCompact (closedBall c f.rOut)

Tactic:
isCompact_closedBall

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₅ : P
h₁ : p₁ ∈ line[k, p₄, p₅]
h₂ : p₂ ∈ line[k, p₄, p₅]
h₃ : p₃ ∈ line[k, p₄, p₅]
⊢ Collinear k {p₁, p₂, p₃}

Tactic:
refine (collinear_insert_insert_insert_left_of_mem_affineSpan_pair h₁ h₂ h₃).subset ?_
  gcongr; simp

Goal state after:
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 ≤ ∞
⊢ Memℓp f ∞

pp: case inr.inr.inr.inr.inr
α : 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
⊢ Memℓp f p

Tactic:
· apply memℓp_infty
    obtain ⟨A, hA⟩ := (hfq.summable hq).tendsto_cofinite_zero.bddAbove_range_of_cofinite
    use A ^ q.toReal⁻¹
    rintro x ⟨i, rfl⟩
    have : 0 ≤ ‖f i‖ ^ q.toReal := by positivity
    simpa [← Real.rpow_mul, mul_inv_cancel₀ hq.ne'] using
      Real.rpow_le_rpow this (hA ⟨i, rfl⟩) (inv_nonneg.mpr hq.le)

Goal state after:
case inr.inr.inr.inr.inr
α : 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
⊢ Memℓp f p
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst✝ : (i : α) → NormedAddCommGroup (F i)
p : ℝ≥0∞
hp✝ : p ≠ 0
x : ↥(lp E p)
y : ↥(lp F p)
h : ∀ (i : α), ‖↑x i‖ ≤ ‖↑y i‖
hp : 0 < p.toReal
s : Finset α
⊢ ∑ i ∈ s, ‖↑x i‖ ^ p.toReal ≤ ∑ i ∈ s, ‖↑y i‖ ^ p.toReal

Tactic:
by gcongr with i _; exact h i

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

Goal state before:
pp: α : Type u_3
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ↥(lp (fun x ↦ E) 1)
⊢ Summable fun a ↦ ‖‖↑f a‖‖

Tactic:
simpa using f.2.summable

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E✝ : α → Type u_4
p q : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E✝ i)
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : CompleteSpace E
f g : ↥(lp (fun x ↦ E) 1)
⊢ Summable fun a ↦ ‖↑f a‖

Tactic:
simpa using f.2.summable

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E✝ : α → Type u_4
p q : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E✝ i)
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : CompleteSpace E
c : 𝕜
f : ↥(lp (fun x ↦ E) 1)
⊢ Summable fun a ↦ ‖↑f a‖

Tactic:
simpa using f.2.summable

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
y : H
⊢ ContDiffAt 𝕜 n f y ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun x ↦ (f x).ofLp i) y

Tactic:
← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiffAt_iff,

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
y : H
⊢ ContDiffAt 𝕜 n (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) y ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun x ↦ (f x).ofLp i) y
Module: Mathlib.Analysis.Calculus.ContDiff.WithLp

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
⊢ ContDiff 𝕜 n f ↔ ∀ (i : ι), ContDiff 𝕜 n fun x ↦ (f x).ofLp i

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiff_iff, contDiff_pi]

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
⊢ (∀ (i : ι), ContDiff 𝕜 n fun x ↦ (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) ↔
    ∀ (i : ι), ContDiff 𝕜 n fun x ↦ (f x).ofLp 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✝¹ : MeasurableAdd G
inst✝ : MeasurableNeg G
x₀ : G
s : Set G
hbg : BddAbove ((fun i ↦ ‖g i‖) '' (fun t ↦ -t + x₀) ⁻¹' s)
hs : MeasurableSet s
h2s : (support fun t ↦ (L (f t)) (g (x₀ - t))) ⊆ s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g (Measure.map (fun t ↦ x₀ - t) (μ.restrict s))
⊢ ConvolutionExistsAt f g x₀ L μ

Tactic:
ConvolutionExistsAt

Goal state after:
𝕜 : 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✝¹ : MeasurableAdd G
inst✝ : MeasurableNeg G
x₀ : G
s : Set G
hbg : BddAbove ((fun i ↦ ‖g i‖) '' (fun t ↦ -t + x₀) ⁻¹' s)
hs : MeasurableSet s
h2s : (support fun t ↦ (L (f t)) (g (x₀ - t))) ⊆ s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g (Measure.map (fun t ↦ x₀ - t) (μ.restrict s))
⊢ Integrable (fun t ↦ (L (f t)) (g (x₀ - t))) μ
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✝⁶ : NormedSpace ℝ F
inst✝⁵ : AddGroup G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalAddGroup G
inst✝² : BorelSpace G
inst✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E'
hbg : BddAbove (range fun x ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
this : ∀ᶠ (x : G) in 𝓝 x₀, ∀ᵐ (t : G) ∂μ, ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖
⊢ ContinuousAt (f ⋆[L, μ] g) x₀

Tactic:
refine continuousAt_of_dominated ?_ this (by fun_prop) ?_

Goal state after:
case refine_1
𝕜 : 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
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalAddGroup G
inst✝² : BorelSpace G
inst✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E'
hbg : BddAbove (range fun x ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
this : ∀ᶠ (x : G) in 𝓝 x₀, ∀ᵐ (t : G) ∂μ, ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖
⊢ ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun a ↦ (L (f a)) (g (x - a))) μ

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✝⁵ : AddGroup G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalAddGroup G
inst✝² : BorelSpace G
inst✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E'
hbg : BddAbove (range fun x ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
this : ∀ᶠ (x : G) in 𝓝 x₀, ∀ᵐ (t : G) ∂μ, ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖
⊢ ∀ᵐ (a : G) ∂μ, ContinuousAt (fun x ↦ (L (f a)) (g (x - a))) x₀
Module: Mathlib.Data.Set.Pointwise.Support

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : One γ
c : α
f : β → γ
x : β
⊢ (x ∈ mulSupport fun x ↦ f (c⁻¹ • x)) ↔ x ∈ c • mulSupport f

Tactic:
simp only [mem_smul_set_iff_inv_smul_mem, mem_mulSupport]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁸ : MeasurableSpace G
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace H
inst✝¹ : SeminormedGroup H
inst✝ : OpensMeasurableSpace H
f : G →* H
hf : Measurable ⇑f
x : G
K : PositiveCompacts G := Classical.arbitrary (PositiveCompacts G)
⊢ ∃ n, 0 < haar (interior ↑K ∩ ⇑f ⁻¹' ball 1 ↑n)

Tactic:
by_contra!
    simp_rw [nonpos_iff_eq_zero, ← measure_iUnion_null_iff, ← inter_iUnion, ← preimage_iUnion,
      iUnion_ball_nat, preimage_univ, inter_univ] at this
    exact this.not_gt <| isOpen_interior.measure_pos _ K.interior_nonempty

Goal state after:
Module: Mathlib.Topology.Metrizable.Urysohn

Goal state before:
pp: case refine_2
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
V : Set X
hVB : V ∈ B
hxV : x ∈ V
U : Set X
hUB : U ∈ B
hxU : x ∈ U
hUV : closure[inst✝²] U ⊆ V
UV : ↑s := ⟨(U, V), ⋯⟩
y : X
hy : ¬y ∈ V
⊢ ε UV ≤ dist ((f UV) y) ((f UV) x)

Tactic:
hfε UV hy,

Goal state after:
case refine_2
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
V : Set X
hVB : V ∈ B
hxV : x ∈ V
U : Set X
hUB : U ∈ B
hxU : x ∈ U
hUV : closure[inst✝²] U ⊆ V
UV : ↑s := ⟨(U, V), ⋯⟩
y : X
hy : ¬y ∈ V
⊢ ε UV ≤ dist ((fun x ↦ ε UV) y) ((f UV) x)
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
x : G
C : Continuous[inst✝⁹, _] fun y ↦ g (y⁻¹ * x)
⊢ HasCompactSupport fun y ↦ g (y⁻¹ * x)

Tactic:
exact h'g.comp_homeomorph ((Homeomorph.inv G).trans (Homeomorph.mulRight x))

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
⊢ ∫ (x : G), ∫ (y : G), f x * (D x)⁻¹ * g (y⁻¹ * x) ∂ν ∂μ = ∫ (y : G), ∫ (x : G), f x * (D x)⁻¹ * g (y⁻¹ * x) ∂μ ∂ν

Tactic:
by
      apply integral_integral_swap_of_hasCompactSupport
      · apply Continuous.mul
        · exact (hf.comp continuous_fst).mul
            ((D_cont.comp continuous_fst).inv₀ (fun x ↦ (D_pos _).ne'))
        · exact hg.comp (continuous_snd.inv.mul continuous_fst)
      · let K := tsupport f
        have K_comp : IsCompact K := h'f
        let L := tsupport g
        have L_comp : IsCompact L := h'g
        let M := (fun (p : G × G) ↦ p.1 * p.2⁻¹) '' (K ×ˢ L)
        have M_comp : IsCompact M :=
          (K_comp.prod L_comp).image (continuous_fst.mul continuous_snd.inv)
        have M'_comp : IsCompact (closure M) := M_comp.closure
        have : ∀ (p : G × G), p ∉ K ×ˢ closure M → f p.1 * (D p.1)⁻¹ * g (p.2⁻¹ * p.1) = 0 := by
          rintro ⟨x, y⟩ hxy
          by_cases H : x ∈ K; swap
          · simp [image_eq_zero_of_notMem_tsupport H]
          have : g (y⁻¹ * x) = 0 := by
            apply image_eq_zero_of_notMem_tsupport
            contrapose hxy
            simp only [mem_prod, H, true_and]
            apply subset_closure
            simp only [M, mem_image, mem_prod, Prod.exists]
            exact ⟨x, y⁻¹ * x, ⟨H, hxy⟩, by group⟩
          simp [this]
        apply HasCompactSupport.intro' (K_comp.prod M'_comp) ?_ this
        exact (isClosed_tsupport f).prod isClosed_closure

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✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun n x ↦ ↑((thickenedIndicator ⋯ {1}) x)
vf_cont : ∀ (n : ℕ), Continuous[inst✝⁷, _] (v n ∘ f)
ν : Measure G
⊢ IsFiniteMeasureOnCompacts ν →
    Tendsto (fun n ↦ ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂ν))

Tactic:
hν

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✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun n x ↦ ↑((thickenedIndicator ⋯ {1}) x)
vf_cont : ∀ (n : ℕ), Continuous[inst✝⁷, _] (v n ∘ f)
ν : Measure G
hν : IsFiniteMeasureOnCompacts ν
⊢ Tendsto (fun n ↦ ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂ν))
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}
m : Set G
m_max : Maximal (fun x ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint fun x ↦ x • k
y : G
hy : y ∈ s
h'y : m ∪ {y} ∈ A
ym : y ∈ m
⊢ y ∈ y • (k * k⁻¹)

Tactic:
simpa using mem_leftCoset y (Set.mul_mem_mul one_k (Set.inv_mem_inv.mpr one_k))

Goal state after: