mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
x✝ : Fin 8
⊢ ↑(χ₈ x✝) * τ ^ ↑x✝ = χ x✝ * ψ₈char x✝

Tactic:
congr

Goal state after:
case e_a.e_a
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
x✝ : Fin 8
⊢ τ = IsCyclotomicExtension.zeta (↑8) F (CyclotomicField (↑8) F)
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case hxy.e'_6.a
ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
⊢ (∫⋯∫⁻_{i, j}, f ∂μ) x = (∫⋯∫⁻_{j} ∪ {i}, f ∂μ) x

Tactic:
congr

Goal state after:
case hxy.e'_6.a.e_s
ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
⊢ {i, j} = {j} ∪ {i}
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case e'_4
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ ∫⋯∫⁻_sᶜ, f ∂μ = ∫⋯∫⁻_{i} ∪ (insert i s)ᶜ, f ∂μ

Tactic:
rw [← insert_compl_insert hi]
      rfl

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

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
T : E →ₗ[𝕜] E
f : E ≃ₗᵢ[𝕜] F
⊢ T.IsSymmetric → ((∀ (x : F), 0 ≤ re ⟪(⇑f ∘ ⇑T ∘ ⇑f.symm) x, x⟫) ↔ ∀ (x : E), 0 ≤ re ⟪T x, x⟫)

Tactic:
Function.comp_apply,

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
T : E →ₗ[𝕜] E
f : E ≃ₗᵢ[𝕜] F
⊢ T.IsSymmetric → ((∀ (x : F), 0 ≤ re ⟪f (T (f.symm x)), x⟫) ↔ ∀ (x : E), 0 ≤ re ⟪T x, x⟫)
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:

Tactic:
∫⁻ x, ‖u x‖ₑ ^ p
      = ∫⁻ x, (‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ))) ^ (#ι : ℝ) := by
        -- a little algebraic manipulation of the exponent
        congr! 2 with x
        rw [← ENNReal.rpow_mul, hp.conjugate_eq]
        field_simp
    _ = ∫⁻ x, ∏ _i : ι, ‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ)) := by
        -- express the left-hand integrand as a product of identical factors
        congr! 2 with x
        simp_rw [prod_const]
        norm_cast
    _ ≤ ∫⁻ x, ∏ i, (∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ) ^ ((1 : ℝ) / (#ι - 1 : ℝ)) := ?_
    _ ≤ (∫⁻ x, ‖fderiv ℝ u x‖ₑ) ^ p := by
        -- apply the grid-lines lemma
        apply lintegral_prod_lintegral_pow_le _ hp
        fun_prop

Goal state after:
ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
⊢ ∫⁻ (x : ι → ℝ), ∏ _i, ‖u x‖ₑ ^ (1 / (↑#ι - 1)) ≤
    ∫⁻ (x : ι → ℝ), ∏ i, (∫⁻ (xᵢ : ℝ), ‖fderiv ℝ u (update x i xᵢ)‖ₑ) ^ (1 / (↑#ι - 1))
Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram

Goal state before:
pp: V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ (↑(continuousLinearMapOfBilin B)).ker = ⊥

Tactic:
LinearMap.ker_eq_bot

Goal state after:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ Function.Injective ⇑↑(continuousLinearMapOfBilin B)
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
⊢ (f.closure.domRestrict f.domain).closure = f.closure

Tactic:
congr

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
⊢ f.closure.domRestrict f.domain = f
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p
v : (ι → ℝ) → F := u ∘ ⇑e.symm
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ ↑(‖↑e.symm‖₊ ^ p) * (∫⁻ (y : ι → ℝ), ‖fderiv ℝ u (e.symm y)‖ₑ) ^ p =
    ↑(‖↑e.symm‖₊ ^ p) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂Measure.map (⇑e.symm) volume) ^ p

Tactic:
congr

Goal state after:
case e_a.e_a
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p
v : (ι → ℝ) → F := u ∘ ⇑e.symm
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ ∫⁻ (y : ι → ℝ), ‖fderiv ℝ u (e.symm y)‖ₑ = ∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂Measure.map (⇑e.symm) volume
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
x : F × E
h : ∀ (a : E) (a_1 : a ∈ T.domain), ⟪↑T ⟨a, ⋯⟩, x.1⟫ = ⟪a, x.2⟫
hx : x.1 ∈ T†.domain
⊢ ∀ v ∈ ↑T.domain, ⟪v, ↑T† ⟨x.1, ⋯⟩⟫ = ⟪v, x.2⟫

Tactic:
rintro a ha

Goal state after:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
x : F × E
h : ∀ (a : E) (a_1 : a ∈ T.domain), ⟪↑T ⟨a, ⋯⟩, x.1⟫ = ⟪a, x.2⟫
hx : x.1 ∈ T†.domain
a : E
ha : a ∈ ↑T.domain
⊢ ⟪a, ↑T† ⟨x.1, ⋯⟩⟫ = ⟪a, x.2⟫
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
h2γ : γ * n' = p'
h3γ : (↑γ - 1) * q = ↑p'
h4γ : ↑γ ≠ 0
h3u : ¬∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ = 0
h4u : ∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ ≠ ∞
h5u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ 0
h6u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ ∞
h7u : Continuous u
v : E → ℝ := fun x ↦ ‖u x‖ ^ ↑γ
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
C : ℝ≥0 := eLpNormLESNormFDerivOneConst μ ↑n'
this✝ :
  (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / ↑n') ≤
    ↑C * ↑γ * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p) * (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q)
this : ↑C * ↑γ = ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p)
⊢ ↑C * ↑γ * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p) =
    ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p)

Tactic:
congr

Goal state after:
case e_a
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
h2γ : γ * n' = p'
h3γ : (↑γ - 1) * q = ↑p'
h4γ : ↑γ ≠ 0
h3u : ¬∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ = 0
h4u : ∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ ≠ ∞
h5u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ 0
h6u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ ∞
h7u : Continuous u
v : E → ℝ := fun x ↦ ‖u x‖ ^ ↑γ
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
C : ℝ≥0 := eLpNormLESNormFDerivOneConst μ ↑n'
this✝ :
  (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / ↑n') ≤
    ↑C * ↑γ * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p) * (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q)
this : ↑C * ↑γ = ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p)
⊢ ↑C * ↑γ = ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p)
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Tactic:
set S : ℕ → Set X := fun n => {x ∈ s | (↑n)⁻¹ ≤ infEDist x t}

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
s : Set ι
hs : s.Countable
t : ι → Set X
⊢ dimH (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)

Tactic:
have := hs.toEncodable

Goal state after:
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
s : Set ι
hs : s.Countable
t : ι → Set X
this : Encodable ↑s
⊢ dimH (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
⊢ mkMetric m₁ ≤ c • mkMetric m₂

Tactic:
rcases (mem_nhdsGE_iff_exists_Ico_subset' zero_lt_one).1 hle with ⟨r, hr0, hr⟩

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
r : ℝ≥0∞
hr0 : r ∈ Ioi 0
hr : Ico 0 r ⊆ {x | (fun x ↦ m₁ x ≤ (c • m₂) x) x}
⊢ mkMetric m₁ ≤ c • mkMetric m₂
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
r : ℝ≥0∞
hr0 : r ∈ Ioi 0
hr : Ico 0 r ⊆ {x | (fun x ↦ m₁ x ≤ (c • m₂) x) x}
s : Set X
r' : ℝ≥0∞
hr' : r' ∈ Ioo 0 r
⊢ (boundedBy (extend fun s x ↦ m₁ (ediam s))) s ≤ c • (boundedBy (extend fun s x ↦ m₂ (ediam s))) s

Tactic:
← smul_apply,

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ ∞
h0 : c ≠ 0
hle : m₁ ≤ᶠ[𝓝[≥] 0] c • m₂
r : ℝ≥0∞
hr0 : r ∈ Ioi 0
hr : Ico 0 r ⊆ {x | (fun x ↦ m₁ x ≤ (c • m₂) x) x}
s : Set X
r' : ℝ≥0∞
hr' : r' ∈ Ioo 0 r
⊢ (boundedBy (extend fun s x ↦ m₁ (ediam s))) s ≤ (c • boundedBy (extend fun s x ↦ m₂ (ediam s))) s
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
hrank' : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction :=
  (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.mk' p (ℝ ∙ v)).direction ⋯)
hf : MeasurableEmbedding ⇑f
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⟨p, ⋯⟩
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⇑(IsometryEquiv.vaddConst p') ∘ ⇑f
hadd : MeasurableEmbedding ⇑(IsometryEquiv.vaddConst p')
hg : MeasurableEmbedding g
⊢ map (⇑(IsometryEquiv.vaddConst p')) volume = map (⇑(IsometryEquiv.vaddConst p')) (‖v‖ₑ • map (⇑f) volume)

Tactic:
congr

Goal state after:
case e_μ
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
hrank' : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction :=
  (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.mk' p (ℝ ∙ v)).direction ⋯)
hf : MeasurableEmbedding ⇑f
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⟨p, ⋯⟩
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⇑(IsometryEquiv.vaddConst p') ∘ ⇑f
hadd : MeasurableEmbedding ⇑(IsometryEquiv.vaddConst p')
hg : MeasurableEmbedding g
⊢ volume = ‖v‖ₑ • map (⇑f) volume
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
b : OrthonormalBasis ι 𝕜 U
h : f.ker = ⊥
bv : OrthonormalBasis ι 𝕜 ↥f.range := orthonormalBasis_range h b
⊢ (algebraMap ℝ 𝕜) ‖((toMatrix b.toBasis bv.toBasis) f.rangeRestrict).det‖ ^ 2 =
    ↑‖(Matrix.of fun i j ↦ (bv.repr (f.rangeRestrict (b j))).ofLp i).det‖ ^ 2

Tactic:
congr

Goal state after:
case pos.e_a.e_6
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
b : OrthonormalBasis ι 𝕜 U
h : f.ker = ⊥
bv : OrthonormalBasis ι 𝕜 ↥f.range := orthonormalBasis_range h b
⊢ (toMatrix b.toBasis bv.toBasis) f.rangeRestrict = Matrix.of fun i j ↦ (bv.repr (f.rangeRestrict (b j))).ofLp i
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inl
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ∞
c : ℝ≥0
hc : c ≠ 0
this : 0 < ↑c ^ (d₂ - d₁)⁻¹
hr₀ : 0 ≤ ↑0
hrc : ↑0 < ↑c ^ (d₂ - d₁)⁻¹
⊢ ↑0 ^ d₂ / ↑0 ^ d₁ ≤ ↑c

Tactic:
rcases lt_or_ge 0 d₂ with (h₂ | h₂)
    · simp only [h₂, ENNReal.zero_rpow_of_pos, zero_le, ENNReal.zero_div, ENNReal.coe_zero]
    · simp only [h.trans_le h₂, ENNReal.div_top, zero_le, ENNReal.zero_rpow_of_neg,
        ENNReal.coe_zero]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℚ
x : E
⊢ ∀ (y : E), inner_ 𝕜 (↑r • x) y = (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y

Tactic:
y

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℚ
x y : E
⊢ inner_ 𝕜 (↑r • x) y = (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℝ
x : E
⊢ ∀ (y : E), inner_ 𝕜 (↑r • x) y = (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y

Tactic:
y

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℝ
x y : E
⊢ inner_ 𝕜 (↑r • x) y = (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
r : ℕ → ℝ≥0∞ := fun x ↦ 0
t : ℕ → Unit → Set X := fun x_1 x_2 ↦ {x}
ht : ∀ᶠ (n : ℕ) in atTop, ∀ (i : Unit), ediam (t n i) ≤ r n
⊢ μH[0] {x} ≤ 1

Tactic:
simpa [t, liminf_const] using hausdorffMeasure_le_liminf_sum 0 {x} r tendsto_const_nhds t ht

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x : E
⊢ ∀ (y : E), inner_ 𝕜 (I • x) y = (starRingEnd 𝕜) I * inner_ 𝕜 x y

Tactic:
y

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
⊢ inner_ 𝕜 (I • x) y = (starRingEnd 𝕜) I * inner_ 𝕜 x y
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: case mp
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
h : ∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0
⊢ ∀ y ∈ S, ⟪y, x⟫.im = 0

Tactic:
y

Goal state after:
case mp
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
h : ∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0
y : H
⊢ y ∈ S → ⟪y, x⟫.im = 0
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : 𝕜
x : E
⊢ ∀ (y : E), inner_ 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner_ 𝕜 x y

Tactic:
y

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : 𝕜
x y : E
⊢ inner_ 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner_ 𝕜 x y
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inr.refine_2
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d ↦ ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → ↑C * x ^ ↑r < R
t : ℕ → Set X
hst : s ⊆ ⋃ n, t n
htδ : ∀ (n : ℕ), ediam (t n) ≤ δ
⊢ ∑' (n : ℕ), ⨆ (_ : ((fun n ↦ f '' (t n ∩ s)) n).Nonempty), ediam ((fun n ↦ f '' (t n ∩ s)) n) ^ d ≤
    ∑' (i : ℕ), ⨆ (_ : (t i).Nonempty), ↑C ^ d * ediam (t i) ^ (↑r * d)

Tactic:
· refine ENNReal.tsum_le_tsum fun n => ?_
      simp only [iSup_le_iff, image_nonempty]
      intro hft
      simp only [Nonempty.mono ((t n).inter_subset_left) hft, ciSup_pos]
      rw [ENNReal.rpow_mul, ← ENNReal.mul_rpow_of_nonneg _ _ hd]
      gcongr
      exact h.ediam_image_inter_le _

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹⁰ : EMetricSpace X
inst✝⁹ : EMetricSpace Y
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
| μH[↑(finrank ℝ E)] (⇑e '' K)

Tactic:
congr

Goal state after:
case a
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹⁰ : EMetricSpace X
inst✝⁹ : EMetricSpace Y
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
| μH[↑(finrank ℝ E)]