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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
⊢ ‖⟪x, r • x⟫‖ / (‖x‖ * ‖r • x‖) = 1

Tactic:
have hx' : ‖x‖ ≠ 0 := by simp [hx]
  have hr' : ‖r‖ ≠ 0 := by simp [hr]
  rw [inner_smul_right, norm_mul, ← inner_self_re_eq_norm, inner_self_eq_norm_mul_norm, norm_smul]
  rw [← mul_assoc, ← div_div, mul_div_cancel_right₀ _ hx', ← div_div, mul_comm,
    mul_div_cancel_right₀ _ hr', div_self hx']

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro ⟨v, hv⟩
eq : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ w, ‖u - ↑w‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : 0 ≤ θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)
⊢ 2 * p ≤ θ * q

Tactic:
have eq₂ :
        θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ =
          θ * (θ * ‖w - v‖ ^ 2 - 2 * ⟪u - v, w - v⟫_ℝ) := by ring

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro ⟨v, hv⟩
eq : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ w, ‖u - ↑w‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : 0 ≤ θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)
eq₂ : θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ = θ * (θ * ‖w - v‖ ^ 2 - 2 * ⟪u - v, w - v⟫_ℝ)
⊢ 2 * p ≤ θ * q
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
⊢ Orthonormal 𝕜 v → ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0

Tactic:
intro hv i j
    split_ifs with h
    · simp [h, inner_self_eq_norm_sq_to_K, hv.norm_eq_one]
    · exact hv.inner_eq_zero h

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

Goal state before:

Tactic:
‖x‖ * ‖x‖ = ‖(⟪x, x⟫ : 𝕜)‖ := by
        rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm]
      _ ≤ ‖innerSL 𝕜 x‖ * ‖x‖ := (innerSL 𝕜 x).le_opNorm _

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
⊢ Kᗮ.reflection v = -K.reflection v

Tactic:
simp [reflection_apply]; abel

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsSymmetric
hf' : f ≠ 0
α : 𝕜
⊢ (α • f).IsSymmetric ↔ IsSelfAdjoint α

