mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case pos.inl
n m : ℕ
hm : NeZero m
h✝¹ : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h✝ : p ∣ ps.prod id * n
h : p ∣ ps.prod id
q : ℕ
hq : q ∈ ps
hq' : p ∣ id q
⊢ False

Tactic:
rw [Finset.mem_filter, Nat.mem_primeFactors,
        ← (Nat.prime_dvd_prime_iff_eq pp hq.1.1).mp hq'] at hq

Goal state after:
case pos.inl
n m : ℕ
hm : NeZero m
h✝¹ : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : p ∣ x
h✝ : p ∣ ps.prod id * n
h : p ∣ ps.prod id
q : ℕ
hq : (Nat.Prime p ∧ p ∣ m ∧ m ≠ 0) ∧ ¬p ∣ x
hq' : p ∣ id q
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ (map (algebraMap K L) (X ^ n - 1)).Splits

Tactic:
by
  rw [Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow,
    Polynomial.map_X]
  obtain ⟨z, hz⟩ := ((isCyclotomicExtension_iff _ _ _).1 H).1 hS (NeZero.ne _)
  exact X_pow_sub_one_splits hz

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

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
⊢ (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s

Tactic:
refine hζ.norm_pow_sub_one_of_prime_pow_ne_two hirr hs fun h => ?_
  rw [← pow_one 2] at h
  replace h :=
    eq_of_prime_pow_eq (prime_iff.1 hpri.out) (prime_iff.1 Nat.prime_two) (k - s).succ_pos h
  exact hodd h

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ Function.Injective ψ.mulShift

Tactic:
intro a

Goal state after:
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
a : R
⊢ ∀ ⦃a₂ : R⦄, ψ.mulShift a = ψ.mulShift a₂ → a = a₂
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
⊢ ψ.IsPrimitive

Tactic:
intro a

Goal state after:
C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
a : ZMod n
⊢ a ≠ 0 → ψ.mulShift a ≠ 1
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

Goal state after:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
a : ZMod n
⊢ (zmodChar n ⋯) a = 1 → a = 0
Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
S : Subgroup Mˣ := rootsOfUnity (Monoid.exponent G) M
this : Finite (G →* ↥S)
⊢ Finite (G →* Mˣ)

Tactic:
refine .of_surjective S.subtype.comp fun f ↦ ?_

Goal state after:
G : Type u_1
M : Type u_2
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
S : Subgroup Mˣ := rootsOfUnity (Monoid.exponent G) M
this : Finite (G →* ↥S)
f : G →* Mˣ
⊢ ∃ a, S.subtype.comp a = f
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x : CyclotomicField n K
hx : x ∈ adjoin A {b | b ^ n = 1}
a : A
⊢ ⟨(algebraMap A (CyclotomicField n K)) a, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
exact Subalgebra.algebraMap_mem _ a

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ ↑(toCircle ↑j) = cexp (2 * ↑π * I * ↑j / ↑N)

Tactic:
by
  rw [toCircle, AddChar.compAddMonoidHom_apply, toCircle_addChar, AddChar.coe_mk,
    AddCircle.toCircle, toAddCircle_intCast, Function.Periodic.lift_coe, Circle.coe_exp]
  push_cast
  ring_nf

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

Goal state after:
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
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'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
⊢ ∀ (a : R), χ a = χ' a

Tactic:
intro a

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
a : R
⊢ χ a = χ' a
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

Goal state after:
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
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:
| zero =>

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'
χ₁ χ₂ : MulChar R R'
a : Rˣ
⊢ (equivToUnitHom (χ₁ * χ₂)) a = (equivToUnitHom χ₁) a * (equivToUnitHom χ₂) a

Tactic:
by
  apply_fun ((↑) : R'ˣ → R') using Units.val_injective
  push_cast
  simp_rw [coe_equivToUnitHom, coeToFun_mul, Pi.mul_apply]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ : MulChar R R'
f : R' →+* R''
⊢ χ.ringHomComp f ^ 0 = (χ ^ 0).ringHomComp f

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ : MulChar R R'
hχ : χ.IsQuadratic
f : R' →+* R''
⊢ (χ.ringHomComp f).IsQuadratic

Tactic:
intro a

Goal state after:
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ : MulChar R R'
hχ : χ.IsQuadratic
f : R' →+* R''
a : R
⊢ (χ.ringHomComp f) a = 0 ∨ (χ.ringHomComp f) a = 1 ∨ (χ.ringHomComp f) a = -1
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
inst✝¹ : Nontrivial R
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
χ : DirichletCharacter R n
a : ℤ
ha : ¬IsCoprime a ↑χ.conductor
⊢ ((changeLevel hm) χ).primitiveCharacter ↑a = χ.primitiveCharacter ↑a

Tactic:
· rw [(apply_eq_zero_iff ..).mpr ha, (apply_eq_zero_iff ..).mpr (by rwa [conductor_changeLevel])]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case zero
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ ψ ^ p ^ 0 = χ (↑p ^ 0) * gaussSum χ ψ

Tactic:
| zero =>

Goal state after:
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
⊢ ¬ringChar FF ∣ 8

Tactic:
change ¬_ ∣ 2 ^ 3

Goal state after:
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
⊢ ¬ringChar FF ∣ 2 ^ 3
Module: Mathlib.Analysis.InnerProductSpace.Affine

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p : P
t : ℝ
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
h : dist p ((AffineMap.lineMap a b) t) ^ 2 = dist a p ^ 2 + t ^ 2 * dist a b ^ 2
⊢ dist p ((AffineMap.lineMap a b) t) ^ 2 = dist p a ^ 2 + t ^ 2 * dist a b ^ 2

Tactic:
dist_comm a p

Goal state after:
V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p : P
t : ℝ
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
h : dist p ((AffineMap.lineMap a b) t) ^ 2 = dist p a ^ 2 + t ^ 2 * dist a b ^ 2
⊢ dist p ((AffineMap.lineMap a b) t) ^ 2 = dist p a ^ 2 + t ^ 2 * dist a b ^ 2
Module: Mathlib.Dynamics.BirkhoffSum.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
f : α → α
φ : α → M
h : φ ∘ f = φ
n : ℕ
x : α
this : ∀ (k : ℕ), φ (f^[k] x) = φ x
⊢ birkhoffSum f φ n x = (n • φ) x

Tactic:
by simp [birkhoffSum, this]

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 < ↑γ
⊢ γ * n' = p'

Tactic:
← NNReal.coe_inj,

Goal state after:
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 < ↑γ
⊢ ↑(γ * n') = ↑p'
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: 𝕜 : 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
y : F
h : ∃ w, ∀ (x : ↥T.domain), ⟪w, ↑x⟫ = ⟪y, ↑T x⟫
⊢ y ∈ T†.domain

Tactic:
by
  obtain ⟨w, hw⟩ := h
  rw [T.mem_adjoint_domain_iff]
  have : Continuous ((innerSL 𝕜 w).comp T.domain.subtypeL) := by fun_prop
  convert this
  exact funext fun x => (hw x).symm

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

Goal state before:
pp: 𝕜 : 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
y : ↥T†.domain
⊢ ↑T† y = 0

Tactic:
classical
  change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _
  simp only [hT, not_false_iff, dif_neg, LinearMap.zero_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
⊢ IsLowerSet ↑T.singularValues.support

Tactic:
intro a

Goal state after:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
a : ℕ
⊢ ∀ ⦃b : ℕ⦄, b ≤ a → a ∈ ↑T.singularValues.support → b ∈ ↑T.singularValues.support
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
g : G →L[𝕜] H
x : E ⊗[𝕜] G
⊢ (mapL f g) x = (map ↑f ↑g) x

Tactic:
simp [mapL, ← LinearMap.rTensor_comp_lTensor]

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

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

Tactic:
simp only [dimH_def, lt_iSup_iff] at h

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : ∃ i, ∃ (_ : μH[↑i] s = ∞), ↑d < ↑i
⊢ μH[↑d] s = ∞
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

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

Tactic:
by
  simp only [dimH_def, lt_iSup_iff] at h
  rcases h with ⟨d', hsd', hdd'⟩
  rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hdd'
  exact top_unique (hsd' ▸ hausdorffMeasure_mono hdd'.le _)

Goal state after:
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
s : Set Y
⊢ volume.addHaarScalarFactor μH[↑d] • μH[↑d] (f ⁻¹' s) = volume.addHaarScalarFactor μH[↑d] • μH[↑d] (s ∩ Set.range f)

Tactic:
Isometry.hausdorffMeasure_preimage hf (by simp)

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
s : Set Y
⊢ volume.addHaarScalarFactor μH[↑d] • μH[↑d] (s ∩ Set.range f) =
    volume.addHaarScalarFactor μH[↑d] • μH[↑d] (s ∩ Set.range f)
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
s : AffineSubspace ℝ P
hs : Nonempty ↥s
t : Set P
ht : MeasurableSet t
p : ↥s
x✝ : ↥s.direction
u : Set ↥(mk' (↑(x✝ +ᵥ p)) s.directionᗮ) := Subtype.val ⁻¹' (t ∩ ↑(mk' (↑(x✝ +ᵥ p)) s.directionᗮ))
hu : MeasurableSet u
x : P
⊢ x ∈ t ∩ ↑(mk' (↑(x✝ +ᵥ p)) s.directionᗮ) ↔ x ∈ Subtype.val '' u

Tactic:
simp [u]

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

Goal state before:
pp: case mpr.zero
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ (H →L[𝕜] H) IsSelfAdjoint
f p : H →L[𝕜] H
⊢ IsPositive 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
𝕜 : 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
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
f : OfKernel K
h : (ContinuousLinearMap.pi fun x ↦ adjoint (kerFun K x)) f = 0
⊢ ⟪↑0, f⟫_𝕜 = 0

Tactic:
| zero =>

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

Goal state before:
pp: case inr
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
iso_smul : Isometry ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v))
⊢ ‖v‖₊ ^ 1 • μH[1] (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s) = ‖v‖₊ • μH[1] s

Tactic:
NNReal.rpow_one,

Goal state after:
case inr
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
iso_smul : Isometry ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v))
⊢ ‖v‖₊ • μH[1] (⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s) = ‖v‖₊ • μH[1] s
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.areaForm x) y ≤ ‖x‖ * ‖y‖

Tactic:
simpa [areaForm_to_volumeForm, Fin.prod_univ_succ] using o.volumeForm_apply_le ![x, y]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : StrongDual 𝕜 E
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
f' : StrongDual 𝕜 (WeakSpace 𝕜 E) :=
  let __LinearMap := ↑f ∘ₗ ↑(toWeakSpace 𝕜 E).symm;
  { toLinearMap := __LinearMap, cont := ⋯ }
hux' : u < (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f') ((toWeakSpace 𝕜 E) x)
y : E
hy : y ∈ s
⊢ (toWeakSpace 𝕜 E) y ∈ {y | (RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f') y ≤ u}

Tactic:
simpa [f'] using (hus y <| subset_closure hy).le

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℂ 𝕜 E
c : 𝕜
⊢ mellin (fun t ↦ c • f t) s = c • mellin f s

Tactic:
simp only [mellin, smul_comm, integral_smul]

Goal state after:
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ mellinInv σ (fun s ↦ 𝓕 g (s.im / (2 * π))) x = ↑x ^ (-↑σ) • g (-Real.log x)

Tactic:
by
      rw [mellinInv_eq_fourierInv _ _ hx, ← hf.fourierInv_fourier_eq hFf hfx]
      simp [mul_div_cancel_left₀ _ (show 2 * π ≠ 0 by simp)]

Goal state after:
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ ((x ^ σ)⁻¹ * x ^ σ) • f x = f x

Tactic:
inv_mul_cancel₀ (ne_of_gt (rpow_pos_of_pos hx σ)),

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ 1 • f x = f x
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case zero
⊢ logTaylor 0 0 = 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
z : ℂ
⊢ HasDerivAt (logTaylor (0 + 1)) (∑ j ∈ Finset.range 0, (-1) ^ j * z ^ j) z

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case zero
s✝ : ℂ
hs✝ : ∀ (m : ℕ), s✝ ≠ -↑m
s : ℂ
hsre : -↑0 < s.re
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ DifferentiableAt ℂ Gamma s

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
ht' : 0 < t
⊢ ‖t ^ (s - 1)‖ * ‖f t‖ ≤ t ^ (s - 1 + -a) * d

Tactic:
rpow_add ht',

Goal state after:
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
ht' : 0 < t
⊢ ‖t ^ (s - 1)‖ * ‖f t‖ ≤ t ^ (s - 1) * t ^ (-a) * d
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ 1 / (1 - ‖z‖) ≤ 2

Tactic:
div_le_iff₀

Goal state after:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ 1 ≤ 2 * (1 - ‖z‖)

z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ 0 < 1 - ‖z‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case zero
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z) - logTaylor 0 z‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖z‖ ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: f : ℕ → ℂ
t : ℂ
hf : (fun n ↦ f n - (1 + t / ↑n)) =o[atTop] fun n ↦ 1 / ↑n
⊢ Tendsto (fun n ↦ f n ^ n) atTop (𝓝 (cexp t))

Tactic:
rw [show (fun n ↦ f n ^ n) = (fun n ↦ (1 + (f n - 1)) ^ n) by ext; simp]

Goal state after:
f : ℕ → ℂ
t : ℂ
hf : (fun n ↦ f n - (1 + t / ↑n)) =o[atTop] fun n ↦ 1 / ↑n
⊢ Tendsto (fun n ↦ (1 + (f n - 1)) ^ n) atTop (𝓝 (cexp t))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case zero
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
⊢ f (x + ↑0) = f x + ∑ m ∈ Finset.range 0, log (x + ↑m)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case inr.zero
z : ℂ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) =
    ((↑π * z * ∏ j ∈ Finset.range 0, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * 0)) /
      ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * 0))

Tactic:
| zero =>

Goal state after: