mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case refine_2.inl.inr
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b : Cardinal.{u}
hbc : a ∣ b * 0
hz : b * 0 = 0
⊢ a ∣ b ∨ a ∣ 0

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: n : ℕ
⊢ ↑n ≠ 0 ↔ n ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.Cardinality

Goal state before:
pp: α : Type u
inst✝ : Infinite α
⊢ #α = #(FractionRing (MvPolynomial α (ULift.{u, 0} ℚ)))

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case refine_3.inl.inl
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
c : Cardinal.{u_1}
hbc : ↑n ∣ 0 * c
h' : 0 * c < ℵ₀
⊢ ↑n ∣ 0 ∨ ↑n ∣ c

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case refine_3.inl.inr.inl
n : ℕ
h : ∀ (a b : ℕ), n ∣ a * b → n ∣ a ∨ n ∣ b
b : Cardinal.{u_1}
hbc : ↑n ∣ b * 0
h' : b * 0 < ℵ₀
⊢ ↑n ∣ b ∨ ↑n ∣ 0

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
⊢ logDeriv (a ^ 0) = ↑0 * logDeriv a

Tactic:
simp

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

Goal state before:
pp: case succ.inl
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
n : ℕ
h2 : logDeriv (0 ^ n) = ↑n * logDeriv 0
⊢ logDeriv (0 ^ (n + 1)) = ↑(n + 1) * logDeriv 0

Tactic:
simp

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

Goal state before:
pp: case empty
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
f : ι → R
h : ∀ x ∈ 0, f x ≠ 0
⊢ logDeriv (Multiset.map f 0).prod = (Multiset.map (fun x ↦ logDeriv (f x)) 0).sum

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
q : F[X]
⊢ p ∣
    q *
      (implicitDeriv
          ((AdjoinRoot.modByMonicHom ⋯)
            (-(aeval (AdjoinRoot.root p)) (mapCoeffs p) / (aeval (AdjoinRoot.root p)) (derivative p))))
        p

Tactic:
apply dvd_mul_of_dvd_right

Goal state after:
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
q : F[X]
⊢ p ∣
    (implicitDeriv
        ((AdjoinRoot.modByMonicHom ⋯)
          (-(aeval (AdjoinRoot.root p)) (mapCoeffs p) / (aeval (AdjoinRoot.root p)) (derivative p))))
      p
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: case zero
k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
x : Extension k p n
⊢ (frob k p n ^ 0) x = x ^ Nat.card k ^ 0

Tactic:
simp

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

Goal state before:
pp: case inl
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
h : f ∣ X ^ Nat.card k ^ 0 - X
⊢ f.natDegree ∣ 0

Tactic:
simp

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

Goal state before:
pp: case inr
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
⊢ f.natDegree ∣ n

Tactic:
cases finite_or_infinite k

Goal state after:
case inr.inl
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Finite k
⊢ f.natDegree ∣ n

case inr.inr
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Infinite k
⊢ f.natDegree ∣ n
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⟨differentialFiniteDimensional F K, ⋯⟩
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
⊢ ((aeval x) (minpoly F x))′ = ((aeval x) (minpoly F x))′

Tactic:
simp

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

Goal state before:
pp: case add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ q✝ : MvPolynomial σ (ZMod p)
⊢ (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝ →
    (frobenius (MvPolynomial σ (ZMod p)) p) q✝ = (expand p) q✝ →
      (frobenius (MvPolynomial σ (ZMod p)) p) p✝ + (frobenius (MvPolynomial σ (ZMod p)) p) q✝ =
        (expand p) p✝ + (expand p) q✝

Tactic:
hf

Goal state after:
case add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ q✝ : MvPolynomial σ (ZMod p)
hf : (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝
⊢ (frobenius (MvPolynomial σ (ZMod p)) p) q✝ = (expand p) q✝ →
    (frobenius (MvPolynomial σ (ZMod p)) p) p✝ + (frobenius (MvPolynomial σ (ZMod p)) p) q✝ =
      (expand p) p✝ + (expand p) q✝
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ : MvPolynomial σ (ZMod p)
n✝ : σ
⊢ (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝ →
    (frobenius (MvPolynomial σ (ZMod p)) p) p✝ * (frobenius (MvPolynomial σ (ZMod p)) p) (X n✝) =
      (expand p) p✝ * X n✝ ^ p

Tactic:
hf

Goal state after:
case mul_X
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f p✝ : MvPolynomial σ (ZMod p)
n✝ : σ
hf : (frobenius (MvPolynomial σ (ZMod p)) p) p✝ = (expand p) p✝
⊢ (frobenius (MvPolynomial σ (ZMod p)) p) p✝ * (frobenius (MvPolynomial σ (ZMod p)) p) (X n✝) = (expand p) p✝ * X n✝ ^ p
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∑ x, ↑(Fintype.card K - 1) * Multiset.count n {x} = Fintype.card K - 1

Tactic:
Nat.cast_id

Goal state after:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
n : σ
⊢ ∑ x, (Fintype.card K - 1) * Multiset.count n {x} = Fintype.card K - 1
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝ : CommSemiring K
p q : MvPolynomial σ K
x : σ → K
⊢ (eval x) (p + q) = ((fun e ↦ (eval e) p) + fun e ↦ (eval e) q) x

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝ : CommSemiring K
a : K
p : MvPolynomial σ K
e : σ → K
⊢ (eval e) (a • p) = ((RingHom.id K) a • fun e ↦ (eval e) p) e

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
c₀ : ι → F := ⋯
u₁ : ι → K := ⋯
i : ι
e : Gal(K/F)
property✝ : e ∈ ⊤
⊢ ∀ (x : Gal(K/F)), e (x (u i)) = ((Equiv.mulLeft e) x) (u i)

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: case e_a
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
c₀ : ι → F := ⋯
u₁ : ι → K := ⋯
ffb : fixedField ⊤ = ⊥
u₀ : ι → F
hu₀ : ∀ (i : ι), (algebraMap F K) (u₀ i) = u₁ i
v₁ : K := ⋯
e : Gal(K/F)
property✝ : e ∈ ⊤
⊢ ∀ (x : Gal(K/F)), e (x v) = ((Equiv.mulLeft e) x) v

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ (↑(Fintype.card Gal(K/F)))′ = 0

Tactic:
simp

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

Goal state before:
pp: case e'_4
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Finite K
this : Fintype K
x : L
hx :
  Ideal.span {X ^ finrank K L - 1} =
    (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
        ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x)).ker
e_1✝ : Fin (X ^ finrank K L - C 1).natDegree = Fin (AdjoinRoot.powerBasis ⋯).dim
i : Fin (X ^ finrank K L - C 1).natDegree
⊢ (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap) ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x))
      ((fun x ↦ x ^ ↑i) X) =
    (AEval'.of (frobeniusAlgHom K L).toLinearMap) ((⇑(frobeniusAlgEquivOfAlgebraic K L))^[↑(Fin.cast ⋯ i)] x)

Tactic:
rw [toSpanSingleton_apply, AEval'.X_pow_smul_of, End.smul_def, End.coe_pow]

Goal state after:
case e'_4
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Finite K
this : Fintype K
x : L
hx :
  Ideal.span {X ^ finrank K L - 1} =
    (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
        ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x)).ker
e_1✝ : Fin (X ^ finrank K L - C 1).natDegree = Fin (AdjoinRoot.powerBasis ⋯).dim
i : Fin (X ^ finrank K L - C 1).natDegree
⊢ (AEval'.of (frobeniusAlgHom K L).toLinearMap) ((⇑(frobeniusAlgHom K L).toLinearMap)^[↑i] x) =
    (AEval'.of (frobeniusAlgHom K L).toLinearMap) ((⇑(frobeniusAlgEquivOfAlgebraic K L))^[↑(Fin.cast ⋯ i)] x)
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ False

Tactic:
eq_univ_iff_forall,

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ False
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : Module.rank F ↥(adjoin F s) = Module.rank F ↥⊤
⊢ (#(Module.rank F E).ord.ToType).ord = Ordinal.type fun x1 x2 ↦ x1 < x2

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.ExtendRight

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
F : IntermediateField K L
M : Type u_3
inst✝⁷ : Field M
inst✝⁶ : Algebra K M
inst✝⁵ : Algebra L M
inst✝⁴ : IsScalarTower K L M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra S ↥F
inst✝¹ : Algebra S M
inst✝ : IsScalarTower S (↥F) M
s : S
⊢ (algebraMap (↥F) L) ((algebraMap S ↥F) s) ∈ ↑F.toSubsemiring

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.ExtendRight

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
F : IntermediateField K L
M : Type u_3
inst✝⁷ : Field M
inst✝⁶ : Algebra K M
inst✝⁵ : Algebra L M
inst✝⁴ : IsScalarTower K L M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra S ↥F
inst✝¹ : Algebra S M
inst✝ : IsScalarTower S (↥F) M
a : ↥(F.extendRight M)
⊢ (algebraMap (↥F) M) ((F.extendRightEquiv' M S).symm a) = ↑a

Tactic:
by
  rw [← algebraMap_extendRightEquiv' F M S, AlgEquiv.apply_symm_apply, algebraMap_apply]

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case neg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : ¬Nonempty ↑(Iio i)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝² : CommSemiring K
inst✝¹ : CommSemiring L
inst✝ : CommSemiring M
i : K →+* L
j : K →+* M
f : L →+* M
p : ℕ
x : K
⊢ (RingHom.id K) x = x ^ p ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : M
n : ℕ
y : L
hy : f y = x ^ p ^ n
⊢ ∃ n y, (f.comp i) y = x ^ p ^ n

Tactic:
obtain ⟨m, z, hz⟩ := pow_mem i p y

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : M
n : ℕ
y : L
hy : f y = x ^ p ^ n
m : ℕ
z : K
hz : i z = y ^ p ^ m
⊢ ∃ n y, (f.comp i) y = x ^ p ^ n
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
h : i y = x ^ p ^ n
⊢ (iterateFrobeniusEquiv M p (Classical.choose ⋯).1).symm (j (Classical.choose ⋯).2) =
    (iterateFrobeniusEquiv M p n).symm (j y)

Tactic:
have h' := Classical.choose_spec (lift_aux i p x)

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
h : i y = x ^ p ^ n
h' : i (Classical.choose ⋯).2 = x ^ p ^ (Classical.choose ⋯).1
⊢ (iterateFrobeniusEquiv M p (Classical.choose ⋯).1).symm (j (Classical.choose ⋯).2) =
    (iterateFrobeniusEquiv M p n).symm (j y)
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : K
L : FiniteGaloisIntermediateField k K
hx : x ∈ L.toIntermediateField
⊢ toAlgEquivAux g x = (((proj L) g).liftNormal K) x

Tactic:
rw [toAlgEquivAux_eq_proj_of_mem g x L hx]

Goal state after:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : K
L : FiniteGaloisIntermediateField k K
hx : x ∈ L.toIntermediateField
⊢ ↑(((proj L) g) ⟨x, hx⟩) = (((proj L) g).liftNormal K) x
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case zero.zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ ↑0 = mk K p (0, ↑0)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Goal state before:
pp: A : ProfiniteGrp.{u}
a : ↑A.toProfinite.toTop
⊢ (Hom.hom (𝟙 A)) a = a

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Goal state before:
pp: A B : ProfiniteGrp.{u}
e : A ≅ B
x : ↑A.toProfinite.toTop
⊢ (Hom.hom e.inv) ((Hom.hom e.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Goal state before:
pp: A B : ProfiniteGrp.{u}
e : A ≅ B
x : ↑B.toProfinite.toTop
⊢ (Hom.hom e.hom) ((Hom.hom e.inv) x) = x

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R}, IsSquare x → m ≠ 0 → ∃ r, x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare s
r : R
hr : s = r ^ m
⊢ x = r ^ n

Tactic:
simp [hm, pow_add, ← hr, hs]

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R}, IsSquare x → m ≠ 0 → ∃ r, x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare (-s)
r : R
hr : -s = r ^ m
⊢ x = r ^ n

Tactic:
simp [hm, pow_add, ← hr, hs]

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : CommRing M
inst✝⁸ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
p : ℕ
inst✝⁷ : ExpChar M p
inst✝⁶ : ExpChar K p
inst✝⁵ : PerfectRing M p
inst✝⁴ : IsPRadical i p
inst✝³ : ExpChar L p
inst✝² : ExpChar N p
inst✝¹ : PerfectRing N p
inst✝ : IsPRadical j p
x✝ : K
⊢ ((fun f ↦ f.comp i) ((lift j k p).comp (lift i j p))) x✝ = ((fun f ↦ f.comp i) (lift i k p)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
this : IsPurelyInseparable (↥k) D → ∀ (x : D), ∃ n, x ^ p ^ n ∈ (algebraMap (↥k) D).range
x : D
hx : IsSeparable (↥k) x
⊢ ∃ x_1, (algebraMap (↥k) D) x_1 = x

Tactic:
Subtype.exists

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
this : IsPurelyInseparable (↥k) D → ∀ (x : D), ∃ n, x ^ p ^ n ∈ (algebraMap (↥k) D).range
x : D
hx : IsSeparable (↥k) x
⊢ ∃ a, ∃ (b : a ∈ k), (algebraMap (↥k) D) ⟨a, b⟩ = x
Module: Mathlib.FieldTheory.Laurent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
x : R[X]
hx : x * (taylor r) p = 0
⊢ x = (taylor (r - r)) x

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.Laurent

Goal state before:
pp: case f
R : Type u
inst✝¹ : CommRing R
f : R⟮X⟯
inst✝ : IsDomain R
p✝ q✝ : R[X]
x✝ : q✝ ≠ 0
⊢ (laurent 0) ((algebraMap R[X] R⟮X⟯) p✝ / (algebraMap R[X] R⟮X⟯) q✝) =
    (algebraMap R[X] R⟮X⟯) p✝ / (algebraMap R[X] R⟮X⟯) q✝

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
⊢ ∀ i ∈ {i ∈ s | (H i).FiniteIndex}, (H i).FiniteIndex

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
hA : Algebra.Transcendental F ↥A
hB : Algebra.Transcendental F ↥B
this✝¹ : Algebra.Transcendental F ↥(A ⊔ B)
this✝ : Infinite ↥A
this : Infinite ↥B
⊢ #↑↑A + #↑↑B = max #↥A #↥B

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
⊢ (liftAlgHom (X ^ n - C a) (Algebra.ofId K K[n√a]) (↑↑1 • root (X ^ n - C a)) ⋯) (root (X ^ n - C a)) =
    1 (root (X ^ n - C a))

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case adjoin_rootSet'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ α ^ finrank K L - eval₂ (algebraMap K L) α (C a) = 0

Tactic:
eval₂_C,

Goal state after:
case adjoin_rootSet'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ α ^ finrank K L - (algebraMap K L) a = 0
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
x : ↥B
⊢ ↑x = (H.mulMapLeftOfSupEqTop H') (1 ⊗ₜ[R] x)

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
S : Type u_3
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Field S
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra K S
inst✝⁴ : Algebra L S
inst✝³ : IsScalarTower K L S
inst✝² : Normal K L
inst✝¹ : DecidableEq L
inst✝ : Fintype Gal(L/K)
c : ConjRootClass K L
x : L
⊢ mk K x = c ↔ (fun x ↦ x ∈ c.carrier) x

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
x✝ : E
⊢ x✝ ∈ (IsScalarTower.toAlgHom F (↥B) E).range ↔ x✝ ∈ B.toSubalgebra

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
⊢ ∀ (r : L), (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) r = 0 → r = 0

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
⊢ ∀ (m : E), (AddMonoidHom.id E) m = 0 → m = 0

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
ι : Type u_1
a : Basis ι F ↥A
H : LinearIndependent L (⇑A.val ∘ ⇑a)
⊢ ∀ (m : E), (AddMonoidHom.id E) m = 0 → m = 0

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
a : F
⊢ (normalizedTrace F K) ((algebraMap F K) a) = a

Tactic:
simp

Goal state after: