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

Goal state before:
pp: n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : eval ((Nat.castRingHom (ZMod p)) a) (cyclotomic n (ZMod p)) = 0
⊢ 0 * eval ((Nat.castRingHom (ZMod p)) a) (∏ x ∈ n.properDivisors, cyclotomic x (ZMod p)) = 0

Tactic:
zero_mul

Goal state after:
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : eval ((Nat.castRingHom (ZMod p)) a) (cyclotomic n (ZMod p)) = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ (expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ

Tactic:
refine eq_of_monic_of_dvd_of_natDegree_le ((cyclotomic.monic _ ℤ).mul (cyclotomic.monic _ ℤ))
    ((cyclotomic.monic n ℤ).expand hp.pos) ?_ ?_

Goal state after:
case inr.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ cyclotomic (n * p) ℤ * cyclotomic n ℤ ∣ (expand ℤ p) (cyclotomic n ℤ)

case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ ((expand ℤ p) (cyclotomic n ℤ)).natDegree ≤ (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : 0 < ∑ i ∈ range n, x ^ i
⊢ 0 < eval x (cyclotomic n R) * ?h.inl.b

Tactic:
rwa [this]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
this : cyclotomic 6 ℤ = X ^ 2 - X + 1
⊢ cyclotomic 6 R = X ^ 2 - X + 1

Tactic:
rw [← map_cyclotomic_int, this]

Goal state after:
R : Type u_1
inst✝ : Ring R
this : cyclotomic 6 ℤ = X ^ 2 - X + 1
⊢ map (Int.castRingHom R) (X ^ 2 - X + 1) = X ^ 2 - X + 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : ∑ i ∈ range n, x ^ i < 0
⊢ eval x (cyclotomic n R) * ?h.inr.inr.b < 0

Tactic:
rwa [this]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)

Tactic:
have hq := zero_lt_one.trans hq'

Goal state after:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case pos
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : n = 0
⊢ IsCyclotomicExtension (S \ {0}) A B

Tactic:
← eq_self_sdiff_zero

Goal state after:
case pos
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : n = 0
⊢ IsCyclotomicExtension S A B
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n

Tactic:
have hq := zero_lt_one.trans hq'

Goal state after:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : Units.mk0 ‖eval (↑q) (cyclotomic n ℂ)‖₊ ⋯ < Units.mk0 (q + 1).toNNReal ⋯ ^ φ n
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n

Tactic:
simp only [← Units.val_lt_val, Units.val_pow_eq_pow_val, Units.val_mk0, ← NNReal.coe_lt_coe,
      coe_nnnorm, NNReal.coe_pow,
      Real.coe_toNNReal'] at this
    convert! this using 2
    · rw [eq_comm]
      simp [cyclotomic_nonneg n hq'.le]
    rw [eq_comm, max_eq_left_iff]
    linarith

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

Goal state before:
pp: case pos
S✝ : Set ℕ
n : ℕ
S : Set ℕ
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (S \ {0}) A B
hn : n = 0
this : insert n S \ {0} = S \ {0}
⊢ Module.Finite A B

Tactic:
← eq_self_sdiff_zero

Goal state after:
case pos
S✝ : Set ℕ
n : ℕ
S : Set ℕ
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension S A B
hn : n = 0
this : insert n S \ {0} = S \ {0}
⊢ Module.Finite A B
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
ζ : B
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
i : ℕ
left✝ : i < n
hx : n ≠ 0 ∧ (ζ ^ i) ^ n = 1
⊢ ζ ^ i ∈ ↑(adjoin A ((cyclotomic n A).rootSet B))

Tactic:
refine SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin ?_) _)

Goal state after:
case refine_2
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
ζ : B
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
i : ℕ
left✝ : i < n
hx : n ≠ 0 ∧ (ζ ^ i) ^ n = 1
⊢ ζ ∈ (cyclotomic n A).rootSet B
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case inl
n : ℕ
hn' : 1 < n
hq : 0 ≠ 1
⊢ (0 - 1) ^ φ n < (eval (↑0) (cyclotomic n ℤ)).natAbs

pp: case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ (q - 1) ^ φ n < (eval (↑q) (cyclotomic n ℤ)).natAbs

Tactic:
· rw [zero_tsub, zero_pow (Nat.totient_pos.2 (pos_of_gt hn')).ne', pos_iff_ne_zero,
      Int.natAbs_ne_zero, Nat.cast_zero, ← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hn']
    exact one_ne_zero

Goal state after:
case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ (q - 1) ^ φ n < (eval (↑q) (cyclotomic n ℤ)).natAbs
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
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
n✝ : ℕ
hi : n✝ ∈ {n}
hi' : n✝ ≠ 0
⊢ ∃ r, IsPrimitiveRoot r n✝

Tactic:
Set.mem_singleton_iff

Goal state after:
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
n✝ : ℕ
hi : n✝ = n
hi' : n✝ ≠ 0
⊢ ∃ r, IsPrimitiveRoot r n✝
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝ : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
b : B
hb : b ∈ {ζ}
⊢ ⟨b, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
Set.mem_singleton_iff

Goal state after:
case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
x✝ : ↥A[ζ]
x : B
hx : x ∈ A[ζ]
b : B
hb✝ : b ∈ {ζ}
hb : b = ζ
⊢ ⟨b, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n p : ℕ
h : p ∈ n.primeFactors
⊢ ¬IsUnit ↑p

Tactic:
rw [isUnit_iff_coprime]

Goal state after:
n p : ℕ
h : p ∈ n.primeFactors
⊢ ¬p.Coprime n
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = 1
⊢ 1 ^ p = 1

pp: case inr.inr
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = -1
⊢ (-1) ^ p = -1

Tactic:
· rw [one_pow]

Goal state after:
case inr.inr
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : χ ↑x = -1
⊢ (-1) ^ p = -1
Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum

Goal state before:
pp: case neg
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : ¬IsUnit a
⊢ gaussSum χ (e.mulShift a) = 0 * gaussSum χ e

Tactic:
zero_mul

Goal state after:
case neg
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : ¬IsUnit a
⊢ gaussSum χ (e.mulShift a) = 0
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℂ E'
T : E' →ₗ[ℂ] E'
⊢ ((∀ (v : E'), ↑(re ⟪T v, v⟫_ℂ) = ⟪T v, v⟫_ℂ) ∧ ∀ (x : E'), 0 ≤ re ⟪T x, x⟫_ℂ) ↔
    (∀ (x : E'), ↑(re ⟪T x, x⟫_ℂ) = ⟪T x, x⟫_ℂ) ∧ ∀ (x : E'), 0 ≤ re ⟪T x, x⟫_ℂ

Tactic:
re_to_complex,

Goal state after:
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℂ E'
T : E' →ₗ[ℂ] E'
⊢ ((∀ (v : E'), ↑(⟪T v, v⟫_ℂ).re = ⟪T v, v⟫_ℂ) ∧ ∀ (x : E'), 0 ≤ (⟪T x, x⟫_ℂ).re) ↔
    (∀ (x : E'), ↑(⟪T x, x⟫_ℂ).re = ⟪T x, x⟫_ℂ) ∧ ∀ (x : E'), 0 ≤ (⟪T x, x⟫_ℂ).re
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
⊢ Antitone fun s ↦ T μ p (∫⋯∫⁻_sᶜ, f ∂μ) s

Tactic:
by
  -- Reformulate (by induction): a function is decreasing on `Finset ι` if it decreases under the
  -- insertion of any element to any set.
  rw [Finset.antitone_iff_forall_insert_le]
  intro s i hi
  -- apply the lemma designed to encapsulate the inductive step
  convert! T_insert_le_T_lmarginal_singleton μ hp₀ s ?_ i hi (hf.lmarginal μ) using 2
  · rw [← lmarginal_union μ f hf]
    · rw [← insert_compl_insert hi]
      rfl
    rw [Finset.disjoint_singleton_left, notMem_compl]
    exact mem_insert_self i s
  · -- the main nontrivial point is to check that an exponent `p` satisfying `0 ≤ p` and
    -- `(#ι - 1) * p ≤ 1` is in the valid range for the inductive-step lemma
    refine le_trans ?_ hp
    gcongr
    suffices (s.card : ℝ) + 1 ≤ #ι by linarith
    rw [← card_add_card_compl s]
    norm_cast
    gcongr
    have hi' : sᶜ.Nonempty := ⟨i, by rwa [Finset.mem_compl]⟩
    rwa [← card_pos] at hi'

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
inst✝ : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
tfae_2_iff_3 : IsStarNormal p ↔ IsSelfAdjoint p
tfae_3_iff_4 : IsSelfAdjoint p ↔ p.IsPositive
⊢ [(↑p).rangeᗮ = (↑p).ker, IsStarNormal p, IsSelfAdjoint p, p.IsPositive].TFAE

Tactic:
tfae_have 3 ↔ 1 := p.isSelfAdjoint_iff_isSymmetric.eq ▸
    (LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range hp.toLinearMap)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
tfae_2_iff_3 : IsStarNormal p ↔ IsSelfAdjoint p
tfae_3_iff_4 : IsSelfAdjoint p ↔ p.IsPositive
tfae_3_iff_1 : IsSelfAdjoint p ↔ (↑p).rangeᗮ = (↑p).ker
⊢ [(↑p).rangeᗮ = (↑p).ker, IsStarNormal p, IsSelfAdjoint p, p.IsPositive].TFAE
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E ≃ₗ[𝕜] E
hT : (↑T).IsPositive
x : E
⊢ ?m.59

Tactic:
simpa using hT.2 (T.symm.toLinearMap x)

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
inst✝ : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : Fin (Module.finrank 𝕜 E) → E := fun i ↦ ↑√(⋯.eigenvalues ⋯ i) • (⋯.eigenvectorBasis ⋯) i
x✝ : E
⊢ T x✝ =
    ∑ x, (↑√(⋯.eigenvalues ⋯ x) * (⟪(⋯.eigenvectorBasis ⋯) x, x✝⟫ * ↑√(⋯.eigenvalues ⋯ x))) • (⋯.eigenvectorBasis ⋯) x

Tactic:
mul_comm (⟪_, _⟫_𝕜),

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : Fin (Module.finrank 𝕜 E) → E := fun i ↦ ↑√(⋯.eigenvalues ⋯ i) • (⋯.eigenvectorBasis ⋯) i
x✝ : E
⊢ T x✝ =
    ∑ x, (↑√(⋯.eigenvalues ⋯ x) * (↑√(⋯.eigenvalues ⋯ x) * ⟪(⋯.eigenvectorBasis ⋯) x, x✝⟫)) • (⋯.eigenvectorBasis ⋯) x
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 : ℝ≥0
hp : (↑(finrank ℝ E)).HolderConjugate p
h0p : 0 < ↑p
⊢ eLpNorm u (↑p) μ ^ ↑p ≤ ↑(eLpNormLESNormFDerivOneConst μ ↑p) ^ ↑p * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂μ) ^ ↑p

Tactic:
← ENNReal.coe_rpow_of_nonneg _ h0p.le,

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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ≥0
hp : (↑(finrank ℝ E)).HolderConjugate p
h0p : 0 < ↑p
⊢ eLpNorm u (↑p) μ ^ ↑p ≤ ↑(eLpNormLESNormFDerivOneConst μ ↑p ^ ↑p) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂μ) ^ ↑p
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))
C : ℝ
hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C
this : Tendsto (fun n ↦ C / ↑n) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0)

Tactic:
refine squeeze_zero_norm (fun n ↦ ?_) this

Goal state after:
α : 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))
C : ℝ
hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C
this : Tendsto (fun n ↦ C / ↑n) atTop (𝓝 0)
n : ℕ
⊢ ‖birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x‖ ≤ C / ↑n
Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : LipschitzWith 1 ⇑f
g : E →L[𝕜] ↥(f.eqLocus 1)
hg_proj : ∀ (x : ↥(f.eqLocus 1)), g ↑x = x
hg_ker : ↑(↑g).ker ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(f - 1).range
y : E
hy : g y = 0
z : E
hz : IsFixedPt (⇑f) z
this✝ :
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    {x | Tendsto (fun x_1 ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop (𝓝 0)}
x : E
this : Bornology.IsBounded (Set.range fun x_1 ↦ _root_.id ((⇑f)^[x_1] x))
H : ∀ (n : ℕ) (x y : E), (⇑f)^[n] (x - y) = (⇑f)^[n] x - (⇑f)^[n] y
⊢ (f - 1) x ∈ {x | Tendsto (fun x_1 ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop (𝓝 0)}

Tactic:
simpa [birkhoffAverage, birkhoffSum, Finset.sum_sub_distrib, smul_sub, H]
    using tendsto_birkhoffAverage_apply_sub_birkhoffAverage 𝕜 this

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

Goal state before:
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
h : ∀ (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:
sub_eq_zero

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
h : ∀ (a : E) (a_1 : a ∈ T.domain), ⟪↑T ⟨a, ⋯⟩, x.1⟫ = ⟪a, x.2⟫
⊢ ∃ (x_1 : x.1 ∈ T†.domain), ↑T† ⟨x.1, ⋯⟩ = x.2
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
i j : ℕ
hij : i ≤ j
hj : j < finrank 𝕜 E
⊢ ⋯.eigenvalues ⋯ ⟨j, hj⟩ ≤ T.singularValues i ^ 2

Tactic:
T.sq_singularValues_fin rfl ⟨i, hij.trans_lt hj⟩

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
i j : ℕ
hij : i ≤ j
hj : j < finrank 𝕜 E
⊢ ⋯.eigenvalues ⋯ ⟨j, hj⟩ ≤ ⋯.eigenvalues ⋯ ⟨i, ⋯⟩
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

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
ι : Type u_6
ι' : Type u_7
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
x : E ⊗[𝕜] F
e : OrthonormalBasis ι 𝕜 E
f : OrthonormalBasis ι' 𝕜 F
this : x = ∑ i, ∑ j, ((e.toBasis.tensorProduct f.toBasis).repr x) (i, j) • e i ⊗ₜ[𝕜] f j
⊢ inner 𝕜 x x = ↑(∑ i, ‖((e.toBasis.tensorProduct f.toBasis).repr x) i‖ ^ 2)

Tactic:
conv_lhs => rw [this]

Goal state after:
𝕜 : 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
ι : Type u_6
ι' : Type u_7
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
x : E ⊗[𝕜] F
e : OrthonormalBasis ι 𝕜 E
f : OrthonormalBasis ι' 𝕜 F
this : x = ∑ i, ∑ j, ((e.toBasis.tensorProduct f.toBasis).repr x) (i, j) • e i ⊗ₜ[𝕜] f j
⊢ inner 𝕜 (∑ i, ∑ j, ((e.toBasis.tensorProduct f.toBasis).repr x) (i, j) • e i ⊗ₜ[𝕜] f j)
      (∑ i, ∑ j, ((e.toBasis.tensorProduct f.toBasis).repr x) (i, j) • e i ⊗ₜ[𝕜] f j) =
    ↑(∑ i, ‖((e.toBasis.tensorProduct f.toBasis).repr x) i‖ ^ 2)
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
a b : ℕ
hl : b ≤ a
ha : 0 < T.singularValues a
⊢ 0 < T.singularValues b

Tactic:
order [T.singularValues_antitone hl]

Goal state after:
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
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ 0 ≤ RCLike.re (∑ x, ∑ x_1, (∑ i, Matrix.vecMulVec (A i) (star (A i))) x_1 x * inner 𝕜 (g x_1) (g x))

Tactic:
Matrix.sum_apply,

Goal state after:
𝕜 : 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
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ 0 ≤ RCLike.re (∑ x, ∑ x_1, (∑ c, Matrix.vecMulVec (A c) (star (A c)) x_1 x) * inner 𝕜 (g x_1) (g x))
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
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
α : Type u_5
inst✝² : AddGroup α
inst✝¹ : AddAction α X
inst✝ : IsIsometricVAdd α X
d : ℕ
⊢ VAddInvariantMeasure α X μHE[d]

Tactic:
rw [euclideanHausdorffMeasure_def]
  infer_instance

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
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
inst✝¹ : AddGroup X
inst✝ : IsIsometricVAdd X X
d : ℕ
⊢ μHE[d].IsAddLeftInvariant

Tactic:
rw [euclideanHausdorffMeasure_def]
  infer_instance

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
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
inst✝¹ : AddGroup X
inst✝ : IsIsometricVAdd Xᵃᵒᵖ X
d : ℕ
⊢ μHE[d].IsAddRightInvariant

Tactic:
rw [euclideanHausdorffMeasure_def]
  infer_instance

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
⊢ (OuterMeasure.mkMetric fun x ↦ ∞) = ⊤.toOuterMeasure

Tactic:
OuterMeasure.mkMetric_top,

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
⊢ ⊤ = ⊤.toOuterMeasure