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

Goal state before:
pp: case left
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ (∏ i ∈ n.properDivisors, cyclotomic i R) * cyclotomic n R = cyclotomic n R * ∏ i ∈ n.properDivisors, cyclotomic i R

Tactic:
mul_comm

Goal state after:
case left
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ cyclotomic n R * ∏ i ∈ n.properDivisors, cyclotomic i R = cyclotomic n R * ∏ i ∈ n.properDivisors, cyclotomic i R
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ n.properDivisors
⊢ (∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R) * (X ^ m - 1) =
    (X ^ m - 1) * ∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R

Tactic:
mul_comm

Goal state after:
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ n.properDivisors
⊢ (X ^ m - 1) * ∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R =
    (X ^ m - 1) * ∏ x ∈ n.properDivisors \ m.divisors, cyclotomic x R
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ k.properDivisors
d : ℕ
hd : k = i * d
⊢ cyclotomic i K = cyclotomic' i K

Tactic:
mul_comm

Goal state after:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
hpos : k > 0
i : ℕ
hi : i ∈ k.properDivisors
d : ℕ
hd : k = d * i
⊢ cyclotomic i K = cyclotomic' i K
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ (∏ i ∈ n.properDivisors, cyclotomic i R) * P = X ^ n - 1

Tactic:
mul_comm

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
Module: Mathlib.FieldTheory.Galois.Abelian

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Field M
inst✝³ : Algebra K M
inst✝² : Algebra L M
inst✝¹ : IsScalarTower K L M
inst✝ : IsAbelianGalois K M
this : IsGalois K L
x y : Gal(M/K)
⊢ (AlgEquiv.restrictNormalHom L) (x * y) = (AlgEquiv.restrictNormalHom L) (y * x)

Tactic:
mul_comm

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Field M
inst✝³ : Algebra K M
inst✝² : Algebra L M
inst✝¹ : IsScalarTower K L M
inst✝ : IsAbelianGalois K M
this : IsGalois K L
x y : Gal(M/K)
⊢ (AlgEquiv.restrictNormalHom L) (y * x) = (AlgEquiv.restrictNormalHom L) (y * x)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
⊢ X ^ (p ^ k * p) - 1 = X ^ (p ^ k * p) - 1

Tactic:
mul_comm

Goal state after:
R : Type u_1
inst✝ : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
⊢ X ^ (p * p ^ k) - 1 = X ^ (p * p ^ k) - 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
x : S
hx : IsIntegral K x
i : Fin (minpoly K x).natDegree
⊢ (powerBasisAux hx) i = ⟨x, ⋯⟩ ^ ↑i

Tactic:
by rw [adjoin.powerBasisAux, Basis.mk_apply]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case neg
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j ∈ Finset.range B.dim
⊢ IsIntegral R ((B.basis.repr (Q.coeff j • B.gen ^ j)) i)

Tactic:
replace hj := Finset.mem_range.1 hj

Goal state after:
case neg
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
⊢ IsIntegral R ((B.basis.repr (Q.coeff j • B.gen ^ j)) i)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ n.totient * p ≤ p * n.totient

Tactic:
mul_comm

Goal state after:
case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ p * n.totient ≤ p * n.totient
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case succ.succ.zero.left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
⊢ 1 < x → 0 < x + 1

Tactic:
intro

Goal state after:
case succ.succ.zero.left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
a✝ : 1 < x
⊢ 0 < x + 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case succ.succ.zero.right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
⊢ 1 ≤ x → 0 ≤ x + 1

Tactic:
intro

Goal state after:
case succ.succ.zero.right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
a✝ : 1 ≤ x
⊢ 0 ≤ x + 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case succ.succ.succ.left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
⊢ 1 < x → 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)

Tactic:
intro

Goal state after:
case succ.succ.succ.left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
a✝ : 1 < x
⊢ 0 < eval x (cyclotomic (n + 1 + 1 + 1) R)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case succ.succ.succ.right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
⊢ 1 ≤ x → 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R)

Tactic:
intro

Goal state after:
case succ.succ.succ.right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
a✝ : 1 ≤ x
⊢ 0 ≤ eval x (cyclotomic (n + 1 + 1 + 1) R)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    (∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)) *
      ↑p ^ padicValNat p n
⊢ False

Tactic:
mul_comm

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case inr
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : GCDMonoid.lcm l n = n * 2
ineq : φ n * φ r ≤ φ (GCDMonoid.lcm l n)
rpos : 0 < r
key : r = 2
⊢ l ∣ 2 * n

Tactic:
mul_comm

Goal state after:
case inr
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : GCDMonoid.lcm l n = 2 * n
ineq : φ n * φ r ≤ φ (GCDMonoid.lcm l n)
rpos : 0 < r
key : r = 2
⊢ l ∣ 2 * n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

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

Tactic:
rw [Complex.norm_real, Real.norm_of_nonneg hq.le]

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

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

Tactic:
rw [hζ, show 1 = algebraMap K L 1 by simp, Algebra.norm_algebraMap, one_pow]

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
⊢ (-1) ^ Fintype.card (L →ₐ[K] E) * ∏ x, (1 - x ζ) = (algebraMap K E) ↑(eval 1 (cyclotomic n ℤ))

Tactic:
AlgHom.card,

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
⊢ (-1) ^ Module.finrank K L * ∏ x, (1 - x ζ) = (algebraMap K E) ↑(eval 1 (cyclotomic n ℤ))
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: case refine_2
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
⊢ (e.mulShift ↑d).mulShift u = e.mulShift (u * ↑d)

Tactic:
mul_comm

Goal state after:
case refine_2
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
⊢ (e.mulShift ↑d).mulShift u = e.mulShift (↑d * u)
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : X ^ p ^ 1 = X ^ Fintype.card (ZMod p)
⊢ IsSplittingField (ZMod p) (ZMod p) (X ^ Fintype.card (ZMod p) - X)

Tactic:
infer_instance

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

Goal state before:
pp: 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

Tactic:
mul_comm

Goal state after:
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, ψ (b * x) = ↑0
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: 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✝ : NeZero ↑n
this✝¹ : NeZero ↑n
this✝ : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : (cyclotomic n K).degree ≠ 0
ζ : (cyclotomic n K).SplittingField
hζ : eval ζ (map (algebraMap K (cyclotomic n K).SplittingField) (cyclotomic n K)) = 0
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)

Tactic:
eval_map,

Goal state after:
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✝ : NeZero ↑n
this✝¹ : NeZero ↑n
this✝ : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : (cyclotomic n K).degree ≠ 0
ζ : (cyclotomic n K).SplittingField
hζ : eval₂ (algebraMap K (cyclotomic n K).SplittingField) ζ (cyclotomic n K) = 0
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: F : Type u_3
K : Type u_4
L : Type u_5
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Finite L
h : Module.finrank F K ∣ Module.finrank F L
⊢ Nonempty (K →ₐ[F] L)

Tactic:
by
  have := Finite.of_injective _ (algebraMap F L).injective
  have := Fintype.ofFinite F
  have := Module.finite_of_finrank_pos (Nat.pos_of_dvd_of_pos h Module.finrank_pos)
  have := Module.finite_of_finite F (M := K)
  have := Fintype.ofFinite K
  have := Fintype.ofFinite L
  refine ⟨Polynomial.IsSplittingField.lift _ (X ^ Fintype.card K - X) ?_⟩
  refine (FiniteField.isSplittingField_sub L F).splits.of_dvd ?_ ?_
  · exact map_ne_zero (FiniteField.X_pow_card_sub_X_ne_zero _ Fintype.one_lt_card)
  · rw [Module.card_eq_pow_finrank (K := F), Module.card_eq_pow_finrank (K := F) (V := L)]
    exact (map_dvd_map' _).mpr (dvd_pow_pow_sub_self_of_dvd h)

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

Goal state before:
pp: case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
⊢ χ⁻¹ a = χ a⁻¹ʳ

Tactic:
rw [inv_apply_eq_inv]

Goal state after:
case pos
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
⊢ (χ a)⁻¹ʳ = χ a⁻¹ʳ
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
x : Rˣ
⊢ χ⁻¹ ↑x = χ ↑x

Tactic:
rw [inv_apply_eq_inv]

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
⊢ (χ ↑x)⁻¹ʳ = χ ↑x
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
⊢ 1 ∣ n

Tactic:
apply one_dvd _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∈ χ.conductorSet
⊢ d ≠ 0

Tactic:
contrapose hd

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d = 0
⊢ d ∉ χ.conductorSet
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝ : NeZero n₂
this : NeZero n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot ((algebraMap (↥C₂) B) ζ₂) n₂
d : ℕ
hd : n₂ = n₁ * d
⊢ n₂ = ?m.112 * ?m.113

Tactic:
mul_comm

Goal state after:
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝ : NeZero n₂
this : NeZero n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot ((algebraMap (↥C₂) B) ζ₂) n₂
d : ℕ
hd : n₂ = n₁ * d
⊢ n₂ = ?b * ?a

case a
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝ : NeZero n₂
this : NeZero n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot ((algebraMap (↥C₂) B) ζ₂) n₂
d : ℕ
hd : n₂ = n₁ * d
⊢ ℕ

case b
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝ : NeZero n₂
this : NeZero n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot ((algebraMap (↥C₂) B) ζ₂) n₂
d : ℕ
hd : n₂ = n₁ * d
⊢ ℕ
Module: Mathlib.Analysis.Hofer

Goal state before:
pp: X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H : ∀ ε' > 0, ∀ (x' : X), ε' ≤ ε → d x' x ≤ 2 * ε → ε * ϕ x ≤ ε' * ϕ x' → ∃ y, d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
x' : X
k : ℕ
⊢ ϕ x * 2 ^ k ≤ ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'

pp: X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H : ∀ ε' > 0, ∀ (x' : X), ε' ≤ ε → d x' x ≤ 2 * ε → ε * ϕ x ≤ ε' * ϕ x' → ∃ y, d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
x' : X
k : ℕ
⊢ 0 < 2 ^ k

Tactic:
mul_comm

Goal state after:
X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H : ∀ ε' > 0, ∀ (x' : X), ε' ≤ ε → d x' x ≤ 2 * ε → ε * ϕ x ≤ ε' * ϕ x' → ∃ y, d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
x' : X
k : ℕ
⊢ 2 ^ k * ϕ x ≤ ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'

X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H : ∀ ε' > 0, ∀ (x' : X), ε' ≤ ε → d x' x ≤ 2 * ε → ε * ϕ x ≤ ε' * ϕ x' → ∃ y, d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
x' : X
k : ℕ
⊢ 0 < 2 ^ k
Module: Mathlib.Analysis.InnerProductSpace.Affine

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
a b : P
⊢ ⟪v, a -ᵥ b⟫_𝕜 = 0 ↔ ⟪v, b -ᵥ a⟫_𝕜 = 0

Tactic:
rw [← neg_vsub_eq_vsub_rev, inner_neg_right, neg_eq_zero]

Goal state after:
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
⊢ ↑(TensorProduct.assoc 𝕜 E E E) ∘ₗ
      adjoint (LinearMap.rTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)) ∘ₗ adjoint (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) =
    adjoint (LinearMap.lTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)) ∘ₗ adjoint (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)

Tactic:
← toLinearEquiv_assocIsometry,

Goal state after:
𝕜 : 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
⊢ ↑(assocIsometry 𝕜 E E E).toLinearEquiv ∘ₗ
      adjoint (LinearMap.rTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)) ∘ₗ adjoint (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) =
    adjoint (LinearMap.lTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)) ∘ₗ adjoint (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x y z : E
⊢ (adjoint comul)
      ((LinearMap.lTensor E (adjoint comul)) ((adjoint ↑(TensorProduct.assoc 𝕜 E E E).symm) (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] z))) =
    (adjoint comul) (x ⊗ₜ[𝕜] (adjoint comul) (y ⊗ₜ[𝕜] z))

Tactic:
← toLinearEquiv_assocIsometry,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x y z : E
⊢ (adjoint comul)
      ((LinearMap.lTensor E (adjoint comul)) ((adjoint ↑(assocIsometry 𝕜 E E E).symm) (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] z))) =
    (adjoint comul) (x ⊗ₜ[𝕜] (adjoint comul) (y ⊗ₜ[𝕜] z))
Module: Mathlib.Analysis.InnerProductSpace.ExteriorPower

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x✝¹ x✝ : Fin n → E
⊢ (of fun i j ↦ ⟪x✝ j, x✝¹ i⟫).det = (of fun i j ↦ ⟪x✝¹ j, x✝ i⟫).det

Tactic:
← Matrix.det_transpose

Goal state after:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x✝¹ x✝ : Fin n → E
⊢ (of fun i j ↦ ⟪x✝ j, x✝¹ i⟫)ᵀ.det = (of fun i j ↦ ⟪x✝¹ j, x✝ i⟫).det
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
⊢ ContDiff ℝ 1 (u ∘ update x i)

Tactic:
exact hu.comp (by convert! contDiff_update 1 x i)

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
I : Type u_2
inst✝¹ : Fintype I
inst✝ : LinearOrder I
b : OrthonormalBasis I ℝ E
n : ℕ
⊢ Orthonormal ℝ ⇑(Module.Basis.exteriorPower n b.toBasis)

Tactic:
rw [orthonormal_iff_ite]
    intro i j
    rw [exteriorPower.coe_basis, OrthonormalBasis.coe_toBasis]
    exact exteriorPower.innerProductForm_ιMulti_family_of_orthonormal b.orthonormal i j

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

Goal state before:

Tactic:
‖u x‖ₑ
    _ ≤ ∫⁻ xᵢ in Iic (x i), ‖deriv (u ∘ update x i) xᵢ‖ₑ := by
        apply le_trans (by simp) (HasCompactSupport.enorm_le_lintegral_Ici_deriv _ _ _)
        · exact hu.comp (by convert! contDiff_update 1 x i)
        · exact h2u.comp_isClosedEmbedding (isClosedEmbedding_update x i)
    _ ≤ ∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ := ?_

Goal state after:
case h₁
ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
⊢ ∫⁻ (xᵢ : ℝ) in Set.Iic (x i), ‖deriv (u ∘ update x i) xᵢ‖ₑ ≤ ∫⁻ (xᵢ : ℝ), ‖fderiv ℝ u (update x i xᵢ)‖ₑ
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 : E →ₗ.[R] F
hf : f.IsClosable
⊢ f.closure.IsClosed

Tactic:
IsClosed,

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 : E →ₗ.[R] F
hf : f.IsClosable
⊢ IsClosed[instTopologicalSpaceProd] ↑f.closure.graph