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

Goal state before:
pp: case h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := ⋯
ζ' : Rˣ := ⋯
h' : ζ' ^ Fintype.card Fˣ = 1
⊢ orderOf (e.symm ⟨ζ', ⋯⟩) = n

Tactic:
rw [e.symm.orderOf_eq, orderOf_eq_iff hn₀]

Goal state after:
case h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card Fˣ = 1
⊢ ⟨ζ', ⋯⟩ ^ n = 1 ∧ ∀ m < n, 0 < m → ⟨ζ', ⋯⟩ ^ m ≠ 1
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: case h.refine_1
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := ⋯
ζ' : Rˣ := ⋯
h' : ζ' ^ Fintype.card Fˣ = 1
⊢ ↑↑(⟨ζ', ⋯⟩ ^ n) = ↑↑1

Tactic:
push_cast

Goal state after:
case h.refine_1
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card Fˣ = 1
⊢ ↑ζ' ^ n = 1
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
a : Rˣ
⊢ ↑((equivToUnitHom (χ₁ * χ₂)) a) = ↑((equivToUnitHom χ₁) a * (equivToUnitHom χ₂) a)

Tactic:
push_cast

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
a : Rˣ
⊢ ↑((equivToUnitHom (χ₁ * χ₂)) a) = ↑((equivToUnitHom χ₁) a) * ↑((equivToUnitHom χ₂) a)
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ n = 0 → χ.conductor = 0

Tactic:
rintro rfl

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R 0
⊢ χ.conductor = 0
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ.primitiveCharacter.IsPrimitive

Tactic:
by_cases h : χ.conductor = 0
  · rw [isPrimitive_def]
    convert! conductor_eq_zero_iff_level_eq_zero.mpr h
  · exact le_antisymm (Nat.le_of_dvd (Nat.pos_of_ne_zero h) (conductor_dvd_level _)) <|
      conductor_le_conductor_mem_conductorSet <| conductor_mem_conductorSet χ

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

Goal state before:
pp: A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝ : NeZero n₂
h : n₁ ∣ n₂
⊢ n₁ ≠ 0

Tactic:
rintro rfl

Goal state after:
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝ : NeZero n₂
h₁ : IsCyclotomicExtension {0} A ↥C₁
h : 0 ∣ n₂
⊢ False
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
H : Set (ZMod n)ˣ
χ : DirichletCharacter R n
⊢ (∀ (x : (↥(Submonoid.map (Units.coeHom (ZMod n)) (Submonoid.closure H)))ˣ), χ ↑↑x = 1) ↔
    ∀ x ∈ Submonoid.closure H, χ ↑x = 1

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

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
H : Set (ZMod n)ˣ
χ : DirichletCharacter R n
hχ : ∀ (x : (↥(Submonoid.map (Units.coeHom (ZMod n)) (Submonoid.closure H)))ˣ), χ ↑↑x = 1
x : (ZMod n)ˣ
hx : x ∈ Submonoid.closure H
⊢ χ ↑x = 1

case refine_2
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
H : Set (ZMod n)ˣ
χ : DirichletCharacter R n
h : ∀ x ∈ Submonoid.closure H, χ ↑x = 1
u : (↥(Submonoid.map (Units.coeHom (ZMod n)) (Submonoid.closure H)))ˣ
⊢ χ ↑↑u = 1
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ (fun x ↦ ‖x‖ * 1) =O[𝓝 0] fun x ↦ x - 0

Tactic:
by
        simp_rw [mul_one, isBigO_norm_left (f' := fun x ↦ x), sub_zero, isBigO_refl]

Goal state after:
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ IsAtom s ↔ ∃ a, s = {a}

Tactic:
simp [← bot_covBy_iff, covBy_iff, eq_comm]

Goal state after:
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
a : α
ha : s \ t = {a}
⊢ insert a t = s

Tactic:
insert_eq,

Goal state after:
case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
a : α
ha : s \ t = {a}
⊢ {a} ∪ t = s
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : 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
⊢ ↑(#s + 1) - 1 = ↑(#s)

Tactic:
push_cast

Goal state after:
ι : 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
⊢ ↑(#s) + 1 - 1 = ↑(#s)
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x y : 𝕜
⊢ (adjoint counit) (x * y) = (adjoint ((LinearMap.lTensor 𝕜 counit ∘ₗ LinearMap.rTensor E counit) ∘ₗ comul)) (x ⊗ₜ[𝕜] y)

Tactic:
comp_assoc,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x y : 𝕜
⊢ (adjoint counit) (x * y) = (adjoint (LinearMap.lTensor 𝕜 counit ∘ₗ LinearMap.rTensor E counit ∘ₗ comul)) (x ⊗ₜ[𝕜] y)
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : 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
⊢ i ∈ sᶜ

Tactic:
by rwa [Finset.mem_compl]

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
I : Type u_2
inst✝¹ : Fintype I
inst✝ : LinearOrder I
b : OrthonormalBasis I ℝ E
n : ℕ
i j : ↑(Set.powersetCard I n)
⊢ inner ℝ (exteriorPower.ιMulti_family ℝ n (⇑b) i) (exteriorPower.ιMulti_family ℝ n (⇑b) j) = if i = j then 1 else 0

Tactic:
exact exteriorPower.innerProductForm_ιMulti_family_of_orthonormal b.orthonormal i j

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ True ∧ ∀ (x_1 : E), 0 ≤ ↑‖⟪x, x_1⟫‖ ^ 2

Tactic:
← RCLike.ofReal_pow,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ True ∧ ∀ (x_1 : E), 0 ≤ ↑(‖⟪x, x_1⟫‖ ^ 2)
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
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
hcf : f.closure.toFun.ker = ⊥
⊢ f.inverse.closure = f.closure.inverse

Tactic:
apply eq_of_eq_graph
  rw [closure_inverse_graph hf hf' hcf,
    ((inverse_isClosable_iff hf hf').mpr hcf).graph_closure_eq_closure_graph]

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

Goal state before:
pp: case mp
𝕜 : 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
⊢ (∃ (x_1 : x.1 ∈ T†.domain), ↑T† ⟨x.1, ⋯⟩ = x.2) → ∀ (a : E) (a_1 : a ∈ T.domain), ⟪↑T ⟨a, ⋯⟩, x.1⟫ - ⟪a, x.2⟫ = 0

pp: case mpr
𝕜 : 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
⊢ (∀ (a : E) (a_1 : a ∈ T.domain), ⟪↑T ⟨a, ⋯⟩, x.1⟫ - ⟪a, x.2⟫ = 0) → ∃ (x_1 : x.1 ∈ T†.domain), ↑T† ⟨x.1, ⋯⟩ = x.2

Tactic:
· rintro ⟨hx, h⟩ a ha
    rw [← h, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩, sub_self]

Goal state after:
case mpr
𝕜 : 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
⊢ (∀ (a : E) (a_1 : a ∈ T.domain), ⟪↑T ⟨a, ⋯⟩, x.1⟫ - ⟪a, x.2⟫ = 0) → ∃ (x_1 : x.1 ∈ T†.domain), ↑T† ⟨x.1, ⋯⟩ = x.2
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) μ
h4v : ∀ (x : E), ‖fderiv ℝ v x‖ ≤ ↑C₂ * ‖fderiv ℝ u x‖
⊢ ↑‖↑toEuclidean.symm‖₊ * ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) *
      (↑‖↑toEuclidean‖₊ * eLpNorm (fderiv ℝ u) (↑p) μ) =
    ↑(‖↑toEuclidean.symm‖₊ * eLpNormLESNormFDerivOfEqInnerConst μ ↑p * ‖↑toEuclidean‖₊) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
push_cast

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) μ
h4v : ∀ (x : E), ‖fderiv ℝ v x‖ ≤ ↑C₂ * ‖fderiv ℝ u x‖
⊢ ↑‖↑toEuclidean.symm‖₊ * ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) *
      (↑‖↑toEuclidean‖₊ * eLpNorm (fderiv ℝ u) (↑p) μ) =
    ↑‖↑toEuclidean.symm‖₊ * ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * ↑‖↑toEuclidean‖₊ * eLpNorm (fderiv ℝ u) (↑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 : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Tactic:
have iUnion_S : ⋃ n, S n = s \ t := by
    refine Subset.antisymm (iUnion_subset S_sub) ?_
    rintro x ⟨hxs, hxt⟩
    rw [mem_iff_infEDist_zero_of_closed ht] at hxt
    rcases ENNReal.exists_inv_nat_lt hxt with ⟨n, hn⟩
    exact mem_iUnion.2 ⟨n, hxs, hn.le⟩

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}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s
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
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < ↑(finrank ℝ E)
hpq : ↑p⁻¹ - (↑(finrank ℝ E))⁻¹ ≤ (↑q)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E))⁻¹)⁻¹
hp' : ↑p'⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
this : ↑q ≤ ↑p'
t : ℝ≥0 := (μ s).toNNReal ^ (1 / ↑q - 1 / ↑p')
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ ↑p
⊢ ↑C * eLpNorm (fderiv ℝ u) (↑p) μ * ↑t = ↑(eLpNormLESNormFDerivOfLeConst F μ s p q) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
simp_rw [eLpNormLESNormFDerivOfLeConst, ENNReal.coe_mul]

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
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < ↑(finrank ℝ E)
hpq : ↑p⁻¹ - (↑(finrank ℝ E))⁻¹ ≤ (↑q)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E))⁻¹)⁻¹
hp' : ↑p'⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
this : ↑q ≤ ↑p'
t : ℝ≥0 := (μ s).toNNReal ^ (1 / ↑q - 1 / ↑p')
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ ↑p
⊢ ↑C * eLpNorm (fderiv ℝ u) (↑p) μ * ↑t =
    ↑((μ s).toNNReal ^ (1 / ↑q - 1 / ↑(p⁻¹ - (↑(finrank ℝ E))⁻¹)⁻¹)) * ↑(SNormLESNormFDerivOfEqConst F μ ↑p) *
      eLpNorm (fderiv ℝ u) (↑p) μ
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : EMetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : EMetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℕ
hf : Isometry f
⊢ map f (volume.addHaarScalarFactor μH[↑d] • μH[↑d]) =
    (volume.addHaarScalarFactor μH[↑d] • μH[↑d]).restrict (Set.range f)

Tactic:
Measure.map_smul,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁵ : EMetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : EMetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℕ
hf : Isometry f
⊢ volume.addHaarScalarFactor μH[↑d] • map f μH[↑d] = (volume.addHaarScalarFactor μH[↑d] • μH[↑d]).restrict (Set.range f)
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (fun n ↦ (pre m (↑n)⁻¹) s) atTop (𝓝 ((mkMetric' m) s))

Tactic:
refine (tendsto_pre m s).comp (tendsto_inf.2 ⟨ENNReal.tendsto_inv_nat_nhds_zero, ?_⟩)

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ Tendsto (fun n ↦ (↑n)⁻¹) atTop (𝓟 (Ioi 0))
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
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : f.range = ⊤
bv' : OrthonormalBasis ι 𝕜 ↥f.range := bv.map (LinearIsometryEquiv.ofTop V f.range h).symm
⊢ f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f).det‖

Tactic:
f.normDet_eq_norm_det_toMatrix_rangeRestrict bu bv'

Goal state after:
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
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : f.range = ⊤
bv' : OrthonormalBasis ι 𝕜 ↥f.range := bv.map (LinearIsometryEquiv.ofTop V f.range h).symm
⊢ ‖((toMatrix bu.toBasis bv'.toBasis) f.rangeRestrict).det‖ = ‖((toMatrix bu.toBasis bv.toBasis) f).det‖
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
f : U →ₗ[𝕜] V
c : 𝕜
hc : c = 0
⊢ (c • f).normDet = ‖c‖ ^ finrank 𝕜 U * f.normDet

Tactic:
nontriviality U
    simp [hc, zero_pow finrank_pos.ne.symm]

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

Goal state before:
pp: E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
⊢ ⇑e '' s ∈ Filter.map (⇑e) (𝓝 x)

Tactic:
exact image_mem_map h

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

Goal state before:
pp: case refine_1
X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun n ↦ ∑' (i : ι n), m (ediam (t n i))) l < c
n : β
hn : ∑' (i : ι n), m (ediam (t n i)) < c
hrn : r n < ε
htn : ∀ (i : ι n), ediam (t n i) ≤ r n
hstn : s ⊆ ⋃ i, t n i
u : ℕ → Set X := fun j ↦ ⋃ b ∈ decode₂ (ι n) j, t n b
j : ℕ
⊢ ediam (u j) ≤ ε

Tactic:
rw [ediam_iUnion_mem_option]
    exact iSup₂_le fun _ _ => (htn _).trans hrn.le

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✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
⊢ LinearMap.det (adjoint f ∘ₗ f) = ↑(∏ x, ⋯.eigenvalues ⋯ x)

Tactic:
push_cast

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✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
⊢ LinearMap.det (adjoint f ∘ₗ f) = ∏ i, ↑(⋯.eigenvalues ⋯ i)
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
⊢ μH[d] (r • s) = ‖r‖₊ ^ d • μH[d] s

Tactic:
have {r : 𝕜} (s : Set E) : μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s := by
    simpa [ENNReal.coe_rpow_of_nonneg, hd]
      using (lipschitzWith_smul r).hausdorffMeasure_image_le hd s
  refine le_antisymm (this s) ?_
  rw [← le_inv_smul_iff_of_pos]
  · dsimp
    rw [← NNReal.inv_rpow, ← nnnorm_inv]
    · refine Eq.trans_le ?_ (this (r • s))
      rw [inv_smul_smul₀ hr]
  · simp [pos_iff_ne_zero, hr]

Goal state after:
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ (↑(rexp (-x)) * cexp (-↑x) ^ (s - 1)) • f = cexp (-s * ↑x) • f

Tactic:
push_cast

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ (cexp (-↑x) * cexp (-↑x) ^ (s - 1)) • f = cexp (-s * ↑x) • f
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ cexp (-(↑s.im * I) * ↑u) • rexp (-s.re * u) • f (rexp (-u)) =
    cexp (↑(-s.im * u) * I) • rexp (-s.re * u) • f (rexp (-u))

Tactic:
push_cast

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ cexp (-(↑s.im * I) * ↑u) • rexp (-s.re * u) • f (rexp (-u)) =
    cexp (-↑s.im * ↑u * I) • rexp (-s.re * u) • f (rexp (-u))
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : ↑x ≠ 0
x✝ : ℝ
⊢ cexp (↑(Real.log x) * -(↑(2 * π * x✝) * I)) • f (↑σ + ↑(2 * π * x✝) * I) =
    cexp (2 * ↑π * (↑x✝ * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑x✝ * I)

Tactic:
push_cast

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : ↑x ≠ 0
x✝ : ℝ
⊢ cexp (↑(Real.log x) * -(2 * ↑π * ↑x✝ * I)) • f (↑σ + 2 * ↑π * ↑x✝ * I) =
    cexp (2 * ↑π * (↑x✝ * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑x✝ * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : 1 + z ∈ slitPlane
⊢ log (1 + z) = z * ∫ (t : ℝ) in 0..1, (1 + t • z)⁻¹

Tactic:
convert!
    (integral_unitInterval_deriv_eq_sub (continuousOn_one_add_mul_inv hz)
        (fun _ ht ↦
          hasDerivAt_log <|
            StarConvex.add_smul_mem starConvex_one_slitPlane hz ht.1 ht.2)).symm using 1
  simp only [log_one, sub_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hz4 : ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2 * 2 / 2
⊢ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖

Tactic:
simp only [isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
    IsUnit.div_mul_cancel] at hz4

Goal state after:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
hz4 : ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2
⊢ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ ≤ 3 / 2 * ‖z‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun x ↦ ↑x * g x) atTop (𝓝 t)
⊢ Tendsto (fun x ↦ dist (↑x * g x) (↑x * log (1 + g x))) atTop (𝓝 0)

Tactic:
refine IsBigO.trans_tendsto ?_ tendsto_inv_atTop_zero.ofReal

Goal state after:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun x ↦ ↑x * g x) atTop (𝓝 t)
⊢ (fun x ↦ dist (↑x * g x) (↑x * log (1 + g x))) =O[atTop] fun x ↦ ↑x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e'_4.e_a.e_a
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ 1 - ↑(-x) = ↑(x + 1)

Tactic:
push_cast

Goal state after:
case e'_4.e_a.e_a
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ 1 - -↑x = ↑x + 1