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

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h✝ : IsCyclotomicExtension {n} A B
x : B
h : x ∈ ↑(nthRoots n 1).toFinset
⊢ x ∈ {b | n ≠ 0 ∧ b ^ n = 1}

Tactic:
by simpa [n.pos_of_neZero, NeZero.ne n] using h

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
⊢ ∀ (a : ZMod n), (zmodChar n ⋯) a = 1 → a = 0

Tactic:
intro a ha

Goal state after:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
a : ZMod n
ha : (zmodChar n ⋯) a = 1
⊢ a = 0
Module: Mathlib.Data.Int.Range

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
⊢ (∀ (r : ℤ), r ∈ m.range n → P r) ↔ ∀ (r : ℤ), m ≤ r → r < n → P r

Tactic:
simp only [mem_range_iff, and_imp]

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
⊢ ∀ (a : R), ¬IsUnit a → (if IsUnit a then 1 else 0) = 0

Tactic:
intro a ha

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
a : R
ha : ¬IsUnit a
⊢ (if IsUnit a then 1 else 0) = 0
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
hm : n ∣ m
a : ℤ
ha : IsCoprime a ↑m
⊢ χ (↑a).cast = χ ↑a

Tactic:
ZMod.cast_intCast hm

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
hm : n ∣ m
a : ℤ
ha : IsCoprime a ↑m
⊢ χ ↑a = χ ↑a
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∣ n
⊢ χ.FactorsThrough d ↔ (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker

Tactic:
refine ⟨fun ⟨_, ⟨χ₀, hχ₀⟩⟩ x hx ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∣ n
x✝ : χ.FactorsThrough d
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap hd).ker
w✝ : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel w✝) χ₀
⊢ x ∈ (toUnitHom χ).ker

case refine_2
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∣ n
h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
⊢ χ.FactorsThrough d
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
⊢ ∀ (a : R), ¬IsUnit a → (if hx : IsUnit a then ↑(f hx.unit) else 0) = 0

Tactic:
intro a ha

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
a : R
ha : ¬IsUnit a
⊢ (if hx : IsUnit a then ↑(f hx.unit) else 0) = 0
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
a✝ : Nontrivial R
⊢ ¬IsUnit a → χ⁻¹ a = χ a⁻¹ʳ

Tactic:
intro ha

Goal state after:
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
a✝ : Nontrivial R
ha : ¬IsUnit a
⊢ χ⁻¹ a = χ a⁻¹ʳ
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
⊢ (χ ^ 0) ↑a = χ ↑a ^ 0

Tactic:
rw [pow_zero, pow_zero, one_apply_coe]

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
inst✝ : NeZero n
⊢ FactorsThrough 1 1

Tactic:
exact (factorsThrough_one_iff _).mpr rfl

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
inst✝ : NeZero n
⊢ primitiveCharacter 1 = 1

Tactic:
have : NeZero (conductor (1 : DirichletCharacter R n)) :=
    ⟨@conductor_one R _ n _ ▸ Nat.one_ne_zero⟩

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
inst✝ : NeZero n
this : NeZero (conductor 1)
⊢ primitiveCharacter 1 = 1
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
⊢ (χ * ψ).conductor ∣ χ.conductor.lcm ψ.conductor

Tactic:
by
  obtain rfl | hn := eq_zero_or_neZero n
  · simp [conductor_eq_zero_iff_level_eq_zero.mpr]
  have h := Nat.lcm_dvd χ.conductor_dvd_level ψ.conductor_dvd_level
  rw [← mem_conductorSet_iff_conductor_dvd _ h, mem_conductorSet_iff]
  refine ⟨h, χ.primitiveCharacter.mul ψ.primitiveCharacter, ?_⟩
  rw [mul, MonoidHom.map_mul, ← changeLevel_trans, ← changeLevel_trans,
    changeLevel_primitiveCharacter, changeLevel_primitiveCharacter]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
h : χ ^ (orderOf χ - 1) = χ⁻¹
⊢ χ⁻¹ (-1) * ↑(Fintype.card R) = χ (-1) * ↑(Fintype.card R)

Tactic:
MulChar.inv_apply',

Goal state after:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
h : χ ^ (orderOf χ - 1) = χ⁻¹
⊢ χ (-1)⁻¹ * ↑(Fintype.card R) = χ (-1) * ↑(Fintype.card R)
Module: Mathlib.Analysis.InnerProductSpace.ExteriorPower

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : LinearOrder ι
b : OrthonormalBasis ι ℝ E
x y : ↥(⋀[ℝ]^n E)
⊢ (innerProductForm x) y =
    ∑ s, ((Module.Basis.exteriorPower n b.toBasis).repr y) s * ((Module.Basis.exteriorPower n b.toBasis).repr x) s

