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

Goal state before:
pp: S : Set ℕ
K : Type w
L : Type z
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
h : NumberField K
inst✝¹ : Finite ↑S
inst✝ : IsCyclotomicExtension S K L
⊢ FiniteDimensional ℚ L

Tactic:
have := charZero_of_injective_algebraMap (algebraMap K L).injective
      have := IsCyclotomicExtension.finite S K L
      exact Module.Finite.trans K _

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

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

Tactic:
Nat.cast_zero,

Goal state after:
case inl
n : ℕ
hn' : 1 < n
hq : 0 ≠ 1
⊢ eval 0 (cyclotomic n ℤ) ≠ 0
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

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:
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S : Set ℕ
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
b : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : b ^ n = 1
⊢ (aeval b) (X ^ n - 1) = 0

Tactic:
simp [h2]

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: ⊢ 0 = 1 * ↑0

Tactic:
Nat.cast_zero,

Goal state after:
⊢ 0 = 1 * 0
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
this✝¹ : Algebra.IsIntegral K L
h : (IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}).toSubalgebra = ⊤.toSubalgebra
b : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : b ^ n = 1
this✝ : NeZero n
this : (X ^ n - 1).Separable
⊢ (aeval b) (X ^ n - 1) = 0

Tactic:
simp [h2]

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case inl
n : ℤ
h : IsUnit ↑n
⊢ IsCoprime (↑0) n

Tactic:
Nat.cast_zero,

Goal state after:
case inl
n : ℤ
h : IsUnit ↑n
⊢ IsCoprime 0 n
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ k)
hk : 2 ≤ k
H : IsCyclotomicExtension {2 ^ k} K L
hirr : Irreducible (cyclotomic (2 ^ k) K)
this : 2 < 2 ^ k
⊢ (Algebra.norm K) (ζ - 1) = 2

Tactic:
replace hirr : Irreducible (cyclotomic (2 ^ k) K) := by simp [hirr]

Goal state after:
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ k)
hk : 2 ≤ k
H : IsCyclotomicExtension {2 ^ k} K L
this : 2 < 2 ^ k
hirr : Irreducible (cyclotomic (2 ^ k) K)
⊢ (Algebra.norm K) (ζ - 1) = 2
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: 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✝ : NeZero ↑n
this✝¹ : NeZero ↑n
this✝ : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : (cyclotomic n K).degree ≠ 0
⊢ (map (algebraMap K (cyclotomic n K).SplittingField) (cyclotomic n K)).degree ≠ 0

Tactic:
degree_map

Goal state after:
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✝ : NeZero ↑n
this✝¹ : NeZero ↑n
this✝ : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : (cyclotomic n K).degree ≠ 0
⊢ (cyclotomic n K).degree ≠ 0
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Fintype K
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
⊢ K ≃+* K'

