mathlib-initiative/mathlib-tactics huggingface dataset:
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 A B
⊢ adjoin A {b | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1} = ⊤

Tactic:
· refine _root_.eq_top_iff.2 ?_
    rw [← ((iff_adjoin_eq_top S A B).1 H).2]
    refine adjoin_mono fun x hx ↦ ?_
    simp only [union_singleton, mem_insert_iff, mem_ofPred_eq] at hx ⊢
    obtain ⟨m, hm, hm'⟩ := hx
    exact ⟨m, ⟨Or.inr hm, hm'⟩⟩

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

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝² : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝¹ : FiniteDimensional K L := finiteDimensional {n} K L
this✝ : IsGalois K L := isGalois {n} K L
Hprod : ∏ σ, (1 - σ ζ) = eval 1 (cyclotomic' n E)
this : NeZero ↑n
⊢ eval 1 (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) = ↑(eval 1 (cyclotomic n ℤ))

Tactic:
← Int.cast_one,

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝² : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝¹ : FiniteDimensional K L := finiteDimensional {n} K L
this✝ : IsGalois K L := isGalois {n} K L
Hprod : ∏ σ, (1 - σ ζ) = eval 1 (cyclotomic' n E)
this : NeZero ↑n
⊢ eval (↑1) (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) = ↑(eval 1 (cyclotomic n ℤ))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case e'_6
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : IsPrimitiveRoot ζ' n
⊢ 1 = ‖ζ'‖

Tactic:
rw [hζ'.norm'_eq_one hn.ne']

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

Goal state before:
pp: case refine_1
n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ {b | n ≠ 0 ∧ b ^ n = 1}.Finite

Tactic:
have : {b : B | n ≠ 0 ∧ b ^ n = 1} = (nthRoots n (1 : B)).toFinset :=
      Set.ext fun x ↦ ⟨fun h ↦ by simpa [n.pos_of_neZero] using h.2,
        fun h ↦ by simpa [n.pos_of_neZero, NeZero.ne n] using h⟩

Goal state after:
case refine_1
n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
this : {b | n ≠ 0 ∧ b ^ n = 1} = ↑(nthRoots n 1).toFinset
⊢ {b | n ≠ 0 ∧ b ^ n = 1}.Finite
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ Module.Finite A B

Tactic:
classical
  rw [Module.finite_def, ← top_toSubmodule, ← ((iff_adjoin_eq_top _ _ _).1 h).2]
  refine fg_adjoin_of_finite ?_ fun b ⟨n, hb⟩ => ?_
  · simp only [mem_singleton_iff, exists_eq_left]
    have : {b : B | n ≠ 0 ∧ b ^ n = 1} = (nthRoots n (1 : B)).toFinset :=
      Set.ext fun x ↦ ⟨fun h ↦ by simpa [n.pos_of_neZero] using h.2,
        fun h ↦ by simpa [n.pos_of_neZero, NeZero.ne n] using h⟩
    rw [this]
    exact (nthRoots n 1).toFinset.finite_toSet
  · simp only [mem_singleton_iff] at hb
    exact ⟨X ^ n - 1,
      ⟨monic_X_pow_sub_C _ (hb.1 ▸ NeZero.ne _), by simpa [sub_eq_zero] using hb.2.2⟩⟩

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 : NumberField K
inst✝¹ : Finite ↑S
inst✝ : IsCyclotomicExtension S K L
⊢ FiniteDimensional ℚ L

Tactic:
by
      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.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
he : ∃ x, ∃ (_ : x ≠ 0), ¬e.mulShift x ≠ 1
⊢ ∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1

Tactic:
not_ne_iff

Goal state after:
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
he : ∃ x, ∃ (_ : x ≠ 0), e.mulShift x = 1
⊢ ∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

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

Tactic:
convert! IntermediateField.algebraMap_mem _ x
    exact AlgHom.commutes _ x

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

Goal state before:
pp: case neg
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)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
hk : k ≠ 0
htwo : ¬p ^ (k - s + 1) = 2
⊢ (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s

Tactic:
exact hζ.norm_pow_sub_one_of_prime_pow_ne_two hirr hs htwo

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' ⋯
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : AddChar F (CyclotomicField (↑ψ.n) F') := ψ.char.compAddMonoidHom (Algebra.trace (ZMod p) F).toAddMonoidHom
a : F
ha : (Algebra.trace (ZMod (ringChar F)) F) (1 * a) ≠ 0
⊢ ψ' ≠ 1

Tactic:
one_mul

Goal state after:
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' ⋯
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : AddChar F (CyclotomicField (↑ψ.n) F') := ψ.char.compAddMonoidHom (Algebra.trace (ZMod p) F).toAddMonoidHom
a : F
ha : (Algebra.trace (ZMod (ringChar F)) F) a ≠ 0
⊢ ψ' ≠ 1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case right.mul
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 y : AlgebraicClosure K
hx : x ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
hy : y ∈ 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}
ihy : f y ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
⊢ f (x * y) ∈ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
rw [map_mul]
    exact mul_mem ihx ihy

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
hn : n % 4 = 1
⊢ χ₄ ↑n = 1

Tactic:
rw [χ₄_int_mod_four, hn]
  rfl

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
hn : n % 4 = 3
⊢ χ₄ ↑n = -1

Tactic:
rw [χ₄_int_mod_four, hn]
  rfl

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
a : R
ha : ¬IsUnit a
⊢ 0 = χ' a

Tactic:
map_nonunit χ' ha

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
a : R
ha : ¬IsUnit a
⊢ 0 = 0
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: case refine_2
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 ∈ (ZMod.unitsMap ⋯).ker
z : ℕ
hz₁ : ↑z = ↑x
hz₂ : ↑z = 1
⊢ z.Coprime m

Tactic:
· exact (ZMod.isUnit_iff_coprime _ _).mp <| hz₂ ▸ isUnit_one

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
⊢ 1 * χ = χ

Tactic:
one_mul

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
⊢ χ = χ
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension S A ↥C₁
h₂ : IsCyclotomicExtension S A ↥C₂
hC : ∀ n ∈ S, n ≠ 0 → ∃ x, IsPrimitiveRoot x n
⊢ C₁ = C₂

Tactic:
(isCyclotomicExtension_iff_eq_adjoin S C₁ hC).mp h₁,

Goal state after:
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension S A ↥C₁
h₂ : IsCyclotomicExtension S A ↥C₂
hC : ∀ n ∈ S, n ≠ 0 → ∃ x, IsPrimitiveRoot x n
⊢ adjoin A {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = C₂
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

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

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

Tactic:
hψ

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

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

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
u : (ZMod N)ˣ
hu : ↑↑(↑u).val = 1
this : (ZMod.castHom hd (ZMod d)) ↑u = ↑↑(↑u).val
⊢ ↑d ∣ ↑(↑u).val - 1

Tactic:
← Int.cast_one,

Goal state after:
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
u : (ZMod N)ˣ
hu : ↑↑(↑u).val = ↑1
this : (ZMod.castHom hd (ZMod d)) ↑u = ↑↑(↑u).val
⊢ ↑d ∣ ↑(↑u).val - 1
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
m : ℕ
χ : DirichletCharacter S m
hχ : χ.Even
x✝ : ZMod m
⊢ 1 * χ x✝ = χ x✝

Tactic:
one_mul

Goal state after:
S : Type u_2
inst✝ : CommRing S
m : ℕ
χ : DirichletCharacter S m
hχ : χ.Even
x✝ : ZMod m
⊢ χ x✝ = χ x✝
Module: Mathlib.NumberTheory.Cyclotomic.Basic

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

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

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ (ψ.mulShift ↑hp.unit) = 1 * gaussSum χ (ψ.mulShift ↑hp.unit)

Tactic:
one_mul

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ (ψ.mulShift ↑hp.unit) = gaussSum χ (ψ.mulShift ↑hp.unit)
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case zero
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ ψ = 1 * gaussSum χ ψ

Tactic:
one_mul

Goal state after:
case zero
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ ψ = gaussSum χ ψ
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : 0 ^ 2 = χ (-1) * ↑(Fintype.card R)
hf : gaussSum χ ψ = 0
⊢ False

Tactic:
zero_pow two_ne_zero,

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : 0 = χ (-1) * ↑(Fintype.card R)
hf : gaussSum χ ψ = 0
⊢ False
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)
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))

Tactic:
have hχ : χ (-1) = 1 := Int.cast_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
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Preorder β
f : Finset α → β
⊢ Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s ≤ f (cons a s ha)

Tactic:
classical simp [monotone_iff_forall_covBy, covBy_iff_exists_cons]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case e'_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)
⊢ 2 ^ (Fintype.card F / 2) = 1 * 2 ^ (Fintype.card F / 2)

Tactic:
one_mul

Goal state after:
case e'_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)
⊢ 2 ^ (Fintype.card F / 2) = 2 ^ (Fintype.card F / 2)
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
T : E →L[𝕜] E
⊢ T.IsPositive ↔ IsSelfAdjoint T ∧ ∀ (x : E), 0 ≤ ⟪T x, x⟫

Tactic:
simp [isSelfAdjoint_iff_isSymmetric, isPositive_iff]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
inst✝ : U.HasOrthogonalProjection
⊢ (∀ (x y : E), True) ∧ ∀ (x : E), 0 ≤ ⟪↑U.starProjection x, ↑T (↑U.starProjection x)⟫

Tactic:
coe_coe,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
inst✝ : U.HasOrthogonalProjection
⊢ (∀ (x y : E), True) ∧ ∀ (x : E), 0 ≤ ⟪U.starProjection x, T (U.starProjection x)⟫
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 →L[𝕜] E
hT : T.IsPositive
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
⊢ (∀ (x y : ↥U), True) ∧ ∀ (x : ↥U), 0 ≤ ⟪↑x, ↑T ↑x⟫

Tactic:
coe_coe,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
⊢ (∀ (x y : ↥U), True) ∧ ∀ (x : ↥U), 0 ≤ ⟪↑x, T ↑x⟫
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
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂Measure.map (⇑e.symm) volume = ∫⁻ (y : ι → ℝ), ‖v y‖ₑ ^ p

Tactic:
refine lintegral_map ?_ e.symm.continuous.measurable

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)⁻¹
hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p
v : (ι → ℝ) → F := u ∘ ⇑e.symm
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ Measurable fun x ↦ ‖u x‖ₑ ^ p
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
⊢ (∫⁻ (y : ι → ℝ), ‖fderiv ℝ v y‖ₑ) ^ p = (∫⁻ (y : ι → ℝ), ‖fderiv ℝ u (e.symm y) ∘SL fderiv ℝ (⇑e.symm) y‖ₑ) ^ p

Tactic:
congr! with y
        apply fderiv_comp _ (hu.differentiable one_ne_zero _)
        exact e.symm.differentiableAt

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

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

Tactic:
rw [← h, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩, sub_self]

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
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
⊢ ∀ x ∈ T.graph.adjoint, x.1 = 0 → x.2 = 0

Tactic:
intro x hx hx'

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
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
x : F × E
hx : x ∈ T.graph.adjoint
hx' : x.1 = 0
⊢ x.2 = 0