mathlib-initiative/mathlib-tactics huggingface dataset:
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 s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this✝² : IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this✝¹ : FiniteDimensional K L
this✝ : IsGalois K L
H : (Algebra.norm K) η₁ = ↑(p ^ (k - s + 1)).minFac
this : p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ (k.succ - 1)
⊢ k.succ - 1 = (k - s).succ - 1 + s

Tactic:
simp only [Nat.succ_sub_succ_eq_sub, tsub_zero]

Goal state after:
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this✝² : IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this✝¹ : FiniteDimensional K L
this✝ : IsGalois K L
H : (Algebra.norm K) η₁ = ↑(p ^ (k - s + 1)).minFac
this : p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ (k.succ - 1)
⊢ k = k - s + s
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case neg
n : ℕ
x : ℤ
h : IsCoprime x ↑n
hn : ¬n = 0
⊢ ↑x * (↑x)⁻¹ = 1

Tactic:
have : NeZero n := ⟨hn⟩

Goal state after:
case neg
n : ℕ
x : ℤ
h : IsCoprime x ↑n
hn : ¬n = 0
this : NeZero n
⊢ ↑x * (↑x)⁻¹ = 1
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case neg
n : ℕ
x : ℤ
h : IsCoprime x ↑n
hn : ¬n = 0
this : NeZero n
⊢ ↑x * (↑x)⁻¹ = 1

Tactic:
← natCast_zmod_val x

Goal state after:
case neg
n : ℕ
x : ℤ
h : IsCoprime x ↑n
hn : ¬n = 0
this : NeZero n
⊢ ↑(↑x).val * (↑(↑x).val)⁻¹ = 1
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
hζ : ζ ^ n = 1
a : ℕ
⊢ (zmodChar n hζ) ↑a = ζ ^ a

Tactic:
rw [pow_eq_pow_mod a hζ, zmodChar_apply, ZMod.val_natCast]

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
ha : (zmodChar n ⋯) a = 1
⊢ a = 0

Tactic:
rw [zmodChar_apply, ← pow_zero ζ] at ha

Goal state after:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
a : ZMod n
ha : ζ ^ a.val = ζ ^ 0
⊢ a = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
⊢ ↑(toCircle j) = ↑(toCircle ↑j.val)

Tactic:
natCast_zmod_val

Goal state after:
N : ℕ
inst✝ : NeZero N
j : ZMod N
⊢ ↑(toCircle j) = ↑(toCircle j)
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✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this✝¹ : NeZero ↑n
k : K
this✝ : ∀ (z : K), ∃ x, z * (algebraMap A K) ↑x.2 = (algebraMap A K) x.1
z : A
w : ↥(nonZeroDivisors A)
hw : k * (algebraMap A K) ↑(z, w).2 = (algebraMap A K) (z, w).1
this : IsScalarTower A K (CyclotomicField n K) := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ (algebraMap K (CyclotomicField n K)) (k * (algebraMap A K) ↑w) = (algebraMap A (CyclotomicField n K)) z

Tactic:
hw,

Goal state after:
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✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this✝¹ : NeZero ↑n
k : K
this✝ : ∀ (z : K), ∃ x, z * (algebraMap A K) ↑x.2 = (algebraMap A K) x.1
z : A
w : ↥(nonZeroDivisors A)
hw : k * (algebraMap A K) ↑(z, w).2 = (algebraMap A K) (z, w).1
this : IsScalarTower A K (CyclotomicField n K) := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ (algebraMap K (CyclotomicField n K)) ((algebraMap A K) (z, w).1) = (algebraMap A (CyclotomicField n K)) z
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
inst✝¹ : NeZero n
inst✝ : Nontrivial R
p : ℕ
hp : Fact (Nat.Prime p)
this : NeZero (n / p ^ n.factorization p)
hcop : p.Coprime (n / p ^ n.factorization p)
ψ : DirichletCharacter R (n / p ^ n.factorization p)
hψ : ψ ↑↑p = 1
⊢ ((changeLevel ⋯) ψ).primitiveCharacter ↑↑p = 1

