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

Goal state before:
pp: case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }.toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h :
  { toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ≤
    { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ (algebraMap (↥L') K)
      (((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g)
        ((algebraMap ↥L
            ↥{ toIntermediateField := L', finiteDimensional := finiteDimensional✝,
                  isGalois := isGalois✝ }.toIntermediateField)
          x)) =
    ↑(((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g) ⟨↑x, ⋯⟩)

Tactic:
]

Goal state after:
case mk.mk
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
L : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L
isGalois✝¹ : IsGalois k ↥L
x : ↥{ toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ }.toIntermediateField
L' : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L'
isGalois✝ : IsGalois k ↥L'
h :
  { toIntermediateField := L, finiteDimensional := finiteDimensional✝¹, isGalois := isGalois✝¹ } ≤
    { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }
this✝ : Algebra ↥L ↥L' := (Subsemiring.inclusion h).toAlgebra
this : IsScalarTower k ↥L ↥L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
⊢ (algebraMap (↥L') K)
      (((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g)
        ((algebraMap ↥L
            ↥{ toIntermediateField := L', finiteDimensional := finiteDimensional✝,
                  isGalois := isGalois✝ }.toIntermediateField)
          x)) =
    ↑(((proj { toIntermediateField := L', finiteDimensional := finiteDimensional✝, isGalois := isGalois✝ }) g) ⟨↑x, ⋯⟩)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
M : Type u_3
inst✝³ : CommSemiring K
inst✝² : CommSemiring M
j : K →+* M
p : ℕ
inst✝¹ : ExpChar M p
inst✝ : PerfectRing M p
x : K
this : (Classical.choose ⋯).2 = x ^ p ^ (Classical.choose ⋯).1
⊢ j x = j x

Tactic:
]

Goal state after:
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' : toAlgEquivAux g x ∈ L.toIntermediateField
hx : x ∈ L.toIntermediateField
⊢ ↑(((proj ?L) g) ⟨x, ?hx⟩) = ↑(((proj L) g) ⟨x, hx⟩)

pp: case L
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' : toAlgEquivAux g x ∈ L.toIntermediateField
hx : x ∈ L.toIntermediateField
⊢ FiniteGaloisIntermediateField k K

pp: case hx
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' : toAlgEquivAux g x ∈ L.toIntermediateField
hx : x ∈ L.toIntermediateField
⊢ x ∈ toIntermediateField ?L

Tactic:
]

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

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
⊢ (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
⊢ ↑(((proj L) g) ⟨x, hx⟩) = (((proj L) g).liftNormal K) x

Tactic:
]

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.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
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i
⊢ (iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)

Tactic:
]

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
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i
⊢ (iterateFrobeniusEquiv M p n').symm (j (Classical.choose ⋯).2) = (iterateFrobeniusEquiv M p n).symm (j y)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ (⇑(frobenius K p))^[z.1 + z2] ((⇑(frobenius K p))^[x.1 + z1] y.2) = (⇑(frobenius K p))^[x.1 + (z2 + (y.1 + z1))] z.2

Tactic:
]

Goal state after:
case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ (⇑(frobenius K p))^[z.1 + z2] ((⇑(frobenius K p))^[x.1 + z1] y.2) = (⇑(frobenius K p))^[x.1 + (z2 + (y.1 + z1))] z.2
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: k✝ : Type u_1
K✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : Field K✝
inst✝⁴ : Algebra k✝ K✝
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 y : K
hx : x ∈ (adjoin k {x, y}).toIntermediateField
hy : y ∈ (adjoin k {x, y}).toIntermediateField
⊢ (((proj (adjoin k {x, y})) g).liftNormal K) x * (((proj (adjoin k {x, y})) g).liftNormal K) y =
    (((proj (adjoin k {x, y})) g).liftNormal K) x * (((proj (adjoin k {x, y})) g).liftNormal K) y

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ (⇑(frobenius K p))^[x.1 + z1] ((⇑(frobenius K p))^[y.1 + z2] z.2) = (⇑(frobenius K p))^[x.1 + (z2 + (y.1 + z1))] z.2

Tactic:
]

Goal state after:
case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ (⇑(frobenius K p))^[x.1 + z1] ((⇑(frobenius K p))^[y.1 + z2] z.2) = (⇑(frobenius K p))^[x.1 + (z2 + (y.1 + z1))] z.2
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ (⇑(frobenius K p))^[x.1 + z1 + (y.1 + z2)] z.2 = (⇑(frobenius K p))^[x.1 + (z2 + (y.1 + z1))] z.2

Tactic:
]

Goal state after:
case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ (⇑(frobenius K p))^[x.1 + z1 + (y.1 + z2)] z.2 = (⇑(frobenius K p))^[x.1 + (z2 + (y.1 + z1))] z.2
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
ih1 : ∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2
ih2 : ∃ z_1, (⇑(frobenius K p))^[z.1 + z_1] y.2 = (⇑(frobenius K p))^[y.1 + z_1] z.2
⊢ ∃ z_1, (⇑(frobenius K p))^[z.1 + z_1] x.2 = (⇑(frobenius K p))^[x.1 + z_1] z.2

Tactic:
obtain ⟨z1, ih1⟩ := ih1
      obtain ⟨z2, ih2⟩ := ih2
      exists z2 + (y.1 + z1)
      rw [← add_assoc, iterate_add_apply, ih1]
      rw [← iterate_add_apply, add_comm, iterate_add_apply, ih2]
      rw [← iterate_add_apply]
      simp only [add_comm, add_left_comm]

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
x : L
n : ℕ
y : K
n' : ℕ := (Classical.choose ⋯).1
h' : i (Classical.choose ⋯).2 = x ^ p ^ n'
h✝ : (Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n' ∈ RingHom.ker i
m : ℕ
h : ((Classical.choose ⋯).2 ^ p ^ n - y ^ p ^ n') ^ p ^ m = 0
⊢ 0 = 0

Tactic:
]

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
⊢ 1 = 1

Tactic:
]

Goal state after:
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
A : Set Gal(K/k)
⊢ (∃ E, FiniteDimensional k ↥E ∧ Normal k ↥E ∧ ↑E.fixingSubgroup ⊆ A) ↔ ∃ L, ↑L.fixingSubgroup ⊆ A

Tactic:
]

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
A : Set Gal(K/k)
⊢ (∃ E, FiniteDimensional k ↥E ∧ Normal k ↥E ∧ ↑E.fixingSubgroup ⊆ A) ↔ ∃ L, ↑L.fixingSubgroup ⊆ A
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
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) → ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop) :=
  {f | f (op L) = 1}
this : ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup = Subtype.val ⁻¹' fix1
⊢ IsOpen (Subtype.val ⁻¹' fix1)

Tactic:
]

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
L : FiniteGaloisIntermediateField k K
fix1 : Set
  ((L : (FiniteGaloisIntermediateField k K)ᵒᵖ) → ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop) :=
  {f | f (op L) = 1}
this : ⇑(mulEquivToLimit k K) '' ↑L.fixingSubgroup = Subtype.val ⁻¹' fix1
⊢ IsOpen (Subtype.val ⁻¹' fix1)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (⇑(frobenius K p))^[n + z] x = (⇑(frobenius K p))^[m + z] y
⊢ mk K p (n + z + m, (⇑(frobenius K p))^[m + z] y) = mk K p (m + z + n, (⇑(frobenius K p))^[m + z] y)

Tactic:
]

Goal state after:
case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (⇑(frobenius K p))^[n + z] x = (⇑(frobenius K p))^[m + z] y
⊢ mk K p (n + z + m, (⇑(frobenius K p))^[m + z] y) = mk K p (m + z + n, (⇑(frobenius K p))^[m + z] y)
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
⊢ x1 ^ p ^ (n1 + n2) * x2 ^ p ^ (n1 + n2) = x1 ^ p ^ (n1 + n2) * x2 ^ p ^ (n1 + n2)

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (⇑(frobenius K p))^[n + z] x = (⇑(frobenius K p))^[m + z] y
⊢ mk K p (m + z + n, (⇑(frobenius K p))^[m + z] y) = mk K p (m + z + n, (⇑(frobenius K p))^[m + z] y)

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

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

Tactic:
]

Goal state after:
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : ℕ × K
⊢ ∃ z, (⇑(frobenius K p))^[(x.1, 1).1 + z] (0, 1).2 = (⇑(frobenius K p))^[(0, 1).1 + z] (x.1, 1).2
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 + 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:
]

Goal state after:
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 + 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)
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:
]

Goal state after:
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)
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
H : Set Gal(K/k)
L : FiniteGaloisIntermediateField k K
le : ↑L.fixingSubgroup ⊆ H
⊢ ∃ t ⊆ (fun a ↦ (mulEquivToLimit k K).toEquiv a) '' H, IsOpen t ∧ 1 ∈ t

Tactic:
]

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
H : Set Gal(K/k)
L : FiniteGaloisIntermediateField k K
le : ↑L.fixingSubgroup ⊆ H
⊢ ∃ t ⊆ (fun a ↦ (mulEquivToLimit k K).toEquiv a) '' H, IsOpen t ∧ 1 ∈ t
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 (j y1) * (iterateFrobeniusEquiv M p n2).symm (j y2) =
    (iterateFrobeniusEquiv M p n1).symm (j y1) * (iterateFrobeniusEquiv M p n2).symm (j y2)

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case succ
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)
⊢ ∃ z,
    (⇑(frobenius K p))^[(x.1, x.2 ^ n * x.2).1 + z]
        ((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 +
            z]
        (x.1, x.2 ^ n * x.2).2

Tactic:
]

Goal state after:
case succ
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)
⊢ ∃ z,
    (⇑(frobenius K p))^[(x.1, x.2 ^ n * x.2).1 + z]
        ((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 +
            z]
        (x.1, x.2 ^ n * x.2).2
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
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case succ
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)
⊢ mk K p (n, ↑x) = mk K p (n + 1, ↑x)

Tactic:
]

Goal state after:
case succ
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)
⊢ mk K p (n, ↑x) = mk K p (n + 1, ↑x)
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, ↑x)
⊢ R K p (n, ↑x) (n + 1, ↑x)

Tactic:
]

Goal state after:
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, ↑x)
⊢ R K p (n, ↑x) (n + 1, ↑x)
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
⊢ x1 ^ p ^ (n1 + n2) + x2 ^ p ^ (n1 + n2) = x1 ^ p ^ (n1 + n2) + x2 ^ p ^ (n1 + n2)

Tactic:
]

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

Goal state after:
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
Module: Mathlib.FieldTheory.PerfectClosure

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

Tactic:
]

Goal state after: