mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ ¬AddCircle.toCircle (x i) = AddCircle.toCircle (y i)

Tactic:
contrapose hi

Goal state after:
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : AddCircle.toCircle (x i) = AddCircle.toCircle (y i)
⊢ x i = y i
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
⊢ ∫ (x : UnitAddTorus d), (mFourier (n + -m)) x = if m = n then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : m = n
⊢ ∫ (x : UnitAddTorus d), (mFourier (n + -m)) x = 1

case neg
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : ¬m = n
⊢ ∫ (x : UnitAddTorus d), (mFourier (n + -m)) x = 0
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: 𝕜 : Type u_2
F : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : NormedSpace 𝕜 F
f : 𝓢(ℝ, F)
⊢ (derivCLM F) ((toTemperedDistributionCLM ℝ F volume) f) =
    (toTemperedDistributionCLM ℝ F volume) ((SchwartzMap.derivCLM 𝕜 F) f)

Tactic:
ext1 g

Goal state after:
𝕜 : Type u_2
F : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : NormedSpace 𝕜 F
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, ℂ)
⊢ ((derivCLM F) ((toTemperedDistributionCLM ℝ F volume) f)) g =
    ((toTemperedDistributionCLM ℝ F volume) ((SchwartzMap.derivCLM 𝕜 F) f)) g
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : 𝓢(E, F)
m : E
⊢ ∂_{m} ((toTemperedDistributionCLM E F μ) f) = (toTemperedDistributionCLM E F μ) (∂_{m} f)

Tactic:
ext1 g

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : 𝓢(E, F)
m : E
g : 𝓢(E, ℂ)
⊢ (∂_{m} ((toTemperedDistributionCLM E F μ) f)) g = ((toTemperedDistributionCLM E F μ) (∂_{m} f)) g
Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality

Goal state before:
pp: G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
⊢ ⟪⇑ψ₁, ⇑ψ₂⟫ₙ_[R] = if ψ₁ = ψ₂ then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ψ₁ = ψ₂
⊢ ⟪⇑ψ₁, ⇑ψ₂⟫ₙ_[R] = 1

case neg
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
⊢ ⟪⇑ψ₁, ⇑ψ₂⟫ₙ_[R] = 0
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case of
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
⊢ (directSumNeZeroMulHom p n) ((if h : n i = 0 then 0 else DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩) x) =
    (DirectSum.of (fun i ↦ ZMod (p i ^ n i)) i) x

Tactic:
split_ifs with h

Goal state after:
case pos
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
h : n i = 0
⊢ (directSumNeZeroMulHom p n) (0 x) = (DirectSum.of (fun i ↦ ZMod (p i ^ n i)) i) x

case neg
ι : Type
inst✝ : DecidableEq ι
p n : ι → ℕ
i : ι
x : ZMod (p i ^ n i)
h : ¬n i = 0
⊢ (directSumNeZeroMulHom p n) ((DirectSum.of (fun j ↦ ZMod (p ↑j ^ n ↑j)) ⟨i, h⟩) x) =
    (DirectSum.of (fun i ↦ ZMod (p i ^ n i)) i) x
Module: Mathlib.Analysis.Fourier.Convolution

Goal state before:
pp: E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℂ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℂ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : CompleteSpace F₃
inst✝¹ : CompleteSpace F₁
inst✝ : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
this : Integrable (fun ξ ↦ (B ((𝓕 f) ξ)) ((𝓕 g) ξ)) volume
x✝ : E
⊢ 𝓕 (⇑f ⋆[B, volume] ⇑g) x✝ = (B ((𝓕 f) x✝)) ((𝓕 g) x✝)

Tactic:
← fourier_convolution_apply B f g,

Goal state after:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℂ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℂ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : CompleteSpace F₃
inst✝¹ : CompleteSpace F₁
inst✝ : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
this : Integrable (fun ξ ↦ (B ((𝓕 f) ξ)) ((𝓕 g) ξ)) volume
x✝ : E
⊢ (𝓕 (((convolution B) f) g)) x✝ = (B ((𝓕 f) x✝)) ((𝓕 g) x✝)
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n : ℕ+
⊢ m.gcd n = n.gcd m

Tactic:
by
  apply eq
  simp only [gcd_coe]
  apply Nat.gcd_comm

Goal state after:
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = m.gcd (a * b)

Tactic:
by rw [gcd_comm]; apply Coprime.factor_eq_gcd_left cop am bn

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

Goal state before:
pp: n : ℕ
⊢ μ n ^ 2 = if Squarefree n then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
n : ℕ
h : Squarefree n
⊢ μ n ^ 2 = 1

case neg
n : ℕ
h : ¬Squarefree n
⊢ μ n ^ 2 = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: n : ℕ
⊢ |μ n| = if Squarefree n then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
n : ℕ
h : Squarefree n
⊢ |μ n| = 1

case neg
n : ℕ
h : ¬Squarefree n
⊢ |μ n| = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
⊢ μ (p ^ k) = if k = 1 then -1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : k = 1
⊢ μ (p ^ k) = -1

case neg
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ μ (p ^ k) = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + f p) = ∑ d ∈ n.divisors, f d

Tactic:
trans (∏ᵖ p ∣ n, ((ζ : ArithmeticFunction R) + f) p)
  · simp_rw [prodPrimeFactors_apply hn.ne_zero, add_apply, natCoe_apply]
    apply prod_congr rfl; intro p hp
    rw [zeta_apply_ne (prime_of_mem_primeFactorsList <| List.mem_toFinset.mp hp).ne_zero, cast_one]
  rw [isMultiplicative_zeta.natCast.prodPrimeFactors_add_of_squarefree h_mult hn,
    coe_zeta_mul_apply]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ ζ ^ j = 1 * ζ ^ i

Tactic:
H,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
hij : i ≤ j
⊢ ζ ^ j = 1 * ζ ^ j
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_4
q : ℚ
h : Odd q.num
⊢ q.den * 2 = (↑q.num / (↑q.den * 2)).den

Tactic:
← Int.cast_ofNat,

Goal state after:
case e'_4
q : ℚ
h : Odd q.num
⊢ q.den * 2 = (↑q.num / (↑q.den * ↑2)).den
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1
hzero : ↑n = 0
⊢ False

Tactic:
exact hdiv ((ZMod.natCast_eq_zero_iff n p).1 hzero)

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

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ cyclotomic n ℤ = ⋯.choose

Tactic:
by
  simp only [cyclotomic, h, dif_neg, not_false_iff]
  ext i
  simp only [coeff_map, Int.cast_id, eq_intCast]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a : R
⊢ (nthRoots n a).card = if ∃ α, α ^ n = a then n else 0

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a : R
h : ∃ α, α ^ n = a
⊢ (nthRoots n a).card = n

case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
a : R
h : ¬∃ α, α ^ n = a
⊢ (nthRoots n a).card = 0
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
f : S ≃ₐ[R] S
h : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
⊢ ↑↑hμ.toRootsOfUnity ^ (↑h.choose).val = ↑↑hμ.toRootsOfUnity ^ h.choose

Tactic:
rw [← rootsOfUnity.coe_pow, ← rootsOfUnity.coe_pow]

Goal state after:
R : Type u_4
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
f : S ≃ₐ[R] S
h : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
⊢ ↑↑(hμ.toRootsOfUnity ^ (↑h.choose).val) = ↑↑(hμ.toRootsOfUnity ^ h.choose)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
H : ∀ (i j : Fin p), α i = α j
i : ℕ
h : i < p
⊢ P.coeff i = (cyclotomic p ℚ * C (α 0)).coeff i

Tactic:
lift i to Fin p using h; simp [cyclotomic_prime, ← hP, H i 0]

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

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero ↑l
⊢ ∃ r, x = (-ζ) ^ r

Tactic:
obtain ⟨a, ha⟩ := hlroot.dvd_of_isCyclotomicExtension n hlzero.1

Goal state after:
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero ↑l
a : ℕ
ha : 2 * n = l * a
⊢ ∃ r, x = (-ζ) ^ r
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
⊢ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} = ⊤

Tactic:
_root_.eq_top_iff,

Goal state after:
case refine_2
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
⊢ ⊤ ≤ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
Module: Mathlib.Data.ZMod.Units

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

Tactic:
· have pps : p ∈ ps := Finset.mem_filter.mpr ⟨Nat.mem_primeFactors.mpr ⟨pp, hpn, hm.out⟩, hpx⟩
    have h := Nat.dvd_sub hp ((Finset.dvd_prod_of_mem id pps).mul_right n)
    rw [Nat.add_sub_cancel] at h
    contradiction

Goal state after:
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 + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
H : -1 - 1 = (algebraMap K L) (-2)
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
⊢ (Algebra.norm K) (-1 - 1) = (-2) ^ 2 ^ k

Tactic:
H,

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 + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
H : -1 - 1 = (algebraMap K L) (-2)
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
⊢ (Algebra.norm K) ((algebraMap K L) (-2)) = (-2) ^ 2 ^ k
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case inr
K : Type u_1
inst✝ : Field K
val✝ : Infinite K
⊢ (X ^ Nat.card K - X).Splits

Tactic:
· rw [← Polynomial.splits_neg_iff]
    simpa [Nat.card_eq_zero_of_infinite, pow_zero, neg_sub] using Splits.X_sub_C (1 : K)

Goal state after:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case intro
p✝¹ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝¹)
n✝ p✝ : ℕ
h_prime : Fact (Nat.Prime p✝)
n : ℕ
K✝ : Type u_1
inst✝⁵ : Field K✝
inst✝⁴ : Algebra (ZMod p✝) K✝
K : Type u_2
K' : Type u_3
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Finite K'
inst✝ : Algebra K K'
val✝ : Fintype K'
p : ℕ
hp : CharP K p
⊢ IsGalois K K'

Tactic:
have : CharP K p := hp

Goal state after:
case intro
p✝¹ : ℕ
inst✝⁶ : Fact (Nat.Prime p✝¹)
n✝ p✝ : ℕ
h_prime : Fact (Nat.Prime p✝)
n : ℕ
K✝ : Type u_1
inst✝⁵ : Field K✝
inst✝⁴ : Algebra (ZMod p✝) K✝
K : Type u_2
K' : Type u_3
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Finite K'
inst✝ : Algebra K K'
val✝ : Fintype K'
p : ℕ
hp : CharP K p
this : CharP K p
⊢ IsGalois K K'
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
⊢ ∑ x, ψ (x * b) = ↑(if b = 0 then Fintype.card R else 0)

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
h : b = 0
⊢ ∑ x, ψ (x * b) = ↑(Fintype.card R)

case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
h : ¬b = 0
⊢ ∑ x, ψ (x * b) = ↑0
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
k : Type u_3
inst✝² : AddCommGroup k
inst✝¹ : Finite k
inst✝ : Module (ZMod p) k
⊢ p ^ Module.finrank (ZMod p) k = Nat.card k

Tactic:
Module.natCard_eq_pow_finrank (K := ZMod p),

Goal state after:
p : ℕ
inst✝³ : Fact (Nat.Prime p)
k : Type u_3
inst✝² : AddCommGroup k
inst✝¹ : Finite k
inst✝ : Module (ZMod p) k
⊢ p ^ Module.finrank (ZMod p) k = Nat.card (ZMod p) ^ Module.finrank (ZMod p) k
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝ : Nontrivial R
a : ℤ
⊢ IsUnit ↑a ↔ IsCoprime a ↑n

Tactic:
ZMod.coe_int_isUnit_iff_isCoprime,

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝ : Nontrivial R
a : ℤ
⊢ IsCoprime (↑n) a ↔ IsCoprime a ↑n
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : StarRing R'
χ χ' : MulChar R R'
⊢ (χ * χ').starComp = χ'.starComp * χ.starComp

Tactic:
ext1
    simp [starComp_apply, mul_comm]

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

Goal state before:
pp: case calc_1
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
⊢ 1 a = if IsUnit a then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : IsUnit a
⊢ 1 a = 1

case neg
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : ¬IsUnit a
⊢ 1 a = 0
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j t : ZMod N
⊢ ∑ i, stdAddChar (t * i) = if t = 0 then ↑N else 0

Tactic:
split_ifs with h

Goal state after:
case pos
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j t : ZMod N
h : t = 0
⊢ ∑ i, stdAddChar (t * i) = ↑N

case neg
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j t : ZMod N
h : ¬t = 0
⊢ ∑ i, stdAddChar (t * i) = 0
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
k : ZMod N
⊢ 𝓕 (⇑χ) k = χ⁻¹ (-k) * gaussSum χ stdAddChar

Tactic:
rw [fourierTransform_eq_gaussSum_mulShift, gaussSum_mulShift_of_isPrimitive _ hχ]

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

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
ι : Type u_2
inst✝ : LinearOrder ι
v : ι → E
hv : Orthonormal ℝ v
s t : ↑(Set.powersetCard ι n)
⊢ (innerProductForm ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm s))))
      ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm t))) =
    if s = t then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
ι : Type u_2
inst✝ : LinearOrder ι
v : ι → E
hv : Orthonormal ℝ v
s t : ↑(Set.powersetCard ι n)
h : s = t
⊢ (innerProductForm ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm s))))
      ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm t))) =
    1

case neg
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
ι : Type u_2
inst✝ : LinearOrder ι
v : ι → E
hv : Orthonormal ℝ v
s t : ↑(Set.powersetCard ι n)
h : ¬s = t
⊢ (innerProductForm ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm s))))
      ((ιMulti ℝ n) (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm t))) =
    0
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : p.IsSymmetricProjection
hq : q.IsSymmetricProjection
⊢ p ≤ q ↔ p.range ≤ q.range

Tactic:
refine ⟨fun ⟨h1, h2⟩ a ha ↦ ?_, fun hpq ↦ (hp.sub_of_range_le_range hq hpq).isPositive⟩
  specialize h2 a
  have hh {T : E →ₗ[𝕜] E} (hT : T.IsSymmetricProjection) : RCLike.re ⟪T a, a⟫_𝕜 = ‖T a‖ ^ 2 := by
    conv_lhs => rw [← hT.isIdempotentElem]
    rw [Module.End.mul_apply, hT.isSymmetric]
    exact inner_self_eq_norm_sq _
  simp_rw [sub_apply, inner_sub_left, map_sub, hh hq, hh hp,
    hp.isIdempotentElem.mem_range_iff.mp ha, sub_nonneg, sq_le_sq, abs_norm] at h2
  obtain ⟨U, _, rfl⟩ := isSymmetricProjection_iff_eq_coe_starProjection.mp hq
  simpa [Submodule.toLinearMap_starProjection_eq_isComplProjection] using
    U.mem_iff_norm_starProjection _ |>.mpr <| le_antisymm (U.norm_starProjection_apply_le a) h2

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
f : E →ₗ[𝕜] E
hf : f.IsPositive
⊢ 0 ≤ (if H : ∃ s, Nonempty (Module.Basis (↥s) 𝕜 E) then traceAux 𝕜 ⋯.some else 0) f

Tactic:
split_ifs with h

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ∃ s, Nonempty (Module.Basis (↥s) 𝕜 E)
⊢ 0 ≤ (traceAux 𝕜 ⋯.some) f

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : f.IsPositive
h : ¬∃ s, Nonempty (Module.Basis (↥s) 𝕜 E)
⊢ 0 ≤ 0 f
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
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫‖
⊢ IsUnit f

Tactic:
rw [isUnit_iff_bijective, bijective_iff_dense_range_and_antilipschitz]
  have h_anti : AntilipschitzWith c⁻¹ f := antilipschitz_of_forall_le_inner_map f hc h
  refine ⟨?_, ⟨_, h_anti⟩⟩
  rw [Submodule.topologicalClosure_eq_top_iff, Submodule.eq_bot_iff]
  intro x hx
  have : ‖x‖ ^ 2 * c = 0 := le_antisymm (by simpa only [hx (f x) ⟨x, rfl⟩, norm_zero] using h x)
    (by positivity)
  aesop

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case hfg
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)⁻¹
hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p
v : (ι → ℝ) → F := u ∘ ⇑e.symm
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
y : ι → ℝ
⊢ ‖fderiv ℝ u (e.symm y) ∘SL ↑e.symm‖ₑ ≤ ‖fderiv ℝ u (e.symm y)‖ₑ * ‖↑e.symm‖ₑ

Tactic:
apply ContinuousLinearMap.opENorm_comp_le

Goal state after:
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: case pos
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f ≤ f.closure

Tactic:
refine le_of_le_graph ?_

Goal state after:
case pos
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : f.IsClosable
⊢ f.graph ≤ f.closure.graph
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hg : g.IsClosable
h : f ≤ g
⊢ f.closure ≤ g.closure

Tactic:
refine le_of_le_graph ?_

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hg : g.IsClosable
h : f ≤ g
⊢ f.closure.graph ≤ g.closure.graph