Tactic:
by
  refine ⟨fun h ↦ ?_, hf.smul⟩
  simp only [ne_eq, LinearMap.ext_iff, zero_apply, ext_iff_inner_left 𝕜 (E := E),
    inner_zero_right] at hf'
  simpa [IsSymmetric, inner_smul_left, inner_smul_right, hf _ _, forall_or_left,
    (forall_comm.eq ▸ hf')] using! h

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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ ((edist f.fst g.fst + edist g.fst h.fst) ^ p.toReal + (edist f.snd g.snd + edist g.snd h.snd) ^ p.toReal) ^
      (1 / p.toReal) ≤
    (edist f.fst g.fst ^ p.toReal + edist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal) +
      (edist g.fst h.fst ^ p.toReal + edist g.snd h.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
have := ENNReal.Lp_add_le {0, 1}
            (if · = 0 then edist f.fst g.fst else edist f.snd g.snd)
            (if · = 0 then edist g.fst h.fst else edist g.snd h.snd) hp
          simp only [Finset.mem_singleton, not_false_eq_true, Finset.sum_insert,
            Finset.sum_singleton, reduceCtorEq] at this
          exact this

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

Goal state before:
pp: case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x y ≤ ↑(2 ^ (1 / p).toReal) * edist x.ofLp y.ofLp

Tactic:
rw [prod_edist_eq_add pos, ENNReal.toReal_div 1 p]

Goal state after:
case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) ≤
    ↑(2 ^ (ENNReal.toReal 1 / p.toReal)) * edist x.ofLp y.ofLp
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp p (α × β)
⊢ dist x y = ‖-x + y‖

Tactic:
rcases p.dichotomy with (rfl | h)
    · simp only [prod_dist_eq_sup, prod_norm_eq_sup, dist_eq_norm, ← norm_neg_add]
      rfl
    · simp only [prod_dist_eq_add (zero_lt_one.trans_le h),
        prod_norm_eq_add (zero_lt_one.trans_le h), dist_eq_norm, ← norm_neg_add]
      rfl

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp.refine_2.inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : ⟨a, ha'⟩ ≠ ⟨b, hb'⟩
hb : b = e
⊢ ⟪↑⟨a, ha'⟩, ↑⟨b, hb'⟩⟫_𝕜 = 0

Tactic:
simpa [hb] using h_end a ha

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: case right
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ A.det * star A.det = 1

Tactic:
· simpa [star, det_transpose] using congr_arg det hA.2

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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : NormSMulClass 𝕜 α
inst✝ : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

Tactic:
rcases p.dichotomy with (rfl | hp)
    · simp only [← prod_nnnorm_ofLp, WithLp.ofLp_smul, nnnorm_smul]
    · have hp0 : 0 < p.toReal := zero_lt_one.trans_le hp
      have hpt : p ≠ ⊤ := p.toReal_pos_iff_ne_top.mp hp0
      rw [prod_nnnorm_eq_add hpt, prod_nnnorm_eq_add hpt, one_div, NNReal.rpow_inv_eq_iff hp0.ne',
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, mul_add,
        ← NNReal.mul_rpow, ← NNReal.mul_rpow, smul_fst, smul_snd, nnnorm_smul, nnnorm_smul]

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

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
this : ↑(Fintype.card ι) = ↑↑(Fintype.card ι)
⊢ ↑↑(Fintype.card ι) ^ (1 / p.toReal) * edist x.ofLp y.ofLp =
    ↑(↑(Fintype.card ι) ^ (1 / p.toReal)) * edist x.ofLp y.ofLp

Tactic:
ENNReal.coe_rpow_of_nonneg _ nonneg

Goal state after:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
this : ↑(Fintype.card ι) = ↑↑(Fintype.card ι)
⊢ ↑↑(Fintype.card ι) ^ (1 / p.toReal) * edist x.ofLp y.ofLp = ↑↑(Fintype.card ι) ^ (1 / p.toReal) * edist x.ofLp y.ofLp
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
⊢ 𝓤 (PiLp p β) = 𝓤 (WithLp p ((i : ι) → β i))

Tactic:
rw [← (isUniformInducing_ofLp_aux p β).comap_uniformity]

Goal state after:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
⊢ comap (fun x ↦ (x.1.ofLp, x.2.ofLp)) (𝓤 ((i : ι) → β i)) = 𝓤 (WithLp p ((i : ι) → β i))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
⊢ volume (univ.pi fun i ↦ Icc (a i) (b i)) = ∏ i, ofReal (b i - a i)

Tactic:
volume_pi_pi

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
⊢ ∏ i, volume (Icc (a i) (b i)) = ∏ i, ofReal (b i - a i)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring 𝕜
inst✝³ : (i : ι) → SeminormedAddCommGroup (α i)
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (α i)
inst✝ : (i : ι) → Module 𝕜 (β i)
c : 𝕜
e : (i : ι) → α i ≃ₗᵢ[𝕜] β i
x : (i : ι) → α i
hp : Fact (1 ≤ ∞)
__LinearEquiv✝ : PiLp ∞ α ≃ₗ[𝕜] PiLp ∞ β :=
  (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → α i) ≪≫ₗ LinearEquiv.piCongrRight fun i ↦ (e i).toLinearEquiv) ≪≫ₗ
    (WithLp.linearEquiv ∞ 𝕜 ((i : ι) → β i)).symm
⊢ ↑(Finset.univ.sup fun b ↦ ‖(e b) (x b)‖₊) = ↑(Finset.univ.sup fun b ↦ ‖x b‖₊)

Tactic:
LinearIsometryEquiv.nnnorm_map

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

Goal state before:
pp: case mpr
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v g : ι → E
t : {i : ι} → ℝ
ht : ∀ {i : ι}, t ∈ Icc 0 1
hg : ∀ {i : ι}, (fun a ↦ a • v i) t = g i
⊢ ∑ i, g i = ∑ i, t • v i

Tactic:
simp_rw [hg]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ (μ.prod volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
rw [Measure.prod_apply]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ ∫⁻ (x : α), volume (Prod.mk x ⁻¹' regionBetween f g s) ∂μ = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet (regionBetween f g s)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

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 : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = ↑e ∘ₗ f ∘ₗ ↑e.symm
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ

Tactic:
have gdet : LinearMap.det g = LinearMap.det f := by rw [hg]; exact LinearMap.det_conj f e

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = ↑e ∘ₗ f ∘ₗ ↑e.symm
gdet : LinearMap.det g = LinearMap.det f
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
⊢ InjOn (fun J ↦ {i | J.lower i = x i}) {J | J ∈ π ∧ x ∈ Box.Icc J}

Tactic:
by
  rintro J₁ ⟨h₁, hx₁⟩ J₂ ⟨h₂, hx₂⟩ (H : { i | J₁.lower i = x i } = { i | J₂.lower i = x i })
  suffices ∀ i, (Ioc (J₁.lower i) (J₁.upper i) ∩ Ioc (J₂.lower i) (J₂.upper i)).Nonempty by
    choose y hy₁ hy₂ using this
    exact π.eq_of_mem_of_mem h₁ h₂ hy₁ hy₂
  intro i
  simp only [Set.ext_iff, mem_ofPred] at H
  rcases (hx₁.1 i).eq_or_lt with hi₁ | hi₁
  · have hi₂ : J₂.lower i = x i := (H _).1 hi₁
    have H₁ : x i < J₁.upper i := by simpa only [hi₁] using J₁.lower_lt_upper i
    have H₂ : x i < J₂.upper i := by simpa only [hi₂] using J₂.lower_lt_upper i
    rw [Set.Ioc_inter_Ioc, hi₁, hi₂, sup_idem, Set.nonempty_Ioc]
    exact lt_min H₁ H₂
  · have hi₂ : J₂.lower i < x i := (hx₂.1 i).lt_of_ne (mt (H _).2 hi₁.ne)
    exact ⟨x i, ⟨hi₁, hx₁.2 i⟩, ⟨hi₂, hx₂.2 i⟩⟩

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
M : Type u_2
inst✝ : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
⊢ ∑ J ∈ π.boxes.biUnion fun J ↦ (πi J).boxes, f J = ∑ J ∈ π.boxes, ∑ J' ∈ (πi J).boxes, f J'

Tactic:
by
  refine Finset.sum_biUnion fun J₁ h₁ J₂ h₂ hne => Finset.disjoint_left.2 fun J' h₁' h₂' => ?_
  exact hne (π.eq_of_le_of_le h₁ h₂ ((πi J₁).le_of_mem h₁') ((πi J₂).le_of_mem h₂'))

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

Goal state before:
pp: n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x✝ : EuclideanSpace ℝ n
⊢ √(∑ x, x✝.ofLp x ^ 2) ≤ r ↔ ∑ x, x✝.ofLp x ^ 2 ≤ r ^ 2

Tactic:
sqrt_le_left hr

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
⊢ (range ⇑I.splitCenterBoxEmb).Pairwise (Function.onFun Disjoint Box.toSet)

Tactic:
rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩ Hne

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
s t : Set ι
Hne : I.splitCenterBoxEmb s ≠ I.splitCenterBoxEmb t
⊢ Function.onFun Disjoint Box.toSet (I.splitCenterBoxEmb s) (I.splitCenterBoxEmb t)
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: case inl
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ≤ I.lower i
⊢ I.splitLower i x ≠ I.splitUpper i x

Tactic:
rw [splitUpper_eq_self.2 h, splitLower_eq_bot.2 h]
    exact WithBot.bot_ne_coe

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
this✝¹ : Module.Finite ℤ ↥L
this✝ : Free ℤ ↥L
e : Free.ChooseBasisIndex ℤ ↥L ≃ ι := (Free.chooseBasis ℤ ↥L).indexEquiv b
this : Fintype ι
⊢ Fintype.card ι = finrank K E

Tactic:
· rw [← Fintype.card_congr e, ← finrank_eq_card_chooseBasisIndex, ZLattice.rank K L]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

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
s : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
I : ∀ (u v : Set E), μ u ≠ 0 → μ u ≠ ∞ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u
⊢ Tendsto (fun r ↦ μ (sᶜ ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)

Tactic:
have A : Tendsto (fun r => μ (closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1) := by
      apply tendsto_const_nhds.congr' _
      filter_upwards [self_mem_nhdsWithin]
      intro r hr
      rw [div_eq_mul_inv, ENNReal.mul_inv_cancel]
      · exact (measure_closedBall_pos μ _ hr).ne'
      · exact measure_closedBall_lt_top.ne

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
I : ∀ (u v : Set E), μ u ≠ 0 → μ u ≠ ∞ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u
A : Tendsto (fun r ↦ μ (closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
⊢ Tendsto (fun r ↦ μ (sᶜ ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B x✝¹ : Box ι
hI₁ : x✝¹ ∈ ↑(Finset.image (fun ν ↦ box n ν) (admissibleIndex n B))
x✝ : Box ι
hI₂ : x✝ ∈ ↑(Finset.image (fun ν ↦ box n ν) (admissibleIndex n B))
h : x✝¹ ≠ x✝
⊢ Function.onFun Disjoint Box.toSet x✝¹ x✝

Tactic:
obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hI₁

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
B x✝ : Box ι
hI₂ : x✝ ∈ ↑(Finset.image (fun ν ↦ box n ν) (admissibleIndex n B))
w✝ : ι → ℤ
left✝ : w✝ ∈ admissibleIndex n B
hI₁ : box n w✝ ∈ ↑(Finset.image (fun ν ↦ box n ν) (admissibleIndex n B))
h : box n w✝ ≠ x✝
⊢ Function.onFun Disjoint Box.toSet (box n w✝) x✝
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
x : M [⋀^ι]→ₗ[R] R
hx✝ : x ≠ 0
hx : x ⇑e ≠ 0
⊢ SameRay R x e.det ∨ rayOfNeZero R x hx✝ = -rayOfNeZero R e.det ⋯

Tactic:
neg_rayOfNeZero,

Goal state after:
case h
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
x : M [⋀^ι]→ₗ[R] R
hx✝ : x ≠ 0
hx : x ⇑e ≠ 0
⊢ SameRay R x e.det ∨ rayOfNeZero R x hx✝ = rayOfNeZero R (-e.det) ⋯
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
inst✝ : CompleteSpace F
h : Integrable I l f vol
h0 : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
π₀ : Prepartition I
hU : π.iUnion = π₀.iUnion
δ : ℝ
δ0 : 0 < δ
δ' : ℝ := δ / (↑(#π₀.boxes) + 1)
H0 : 0 < ↑(#π₀.boxes) + 1
δ'0 : 0 < δ'
C : ℝ≥0 := max π₀.distortion π₀.compl.distortion
πi : (J : Box ι) → TaggedPrepartition J
hπip : ∀ J ∈ π₀, (πi J).IsPartition
hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'
hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)
this✝ : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi)
hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion
this : dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) ≤ ε + δ'
⊢ dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ

Tactic:
calc
    dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤
        dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) +
          dist (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) (∑ J ∈ π₀.boxes, integral J l f vol) :=
      dist_triangle _ _ _
    _ ≤ ε + δ' + ∑ _J ∈ π₀.boxes, δ' := add_le_add this (dist_sum_sum_le_of_le _ hπiδ')
    _ = ε + δ := by simp [field, δ']; ring

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₁ π₂ : Prepartition I
hU : π₁.iUnion = π₂.iUnion
⊢ Tendsto (integralSum f vol) (toFilteriUnion I π₁) (𝓝 (∑ J ∈ π₂.boxes, integral J l f vol))

Tactic:
l.toFilteriUnion_congr _ hU

Goal state after:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₁ π₂ : Prepartition I
hU : π₁.iUnion = π₂.iUnion
⊢ Tendsto (integralSum f vol) (toFilteriUnion I π₂) (𝓝 (∑ J ∈ π₂.boxes, integral J l f vol))
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : InnerProductSpace ℝ F
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : FiniteDimensional ℝ E
inst✝ : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
⊢ MeasurePreserving (⇑f) volume volume

Tactic:
refine ⟨f.continuous.measurable, ?_⟩

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : InnerProductSpace ℝ F
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : FiniteDimensional ℝ E
inst✝ : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
⊢ map (⇑f) volume = volume
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ι : Type u_2
inst✝ : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
⊢ c • {x | x ∈ X ∧ F x ≤ 1} = {x | x ∈ X ∧ F x ≤ c ^ card ι}

Tactic:
ext x
  simp_rw [Set.mem_smul_set_iff_inv_smul_mem₀ hc.ne', Set.mem_ofPred_eq, hF₁ _
    (inv_pos_of_pos hc).le, inv_pow, inv_mul_le_iff₀ (pow_pos hc _), mul_one, and_congr_left_iff]
  exact fun _ ↦ ⟨fun h ↦ (smul_inv_smul₀ hc.ne' x) ▸ hX h hc, fun h ↦ hX h (inv_pos_of_pos hc)⟩

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ Bornology.IsBounded (range f) ↔ f =O[cocompact D] 1

Tactic:
constructor <;> intro h
  · rw [isBounded_iff_forall_norm_le] at h
    obtain ⟨c, hc⟩ := h
    simp only [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff] at hc
    rw [isBigO_iff]
    use c
    apply Eventually.of_forall
    simpa using hc
  · simp_rw [isBigO_iff, Filter.Eventually, Filter.mem_cocompact] at h
    simp only [Pi.one_apply, norm_one, mul_one] at h
    obtain ⟨c, t, hcompact, h⟩ := h
    rw [← Set.image_union_image_compl_eq_range (s := t)]
    apply IsBounded.union
    · apply (IsCompact.image hcompact hf).isBounded
    · rw [isBounded_iff_forall_norm_le]
      refine ⟨c, fun x hx ↦ ?_⟩
      rw [Set.mem_image] at hx
      obtain ⟨y, hy, rfl⟩ := hx
      simpa using mem_of_mem_of_subset hy h

Goal state after: