mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this✝ : ∀ (f : K →ₐ[F] E), Finite (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
⊢ ∑ a, Nat.card (↥K⟮x⟯ →ₐ[K] E) = Nat.card (K →ₐ[F] E) * (minpoly K x).natDegree

Tactic:
Nat.card_eq_fintype_card

Goal state after:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this✝ : ∀ (f : K →ₐ[F] E), Finite (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
⊢ ∑ a, Nat.card (↥K⟮x⟯ →ₐ[K] E) = Fintype.card (K →ₐ[F] E) * (minpoly K x).natDegree
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: case h
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
x✝ : G
ha : x✝ ∈ ⋃ n, V ^ (n + 1)
k : ℕ
hk : x✝ ∈ V ^ (k + 1)
⊢ x✝⁻¹ ∈ V⁻¹ ^ (k + 1)

Tactic:
simpa only [inv_pow, Set.mem_inv, inv_inv] using hk

Goal state after:
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K L : IntermediateField F E
inst✝¹ : IsGalois F ↥K
inst✝ : FiniteDimensional F ↥K
h : K ⊔ L = ⊤
⊢ IsGalois (↥L) E

Tactic:
obtain ⟨T, hT₁, hT₂⟩ := IsGalois.is_separable_splitting_field F K
  let T' := T.map (algebraMap F L)
  suffices T'.IsSplittingField L E from IsGalois.of_separable_splitting_field (p := T') hT₁.map
  rw [isSplittingField_iff_intermediateField] at hT₂ ⊢
  constructor
  · rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq]
    exact Polynomial.Splits.of_algHom hT₂.1 (IsScalarTower.toAlgHom _ _ _)
  · have h' : T'.rootSet E = T.rootSet E := by simp [Set.ext_iff, Polynomial.mem_rootSet', T']
    rw [← lift_inj, lift_adjoin, ← coe_val, hT₂.1.image_rootSet] at hT₂
    rw [← restrictScalars_eq_top_iff (K := F), restrictScalars_adjoin, adjoin_union, adjoin_self,
      h', hT₂.2, lift_top, sup_comm, h]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type ?u.5
S : Type ?u.7
M : Type ?u.9
inst✝⁶ : CommRing R
inst✝⁵ : Field S
inst✝⁴ : AddCommGroup M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
B : BilinForm S M
N : Submodule R M
y : M
x✝ : y ∈ N
⊢ (B 0) y ∈ 1

Tactic:
rw [B.zero_left]

Goal state after:
R : Type ?u.5
S : Type ?u.7
M : Type ?u.9
inst✝⁶ : CommRing R
inst✝⁵ : Field S
inst✝⁴ : AddCommGroup M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
B : BilinForm S M
N : Submodule R M
y : M
x✝ : y ∈ N
⊢ 0 ∈ 1
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H :
  Polynomial.map (algebraMap R K) p =
    Polynomial.map (algebraMap R K) a' * C a.leadingCoeff * (Polynomial.map (algebraMap R K) b' * C b.leadingCoeff)
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit b

Tactic:
mul_comm _ (C b.leadingCoeff),

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H :
  Polynomial.map (algebraMap R K) p =
    Polynomial.map (algebraMap R K) a' * C a.leadingCoeff * (C b.leadingCoeff * Polynomial.map (algebraMap R K) b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit b
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : Polynomial.map (algebraMap R K) q ∣ Polynomial.map (algebraMap R K) p
⊢ q ∣ p

Tactic:
obtain ⟨r, hr⟩ := h
  obtain ⟨d', hr'⟩ := IsIntegrallyClosed.eq_map_mul_C_of_dvd K hp (dvd_of_mul_left_eq _ hr.symm)
  rw [Monic.leadingCoeff, C_1, mul_one] at hr'
  · rw [← hr', ← Polynomial.map_mul] at hr
    exact dvd_of_mul_right_eq _ (Polynomial.map_injective _ (IsFractionRing.injective R K) hr.symm)
  · exact Monic.of_mul_monic_left (hq.map (algebraMap R K)) (by simpa [← hr] using hp.map _)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
con : (algebraMap R K) ((integerNormalization R⁰ p).content * ↑u) = 0
⊢ False

Tactic:
replace con := (injective_iff_map_eq_zero (algebraMap R K)).1 (IsFractionRing.injective _ _) _ con

Goal state after:
case hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
con : (integerNormalization R⁰ p).content * ↑u = 0
⊢ False
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : (X ^ n - C x).degree ≠ 0
hx : x = 0
⊢ 0 ^ n = x

Tactic:
rw [hx, pow_eq_zero_iff hn'.ne']

Goal state after:
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun g ↦ g.carrier) gp = S
M : IntermediateField k K
sub : (fun g ↦ g.carrier) M.fixingSubgroup ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
this : FiniteDimensional k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥M) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
⊢ FiniteDimensional k ↥L

Tactic:
have : L ≤ L'.1 := by
    apply le_trans _ (IntermediateField.le_normalClosure M)
    rw [← fixedField_fixingSubgroup M, IntermediateField.le_iff_le]
    exact sub

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun g ↦ g.carrier) gp = S
M : IntermediateField k K
sub : (fun g ↦ g.carrier) M.fixingSubgroup ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
this✝ : FiniteDimensional k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥M) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
this : L ≤ L'.toIntermediateField
⊢ FiniteDimensional k ↥L
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝⁵ : Field k
K : Type v
inst✝⁴ : Field K
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Normal F E
⊢ Normal F ↥(separableClosure F E)

Tactic:
by
    rw [← separableClosure.normalClosure_eq_self]
    exact normalClosure.normal F _ E

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
this : NormalizedGCDMonoid R
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
con : map (algebraMap R K) p = 0
⊢ map (algebraMap R K) p = map (algebraMap R K) 0

Tactic:
simp [con]

Goal state after:
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁶ : Group G
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
inst✝² : MulSemiringAction G B
hG : IsGaloisGroup G A B
H : Type u_5
inst✝¹ : Group H
inst✝ : MulSemiringAction H B
e : H ≃* G
he : ∀ (h : H) (x : B), e h • x = h • x
b : B
h : ∀ (g : H), g • b = b
g : G
x : B
⊢ e.symm g • x = g • x

Tactic:
by simp [← he]

Goal state after:
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
d_pos' : 0 < (minpoly K pb.gen).natDegree
this : Nonempty (Fin pb.dim)
⊢ -(minpoly K pb.gen).coeff (Fintype.card (Fin (minpoly K pb.gen).natDegree) - 1) = -(minpoly K pb.gen).nextCoeff

Tactic:
Fintype.card_fin,

Goal state after:
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
d_pos' : 0 < (minpoly K pb.gen).natDegree
this : Nonempty (Fin pb.dim)
⊢ -(minpoly K pb.gen).coeff ((minpoly K pb.gen).natDegree - 1) = -(minpoly K pb.gen).nextCoeff
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
s : Finset C
b : Basis (↥s) B C
this✝ : Algebra A B := (↑e).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.symm he)
⊢ ∀ (c : B) (x : C), e.symm c • x = c • x

Tactic:
by simp [Algebra.smul_def, ← he]

Goal state after:
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
s : Finset C
b : Basis (↥s) A C
⊢ ∀ (c : A) (x : C), e c • x = c • x

Tactic:
by simp [Algebra.smul_def, ← he]

Goal state after:
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case e_f.e_f
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β x y : κ
⊢ P y α * (trace A B) (b y * P x β • b x) = P y α * traceMatrix A b y x * P x β

Tactic:
ring_nf

Goal state after:
case e_f.e_f
κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
α β x y : κ
⊢ P y α * (trace A B) (b y * P x β • b x) = P y α * P x β * traceMatrix A b y x
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: case inl
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
val✝ : Fintype G
this : FaithfulSMul G L
⊢ Nat.card G = finrank (↥(FixedPoints.intermediateField G)) L

Tactic:
Nat.card_eq_fintype_card

Goal state after:
case inl
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁵ : Group G
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : MulSemiringAction G L
inst✝ : IsGaloisGroup G K L
val✝ : Fintype G
this : FaithfulSMul G L
⊢ Fintype.card G = finrank (↥(FixedPoints.intermediateField G)) L
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : Algebra A B
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : MulSemiringAction G B
inst✝¹¹ : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : IsFractionRing (A ⧸ P) K
inst✝ : IsFractionRing (B ⧸ Q) L
σ : ↥(MulAction.stabilizer G Q)
x : B
⊢ ((stabilizerHom G P Q K L) σ) ((algebraMap (B ⧸ Q) L) ((Ideal.Quotient.mk Q) x)) =
    (algebraMap (B ⧸ Q) L) ((Ideal.Quotient.mk Q) (↑σ • x))

Tactic:
simp [IsFractionRing.stabilizerHom, MulAction.subgroup_smul_def]

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

Goal state before:
pp: case succ
p a m d : ℕ
hd : (p * a + 1) ^ p ^ m - 1 = p ^ m * d
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]

Tactic:
tsub_eq_iff_eq_add_of_le (Nat.one_le_pow' _ _),

Goal state after:
case succ
p a m d : ℕ
hd : (p * a + 1) ^ p ^ m = p ^ m * d + 1
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case succ.zero.zero
p a d : ℕ
hd : p * a = d
hk : 0 ∈ range p
⊢ p ∣ (p ^ 0 * d) ^ 0 * ↑(p.choose (0 + 1))

Tactic:
simp [← hd, mul_assoc, pow_succ']

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

Goal state before:
pp: case succ.zero.succ
p a d : ℕ
hd : p * a = d
n✝ : ℕ
hk : n✝ + 1 ∈ range p
⊢ p ∣ (p ^ 0 * d) ^ (n✝ + 1) * ↑(p.choose (n✝ + 1 + 1))

Tactic:
simp [← hd, mul_assoc, pow_succ']

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst✝¹ : EquivLike E M ↥N
inst✝ : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
⊢ (LinearMap.det (N.subtype ∘ₗ (↑e).toIntLinearMap)).natAbs = Nat.card (M ⧸ N)

Tactic:
have h : Module.finrank ℤ N = Module.finrank ℤ M :=
    (AddEquiv.toIntLinearEquiv e : M ≃ₗ[ℤ] N).symm.finrank_eq

Goal state after:
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Free ℤ M
inst✝² : Module.Finite ℤ M
N : Submodule ℤ M
E : Type u_2
inst✝¹ : EquivLike E M ↥N
inst✝ : AddEquivClass E M ↥N
e : E
b : Basis (Free.ChooseBasisIndex ℤ M) ℤ M := Free.chooseBasis ℤ M
h : finrank ℤ ↥N = finrank ℤ M
⊢ (LinearMap.det (N.subtype ∘ₗ (↑e).toIntLinearMap)).natAbs = Nat.card (M ⧸ N)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Fintype.card F / 2) = Fintype.card F - 1
h : (fun x ↦ g ^ x) n ^ (Fintype.card F / 2) = 1
⊢ IsSquare ((fun x ↦ g ^ x) n)

Tactic:
rw [← Nat.card_eq_fintype_card] at hodd h

Goal state after:
case mpr
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
g : Fˣ
hg : ∀ (x : Fˣ), x ∈ Subgroup.zpowers g
n : ℕ
hodd : 2 * (Nat.card F / 2) = Nat.card F - 1
h : (fun x ↦ g ^ x) n ^ (Nat.card F / 2) = 1
⊢ IsSquare ((fun x ↦ g ^ x) n)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
⊢ f (a * b) = f a * f b

Tactic:
obtain ⟨ua, a_eq⟩ := prod_normalizedFactors ha0

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
⊢ f (a * b) = f a * f b
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
s : Finset C
b : Basis (↥s) B C
this✝ : Algebra A B := (↑e).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.symm he)
⊢ ∀ (c : B) (x : C), e.symm c • x = c • x

Tactic:
by simp [Algebra.smul_def, ← he]

Goal state after:
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
h : ¬∃ s, Nonempty (Basis (↥s) B C)
s : Finset C
b : Basis (↥s) A C
⊢ ∀ (c : A) (x : C), e c • x = c • x

Tactic:
by simp [Algebra.smul_def, ← he]

Goal state after:
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: A : Type u_8
B : Type u_9
C : Type u_10
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Ring C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
⊢ e ((norm A) x) = (norm B) x

Tactic:
by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
  · obtain ⟨s, ⟨b⟩⟩ := h
    let : Algebra A B := RingHom.toAlgebra e
    let : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' he.symm
    rw [Algebra.norm_eq_matrix_det b,
      Algebra.norm_eq_matrix_det (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he])),
      e.map_det]
    congr
    ext i j
    simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]
  rw [norm_eq_one_of_not_exists_basis _ h, norm_eq_one_of_not_exists_basis, map_one]
  intro ⟨s, ⟨b⟩⟩
  exact h ⟨s, ⟨b.mapCoeffs e (by simp [Algebra.smul_def, ← he])⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : absNorm I = 0
⊢ I = ⊥

Tactic:
← le_bot_iff

Goal state after:
case mp
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
hI : absNorm I = 0
⊢ I ≤ ⊥
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
⊢ closure[inst✝¹] (closedPoints X) ⊆ closedPoints X

Tactic:
closure_subset_iff_isClosed,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
⊢ IsClosed[inst✝¹] (closedPoints X)
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
⊢ length A M = length B M * length (ResidueField A) (ResidueField B)

Tactic:
by_cases h : IsFiniteLength B M

Goal state after:
case pos
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : IsFiniteLength B M
⊢ length A M = length B M * length (ResidueField A) (ResidueField B)

case neg
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : ¬IsFiniteLength B M
⊢ length A M = length B M * length (ResidueField A) (ResidueField B)
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
p : Ideal R
q : Ideal S
inst✝⁶ : Module.Finite R S
inst✝⁵ : q.IsPrime
inst✝⁴ : q.LiesOver p
inst✝³ : IsDedekindDomain R
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ R
inst✝ : Module.Free ℤ S
hp : p = ⊥
⊢ absNorm p ^ q.inertiaDeg R = absNorm q

Tactic:
subst hp

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
q : Ideal S
inst✝⁶ : Module.Finite R S
inst✝⁵ : q.IsPrime
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ R
inst✝¹ : Module.Free ℤ S
inst✝ : q.LiesOver ⊥
⊢ absNorm ⊥ ^ q.inertiaDeg R = absNorm q