Tactic:
by
  choose p _char_p_K using CharP.exists K
  choose p' _char_p'_K' using CharP.exists K'
  choose n hp hK using FiniteField.card K p
  choose n' hp' hK' using FiniteField.card K' p'
  have hpp' : p = p' := by
    by_contra hne
    simpa [← hK, hK', hKK', hp'.ne_one] using Nat.coprime_pow_primes n n' hp hp' hne
  rw [← hpp'] at _char_p'_K'
  haveI := fact_iff.2 hp
  letI : Algebra (ZMod p) K := ZMod.algebra _ _
  letI : Algebra (ZMod p) K' := ZMod.algebra _ _
  exact ↑(algEquivOfCardEq p hKK')

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed

Goal state before:
pp: F : Type u_1
inst✝² : Field F
n k : ℕ
inst✝¹ : NeZero ↑n
inst✝ : IsSepClosed F
⊢ NeZero ↑(n ^ k)

Tactic:
exact_mod_cast ‹NeZero (n : F)›.pow

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

Goal state before:
pp: case inr
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
⊢ χ a ∈ ℤ[μ]

Tactic:
obtain ⟨ζ, hζ₁, hζ₂⟩ := apply_mem_rootsOfUnity_of_pow_eq_one hχ h

Goal state after:
case inr
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
ζ : Rˣ
hζ₁ : ζ ∈ rootsOfUnity n R
hζ₂ : ↑ζ = χ a
⊢ χ a ∈ ℤ[μ]
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
this : NeZero n
h : ((changeLevel hm) χ).conductor ∣ χ.conductor
⊢ ((changeLevel hm) χ).conductor = χ.conductor

Tactic:
refine h.antisymm <| conductor_dvd_of_mem_conductorSet _
    ⟨h.trans χ.conductor_dvd_level, (changeLevel hm χ).primitiveCharacter, ?_⟩

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
this : NeZero n
h : ((changeLevel hm) χ).conductor ∣ χ.conductor
⊢ χ = (changeLevel ⋯) ((changeLevel hm) χ).primitiveCharacter
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
⊢ (∑ x, if x = 1 then χ x * ↑(Fintype.card R) else χ x * ↑0) = ↑(Fintype.card R)

Tactic:
Nat.cast_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 χ x * 0) = ↑(Fintype.card R)
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
hst : s ⊆ t
this : (∃ a ⊆ t, Disjoint a s ∧ a ∪ s = u) ↔ s ⊆ u ∧ u ⊆ t
⊢ (u ∈ if s ⊆ t then map { toFun := fun u ↦ (↑u).disjUnion s ⋯, inj' := ⋯ } (t \ s).powerset.attach else ∅) ↔
    s ⊆ u ∧ u ⊆ t

Tactic:
by
          simpa [hst, subset_sdiff, and_assoc]

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

Tactic:
have h₁ : (fun (a : Fin 8) ↦ ↑(χ₈ a) * τ ^ (a : ℕ)) = fun a ↦ χ a * ↑(ψ₈char a) := by
    ext1; congr; apply pow_one

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

Goal state before:
pp: X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H : ∀ ε' > 0, ∀ (x' : X), ε' ≤ ε → d x' x ≤ 2 * ε → ε * ϕ x ≤ ε' * ϕ x' → ∃ y, d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
x' : X
k : ℕ
⊢ ε * ϕ x ≤ ε * ϕ x' / 2 ^ k ↔ 2 ^ k * ϕ x ≤ ϕ x'

Tactic:
le_div_iff₀,

Goal state after:
X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H : ∀ ε' > 0, ∀ (x' : X), ε' ≤ ε → d x' x ≤ 2 * ε → ε * ϕ x ≤ ε' * ϕ x' → ∃ y, d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
x' : X
k : ℕ
⊢ ε * ϕ x * 2 ^ k ≤ ε * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'

X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H : ∀ ε' > 0, ∀ (x' : X), ε' ≤ ε → d x' x ≤ 2 * ε → ε * ϕ x ≤ ε' * ϕ x' → ∃ y, d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
x' : X
k : ℕ
⊢ 0 < 2 ^ k
Module: Mathlib.Analysis.Hofer

Goal state before:
pp: X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'
this : Nonempty X
F : ℕ → X → X
hF : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → d x' (F k x') ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun n ↦ Nat.recOn n x F
hu :
  ∀ (n : ℕ), d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) → d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
n : ℕ
IH : ∀ m ≤ n, d (u m) (u (m + 1)) ≤ ε / 2 ^ m ∧ 2 * ϕ (u m) < ϕ (u (m + 1))
A : d (u (n + 1)) x ≤ 2 * ε
m : ℕ
hm : m < n + 1
⊢ 2 * (ϕ ∘ u) m ≤ (ϕ ∘ u) (m + 1)

Tactic:
exact (IH _ <| Nat.lt_add_one_iff.1 hm).2.le

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case convert_2
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
hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3)
hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * ↑(Fintype.card (ZMod 8))
h : ↑8 ^ (Fintype.card F / 2) = χ ↑(Fintype.card F)
⊢ 8 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))

Tactic:
apply (algebraMap F FF).injective

Goal state after:
case convert_2
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 := ⋯
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 := ⋯
ψ₈char : AddChar (ZMod 8) FF := ⋯
τ : FF := ⋯
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := ⋯
hχ : χ (-1) = 1
hq : χ.IsQuadratic
h₁ : (fun a ↦ ↑(χ₈ a) * τ ^ ↑a) = fun a ↦ χ a * ψ₈char a
hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3)
hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * ↑(Fintype.card (ZMod 8))
h : ↑8 ^ (Fintype.card F / 2) = χ ↑(Fintype.card F)
⊢ (algebraMap F FF) (8 ^ (Fintype.card F / 2)) = (algebraMap F FF) ↑(χ₈ ↑(Fintype.card F))
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 : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹
⊢ C * c ^ p = c * ‖↑e.symm‖₊ ^ p

