mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ Continuous ⇑(mulEquivToLimit k K).symm

Tactic:
by

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
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
⊢ i 0 = 0 ^ p ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
n : ℕ
ih : mk K p x ^ n = mk K p (x.1, x.2 ^ n)
⊢ (⇑(frobenius K p))^[(x.1, x.2 ^ n * x.2).1 + 0]
      ((x.1, x.2 ^ n).1 + x.1,
          (⇑(frobenius K p))^[x.1] (x.1, x.2 ^ n).2 * (⇑(frobenius K p))^[(x.1, x.2 ^ n).1] x.2).2 =
    (⇑(frobenius K
            p))^[((x.1, x.2 ^ n).1 + x.1,
              (⇑(frobenius K p))^[x.1] (x.1, x.2 ^ n).2 * (⇑(frobenius K p))^[(x.1, x.2 ^ n).1] x.2).1 +
          0]
      (x.1, x.2 ^ n * x.2).2

Tactic:
by

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
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
⊢ liftAux i j p 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
n : ℕ
⊢ mk K p x ^ n = mk K p (x.1, x.2 ^ n)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
isSquare_of_nonneg : ∀ {x : R}, 0 ≤ x → IsSquare x
exists_isRoot_of_odd_natDegree : ∀ {f : R[X]}, Odd f.natDegree → ∃ x, f.IsRoot x
x : R
⊢ IsSquare x ∨ IsSquare (-x)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : ¬IsSquare (-x)
⊢ IsSquare x

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : ¬IsSquare x
⊢ IsSquare (-x)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hn : Odd n
⊢ Odd (X ^ n - C x).natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hn : Odd n
r : R
hr : (X ^ n - C x).IsRoot r
⊢ r ^ n - x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hn : Odd n
r : R
hr : (X ^ n - C x).IsRoot r
⊢ x = r ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hn : Odd n
⊢ ∃ r, x = r ^ n

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
this : R K p (n, ↑x) (n.succ, (frobenius K p) ↑x)
⊢ R K p (n, ↑x) (n + 1, ↑x)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd ↑n
⊢ Odd n

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd (-↑n)
⊢ Odd ?m.72

Tactic:
by

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:
by

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

Goal state before:
pp: A B C : ProfiniteGrp.{u}
f : A ⟶ B
g : B ⟶ C
a : ↑A.toProfinite.toTop
⊢ (Hom.hom (f ≫ g)) a = (Hom.hom g) ((Hom.hom f) a)

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

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

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd (-↑n)
r : R
hr : x = r ^ n
⊢ x = r⁻¹ ^ (-↑n)

Tactic:
by

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:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
k : ℤ
hk : Odd k
⊢ ∃ r, x = r ^ k

Tactic:
by

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

Goal state before:
pp: X Y Z : Type u
inst✝¹⁴ : Group X
inst✝¹³ : TopologicalSpace X
inst✝¹² : IsTopologicalGroup X
inst✝¹¹ : CompactSpace X
inst✝¹⁰ : TotallyDisconnectedSpace X
inst✝⁹ : Group Y
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : IsTopologicalGroup Y
inst✝⁶ : CompactSpace Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : Group Z
inst✝³ : TopologicalSpace Z
inst✝² : IsTopologicalGroup Z
inst✝¹ : CompactSpace Z
inst✝ : TotallyDisconnectedSpace Z
G H : FiniteGrp.{u}
f : G ⟶ H
⊢ Continuous (↑(GrpCat.Hom.hom f.hom)).toFun

Tactic:
by

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

Goal state before:
pp: X Y Z : Type u
inst✝¹⁴ : Group X
inst✝¹³ : TopologicalSpace X
inst✝¹² : IsTopologicalGroup X
inst✝¹¹ : CompactSpace X
inst✝¹⁰ : TotallyDisconnectedSpace X
inst✝⁹ : Group Y
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : IsTopologicalGroup Y
inst✝⁶ : CompactSpace Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : Group Z
inst✝³ : TopologicalSpace Z
inst✝² : IsTopologicalGroup Z
inst✝¹ : CompactSpace Z
inst✝ : TotallyDisconnectedSpace Z
X✝ Y✝ : ProfiniteGrp.{?u.56}
f : X✝ ⟶ Y✝
⊢ Continuous ⇑(Hom.hom f)

Tactic:
by

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
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ i (y1 ^ p ^ n2 + y2 ^ p ^ n1) = (x1 + x2) ^ p ^ (n1 + n2)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ∃ z, (⇑(frobenius K p))^[(0, ↑y).1 + z] (0, ↑x).2 = (⇑(frobenius K p))^[(0, ↑x).1 + z] (0, ↑y).2
⊢ ↑x = ↑y

Tactic:
obtain ⟨z, H⟩ := H

Goal state after:
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y z : ℕ
H : (⇑(frobenius K p))^[(0, ↑y).1 + z] (0, ↑x).2 = (⇑(frobenius K p))^[(0, ↑x).1 + z] (0, ↑y).2
⊢ ↑x = ↑y
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Goal state before:
pp: X✝ Y✝ Z : Type u
inst✝¹⁴ : Group X✝
inst✝¹³ : TopologicalSpace X✝
inst✝¹² : IsTopologicalGroup X✝
inst✝¹¹ : CompactSpace X✝
inst✝¹⁰ : TotallyDisconnectedSpace X✝
inst✝⁹ : Group Y✝
inst✝⁸ : TopologicalSpace Y✝
inst✝⁷ : IsTopologicalGroup Y✝
inst✝⁶ : CompactSpace Y✝
inst✝⁵ : TotallyDisconnectedSpace Y✝
inst✝⁴ : Group Z
inst✝³ : TopologicalSpace Z
inst✝² : IsTopologicalGroup Z
inst✝¹ : CompactSpace Z
inst✝ : TotallyDisconnectedSpace Z
X Y : ProfiniteGrp.{u_1}
f : X ⟶ Y
x✝ : IsIso ((forget₂ ProfiniteGrp.{u_1} Profinite).map f)
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
⊢ ↑x = ↑y ↔ ↑x = ↑y

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
a✝ b✝ : (j : J) → ↑(F.obj j).toProfinite.toTop
hx : a✝ ∈ {x | ∀ ⦃i j : J⦄ (π : i ⟶ j), (Hom.hom (F.map π)) (x i) = x j}
hy : b✝ ∈ {x | ∀ ⦃i j : J⦄ (π : i ⟶ j), (Hom.hom (F.map π)) (x i) = x j}
x✝¹ x✝ : J
π : x✝¹ ⟶ x✝
⊢ (Hom.hom (F.map π)) ((a✝ * b✝) x✝¹) = (a✝ * b✝) x✝

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
⊢ 1 ∈ {x | ∀ ⦃i j : J⦄ (π : i ⟶ j), (Hom.hom (F.map π)) (x i) = x j}

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
x✝² : (j : J) → ↑(F.obj j).toProfinite.toTop
h : x✝² ∈ {x | ∀ ⦃i j : J⦄ (π : i ⟶ j), (Hom.hom (F.map π)) (x i) = x j}
x✝¹ x✝ : J
π : x✝¹ ⟶ x✝
⊢ (Hom.hom (F.map π)) (x✝²⁻¹ x✝¹) = x✝²⁻¹ x✝

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ CharP (PerfectClosure K p) p

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ (frobenius (PerfectClosure K p) p) (mk K p x) = mk K p (x.1, x.2 ^ p)

Tactic:
by

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
⊢ m < n

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
j : J
⊢ Continuous fun x ↦ ↑x j

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝¹ : PerfectClosure K p
x : ℕ × K
x✝ : IsNilpotent (mk K p x)
n : ℕ
h : mk K p x ^ n = 0
⊢ mk K p x ^ p ^ n = 0

Tactic:
by

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
⊢ m ≠ 0

Tactic:
by

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)
⊢ m < n

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝¹ : PerfectClosure K p
x : ℕ × K
x✝ : IsNilpotent (mk K p x)
n m : ℕ
h : (iterateFrobenius K p m) (x.2 ^ p ^ n) = 0
⊢ (iterateFrobenius K p (n + m)) x.2 = 0

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
i j : J
f : i ⟶ j
⊢ ((Functor.const J).obj (ofProfinite (Profinite.limitCone (F ⋙ forget₂ ProfiniteGrp.{max u v} Profinite)).pt)).map f ≫
      { hom' := { toFun := fun x ↦ ↑x j, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ } } =
    { hom' := { toFun := fun x ↦ ↑x i, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ } } ≫ F.map f

Tactic:
by

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)
⊢ m ≠ 0

Tactic:
by

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:
by

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
cone : Limits.Cone F
m : cone.pt ⟶ (limitCone F).pt
h : ∀ (j : J), m ≫ (limitCone F).π.app j = cone.π.app j
⊢ m =
    ofHom
      (let __src :=
        TopCat.Hom.hom
          ((Profinite.limitConeIsLimit (F ⋙ forget₂ ProfiniteGrp.{max u v} Profinite)).lift
              ((forget₂ ProfiniteGrp.{max u v} Profinite).mapCone cone)).hom;
      { toFun := __src.toFun, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ })

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝¹ : PerfectClosure K p
x : ℕ × K
x✝ : IsNilpotent (mk K p x)
n : ℕ
h : mk K p x ^ n = 0
⊢ mk K p x = 0

Tactic:
by

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:
by

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
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ (iterateFrobeniusEquiv M p n1).symm ((iterateFrobeniusEquiv M p n2).symm ((iterateFrobeniusEquiv M p n2) (j y1))) +
      (iterateFrobeniusEquiv M p (n1 + n2)).symm (j y2 ^ p ^ n1) =
    (iterateFrobeniusEquiv M p n1).symm (j y1) + (iterateFrobeniusEquiv M p n2).symm (j y2)

Tactic:
rw [RingEquiv.symm_apply_apply, add_comm n1, iterateFrobeniusEquiv_symm_add_apply,
      ← iterateFrobeniusEquiv_def, RingEquiv.symm_apply_apply]

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hn : n ≠ 0
⊢ ∃ r, x = r ^ n

Tactic:
by

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
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
⊢ liftAux i j p (x1 + x2) = liftAux i j p x1 + liftAux i j p x2

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : ↑n ≠ 0
⊢ n ≠ 0

Tactic:
by

Goal state after:
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
inst✝ : ExpChar L p
x : K
⊢ i x = i x ^ p ^ 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : -↑n ≠ 0
⊢ ?m.78 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ Bijective fun x ↦ x ^ p

Tactic:
by

Goal state after:
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
inst✝ : ExpChar L p
x : K
⊢ (lift i j p) (i x) = j x

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : -↑n ≠ 0
r : R
hr : x = r ^ n
⊢ x = r⁻¹ ^ (-↑n)

Tactic:
by

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
⊢ (fun f ↦ f.comp i) ((lift j k p).comp (lift i j p)) = (fun f ↦ f.comp i) (lift i k p)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
k : ℤ
hk : k ≠ 0
⊢ ∃ r, x = r ^ k

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : IsRealClosed R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
h : 0 ≤ x
this : IsSquare (-x) → x = 0
⊢ IsSquare x

Tactic:
by

Goal state after:
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
inst✝² : ExpChar L p
inst✝¹ : IsPRadical j p
inst✝ : PerfectRing L p
x : L
⊢ (lift j i p) ((lift i j p) x) = x

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : IsRealClosed R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
h : 0 ≤ x
⊢ IsSquare x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
⊢ (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)) = (of K p) x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.Isaacs

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
s : E
hs : s ∈ S
⊢ (Polynomial.map (algebraMap F K') (minpoly F s)).Splits

Tactic:
by

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
g : L →+* 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✝¹ : IsPRadical g p
inst✝ : IsPRadical (g.comp i) p
⊢ lift g (lift i j p) p = lift (g.comp i) j p

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
⊢ PerfectClosure K p → L

Tactic:
by

Goal state after:
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✝⁴ : ExpChar L p
inst✝³ : PerfectRing L p
inst✝² : IsPerfectClosure i p
inst✝¹ : PerfectRing M p
inst✝ : IsPerfectClosure j p
x : M
n : ℕ
y : K
h : j y = x ^ p ^ n
⊢ (equiv i j p).symm x = (iterateFrobeniusEquiv L p n).symm (i y)

Tactic:
by

Goal state after:
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✝⁴ : ExpChar L p
inst✝³ : PerfectRing L p
inst✝² : IsPerfectClosure i p
inst✝¹ : PerfectRing M p
inst✝ : IsPerfectClosure j p
x : L
⊢ (equiv j i p) ((equiv i j p) x) = x

Tactic:
by

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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ : PerfectClosure K p
x : ℕ × K
⊢ (of K p) x.2 = mk K p x ^ p ^ x.1

Tactic:
by

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
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
h : x ∈ RingHom.ker (of K p)
⊢ x ∈ pNilradical K p

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
⊢ ∀ (x y : PerfectClosure K p),
    (x * y).liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯ =
      x.liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯ *
        y.liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : K →+* L
⊢ ∀ (x y : PerfectClosure K p),
    (x + y).liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯ =
      x.liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯ +
        y.liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : PerfectClosure K p →+* L
⊢ (fun f ↦
        { toFun := fun e ↦ e.liftOn (fun x ↦ (⇑(frobeniusEquiv L p).symm)^[x.1] (f x.2)) ⋯, map_one' := ⋯,
          map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
      ((fun f ↦ f.comp (of K p)) f) =
    f

Tactic:
by

Goal state after: