mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
f g : ℕ → R
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n

Tactic:
rw [sum_eq_iff_sum_smul_moebius_eq]
  apply forall_congr'
  refine fun a => imp_congr_right fun _ => (sum_congr rfl fun x _hx => ?_).congr_left
  rw [zsmul_eq_mul]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
by
  constructor
  · intro h
    let G := fun (n : ℕ) => (∑ i ∈ n.divisors, f i)
    intro n hn hnP
    suffices ∑ d ∈ n.divisors, μ (n / d) • G d = f n by
      rw [sum_divisorsAntidiagonal' (f := fun x y => μ x • g y), ← this, sum_congr rfl]
      intro d hd
      rw [← h d (pos_of_mem_divisors hd) <| hs d n (dvd_of_mem_divisors hd) hnP]
    rw [← sum_divisorsAntidiagonal' (f := fun x y => μ x • G y)]
    apply sum_eq_iff_sum_smul_moebius_eq.mp _ n hn
    intro _ _; rfl
  · intro h
    let F := fun (n : ℕ) => ∑ x ∈ n.divisorsAntidiagonal, μ x.fst • g x.snd
    intro n hn hnP
    suffices ∑ d ∈ n.divisors, F d = g n by
      rw [← this, sum_congr rfl]
      intro d hd
      rw [← h d (pos_of_mem_divisors hd) <| hs d n (dvd_of_mem_divisors hd) hnP]
    apply sum_eq_iff_sum_smul_moebius_eq.mpr _ n hn
    intro _ _; rfl

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

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ primitiveRoots 0 R = ∅

Tactic:
by
  classical
  rw [primitiveRoots, nthRoots_zero, Multiset.toFinset_zero, Finset.filter_empty]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Periodic

Goal state before:
pp: case e'_2
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : AddCommGroup X
inst✝³ : ContinuousAdd X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n ↦ f.comp (ContinuousMap.addRight (n • p))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (c : ℤ), f.comp (ContinuousMap.addRight ((Equiv.addRight 1) c • p))) x

Tactic:
have : Summable fun (c : ℤ) => f.comp (ContinuousMap.addRight (Equiv.addRight 1 c • p)) :=
      (Equiv.addRight (1 : ℤ)).summable_iff.mpr h

Goal state after:
case e'_2
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : AddCommGroup X
inst✝³ : ContinuousAdd X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n ↦ f.comp (ContinuousMap.addRight (n • p))
this : Summable fun c ↦ f.comp (ContinuousMap.addRight ((Equiv.addRight 1) c • p))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (c : ℤ), f.comp (ContinuousMap.addRight ((Equiv.addRight 1) c • p))) x
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K = (∏ i ∈ Finset.cons n n.properDivisors ⋯, cyclotomic' i K) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K

Tactic:
Finset.prod_cons

Goal state after:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K =
    (cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x K) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case h.inl
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
ihk : ∀ m < 0, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
h : IsPrimitiveRoot ζ 0
⊢ cyclotomic' 0 K ∈ lifts (Int.castRingHom K)

Tactic:
use 1

Goal state after:
case h
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
ihk : ∀ m < 0, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
h : IsPrimitiveRoot ζ 0
⊢ (mapRingHom (Int.castRingHom K)) 1 = cyclotomic' 0 K
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case left
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
⊢ cyclotomic' k K * B = ∏ i ∈ Finset.cons k k.properDivisors ⋯, cyclotomic' i K

Tactic:
Finset.prod_cons

Goal state after:
case left
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
⊢ cyclotomic' k K * B = cyclotomic' k K * ∏ x ∈ k.properDivisors, cyclotomic' x K
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
⊢ cyclotomic n R = (∏ i ∈ cons n n.properDivisors ⋯, cyclotomic i R) /ₘ ∏ i ∈ n.properDivisors, cyclotomic i R

Tactic:
Finset.prod_cons

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
⊢ cyclotomic n R = (cyclotomic n R * ∏ x ∈ n.properDivisors, cyclotomic x R) /ₘ ∏ i ∈ n.properDivisors, cyclotomic i R
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: case e_f
E : Type u_1
V : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
f : V → E
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm
w : StrongDual ℝ V
v : V
⊢ 𝐞 (-w v) • f v = 𝐞 (-⟪v, A w⟫) • f v

Tactic:
← inner_conj_symm,

Goal state after:
case e_f
E : Type u_1
V : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
f : V → E
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm
w : StrongDual ℝ V
v : V
⊢ 𝐞 (-w v) • f v = 𝐞 (-(starRingEnd ℝ) ⟪A w, v⟫) • f v
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hcycl : P = cyclotomic n R
⊢ cyclotomic n R * ∏ i ∈ n.properDivisors, cyclotomic i R = ∏ i ∈ cons n n.properDivisors ⋯, cyclotomic i R

Tactic:
Finset.prod_cons

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hcycl : P = cyclotomic n R
⊢ cyclotomic n R * ∏ i ∈ n.properDivisors, cyclotomic i R = cyclotomic n R * ∏ x ∈ n.properDivisors, cyclotomic x R
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
⊢ (cyclotomic n R).roots.Nodup

Tactic:
obtain h | ⟨ζ, hζ⟩ := (cyclotomic n R).roots.empty_or_exists_mem
  · exact h.symm ▸ Multiset.nodup_zero
  rw [mem_roots <| cyclotomic_ne_zero n R, isRoot_cyclotomic_iff] at hζ
  refine Multiset.nodup_of_le
    (roots.le_of_dvd (X_pow_sub_C_ne_zero (NeZero.pos_of_neZero_natCast R) 1) <|
      cyclotomic.dvd_X_pow_sub_one n R) hζ.nthRoots_one_nodup

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

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
μ : R
n : ℕ
inst✝¹ : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (cyclotomic n K)
inst✝ : NeZero ↑n
⊢ cyclotomic n K = minpoly K μ

Tactic:
by
  have := NeZero.of_faithfulSMul K R n
  refine minpoly.eq_of_irreducible_of_monic h ?_ (cyclotomic.monic n K)
  rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← IsRoot.def, isRoot_cyclotomic_iff]

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

Goal state before:
pp: case inr
n m : ℕ
h : n ≠ m
hnzero : n > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)

Tactic:
rcases m.eq_zero_or_pos with (rfl | hmzero)

Goal state after:
case inr.inl
n : ℕ
hnzero : n > 0
h : n ≠ 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic 0 ℚ)

case inr.inr
n m : ℕ
h : n ≠ m
hnzero : n > 0
hmzero : m > 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
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 η
⊢ p ^ (k + 1) = p ^ (s + (k + 1 - s))

Tactic:
add_comm s,

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 η
⊢ p ^ (k + 1) = p ^ (k + 1 - s + s)
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case refine_2
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 η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
⊢ η + 1 ∈ K⟮η⟯

Tactic:
exact add_mem (IntermediateField.mem_adjoin_simple_self K η) (one_mem _)

Goal state after:
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
⊢ cyclotomic n B ≠ 0 ∧ (cyclotomic n B).IsRoot ζ

Tactic:
exact ⟨cyclotomic_ne_zero n B, hζ.isRoot_cyclotomic (NeZero.pos n)⟩

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

Goal state before:
pp: case refine_2.e_a
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
⊢ k - s + 1 ≠ 0

Tactic:
exact Nat.succ_ne_zero _

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'
a : R
h : 0 < ringChar R
⊢ ⋯.unit ∈ rootsOfUnity (↑(ringChar R).toPNat') R'

Tactic:
simp only [mem_rootsOfUnity', IsUnit.unit_spec, Nat.toPNat'_coe, h, ↓reduceIte,
    ← map_nsmul_eq_pow, nsmul_eq_mul, CharP.cast_eq_zero, zero_mul, map_zero_eq_one]

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

Goal state before:
pp: case right
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
⊢ Normal K L

Tactic:
obtain ⟨i⟩ := nonempty_algEquiv_adjoin_of_isSepClosed S K L (AlgebraicClosure K)

Goal state after:
case right
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
⊢ Normal K L
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case right
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
f : AlgebraicClosure K →ₐ[K] AlgebraicClosure K
y : AlgebraicClosure K
hy : y ∈ (IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}).toSubalgebra
⊢ f y ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
IntermediateField.mem_toSubalgebra

Goal state after:
case right
S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
f : AlgebraicClosure K →ₐ[K] AlgebraicClosure K
y : AlgebraicClosure K
hy : y ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
⊢ f y ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ ((4 * (n / 4) + n % 4) / 2)

Tactic:
show 4 = 2 * 2 by lia

Goal state after:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ ((2 * 2 * (n / 4) + n % 4) / 2)
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:
by
    intro a ha
    simp only [ha, if_false]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
hm : n ∣ m
a : ℤ
ha : IsCoprime a ↑m
⊢ ((changeLevel hm) χ) ↑a = χ ↑a

Tactic:
← ZMod.coe_unitOfIsCoprime _ ha,

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
hm : n ∣ m
a : ℤ
ha : IsCoprime a ↑m
⊢ ((changeLevel hm) χ) ↑(ZMod.unitOfIsCoprime a ha) = χ ↑a
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'
x : Rˣ
⊢ (⇑χ⁻¹ * ⇑χ) ↑x = 1 ↑x

Tactic:
Pi.mul_apply,

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
x : Rˣ
⊢ χ⁻¹ ↑x * χ ↑x = 1 ↑x
Module: Mathlib.NumberTheory.MulChar.Lemmas

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

Tactic:
· rw [Subtype.ext_iff, Units.ext_iff] at h
    push_cast at h
    exact ((Nat.le_of_dvd hm₀ <| hζ.dvd_of_pow_eq_one _ h).trans_lt hm).false

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

Goal state before:
pp: α : Type u_1
a : α
⊢ ∅ ⋖ {a}

Tactic:
classical exact insert_empty_eq (β := Finset α) a ▸ covBy_insert <| notMem_empty a

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

Goal state before:
pp: case mp
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (∃ a ∉ t, insert a t = s) → t ⊆ s ∧ #(s \ t) = 1

pp: case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ t ⊆ s ∧ #(s \ t) = 1 → ∃ a ∉ t, insert a t = s

Tactic:
· rintro ⟨a, ha, rfl⟩
    simp [*]

Goal state after:
case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ t ⊆ s ∧ #(s \ t) = 1 → ∃ a ∉ t, insert a t = s
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

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

Tactic:
← map_tmul,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x y : 𝕜
⊢ (adjoint counit) (x * y) = (adjoint comul) ((map (adjoint counit) (adjoint counit)) (x ⊗ₜ[𝕜] y))
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
hT' : T ≠ 0
α : 𝕜
h : (α • T).IsPositive
x : E
hx : 0 < ⟪x, T x⟫
⊢ ?m.78

Tactic:
by simpa [inner_smul_right] using h.inner_nonneg_right x

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
⊢ T.IsFinitelySemisimple

Tactic:
refine Module.End.isFinitelySemisimple_iff.mpr fun p hp₁ hp₂ q hq₁ hq₂ ↦
    ⟨qᗮ ⊓ p, inf_le_right, Module.End.invtSubmodule.inf_mem ?_ hp₁, ?_, ?_⟩
  · exact orthogonalComplement_mem_invtSubmodule hT hq₁
  · simp [disjoint_iff, ← inf_assoc, Submodule.inf_orthogonal_eq_bot q]
  · suffices q ⊔ qᗮ = ⊤ by rw [← sup_inf_assoc_of_le _ hq₂, this, top_inf_eq p]
    replace hp₂ : Module.Finite 𝕜 q := Submodule.finiteDimensional_of_le hq₂
    exact Submodule.sup_orthogonal_of_hasOrthogonalProjection

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✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : E →L[𝕜] F
⊢ (S ∘SL T ∘SL adjoint S).IsPositive

Tactic:
refine isPositive_def'.mpr ⟨hT.isSelfAdjoint.conj_adjoint S, fun x => ?_⟩

Goal state after:
𝕜 : 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✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : T.IsPositive
S : E →L[𝕜] F
x : F
⊢ 0 ≤ (S ∘SL T ∘SL adjoint S).reApplyInnerSelf x
Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram

Goal state before:
pp: V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ IsClosed ↑(↑(continuousLinearMapOfBilin B)).range

Tactic:
by
  rcases coercive.antilipschitz with ⟨_, _, antilipschitz⟩
  exact antilipschitz.isClosed_range B♯.uniformContinuous

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
⊢ ↑p < ↑n

Tactic:
exact h2p

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
S : F →ₗ.[𝕜] E
h : T.IsFormalAdjoint S
y : ↥S.domain
x✝ : ↥T.domain
⊢ ⟪↑S y, ↑x✝⟫ = ⟪↑y, ↑T x✝⟫

Tactic:
← inner_conj_symm,

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
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
h : T.IsFormalAdjoint S
y : ↥S.domain
x✝ : ↥T.domain
⊢ (starRingEnd 𝕜) ⟪↑x✝, ↑S y⟫ = ⟪↑y, ↑T x✝⟫
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: case h
𝕜 : 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⟫
a : E
ha : a ∈ T.domain
⊢ ⟪x.2, ↑⟨a, ha⟩⟫ = ⟪x.1, ↑T ⟨a, ha⟩⟫

Tactic:
← inner_conj_symm,

Goal state after:
case h
𝕜 : 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⟫
a : E
ha : a ∈ T.domain
⊢ (starRingEnd 𝕜) ⟪↑⟨a, ha⟩, x.2⟫ = ⟪x.1, ↑T ⟨a, ha⟩⟫
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'
⊢ ↑C * eLpNorm (fderiv ℝ v) 1 μ = ↑C * ∫⁻ (x : E), ‖fderiv ℝ v x‖ₑ ∂μ

Tactic:
by rw [eLpNorm_one_eq_lintegral_enorm]

Goal state after: