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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
heq : (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0
⊢ (X ^ n - 1).coeff 0 = -1

Tactic:
rw [coeff_zero_eq_eval_zero _]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
heq : (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0
⊢ eval 0 (X ^ n - 1) = -1
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: K : Type u_1
S : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing S
inst✝⁴ : Algebra K S
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i : Fin B.dim
j : Fin B'.dim
⊢ IsIntegral R (B.basis.toMatrix (⇑B'.basis) i j)

Tactic:
B.basis.toMatrix_apply,

Goal state after:
K : Type u_1
S : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing S
inst✝⁴ : Algebra K S
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i : Fin B.dim
j : Fin B'.dim
⊢ IsIntegral R ((B.basis.repr (B'.basis j)) i)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

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

Tactic:
exact not_odd_iff_even.2 (even_iff_two_dvd.mpr hi.2.1) hk

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

Goal state before:
pp: case refine_1.inl
S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ
hn' : n✝ ≠ 0
hn : n✝ ∈ S
⊢ ∃ r, IsPrimitiveRoot r n✝

Tactic:
obtain ⟨b, hb⟩ := ((isCyclotomicExtension_iff _ _ _).1 hS).1 hn hn'

Goal state after:
case refine_1.inl
S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ
hn' : n✝ ≠ 0
hn : n✝ ∈ S
b : B
hb : IsPrimitiveRoot b n✝
⊢ ∃ r, IsPrimitiveRoot r n✝
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
this : ¬SameRay ℝ (↑q) ζ
⊢ q - 1 < ‖↑q - ζ‖

Tactic:
convert! lt_norm_sub_of_not_sameRay this <;>
        simp only [hζ.norm'_eq_one hn.ne', Real.norm_of_nonneg hq.le, Complex.norm_real]

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

Goal state before:
pp: case e'_1
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))
HKη : K⟮η⟯ = K⟮η + 1⟯
H : K⟮η + 1⟯.toSubalgebra = K[η + 1]
hη' : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
⊢ {p ^ (k - s + 1)} = {p ^ (k + 1 - s)}

Tactic:
Nat.sub_add_comm hs

Goal state after:
case e'_1
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))
HKη : K⟮η⟯ = K⟮η + 1⟯
H : K⟮η + 1⟯.toSubalgebra = K[η + 1]
hη' : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
⊢ {p ^ (k - s + 1)} = {p ^ (k - s + 1)}
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case e'_4
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))
this : IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η⟯
⊢ p ^ (k - s + 1) = p ^ (k + 1 - s)

Tactic:
Nat.sub_add_comm hs

Goal state after:
case e'_4
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))
this : IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η⟯
⊢ p ^ (k - s + 1) = p ^ (k - s + 1)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

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

Tactic:
refine subset_adjoin ?_

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

Goal state before:
pp: case pos
p : ℕ
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hpri : Fact (Nat.Prime p)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
hs : s = k
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hcycl : IsCyclotomicExtension {2 ^ (k + 1)} K L
k₁ : ℕ
hk₁ : k = k₁.succ
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = ↑2 ^ 2 ^ k

Tactic:
rw [hζ.norm_pow_sub_one_two hirr, hk₁, _root_.pow_succ', pow_mul, neg_eq_neg_one_mul,
      mul_pow, neg_one_sq, one_mul, ← pow_mul, ← _root_.pow_succ']

Goal state after:
case pos
p : ℕ
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hpri : Fact (Nat.Prime p)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
hs : s = k
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hcycl : IsCyclotomicExtension {2 ^ (k + 1)} K L
k₁ : ℕ
hk₁ : k = k₁.succ
⊢ 2 ^ 2 ^ (k₁ + 1) = ↑2 ^ 2 ^ (k₁ + 1)
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'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
⊢ CharP (ZMod p) p

Tactic:
exact ZMod.charP p

Goal state after:
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'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst✝¹ : Algebra (ZMod p) K
inst✝ : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this : CharP K p
⊢ CharP (ZMod p) p

Tactic:
exact ZMod.charP p

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

Goal state before:
pp: case right.inv
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 x : AlgebraicClosure K
hx : x ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
ihx : f x ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
⊢ f x⁻¹ ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
rw [map_inv₀]

Goal state after:
case right.inv
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 x : AlgebraicClosure K
hx : x ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
ihx : f x ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
⊢ (f x)⁻¹ ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
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'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hpp' : p = p'
this✝ : Fact (Nat.Prime p)
this : Algebra (ZMod p) K := ZMod.algebra K p
⊢ K ≃+* K'

Tactic:
letI : Algebra (ZMod p) K' := ZMod.algebra _ _

Goal state after:
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'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hpp' : p = p'
this✝¹ : Fact (Nat.Prime p)
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) K' := ZMod.algebra K' p
⊢ K ≃+* K'
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
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✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x : CyclotomicField n K
hx : x ∈ adjoin A {b | b ^ n = 1}
y : CyclotomicField n K
hy : y ∈ {b | b ^ n = 1}
⊢ ⟨y, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
refine subset_adjoin ?_

Goal state after:
case refine_1
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✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x : CyclotomicField n K
hx : x ∈ adjoin A {b | b ^ n = 1}
y : CyclotomicField n K
hy : y ∈ {b | b ^ n = 1}
⊢ ⟨y, ⋯⟩ ∈ {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : (χ ^ n) ↑a = χ ↑a ^ n
⊢ (χ ^ n * χ) ↑a = χ ↑a ^ n * χ ↑a

Tactic:
mul_apply,

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : (χ ^ n) ↑a = χ ↑a ^ n
⊢ (χ ^ n) ↑a * χ ↑a = χ ↑a ^ n * χ ↑a
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero n
ψ : DirichletCharacter R m
h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ
x : (ZMod n)ˣ
hx : ↑(↑x).val = ↑1
⊢ (↑x).val ≡ 1 [MOD n.gcd m]

Tactic:
ZMod.natCast_eq_natCast_iff

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero n
ψ : DirichletCharacter R m
h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ
x : (ZMod n)ˣ
hx : (↑x).val ≡ 1 [MOD n.gcd m]
⊢ (↑x).val ≡ 1 [MOD n.gcd m]
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
n : ℕ
hχ : χ ^ n = 1
a : F
ha : a ≠ 0
⊢ ∃ ζ ∈ rootsOfUnity n R, ↑ζ = χ a

Tactic:
obtain ⟨μ, hμ₁, hμ₂⟩ := χ.apply_mem_rootsOfUnity_orderOf ha
  exact ⟨μ, rootsOfUnity_le_of_dvd (orderOf_dvd_of_pow_eq_one hχ) hμ₁, hμ₂⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ ((χ ^ (-1)) ^ (-1)).conductor ∣ (χ ^ (-1)).conductor

Tactic:
exact conductor_zpow_dvd ..

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
hn : NeZero n
h : χ.conductor.lcm ψ.conductor ∣ n
⊢ (χ * ψ).conductor ∣ χ.conductor.lcm ψ.conductor

Tactic:
rw [← mem_conductorSet_iff_conductor_dvd _ h, mem_conductorSet_iff]

Goal state after:
case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
hn : NeZero n
h : χ.conductor.lcm ψ.conductor ∣ n
⊢ (χ * ψ).FactorsThrough (χ.conductor.lcm ψ.conductor)
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case inl
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'
b : R
hb : b = 0
⊢ ∑ a, χ (a * b⁻¹) * ψ (a - b) = ∑ c, χ c * ψ (b * (c - 1))

pp: case inr
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'
b : R
hb : b ≠ 0
⊢ ∑ a, χ (a * b⁻¹) * ψ (a - b) = ∑ c, χ c * ψ (b * (c - 1))

Tactic:
· -- case `b = 0`
    simp only [hb, inv_zero, mul_zero, MulChar.map_zero, zero_mul,
      Finset.sum_const_zero, map_zero_eq_one, mul_one, χ.sum_eq_zero_of_ne_one hχ]

Goal state after:
case inr
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'
b : R
hb : b ≠ 0
⊢ ∑ a, χ (a * b⁻¹) * ψ (a - b) = ∑ c, χ c * ψ (b * (c - 1))
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Function.Even (𝓕 Φ) ↔ Function.Even Φ

Tactic:
have h {f : ZMod N → ℂ} (hf : f.Even) : (𝓕 f).Even := by
    simp only [Function.Even, ← congr_fun (dft_comp_neg f), funext hf, implies_true]

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
h : ∀ {f : ZMod N → ℂ}, Function.Even f → Function.Even (𝓕 f)
⊢ Function.Even (𝓕 Φ) ↔ Function.Even Φ
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
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
⊢ LinearMap.lTensor E ((innerₛₗ 𝕜) (e.symm 1)) ∘ₗ adjoint (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) =
    (TensorProduct.mk 𝕜 E 𝕜).flip 1

Tactic:
by
    rw [← adjoint_toSpanSingleton, ← adjoint_lTensor, ← adjoint_comp, ← toLinearMap_symm_rid,
      ← comm_trans_lid, ← toLinearEquiv_commIsometry, ← toLinearEquiv_lidIsometry,
      ← toLinearEquiv_trans, ← toLinearEquiv_symm, ← adjoint_toLinearMap_eq_symm]
    congr 1; ext; simp

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
f₁ f₂ : E →ₗ[𝕜] E
h₁ : (f₂ - f₁).IsPositive
h₂ : (f₁ - f₂).IsPositive
x : E
hba2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← h₂.isSymmetric.coe_re_inner_apply_self, RCLike.ofReal_eq_zero]

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
f₁ f₂ : E →ₗ[𝕜] E
h₁ : (f₂ - f₁).IsPositive
h₂ : (f₁ - f₂).IsPositive
x : E
hba2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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)⁻¹
hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p
v : (ι → ℝ) → F := u ∘ ⇑e.symm
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ (‖↑e.symm‖ₑ * ∫⁻ (y : ι → ℝ), ‖fderiv ℝ u (e.symm y)‖ₑ) ^ p =
    ↑(‖↑e.symm‖₊ ^ p) * (∫⁻ (y : ι → ℝ), ‖fderiv ℝ u (e.symm y)‖ₑ) ^ p

Tactic:
by
        rw [ENNReal.mul_rpow_of_nonneg _ _ h0p, enorm_eq_nnnorm, ← ENNReal.coe_rpow_of_nonneg _ h0p]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: d : ℕ
h0 : volume.addHaarScalarFactor μH[↑d] = 0
h : volume = volume.addHaarScalarFactor μH[↑d] • μH[↑d]
⊢ False

Tactic:
obtain h := congr($h (parallelepiped (stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin d)))))

Goal state after:
d : ℕ
h0 : volume.addHaarScalarFactor μH[↑d] = 0
h✝ : volume = volume.addHaarScalarFactor μH[↑d] • μH[↑d]
h :
  volume (parallelepiped ⇑(stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin d)))) =
    (volume.addHaarScalarFactor μH[↑d] • μH[↑d]) (parallelepiped ⇑(stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin d))))
⊢ False
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
⊢ dimH (Metric.ball x r) = ↑(Fintype.card ι)

Tactic:
by
  cases isEmpty_or_nonempty ι
  · rwa [dimH_subsingleton, eq_comm, Nat.cast_eq_zero, Fintype.card_eq_zero_iff]
    exact fun x _ y _ => Subsingleton.elim x y
  · rw [← ENNReal.coe_natCast]
    have : μH[Fintype.card ι] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι) := by
      rw [hausdorffMeasure_pi_real, Real.volume_pi_ball _ hr]
    refine dimH_of_hausdorffMeasure_ne_zero_ne_top ?_ ?_ <;> rw [NNReal.coe_natCast, this]
    · simp [pow_pos (mul_pos (zero_lt_two' ℝ) hr)]
    · exact ENNReal.ofReal_ne_top

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
⊢ ∀ (b : OuterMeasure X), (∀ (i : ℝ≥0∞), ⨆ (_ : i > 0), ⊤ ≤ b) → ⊤ ≤ b

Tactic:
intro b

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
b : OuterMeasure X
⊢ (∀ (i : ℝ≥0∞), ⨆ (_ : i > 0), ⊤ ≤ b) → ⊤ ≤ b
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
⊢ dimH s = ↑(finrank ℝ ↥(vectorSpan ℝ s))

Tactic:
have := hne.to_subtype

Goal state after:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
this : Nonempty ↑s
⊢ dimH s = ↑(finrank ℝ ↥(vectorSpan ℝ s))
Module: Mathlib.Analysis.InnerProductSpace.StarOrder

Goal state before:
pp: 𝕜 : Type u_1
H : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : CompleteSpace H
inst✝¹ : Algebra ℝ (H →L[𝕜] H)
inst✝ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c✝ : ℝ
c : ℝ := -c✝
hc : 0 < c
x : H
⊢ ‖x‖ ^ 2 * c = re ⟪(c • 1) x, x⟫_𝕜

Tactic:
← algebraMap_smul 𝕜 c (1 : (H →L[𝕜] H)),

Goal state after:
𝕜 : Type u_1
H : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : CompleteSpace H
inst✝¹ : Algebra ℝ (H →L[𝕜] H)
inst✝ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c✝ : ℝ
c : ℝ := -c✝
hc : 0 < c
x : H
⊢ ‖x‖ ^ 2 * c = re ⟪((algebraMap ℝ 𝕜) c • 1) x, x⟫_𝕜
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℂ H
S : StandardSubspace H
⊢ S.toClosedSubmodule.mulI ⊓ S.toClosedSubmodule.mulI.mulI = ⊥

Tactic:
by simpa [mulI_mulI_eq, inf_comm] using S.IsSeparating

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
⊢ (trace 𝕜 E) T = ∑ i, ⟪b i, T (b i)⟫_𝕜

Tactic:
classical
  rw [LinearMap.trace_eq_matrix_trace 𝕜 b.toBasis T]
  apply Fintype.sum_congr
  intro i
  rw [Matrix.diag_apply, T.toMatrix_apply, b.coe_toBasis, b.coe_toBasis_repr_apply,
    b.repr_apply_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case a.d
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹⁰ : EMetricSpace X
inst✝⁹ : EMetricSpace Y
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
| ↑(finrank ℝ E)

Tactic:
← Fintype.card_fin (finrank ℝ E)

Goal state after:
case a.d
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹⁰ : EMetricSpace X
inst✝⁹ : EMetricSpace Y
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
| ↑(Fintype.card (Fin (finrank ℝ E)))