Tactic:
primitiveCharacter_changeLevel_apply,

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
inst✝¹ : NeZero n
inst✝ : Nontrivial R
p : ℕ
hp : Fact (Nat.Prime p)
this : NeZero (n / p ^ n.factorization p)
hcop : p.Coprime (n / p ^ n.factorization p)
ψ : DirichletCharacter R (n / p ^ n.factorization p)
hψ : ψ ↑↑p = 1
⊢ ψ.primitiveCharacter ↑↑p = 1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: K : Type w
L : Type z
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
n₁ n₂ : ℕ
F₁ F₂ : IntermediateField K L
h₁ : IsCyclotomicExtension {n₁} K ↥F₁
h₂ : IsCyclotomicExtension {n₂} K ↥F₂
inst✝¹ : NeZero n₁
inst✝ : NeZero n₂
⊢ IsCyclotomicExtension {n₁.lcm n₂} K ↥(F₁ ⊔ F₂)

Tactic:
have : FiniteDimensional K F₁ := IsCyclotomicExtension.finite_of_singleton n₁ K F₁
  have := IsCyclotomicExtension.lcm_sup n₁ n₂ F₁.toSubalgebra F₂.toSubalgebra
  rwa [← sup_toSubalgebra_of_left] at this

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'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ y, ∑ x, χ y * ψ (x * (y - 1)) = ↑(Fintype.card R)

Tactic:
simp_rw [← Finset.mul_sum, sum_mulShift _ hψ, sub_eq_zero, apply_ite, Nat.cast_zero, mul_zero]

Goal state after:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ (∑ x, if x = 1 then χ x * ↑(Fintype.card R) else 0) = ↑(Fintype.card R)
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: 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 χ (ψ.mulShift ↑p) = χ ↑p ^ 2 * gaussSum χ (ψ.mulShift ↑p)

Tactic:
← pow_apply' _ two_ne_zero,

Goal state after:
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 χ (ψ.mulShift ↑p) = (χ ^ 2) ↑p * gaussSum χ (ψ.mulShift ↑p)
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁✝ : ringChar F' ≠ ringChar F
hch₁ : ¬ringChar F' = ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ ↑n'
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁✝
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
hchar : ringChar F' = ringChar FF'
this✝ : Fact (Nat.Prime (ringChar F'))
this : Fact (Nat.Prime (ringChar FF'))
⊢ ((χ.ringHomComp (algebraMap F' FF')) (-1) * ↑(Fintype.card F)) ^ (ringChar FF' ^ ↑n' / 2) =
    (χ.ringHomComp (algebraMap F' FF')) (↑(ringChar FF') ^ ↑n')

Tactic:
← Nat.prime_dvd_prime_iff_eq hp' hp,

Goal state after:
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
F' : Type u_2
inst✝¹ : Field F'
inst✝ : Fintype F'
χ : MulChar F F'
hχ₁ : χ ≠ 1
hχ₂ : χ.IsQuadratic
hch₁✝ : ringChar F' ≠ ringChar F
hch₁ : ¬ringChar F' ∣ ringChar F
hch₂ : ringChar F' ≠ 2
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
n' : ℕ+
hp' : Nat.Prime (ringChar F')
hc' : Fintype.card F' = ringChar F' ^ ↑n'
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' hch₁✝
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
hchar : ringChar F' = ringChar FF'
this✝ : Fact (Nat.Prime (ringChar F'))
this : Fact (Nat.Prime (ringChar FF'))
⊢ ((χ.ringHomComp (algebraMap F' FF')) (-1) * ↑(Fintype.card F)) ^ (ringChar FF' ^ ↑n' / 2) =
    (χ.ringHomComp (algebraMap F' FF')) (↑(ringChar FF') ^ ↑n')
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
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))

Tactic:
have FFp := hchar.subst hp

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)
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
Module: Mathlib.NumberTheory.GaussSum

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

Tactic:
show χ₈ 2 = 0 from rfl,

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
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
h₁ : (fun a ↦ ↑(χ₈ a) * τ ^ ↑a) = fun a ↦ χ a * ψ₈char a
⊢ ↑0 * τ ^ ↑0 + ↑1 * τ ^ ↑1 + ↑0 * τ ^ ↑2 + ↑(χ₈ 3) * τ ^ ↑3 + ↑(χ₈ 4) * τ ^ ↑4 + ↑(χ₈ 5) * τ ^ ↑5 + ↑(χ₈ 6) * τ ^ ↑6 +
      ↑(χ₈ 7) * τ ^ ↑7 =
    2 * (τ - τ ^ 3)
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 : IsIdempotentElem T
⊢ T.IsPositive ↔ T.IsSymmetric

Tactic:
refine ⟨fun h => h.isSymmetric, fun h => ⟨h, fun x => ?_⟩⟩
  rw [← hT.eq, Module.End.mul_apply, h]
  exact inner_self_nonneg

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] E
hT : T.IsPositive
S : F →ₗ[𝕜] E
⊢ (LinearMap.adjoint S ∘ₗ T ∘ₗ S).IsPositive

Tactic:
convert! hT.conj_adjoint S.adjoint
  rw [LinearMap.adjoint_adjoint]

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
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
inst✝ : U.HasOrthogonalProjection
⊢ (∀ (x y : E), ⟪U.starProjection (T (U.starProjection x)), y⟫ = ⟪x, U.starProjection (T (U.starProjection y))⟫) ∧
    ∀ (x : E), 0 ≤ ⟪U.starProjection (T (U.starProjection x)), x⟫

Tactic:
simp_rw [← coe_coe, U.starProjection_isSymmetric _, hT.isSymmetric _,
    U.starProjection_isSymmetric _, ← U.starProjection_isSymmetric _, coe_coe,
    hT.inner_nonneg_right, implies_true, and_self]

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✝ = ↑T x✝

Tactic:
coe_coe

Goal state after:
Module: Mathlib.Dynamics.BirkhoffSum.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝ : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
⊢ birkhoffSum f g n (f x) - (birkhoffSum f g (n + 1) x - g (f^[n] x)) =
    g (f^[n] x) - (birkhoffSum f g (n + 1) x - birkhoffSum f g n (f x))

Tactic:
← sub_add,

Goal state after:
α : Type u_1
G : Type u_2
inst✝ : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
⊢ birkhoffSum f g n (f x) - birkhoffSum f g (n + 1) x + g (f^[n] x) =
    g (f^[n] x) - (birkhoffSum f g (n + 1) x - birkhoffSum f g n (f x))
Module: Mathlib.Dynamics.BirkhoffSum.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝ : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
⊢ birkhoffSum f g n (f x) - birkhoffSum f g (n + 1) x + g (f^[n] x) =
    g (f^[n] x) - (birkhoffSum f g (n + 1) x - birkhoffSum f g n (f x))

Tactic:
← sub_add,

Goal state after:
α : Type u_1
G : Type u_2
inst✝ : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
⊢ birkhoffSum f g n (f x) - birkhoffSum f g (n + 1) x + g (f^[n] x) =
    g (f^[n] x) - birkhoffSum f g (n + 1) x + birkhoffSum f g n (f x)
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)
n : ℕ
⊢ dist (birkhoffAverage 𝕜 f g n (f x)) (birkhoffAverage 𝕜 f g n x) ≤ C / ↑n

Tactic:
dist_birkhoffAverage_apply_birkhoffAverage

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 : ℕ
⊢ dist (g (f^[n] x)) (g x) / ↑n ≤ C / ↑n
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

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

Tactic:
rw [eLpNorm_nnreal_eq_lintegral h0p]
        congr
        norm_cast at this ⊢

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
f₂ : H →L[𝕜] E
x✝ : H ⊗[𝕜] G
⊢ (rTensor G (f₁ ∘SL f₂)) x✝ = (rTensor G f₁ ∘SL rTensor G f₂) x✝

Tactic:
simp [LinearMap.rTensor_comp]

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
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] (F ⊗[𝕜] G)
⊢ x = y ↔ ∀ (a : E) (b : F) (c : G), inner 𝕜 x (a ⊗ₜ[𝕜] (b ⊗ₜ[𝕜] c)) = inner 𝕜 y (a ⊗ₜ[𝕜] (b ⊗ₜ[𝕜] c))

Tactic:
simp only [← (assocIsometry 𝕜 E F G).symm.injective.eq_iff,
    ext_iff_inner_right_threefold, LinearIsometryEquiv.inner_map_eq_flip]
  simp

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

Goal state before:
pp: X : Type u_2
inst✝¹ : EMetricSpace X
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
d : ℝ≥0
hd : ⨆ i, dimH (s i) < ↑d
this : ∀ (i : ι), μH[↑d] (s i) = 0
⊢ μH[↑d] (⋃ i, s i) ≠ ∞

Tactic:
rw [measure_iUnion_null this]

Goal state after:
X : Type u_2
inst✝¹ : EMetricSpace X
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
d : ℝ≥0
hd : ⨆ i, dimH (s i) < ↑d
this : ∀ (i : ι), μH[↑d] (s i) = 0
⊢ 0 ≠ ∞
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, dimH t ≤ r
⊢ dimH s ≤ r

Tactic:
choose! t htx htr using h

Goal state after:
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
t : X → Set X
htx : ∀ x ∈ s, t x ∈ 𝓝[s] x
htr : ∀ x ∈ s, dimH (t x) ≤ r
⊢ dimH s ≤ r
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ (mkMetric' m) s = (⨆ n, pre m (↑n)⁻¹) s

Tactic:
rw [iSup_apply]

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s : Set X
⊢ (mkMetric' m) s = ⨆ i, (pre m (↑i)⁻¹) s
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case pos.e_f
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
r : ℝ≥0∞
x✝ : r > 0
t : ℕ → Set X
ht : s ⊆ iUnion t
htr : ∀ (n : ℕ), ediam (t n) ≤ r
n : ℕ
⊢ ⨆ (_ : (t n).Nonempty), ⨅ (_ : ediam (t n) ≤ r), m (ediam (t n)) = ⨆ (_ : (t n).Nonempty), m (ediam (t n))

Tactic:
simp only [iInf_eq_if, htr n, if_true]

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
β : 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∞
⊢ (mkMetric m) s ≤ liminf (fun n ↦ ∑' (i : ι n), m (ediam (t n i))) l

Tactic:
have : ∀ n, Encodable (ι n) := fun n => Encodable.ofCountable _

Goal state after:
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)
⊢ (mkMetric m) s ≤ liminf (fun n ↦ ∑' (i : ι n), m (ediam (t n i))) l
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 ≤ μH[d₁] s

Tactic:
by
  rcases h.eq_or_lt with (rfl | h); · exact le_rfl
  rcases hausdorffMeasure_zero_or_top h s with hs | hs <;> simp [hs]

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
x : X
this :
  1 ≤
    ⨅ t, ⨅ (_ : {x} ⊆ ⋃ n, t n), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ 1), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ 0
⊢ 1 ≤
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : {x} ⊆ ⋃ n, t n),
            ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ 0

Tactic:
apply le_trans this _
      convert! le_iSup₂ (α := ℝ≥0∞) (1 : ℝ≥0∞) zero_lt_one
      rfl

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
⊢ ∀ (x y : F),
    Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x_1 ↦ ⟪y, (star x_1) x⟫_𝕜

Tactic:
star_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
⊢ ∀ (x y : F),
    Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x_1 ↦
      ⟪y, (star x_1.toCLM) x⟫_𝕜
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: E : Type u_5
P : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
x y : P
⊢ μH[1] (⇑(AffineMap.lineMap x y) '' Icc 0 1) = edist x y

Tactic:
hausdorffMeasure_lineMap_image,

Goal state after:
E : Type u_5
P : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
x y : P
⊢ nndist x y • μH[1] (Icc 0 1) = edist x y
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this : Nontrivial ↥Kᗮ
w : ↥Kᗮ
hw₀ : w ≠ 0
⊢ ‖x‖ ≤ ‖o.rightAngleRotationAux₁ x‖

Tactic:
have hw' : ⟪x, (w : E)⟫ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2

Goal state after:
case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this : Nontrivial ↥Kᗮ
w : ↥Kᗮ
hw₀ : w ≠ 0
hw' : ⟪x, ↑w⟫ = 0
⊢ ‖x‖ ≤ ‖o.rightAngleRotationAux₁ x‖