Tactic:
conv_lhs =>
    rw [← (b.toBasis.exteriorPower n).sum_repr x, ← (b.toBasis.exteriorPower n).sum_repr y]
  simp

Goal state after:
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
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
⊢ (↑(continuousLinearMapOfBilin B)).range = ⊤

Tactic:
← B♯.range.orthogonal_orthogonal

Goal state after:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
⊢ (↑(continuousLinearMapOfBilin B)).rangeᗮᗮ = ⊤
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_4
inst✝ : Finite n
M : Matrix n n 𝕜
this : Fintype n
⊢ (∃ m u, M = ∑ x, vecMulVec (u x).ofLp (star (u x).ofLp)) ↔ ∃ m v, M = ∑ i, vecMulVec (v i) (star (v i))

Tactic:
exact ⟨fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ (u i).ofLp, hu⟩,
    fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ WithLp.toLp 2 (u i), hu⟩⟩

Goal state after:
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
hf : f.IsClosable
⊢ f.graph.topologicalClosure = f.closure.graph

Tactic:
closure_def hf

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
hf : f.IsClosable
⊢ f.graph.topologicalClosure = (Exists.choose hf).graph
Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
𝕜 : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → α
g : α → E
x : α
h : Bornology.IsBounded (range fun x_1 ↦ g (f^[x_1] x))
⊢ Tendsto (fun n ↦ birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0)

Tactic:
by
  rcases Metric.isBounded_range_iff.1 h with ⟨C, hC⟩
  have : Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0) :=
    tendsto_const_nhds.div_atTop tendsto_natCast_atTop_atTop
  refine squeeze_zero_norm (fun n ↦ ?_) this
  rw [← dist_eq_norm, dist_birkhoffAverage_apply_birkhoffAverage]
  gcongr
  exact hC n 0

Goal state after:
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'
⊢ ↑C * ↑γ * ∫⁻ (x : E), ‖u x‖ₑ ^ (↑γ - 1) * ‖fderiv ℝ u x‖ₑ ∂μ ≤
    ↑C * ↑γ * ((∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p))

Tactic:
by
        gcongr
        convert!
          ENNReal.lintegral_mul_le_Lp_mul_Lq μ (.symm <| .conjExponent <| show 1 < (p : ℝ) from hp)
            ?_ ?_ using 5
        · simp [γ, n, q, ← ENNReal.rpow_mul, ← h3γ]
        · borelize F'
          fun_prop
        · fun_prop

Goal state after:
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
inst✝ : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖↑e.symm‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ ↑p
C₂ : ℝ≥0 := ‖↑e‖₊
v : E → F' := ⇑e ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this : eLpNorm v (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ v) (↑p) μ
x : E
⊢ ‖fderiv ℝ (⇑e) (u x)‖ * ‖fderiv ℝ u x‖ = ↑C₂ * ‖fderiv ℝ u x‖

Tactic:
e.fderiv,

Goal state after:
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
inst✝ : FiniteDimensional ℝ F
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hn : 0 < finrank ℝ E
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
F' : Type := EuclideanSpace ℝ (Fin (finrank ℝ F))
e : F ≃L[ℝ] F' := toEuclidean
C₁ : ℝ≥0 := ‖↑e.symm‖₊
C : ℝ≥0 := eLpNormLESNormFDerivOfEqInnerConst μ ↑p
C₂ : ℝ≥0 := ‖↑e‖₊
v : E → F' := ⇑e ∘ u
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
this : eLpNorm v (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ v) (↑p) μ
x : E
⊢ ‖↑e‖ * ‖fderiv ℝ u x‖ = ↑C₂ * ‖fderiv ℝ u x‖
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
G : Type u_4
H : Type u_5
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : InnerProductSpace 𝕜 G
inst✝⁶ : NormedAddCommGroup H
inst✝⁵ : InnerProductSpace 𝕜 H
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace G
inst✝² : CompleteSpace (E ⊗[𝕜] H)
inst✝¹ : CompleteSpace (E ⊗[𝕜] G)
inst✝ : CompleteSpace H
g : G →L[𝕜] H
⊢ ContinuousLinearMap.adjoint (ContinuousLinearMap.lTensor E g) =
    ContinuousLinearMap.lTensor E (ContinuousLinearMap.adjoint g)

Tactic:
simp [ContinuousLinearMap.lTensor_eq_mapL]

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

Goal state before:
pp: 𝕜 : 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
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 ↥f.range
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
⊢ Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)

Tactic:
rw [hrank]

Goal state after:
𝕜 : 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
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 ↥f.range
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
⊢ Nonempty (OrthonormalBasis (Fin (finrank 𝕜 ↥f.range)) 𝕜 ↥f.range)
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : X → ℝ≥0
t : X → Set X
htn : ∀ x ∈ s, t x ∈ 𝓝[s] x
hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)
u : Set X
hus : u ⊆ s
huc : u.Countable
huU : ⋃ i ∈ u, s ∩ t i = s
⊢ dimH (f '' s) ≤ dimH s / ↑r

Tactic:
← huU,

Goal state after:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
s : Set X
C : X → ℝ≥0
t : X → Set X
htn : ∀ x ∈ s, t x ∈ 𝓝[s] x
hC : ∀ x ∈ s, HolderOnWith (C x) r f (t x)
u : Set X
hus : u ⊆ s
huc : u.Countable
huU : ⋃ i ∈ u, s ∩ t i = s
⊢ dimH (f '' ⋃ i ∈ u, s ∩ t i) ≤ dimH (⋃ i ∈ u, s ∩ t i) / ↑r
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : 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
f : U →ₗ[𝕜] V
⊢ f.normDet = 0 ↔ finrank 𝕜 ↥f.range ≠ finrank 𝕜 U

Tactic:
by
  simp [normDet_eq_zero_iff_ker_ne_bot, ← f.finrank_range_add_finrank_ker]

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ dimH (Metric.ball x r) = ↑(Fintype.card ι)

Tactic:
rw [← ENNReal.coe_natCast]
    have : μH[Fintype.card ι] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι) := by
      rw [hausdorffMeasure_pi_real, Real.volume_pi_ball _ hr]
    refine dimH_of_hausdorffMeasure_ne_zero_ne_top ?_ ?_ <;> rw [NNReal.coe_natCast, this]
    · simp [pow_pos (mul_pos (zero_lt_two' ℝ) hr)]
    · exact ENNReal.ofReal_ne_top

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ dimH (Metric.ball x r) = ↑(Fintype.card ι)

Tactic:
· rw [← ENNReal.coe_natCast]
    have : μH[Fintype.card ι] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι) := by
      rw [hausdorffMeasure_pi_real, Real.volume_pi_ball _ hr]
    refine dimH_of_hausdorffMeasure_ne_zero_ne_top ?_ ?_ <;> rw [NNReal.coe_natCast, this]
    · simp [pow_pos (mul_pos (zero_lt_two' ℝ) hr)]
    · exact ENNReal.ofReal_ne_top

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

Goal state before:
pp: 𝕜 : 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
inst✝ : Subsingleton U
f : U →ₗ[𝕜] V
h : f.ker = ⊥
hrank : finrank 𝕜 U = 0
⊢ Fin (finrank 𝕜 U) ≃ Fin 0

Tactic:
rw [hrank]

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

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
⊢ ⇑(mkMetric m) = ⇑(Measure.mkMetric m)

Tactic:
by
  rw [← Measure.mkMetric_toOuterMeasure, Measure.coe_toOuterMeasure]

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: ⊢ ↑(finrank ℝ ℝ) = 1

Tactic:
Module.finrank_self,

Goal state after:
⊢ ↑1 = 1
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : 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
inst✝ : CompleteSpace V
f : U →L[𝕜] V
this✝ : CompleteSpace U
this : CompleteSpace ↥(↑f).range
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
h : ¬(↑f).ker = ⊥
⊢ (↑(ContinuousLinearMap.adjoint f ∘SL f)).ker ≠ ⊥

Tactic:
ContinuousLinearMap.ker_adjoint_comp_self

Goal state after:
𝕜 : 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
inst✝ : CompleteSpace V
f : U →L[𝕜] V
this✝ : CompleteSpace U
this : CompleteSpace ↥(↑f).range
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
h : ¬(↑f).ker = ⊥
⊢ (↑f).ker ≠ ⊥
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
⊢ μH[d₂] s = 0 ∨ μH[d₁] s = ∞

Tactic:
by
  by_contra! H
  suffices ∀ c : ℝ≥0, c ≠ 0 → μH[d₂] s ≤ c * μH[d₁] s by
    rcases ENNReal.exists_nnreal_pos_mul_lt H.2 H.1 with ⟨c, hc0, hc⟩
    exact hc.not_ge (this c (pos_iff_ne_zero.1 hc0))
  intro c hc
  refine le_iff'.1 (mkMetric_mono_smul ENNReal.coe_ne_top (mod_cast hc) ?_) s
  have : 0 < ((c : ℝ≥0∞) ^ (d₂ - d₁)⁻¹) := by
    rw [← ENNReal.coe_rpow_of_ne_zero hc, pos_iff_ne_zero, Ne, ENNReal.coe_eq_zero,
      NNReal.rpow_eq_zero_iff]
    exact mt And.left hc
  filter_upwards [Ico_mem_nhdsGE this]
  rintro r ⟨hr₀, hrc⟩
  lift r to ℝ≥0 using ne_top_of_lt hrc
  rw [Pi.smul_apply, smul_eq_mul,
    ← ENNReal.div_le_iff_le_mul (Or.inr ENNReal.coe_ne_top) (Or.inr <| mt ENNReal.coe_eq_zero.1 hc)]
  rcases eq_or_ne r 0 with (rfl | hr₀)
  · 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]
  · have : (r : ℝ≥0∞) ≠ 0 := by simpa only [ENNReal.coe_eq_zero, Ne] using hr₀
    rw [← ENNReal.rpow_sub _ _ this ENNReal.coe_ne_top]
    refine (ENNReal.rpow_lt_rpow hrc (sub_pos.2 h)).le.trans ?_
    rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (sub_pos.2 h).ne', ENNReal.rpow_one]

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 y : E
a b : 𝕜
⊢ inner_ 𝕜 ((a + b) • x) y = inner_ 𝕜 (a • x) y + inner_ 𝕜 (b • x) y

Tactic:
simpa [add_smul] using add_left (a • x) (b • x) y

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
C : ℝ
s : Set X
hC : ∀ x ∈ s, ‖kerFun H x‖ ≤ C
ι : Type u_5
l : Filter ι
F : ι → H
f : H
h : Tendsto F l (𝓝 f)
ε : ℝ
hε : ε > 0
hnorm : Tendsto (fun x ↦ ‖F x - f‖ * C) l (𝓝 0)
n : ι
hn : ‖F n - f‖ * C < ε
x : X
hx : x ∈ s
⊢ ‖(F n - f) x‖ < ε

Tactic:
grw [norm_apply_le, ← norm_kerFun_eq_sqrt_norm_kernel, hC x hx, hn]

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

Goal state before:
pp: case inr.inr
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
dpos : 0 < d
this : NullSingletonClass μH[d]
⊢ μH[d] {x} ≤ 1

Tactic:
simp only [zero_le, measure_singleton]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
this : ∀ {h p1 p2 p3 : Prop}, (h → [p1, p2, p3].TFAE) → [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
hHerm : K.IsHermitian
⊢ [∀ (x : X →₀ V →L[𝕜] V), 0 ≤ x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * K i j * xj,
      ∀ (f : X × V →₀ 𝕜),
        0 ≤ RCLike.re (f.sum fun xv z ↦ f.sum fun xv' w ↦ (starRingEnd 𝕜) z * w * ⟪(K xv'.1 xv.1) xv.2, xv'.2⟫_𝕜),
      ∀ (vv : X →₀ V), 0 ≤ RCLike.re (vv.sum fun x w ↦ vv.sum fun x' w' ↦ ⟪(K x' x) w, w'⟫_𝕜)].TFAE

Tactic:
simp only [nonneg_iff_isPositive, isPositive_def', isSelfAdjoint_finsuppSum hHerm,
    reApplyInnerSelf_apply, true_and]

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
this : ∀ {h p1 p2 p3 : Prop}, (h → [p1, p2, p3].TFAE) → [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
hHerm : K.IsHermitian
⊢ [∀ (x : X →₀ V →L[𝕜] V) (x_1 : V),
        0 ≤ RCLike.re ⟪(x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * K i j * xj) x_1, x_1⟫_𝕜,
      ∀ (f : X × V →₀ 𝕜),
        0 ≤ RCLike.re (f.sum fun xv z ↦ f.sum fun xv' w ↦ (starRingEnd 𝕜) z * w * ⟪(K xv'.1 xv.1) xv.2, xv'.2⟫_𝕜),
      ∀ (vv : X →₀ V), 0 ≤ RCLike.re (vv.sum fun x w ↦ vv.sum fun x' w' ↦ ⟪(K x' x) w, w'⟫_𝕜)].TFAE
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inl.inr.inr
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
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
d : ℝ
hd : 0 ≤ d
h : HolderOnWith 0 r f s
x : X
hx : x ∈ s
this✝ : f '' s = {f x}
h'd : 0 < d
this : NullSingletonClass μH[d]
⊢ μH[d] {f x} ≤ ↑0 ^ d * μH[↑r * d] s

Tactic:
simp only [zero_le, measure_singleton]

Goal state after: