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

Goal state before:
pp: p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
⊢ (expand R p) (cyclotomic n R) = cyclotomic (n * p) R * cyclotomic n R

Tactic:
rcases Nat.eq_zero_or_pos n with (rfl | hnpos)
  · simp
  have := NeZero.of_pos hnpos
  suffices expand ℤ p (cyclotomic n ℤ) = cyclotomic (n * p) ℤ * cyclotomic n ℤ by
    rw [← map_cyclotomic_int, ← map_expand, this, Polynomial.map_mul, map_cyclotomic_int,
      map_cyclotomic]
  refine eq_of_monic_of_dvd_of_natDegree_le ((cyclotomic.monic _ ℤ).mul (cyclotomic.monic _ ℤ))
    ((cyclotomic.monic n ℤ).expand hp.pos) ?_ ?_
  · refine (IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast _ _
      ((cyclotomic.isPrimitive (n * p) ℤ).mul (cyclotomic.isPrimitive n ℤ))).2 ?_
    rw [Polynomial.map_mul, map_cyclotomic_int, map_cyclotomic_int, map_expand, map_cyclotomic_int]
    refine IsCoprime.mul_dvd (cyclotomic.isCoprime_rat fun h => ?_) ?_ ?_
    · replace h : n * p = n * 1 := by simp [h]
      exact Nat.Prime.ne_one hp (mul_left_cancel₀ hnpos.ne' h)
    · have hpos : 0 < n * p := mul_pos hnpos hp.pos
      have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne'
      rw [cyclotomic_eq_minpoly_rat hprim hpos]
      refine minpoly.dvd ℚ _ ?_
      rw [← eval_map_algebraMap, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def,
        @isRoot_cyclotomic_iff]
      convert! IsPrimitiveRoot.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n)
      rw [Nat.mul_div_cancel _ (Nat.Prime.pos hp)]
    · have hprim := Complex.isPrimitiveRoot_exp _ hnpos.ne.symm
      rw [cyclotomic_eq_minpoly_rat hprim hnpos]
      refine minpoly.dvd ℚ _ ?_
      rw [← eval_map_algebraMap, map_expand, expand_eval, ← IsRoot.def, ←
        cyclotomic_eq_minpoly_rat hprim hnpos, map_cyclotomic, @isRoot_cyclotomic_iff]
      exact IsPrimitiveRoot.pow_of_prime hprim hp hdiv
  · rw [natDegree_expand, natDegree_cyclotomic,
      natDegree_mul (cyclotomic_ne_zero _ ℤ) (cyclotomic_ne_zero _ ℤ), natDegree_cyclotomic,
      natDegree_cyclotomic, mul_comm n,
      Nat.totient_mul ((Nat.Prime.coprime_iff_not_dvd hp).2 hdiv), Nat.totient_prime hp,
      mul_comm (p - 1), ← Nat.mul_succ, Nat.sub_one, Nat.succ_pred_eq_of_pos hp.pos]

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

Goal state before:
pp: case inr.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ (aeval (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p)))) ((expand ℤ p) (cyclotomic n ℤ)) = 0

Tactic:
rw [← eval_map_algebraMap, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def,
      @isRoot_cyclotomic_iff]

Goal state after:
case inr.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p)) ^ p) n
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
⊢ Module.finrank (ZMod p) (GaloisField p n) = n

Tactic:
have : Fintype (GaloisField p n) := Fintype.ofFinite (GaloisField p n)

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
⊢ Module.finrank (ZMod p) (GaloisField p n) = n
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2.inl
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hn : n ∈ S ∧ n ≠ 0 ∧ x ^ n = 1
⊢ x ∈ {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}

pp: case refine_2.inr
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hn : n ∈ T ∧ n ≠ 0 ∧ x ^ n = 1
⊢ x ∈ {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}

Tactic:
· exact ⟨n, Or.inl hn.1, hn.2⟩

Goal state after:
case refine_2.inr
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hn : n ∈ T ∧ n ≠ 0 ∧ x ^ n = 1
⊢ x ∈ {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case neg
n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
h1 : 2 ≤ n
⊢ (Algebra.norm K) ζ = 1

Tactic:
← hζ.powerBasis_gen K,

Goal state after:
case neg
n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
h1 : 2 ≤ n
⊢ (Algebra.norm K) (IsPrimitiveRoot.powerBasis K hζ).gen = 1
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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)

Tactic:
have : ¬eval (↑q) (cyclotomic n ℂ) = 0 := by simpa using (cyclotomic_pos' n hq').ne'

Goal state after:
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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this : ¬eval (↑q) (cyclotomic n ℂ) = 0
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case empty
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension ∅ A B
⊢ Module.Finite A B

Tactic:
refine Module.finite_def.2 ⟨({1} : Finset B), ?_⟩

Goal state after:
case empty
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension ∅ A B
⊢ Submodule.span A ↑{1} = ⊤
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ ↑((q - 1) ^ φ n) < ↑(eval (↑q) (cyclotomic n ℤ)).natAbs

Tactic:
Nat.cast_pow,

Goal state after:
case inr
n q : ℕ
hn' : 1 < n
hq : q ≠ 1
hq' : 1 < q
⊢ ↑(q - 1) ^ φ n < ↑(eval (↑q) (cyclotomic n ℤ)).natAbs
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
a b : R
h : ψ.mulShift (a + -b) = 1
⊢ a = b

Tactic:
simpa [← sub_eq_add_neg, sub_eq_zero] using (hψ · h)

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

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
b : Module.Basis (↥(IsNoetherian.finsetBasisIndex (ZMod p) (GaloisField p n))) (ZMod p) (GaloisField p n) :=
  IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)
⊢ Nat.card (GaloisField p n) = p ^ n

Tactic:
have : Fintype (GaloisField p n) := Fintype.ofFinite (GaloisField p n)

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
b : Module.Basis (↥(IsNoetherian.finsetBasisIndex (ZMod p) (GaloisField p n))) (ZMod p) (GaloisField p n) :=
  IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)
this : Fintype (GaloisField p n)
⊢ Nat.card (GaloisField p n) = p ^ n
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
h₁ : ψ 1 = 1
a : ZMod n
ha₁ : a = a.val • 1
⊢ ψ (a.val • 1) = 1

Tactic:
map_nsmul_eq_pow,

Goal state after:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ψ : AddChar (ZMod n) C
h₁ : ψ 1 = 1
a : ZMod n
ha₁ : a = a.val • 1
⊢ ψ 1 ^ a.val = 1
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
⊢ ∑ a, ψ a = 0

Tactic:
rcases ne_one_iff.1 hψ with ⟨b, hb⟩

Goal state after:
R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
⊢ ∑ a, ψ a = 0
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
this : Finite K
⊢ Nat.card ↥(Units.map (Algebra.norm K)).ker ≤ (Nat.card K' - 1) / (Nat.card K - 1)

Tactic:
classical
    have := Fintype.ofFinite K'ˣ
    convert!
      IsCyclic.card_pow_eq_one_le (α := K'ˣ) <|
        Nat.div_pos
            (Nat.sub_le_sub_right (Nat.card_le_card_of_injective _ (algebraMap K K').injective)
              _) <|
          Nat.sub_pos_of_lt Finite.one_lt_card
    rw [← Set.ncard_coe_finset, ← SetLike.coe_sort_coe, Nat.card_coe_set_eq]; congr 1; ext
    simp [Units.ext_iff, ← (algebraMap K K').injective.eq_iff, algebraMap_norm_eq_pow]

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

Goal state before:
pp: case refine_2
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✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this✝¹ : NeZero ↑n
k : K
this✝ : ∀ (z : K), ∃ x, z * (algebraMap A K) ↑x.2 = (algebraMap A K) x.1
z : A
w : ↥(nonZeroDivisors A)
hw : k * (algebraMap A K) ↑(z, w).2 = (algebraMap A K) (z, w).1
this : IsScalarTower A K (CyclotomicField n K) := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ (algebraMap K (CyclotomicField n K)) ((algebraMap A K) (z, w).1) = (algebraMap A (CyclotomicField n K)) z

Tactic:
← IsScalarTower.algebraMap_apply

Goal state after:
case refine_2
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✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this✝¹ : NeZero ↑n
k : K
this✝ : ∀ (z : K), ∃ x, z * (algebraMap A K) ↑x.2 = (algebraMap A K) x.1
z : A
w : ↥(nonZeroDivisors A)
hw : k * (algebraMap A K) ↑(z, w).2 = (algebraMap A K) (z, w).1
this : IsScalarTower A K (CyclotomicField n K) := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ (algebraMap A (CyclotomicField n K)) (z, w).1 = (algebraMap A (CyclotomicField n K)) z
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
⊢ ∀ (x y : R), (if IsUnit (x * y) then 1 else 0) = (if IsUnit x then 1 else 0) * if IsUnit y then 1 else 0

Tactic:
intro x y
    classical
      simp only [IsUnit.mul_iff, boole_mul]
      split_ifs <;> tauto

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommMonoid R
R' : Type u_2
inst✝³ : CommMonoidWithZero R'
S : Type u_3
inst✝² : SetLike S R
inst✝¹ : SubmonoidClass S R
T : S
R'' : Type u_4
inst✝ : CommMonoidWithZero R''
x : (↥T)ˣ
⊢ (if IsUnit ↑x then 1 ↑↑x else 0) = 1 ↑x

Tactic:
if_pos x.isUnit,

Goal state after:
R : Type u_1
inst✝⁴ : CommMonoid R
R' : Type u_2
inst✝³ : CommMonoidWithZero R'
S : Type u_3
inst✝² : SetLike S R
inst✝¹ : SubmonoidClass S R
T : S
R'' : Type u_4
inst✝ : CommMonoidWithZero R''
x : (↥T)ˣ
⊢ 1 ↑↑x = 1 ↑x
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
⊢ orderOf χ ∣ Fintype.card F - 1

Tactic:
classical
  rw [← Fintype.card_units]
  exact orderOf_dvd_of_pow_eq_one χ.pow_card_eq_one

Goal state after:
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 ∈ (ZMod.unitsMap ⋯).ker
z : ℕ
hz₁ : ↑z = ↑x
hz₂ : ↑z = 1
hz₀ : z.gcd (n * m) = 1
this✝ : ((changeLevel ⋯) χ) ↑z = χ ↑z
this : ((changeLevel ⋯) ψ) ↑z = ψ ↑z
⊢ ψ ↑z = 1

Tactic:
hz₂,

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 ∈ (ZMod.unitsMap ⋯).ker
z : ℕ
hz₁ : ↑z = ↑x
hz₂ : ↑z = 1
hz₀ : z.gcd (n * m) = 1
this✝ : ((changeLevel ⋯) χ) ↑z = χ ↑z
this : ((changeLevel ⋯) ψ) ↑z = ψ ↑z
⊢ ψ 1 = 1
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ ‖x‖ ^ 2 ≠ 0 ∨ 1 ≤ p / 2

Tactic:
simp [hx]

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

Goal state before:
pp: α : Type u_1
⊢ ∀ ⦃x : Set α⦄,
    x ∈ Set.range SetLike.coe → ∀ ⦃y : Set α⦄, y ∈ Set.range SetLike.coe → Set.Icc x y ⊆ Set.range SetLike.coe

Tactic:
rintro _ _ _ ⟨s, rfl⟩ t ht; exact ⟨_, (s.finite_toSet.subset ht.2).coe_toFinset⟩

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Filter.Tendsto (fderiv ℝ fun x ↦ ‖x‖ ^ p) (𝓝 0) (𝓝 ((p * ‖0‖ ^ (p - 2)) • (innerSL ℝ) 0))

Tactic:
norm_zero,

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ Filter.Tendsto (fderiv ℝ fun x ↦ ‖x‖ ^ p) (𝓝 0) (𝓝 ((p * 0 ^ (p - 2)) • (innerSL ℝ) 0))
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : ¬x = 0
⊢ ContinuousAt (fderiv ℝ fun x ↦ ‖x‖ ^ p) x

Tactic:
simp_rw [funext fun x ↦ fderiv_norm_rpow (E := E) (x := x) hp]

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : ¬x = 0
⊢ ContinuousAt (fun x ↦ (p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: case funProp.discharger
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : ¬x = 0
⊢ ‖x‖ ≠ 0 ∨ 0 ≤ p - 2

Tactic:
simp [hx]

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

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : ¬x = 0
⊢ ContinuousAt (fderiv ℝ fun x ↦ ‖x‖ ^ p) x

Tactic:
simp_rw [funext fun x ↦ fderiv_norm_rpow (E := E) (x := x) hp]
    fun_prop (discharger := simp [hx])

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
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 : (χ (-1) * ↑8) ^ (ringChar FF ^ ↑n / 2) = χ (↑(ringChar FF) ^ ↑n)
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))

Tactic:
← hchar,

Goal state after:
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
h₁ : (fun a ↦ ↑(χ₈ a) * τ ^ ↑a) = fun a ↦ χ a * ψ₈char a
hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3)
hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * ↑(Fintype.card (ZMod 8))
h : (χ (-1) * ↑8) ^ (ringChar F ^ ↑n / 2) = χ (↑(ringChar F) ^ ↑n)
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card 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
T : E →ₗ[𝕜] E
⊢ T.IsPositive ↔ T.IsSymmetric ∧ ∀ (x : E), 0 ≤ ⟪T x, x⟫

Tactic:
simp_rw [IsPositive, and_congr_right_iff, ← RCLike.ofReal_nonneg (K := 𝕜)]
  intro hT
  simp [hT]

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
T : E →ₗ[𝕜] E
hT : T.IsPositive
c : 𝕜
hc : 0 ≤ c
hc' : (starRingEnd 𝕜) c = c
x : E
⊢ 0 ≤ re ⟪(c • T) x, x⟫

Tactic:
rw [smul_apply, inner_smul_left, hc', mul_re, conj_eq_iff_im.mp hc', zero_mul, sub_zero]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsPositive
c : 𝕜
hc : 0 ≤ c
hc' : (starRingEnd 𝕜) c = c
x : E
⊢ 0 ≤ re c * re ⟪T x, x⟫
Module: Mathlib.Analysis.InnerProductSpace.ExteriorPower

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ innerProductForm.flip = innerProductForm

Tactic:
apply linearMap_ext

Goal state after:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ innerProductForm.flip.compAlternatingMap (ιMulti ℝ n) = innerProductForm.compAlternatingMap (ιMulti ℝ n)
Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H : ∀ a_1 ∈ (T a).eigenspace (f a), ∀ a_2 ∈ (T a).eigenspace (g a), inner 𝕜 a_1 a_2 = 0
⊢ inner 𝕜 (((fun γ ↦ (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) f) Ef)
      (((fun γ ↦ (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) g) Eg) =
    0

Tactic:
apply H

Goal state after:
case b
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H : ∀ a_1 ∈ (T a).eigenspace (f a), ∀ a_2 ∈ (T a).eigenspace (g a), inner 𝕜 a_1 a_2 = 0
⊢ ((fun γ ↦ (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) f) Ef ∈ (T a).eigenspace (f a)

case b
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H : ∀ a_1 ∈ (T a).eigenspace (f a), ∀ a_2 ∈ (T a).eigenspace (g a), inner 𝕜 a_1 a_2 = 0
⊢ ((fun γ ↦ (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) g) Eg ∈ (T a).eigenspace (g a)
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:
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
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)
⊢ 1 < ↑p * (↑n - 1) / (↑n - ↑p)

Tactic:
one_lt_div hnp,

Goal state after:
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)
⊢ ↑n - ↑p < ↑p * (↑n - 1)