Tactic:
h0C,

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 : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹
⊢ c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹ * c ^ p = c * ‖↑e.symm‖₊ ^ p
Module: Mathlib.Dynamics.BirkhoffSum.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
f : α → α
g g' : α → M
n : ℕ
x : α
⊢ birkhoffSum f (g + g') n x = birkhoffSum f g n x + birkhoffSum f g' n x

Tactic:
by
  simpa [birkhoffSum] using sum_add_distrib

Goal state after:
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
x : E
⊢ Tendsto (fun x_1 ↦ birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop (𝓝 ↑(g x))

Tactic:
by
  /- Any point can be represented as a sum of `y ∈ LinearMap.ker g` and a fixed point `z`. -/
  obtain ⟨y, hy, z, hz, rfl⟩ : ∃ y, g y = 0 ∧ ∃ z, IsFixedPt f z ∧ x = y + z :=
    ⟨x - g x, by simp [hg_proj], g x, (g x).2, by simp⟩
  /- For a fixed point, the theorem is trivial,
  so it suffices to prove it for `y ∈ LinearMap.ker g`. -/
  suffices Tendsto (birkhoffAverage 𝕜 f _root_.id · y) atTop (𝓝 0) by
    have hgz : g z = z := congr_arg Subtype.val (hg_proj ⟨z, hz⟩)
    simpa [hy, hgz, birkhoffAverage, birkhoffSum, Finset.sum_add_distrib, smul_add]
      using this.add (hz.tendsto_birkhoffAverage 𝕜 _root_.id)
  /- By continuity, it suffices to prove the theorem on a dense subset of `LinearMap.ker g`.
  By assumption, `LinearMap.range (f - 1)` is dense in the kernel of `g`,
  so it suffices to prove the theorem for `y = f x - x`. -/
  have : IsClosed {x | Tendsto (birkhoffAverage 𝕜 f _root_.id · x) atTop (𝓝 0)} :=
    isClosed_setOfPred_tendsto_birkhoffAverage 𝕜 hf uniformContinuous_id continuous_const
  refine closure_minimal (Set.forall_mem_range.2 fun x ↦ ?_) this (hg_ker hy)
  /- Finally, for `y = f x - x` the average is equal to the difference between averages
  along the orbits of `f x` and `x`, and most of the terms cancel. -/
  have : IsBounded (Set.range (_root_.id <| f^[·] x)) :=
    isBounded_iff_forall_norm_le.2 ⟨‖x‖, Set.forall_mem_range.2 fun n ↦ by
      have H : f^[n] 0 = 0 := iterate_map_zero (f : E →+ E) n
      simpa [H] using (hf.iterate n).dist_le_mul x 0⟩
  have H : ∀ n x y, f^[n] (x - y) = f^[n] x - f^[n] y := iterate_map_sub (f : E →+ E)
  simpa [birkhoffAverage, birkhoffSum, Finset.sum_sub_distrib, smul_sub, H]
    using tendsto_birkhoffAverage_apply_sub_birkhoffAverage 𝕜 this

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
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
⊢ Function.Injective ⇑T ↔ ∀ i < finrank 𝕜 E, 0 < T.singularValues i

Tactic:
← adjoint_comp_self_injective_iff,

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
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
⊢ Function.Injective (⇑(adjoint T) ∘ ⇑T) ↔ ∀ i < finrank 𝕜 E, 0 < T.singularValues i
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
n : ℕ
hn : ↑T.singularValues.support = Set.Iio n
⊢ T.singularValues.support = Finset.range (finrank 𝕜 ↥T.range)

Tactic:
← Finset.coe_Iio,

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
n : ℕ
hn : ↑T.singularValues.support = ↑(Finset.Iio n)
⊢ T.singularValues.support = Finset.range (finrank 𝕜 ↥T.range)
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case e'_4.h
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
⊢ 0 ≤ 1 / ↑q - 1 / ↑p'

Tactic:
rw [one_div, one_div]
          norm_cast
          rw [hp']
          simpa using hpq

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

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 ↥f.range
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
⊢ f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖

Tactic:
simp only [normDet, h, ↓reduceDIte]

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 ↥f.range
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
⊢ ‖((toMatrix (stdOrthonormalBasis 𝕜 U).toBasis ⋯.some.toBasis) f.rangeRestrict).det‖ =
    ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖
Module: Mathlib.Geometry.Euclidean.Volume.Measure

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

Tactic:
Measure.smul_apply,

Goal state after:
𝕜 : Type u_3
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℕ
r : 𝕜
hr : r ≠ 0
s : Set E
⊢ volume.addHaarScalarFactor μH[↑d] • μH[↑d] (r • s) = ‖r‖₊ ^ d • (volume.addHaarScalarFactor μH[↑d] • μH[↑d]) s
Module: Mathlib.Geometry.Euclidean.Volume.Measure

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

Tactic:
Measure.smul_apply,

Goal state after:
𝕜 : Type u_3
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℕ
r : 𝕜
hr : r ≠ 0
s : Set E
⊢ volume.addHaarScalarFactor μH[↑d] • ‖r‖₊ ^ ↑d • μH[↑d] s = ‖r‖₊ ^ d • volume.addHaarScalarFactor μH[↑d] • μH[↑d] s
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 ↥f.range
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
h1 : bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis = 1
⊢ ‖(h.some.toBasis.toMatrix ⇑bv.toBasis * (toMatrix bu.toBasis bv.toBasis) f.rangeRestrict *
          bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis).det‖ =
    ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖

Tactic:
have h2 : (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix bu.toBasis *
      bu.toBasis.toMatrix (stdOrthonormalBasis 𝕜 U).toBasis = 1 :=
    Basis.toMatrix_mul_toMatrix_flip _ _

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 ↥f.range
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
h1 : bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis = 1
h2 : (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis * bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis = 1
⊢ ‖(h.some.toBasis.toMatrix ⇑bv.toBasis * (toMatrix bu.toBasis bv.toBasis) f.rangeRestrict *
          bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis).det‖ =
    ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