mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : CharZero k
s : Simplex k P n
⊢ ∑ i, (s.points i -ᵥ s.centroid) = 0

Tactic:
have h := centroid_vsub_eq s s.centroid

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✝ : CharZero k
s : Simplex k P n
h : s.centroid -ᵥ s.centroid = (↑n + 1)⁻¹ • ∑ x, (s.points x -ᵥ s.centroid)
⊢ ∑ i, (s.points i -ᵥ s.centroid) = 0
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ (adjoint A ∘ₗ A).ker = ⊥ ↔ A.ker = ⊥

Tactic:
ker_adjoint_comp_self

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ A.ker = ⊥ ↔ A.ker = ⊥
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 ι
n : ℕ
hc : #s = n + 1
hi' : AffineIndependent k fun x ↦ ↑x
hc' : #(Finset.image p s) = n + 1
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p s)) = n

Tactic:
have hn : (s.image p).Nonempty := by simp [hc', ← 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 ι
n : ℕ
hc : #s = n + 1
hi' : AffineIndependent k fun x ↦ ↑x
hc' : #(Finset.image p s) = n + 1
hn : (Finset.image p s).Nonempty
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p s)) = n
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 ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ AffineIndependent k p ↔ n ≤ finrank k ↥(vectorSpan k (Set.range p))

Tactic:
rw [affineIndependent_iff_finrank_vectorSpan_eq k p hc]

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 ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k ↥(vectorSpan k (Set.range p)) = n ↔ n ≤ finrank k ↥(vectorSpan k (Set.range p))
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:
rw [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.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ (convexHull ℝ) (range ⇑b) = ⋂ i, ⇑(b.coord i) ⁻¹' Ici 0

Tactic:
rw [b.convexHull_eq_nonneg_coord, ofPred_forall]

Goal state after:
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ ⋂ i, {x | 0 ≤ (b.coord i) x} = ⋂ i, ⇑(b.coord i) ⁻¹' Ici 0
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
⊢ ∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤

Tactic:
have hεyq : ∀ y ∉ s, ε / dist y q ≠ 0 := fun y hy =>
    div_ne_zero ε0.ne' (dist_ne_zero.2 (ne_of_mem_of_not_mem hq hy).symm)

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
⊢ ∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
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✝¹ : MeasurableMul G
f : G → F
inst✝ : μ.IsMulRightInvariant
hf : Integrable f μ
g : G
⊢ Integrable (fun t ↦ f (t / g)) μ

Tactic:
by
  simp_rw [div_eq_mul_inv]
  exact hf.comp_mul_right g⁻¹

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

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖
hg₁ : ∀ (i : α), 0 ≤ ‖↑g i‖
⊢ (Summable fun i ↦ ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖

Tactic:
have hf₂ := lp.hasSum_norm hpq.pos f

Goal state after:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖
hg₁ : ∀ (i : α), 0 ≤ ‖↑g i‖
hf₂ : HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
⊢ (Summable fun i ↦ ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst✝ : (i : α) → NormedAddCommGroup (F i)
hp : 0 ≠ 0
x : ↥(lp E 0)
y : ↥(lp F 0)
h : ∀ (i : α), ‖↑x i‖ ≤ ‖↑y i‖
⊢ ‖x‖ ≤ ‖y‖

Tactic:
exact hp rfl |>.elim

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: case inl
x y : ℝ
hxy : x ≤ y
hx : x ≤ 0
⊢ expNegInvGlue x ≤ expNegInvGlue y

pp: case inr
x y : ℝ
hxy : x ≤ y
hx : 0 < x
⊢ expNegInvGlue x ≤ expNegInvGlue y

Tactic:
· simp [zero_of_nonpos hx, nonneg]

Goal state after:
case inr
x y : ℝ
hxy : x ≤ y
hx : 0 < x
⊢ expNegInvGlue x ≤ expNegInvGlue y
Module: Mathlib.Analysis.Calculus.BumpFunction.InnerProduct

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x✝¹ : ℝ
x✝ : E
⊢ ((x✝¹ - ‖-x✝‖) / (x✝¹ - 1)).smoothTransition = ((x✝¹ - ‖x✝‖) / (x✝¹ - 1)).smoothTransition

Tactic:
by simp only [norm_neg]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ ContDiffOn ℝ (↑⊤) (uncurry fun R x ↦ ((R - ‖x‖) / (R - 1)).smoothTransition) (Set.Ioi 1 ×ˢ Set.univ)

Tactic:
rintro ⟨R, x⟩ ⟨hR : 1 < R, -⟩
    apply ContDiffAt.contDiffWithinAt
    rw [← sub_pos] at hR
    rcases eq_or_ne x 0 with rfl | hx
    · have A : ContinuousAt (fun p : ℝ × E ↦ (p.1 - ‖p.2‖) / (p.1 - 1)) (R, 0) := by
        fun_prop (disch := positivity)
      have B : ∀ᶠ p in 𝓝 (R, (0 : E)), 1 ≤ (p.1 - ‖p.2‖) / (p.1 - 1) :=
        A.eventually <| le_mem_nhds <| (one_lt_div hR).2 <| sub_lt_sub_left (by simp) _
      refine (contDiffAt_const (c := 1)).congr_of_eventuallyEq <| B.mono fun _ ↦
        smoothTransition.one_of_one_le
    · refine smoothTransition.contDiffAt.comp _ (ContDiffAt.div ?_ (by fun_prop) hR.ne')
      exact contDiffAt_fst.sub (contDiffAt_snd.norm ℝ hx)

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

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
⊢ (fderiv ℝ fun x ↦ ‖x‖ ^ 2) = 2 • ⇑(innerSL ℝ)

Tactic:
by
  ext1; simp

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

Goal state before:
pp: ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f f' : ι → 𝕜 → G
x : 𝕜
inst✝ : IsRCLikeNormedField 𝕜
r : ℝ
hf' : UniformCauchySeqOn f' l (Metric.ball x r)
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
⊢ UniformCauchySeqOn f l (Metric.ball x r)

Tactic:
simp_rw [hasDerivAt_iff_hasFDerivAt] at hf
  have hf' :
    UniformCauchySeqOn (fun n => fun z => (1 : 𝕜 →L[𝕜] 𝕜).smulRight (f' n z)) l
      (Metric.ball x r) :=
    (ContinuousLinearMap.smulRightL 𝕜 𝕜 G 1).uniformContinuous.comp_uniformCauchySeqOn hf'
  exact uniformCauchySeqOn_ball_of_fderiv hf' hf hfg

Goal state after:
Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : ProperSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a z : α
r : ℝ
hf : ContinuousOn f (closedBall a r)
hz : z ∈ closedBall a r
hf1 : ∀ z' ∈ sphere a r, f z < f z'
⊢ ∃ z ∈ ball a r, IsLocalMin f z

Tactic:
simp_rw [← closedBall_sdiff_ball] at hf1
  exact (isCompact_closedBall a r).exists_isLocalMin_mem_open ball_subset_closedBall hf hz hf1
    isOpen_ball

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 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✝⁴ : 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₀ ≤ ε
x : G
hx : x ∈ (fun t ↦ x₀ - t) ⁻¹' ball 0 R
⊢ x ∈ ball x₀ R

Tactic:
mem_ball_iff_norm,

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✝⁴ : 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₀ ≤ ε
x : G
hx : x ∈ (fun t ↦ x₀ - t) ⁻¹' ball 0 R
⊢ ‖x - x₀‖ < R
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 ≤ ‖(fun x ↦ ε UV) y‖

Tactic:
exact le_abs_self _

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

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n ↦ ↑(g0 n)
⊢ ∃ f, support f = s ∧ ContDiff ℝ (↑n) f ∧ range f ⊆ Icc 0 1

Tactic:
have g_s : ∀ n, support (g n) ⊆ s := fun n => (g0 n).2.1

Goal state after:
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n ↦ ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
⊢ ∃ f, support f = s ∧ ContDiff ℝ (↑n) f ∧ range f ⊆ Icc 0 1
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), f x ∂μ = ∫ (x : G), f x * (D x)⁻¹ * D x ∂μ

Tactic:
congr with x; rw [mul_assoc, inv_mul_cancel₀ (D_pos x).ne', mul_one]

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case pos
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'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst✝ : NullSingletonClass ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : 0 < t
⊢ (L ((Ioi 0).indicator f t)) ((Ioi 0).indicator g (x - t)) = 0

pp: case neg
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'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst✝ : NullSingletonClass ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : ¬0 < t
⊢ (L ((Ioi 0).indicator f t)) ((Ioi 0).indicator g (x - t)) = 0

Tactic:
· rw [indicator_of_notMem (_ : x - t ∉ Ioi 0), map_zero]
      rw [notMem_Ioi] at h ⊢
      exact sub_nonpos.mpr (h.trans ht.le)

Goal state after:
case neg
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'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst✝ : NullSingletonClass ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : ¬0 < t
⊢ (L ((Ioi 0).indicator f t)) ((Ioi 0).indicator g (x - t)) = 0
Module: Mathlib.Analysis.Calculus.BumpFunction.Normed

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

Tactic:
rw [support_div, f.support_eq, support_const f.integral_pos.ne', inter_univ]

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)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (fun n ↦ ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂ν))
⊢ μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ • μ (f ⁻¹' {1})

Tactic:
have M n : ∫ (x : G), v n (f x) ∂μ' = ∫ (x : G), v n (f x) ∂(haarScalarFactor μ' μ • μ) := by
    apply integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ (vf_cont n)
    apply h'f.comp_left
    simp only [v, thickenedIndicator_apply, NNReal.coe_eq_zero]
    rw [thickenedIndicatorAux_zero (u_mem n).1]
    · simp only [ENNReal.toNNReal_zero]
    · simpa using (u_mem n).2.le

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)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (fun n ↦ ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), ∫ (x : G), v n (f x) ∂μ' = ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ
⊢ μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ • μ (f ⁻¹' {1})
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
this : ContDiffOn ℝ ∞ (uncurry y ∘ fun p ↦ ((p.1 - 1) / (p.1 + 1), ((p.1 + 1) / 2)⁻¹ • p.2)) (Ioi 1 ×ˢ univ)
⊢ ContDiffOn ℝ ∞ (uncurry fun R x ↦ if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0) (Ioi 1 ×ˢ univ)

Tactic:
by
          apply this.congr
          rintro ⟨R, x⟩ ⟨hR : 1 < R, _⟩
          simp only [hR, uncurry_apply_pair, if_true, Function.comp_apply]

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✝² : IsFiniteMeasureOnCompacts μ'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst✝⁹] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst✝⁹, _] f
hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure[inst✝⁹] s)
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst✝⁹] t
t_comp : IsCompact t
st : s ⊆ t
A : ν (t \ s) ≤ μ' (t \ s)
⊢ μ' s ≤ ν s

Tactic:
have B : μ' t = ν t :=
    measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport _ _ f_cont f_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✝² : IsFiniteMeasureOnCompacts μ'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst✝⁹] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst✝⁹, _] f
hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure[inst✝⁹] s)
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst✝⁹] t
t_comp : IsCompact t
st : s ⊆ t
A : ν (t \ s) ≤ μ' (t \ s)
B : μ' t = ν t
⊢ μ' s ≤ ν s
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ ∃ δ,
    0 < δ ∧
      δ < 1 ∧
        ∀ (s : Finset E), (∀ c ∈ s, ‖c‖ ≤ 2) → (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) → s.card ≤ multiplicity E

Tactic:
by_contra! h

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
h :
  ∀ (δ : ℝ),
    0 < δ → δ < 1 → ∃ s, (∀ c ∈ s, ‖c‖ ≤ 2) ∧ (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) ∧ multiplicity E < s.card
⊢ False