awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (hypothesis)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
L : Type v
inst_3 : CommSemiring L
inst_4 : CharP L p
inst_5 : PerfectRing L p
f : K →+* L
x_1 : PerfectClosure K p
n : ℕ
x : K
y_1 : PerfectClosure K p
m : ℕ
y : K
⊢ HAdd.hAdd (α := L) (β := L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
          ((⇑(frobenius L p) : (a : L) → L)^[m] ((f : (a : K) → L) x)) :
        L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
          ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : K) → L) y)) :
        L) =
    HAdd.hAdd (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m] ((f : (a : K) → L) y) : L)
have this : ∀ (n : ℕ),
  LeftInverse (α := L) (⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] (⇑(frobenius L p) : (a : L) → L)^[n]
Tactic: have := LeftInverse.iterate (frobeniusEquiv_symm_apply_frobenius L p)
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
L : Type v
inst_3 : CommSemiring L
inst_4 : CharP L p
inst_5 : PerfectRing L p
f : K →+* L
x_1 : PerfectClosure K p
n : ℕ
x : K
y_1 : PerfectClosure K p
m : ℕ
y : K
this :
  ∀ (n : ℕ),
    LeftInverse (α := L) (⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] (⇑(frobenius L p) : (a : L) → L)^[n]
⊢ HAdd.hAdd (α := L) (β := L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
          ((⇑(frobenius L p) : (a : L) → L)^[m] ((f : (a : K) → L) x)) :
        L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
          ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : K) → L) y)) :
        L) =
    HAdd.hAdd (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m] ((f : (a : K) → L) y) : L)
have mk : HAdd.hAdd (α := L) (β := L)
    ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m]
          ((⇑(frobenius L p) : (a : L) → L)^[m] ((f : (a : K) → L) x))) :
      L)
    ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
        ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : K) → L) y)) :
      L) =
  HAdd.hAdd (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
    ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m] ((f : (a : K) → L) y) : L)
Tactic: rw [iterate_add_apply, this _ _, add_comm n, iterate_add_apply, this _ _]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
L : Type v
inst_3 : CommSemiring L
inst_4 : CharP L p
inst_5 : PerfectRing L p
f : K →+* L
x_1 : PerfectClosure K p
n : ℕ
x : K
y_1 : PerfectClosure K p
m : ℕ
y : K
this :
  ∀ (n : ℕ),
    LeftInverse (α := L) (⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] (⇑(frobenius L p) : (a : L) → L)^[n]
mk :
  HAdd.hAdd (α := L) (β := L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
          ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m]
            ((⇑(frobenius L p) : (a : L) → L)^[m] ((f : (a : K) → L) x))) :
        L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
          ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : K) → L) y)) :
        L) =
    HAdd.hAdd (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m] ((f : (a : K) → L) y) : L)
⊢ HAdd.hAdd (α := L) (β := L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
          ((⇑(frobenius L p) : (a : L) → L)^[m] ((f : (a : K) → L) x)) :
        L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
          ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : K) → L) y)) :
        L) =
    HAdd.hAdd (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m] ((f : (a : K) → L) y) : L)
have mk₁ : HAdd.hAdd (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
    ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
        ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : K) → L) y)) :
      L) =
  HAdd.hAdd (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
    ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m] ((f : (a : K) → L) y) : L)
Tactic: rw [iterate_add_apply, this _ _, add_comm n, iterate_add_apply, this _ _]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
L : Type v
inst_3 : CommSemiring L
inst_4 : CharP L p
inst_5 : PerfectRing L p
f : K →+* L
x_1 : PerfectClosure K p
n : ℕ
x : K
y_1 : PerfectClosure K p
m : ℕ
y : K
this :
  ∀ (n : ℕ),
    LeftInverse (α := L) (⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] (⇑(frobenius L p) : (a : L) → L)^[n]
mk :
  HAdd.hAdd (α := L) (β := L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
          ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m]
            ((⇑(frobenius L p) : (a : L) → L)^[m] ((f : (a : K) → L) x))) :
        L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
          ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : K) → L) y)) :
        L) =
    HAdd.hAdd (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m] ((f : (a : K) → L) y) : L)
mk₁ :
  HAdd.hAdd (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
          ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : K) → L) y)) :
        L) =
    HAdd.hAdd (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m] ((f : (a : K) → L) y) : L)
⊢ HAdd.hAdd (α := L) (β := L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
          ((⇑(frobenius L p) : (a : L) → L)^[m] ((f : (a : K) → L) x)) :
        L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n + m]
          ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : K) → L) y)) :
        L) =
    HAdd.hAdd (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m] ((f : (a : K) → L) y) : L)
have mk₂ : HAdd.hAdd (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
    ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m + n]
        ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : K) → L) y)) :
      L) =
  HAdd.hAdd (α := L) (β := L) ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n] ((f : (a : K) → L) x) : L)
    ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[m] ((f : (a : K) → L) y) : L)
Tactic: rw [iterate_add_apply, this _ _, add_comm n, iterate_add_apply, this _ _]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
L : Type v
inst_3 : CommSemiring L
inst_4 : CharP L p
inst_5 : PerfectRing L p
f : RingHom.{u, v} (PerfectClosure K p) L
⊢ (fun (f : K →+* L) ↦
        {
          toFun := fun (e : PerfectClosure K p) ↦
            e.liftOn
              (fun (x : ℕ × K) ↦ (⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[x.1] ((f : (a : K) → L) x.2))
              ⋯,
          map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ : RingHom.{u, v} (PerfectClosure K p) L })
      ((fun (f : RingHom.{u, v} (PerfectClosure K p) L) ↦ f.comp (of K p)) f) =
    f
have a : ∀ (x : PerfectClosure K p) (n : ℕ) (x : K),
  Eq.{v + 1} (α := L)
    (((fun (f : K →+* L) ↦
              {
                toFun := fun (e : PerfectClosure K p) ↦
                  e.liftOn
                    (fun (x : ℕ × K) ↦
                      (⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[x.1] ((f : (a : K) → L) x.2))
                    sorry,
                map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry : RingHom.{u, v} (PerfectClosure K p) L })
            ((fun (f : RingHom.{u, v} (PerfectClosure K p) L) ↦ f.comp (of K p)) f) :
          (a : PerfectClosure K p) → L)
        (Quot.mk (R K p) (n, x)) :
      L)
    ((f : (a : PerfectClosure K p) → L) (Quot.mk (R K p) (n, x)) : L)
Tactic: ext ⟨n, x⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
L : Type v
inst_3 : CommSemiring L
inst_4 : CharP L p
inst_5 : PerfectRing L p
f : RingHom.{u, v} (PerfectClosure K p) L
x_1 : PerfectClosure K p
n : ℕ
x : K
⊢ Eq.{v + 1} (α := L)
    (((fun (f : K →+* L) ↦
              {
                toFun := fun (e : PerfectClosure K p) ↦
                  e.liftOn
                    (fun (x : ℕ × K) ↦
                      (⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[x.1] ((f : (a : K) → L) x.2))
                    ⋯,
                map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ : RingHom.{u, v} (PerfectClosure K p) L })
            ((fun (f : RingHom.{u, v} (PerfectClosure K p) L) ↦ f.comp (of K p)) f) :
          (a : PerfectClosure K p) → L)
        (Quot.mk (R K p) (n, x)) :
      L)
    ((f : (a : PerfectClosure K p) → L) (Quot.mk (R K p) (n, x)) : L)
have a : Eq (α := L)
  ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
      ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p)) :
    L)
  ((f : (a : PerfectClosure K p) → L) (mk K p (n, x)) : L)
Tactic: simp only [quot_mk_eq_mk, RingHom.comp_apply, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
      liftOn_mk]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
L : Type v
inst_3 : CommSemiring L
inst_4 : CharP L p
inst_5 : PerfectRing L p
f : RingHom.{u, v} (PerfectClosure K p) L
x_1 : PerfectClosure K p
n : ℕ
x : K
⊢ Eq (α := L)
    ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
        ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p)) :
      L)
    ((f : (a : PerfectClosure K p) → L) (mk K p (n, x)) : L)
have a : Eq (α := L)
  ((⇑(frobenius L p) : (a : L) → L)^[n]
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
        ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p))) :
    L)
  ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : PerfectClosure K p) → L) (mk K p (n, x))) : L)
Tactic: apply (injective_frobenius L p).iterate n
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
L : Type v
inst_3 : CommSemiring L
inst_4 : CharP L p
inst_5 : PerfectRing L p
f : RingHom.{u, v} (PerfectClosure K p) L
x_1 : PerfectClosure K p
n : ℕ
x : K
⊢ Eq (α := L)
    ((⇑(frobenius L p) : (a : L) → L)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
          ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p))) :
      L)
    ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : PerfectClosure K p) → L) (mk K p (n, x))) : L)
have a : Eq (α := L)
  ((⇑(frobenius L p) : (a : L) → L)^[n]
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
        ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p))) :
    L)
  ((f : (a : PerfectClosure K p) → L)
      ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[n] (mk K p (n, x))) :
    L)
Tactic: rw [← f.map_iterate_frobenius, iterate_frobenius_mk,
      RightInverse.iterate (frobenius_apply_frobeniusEquiv_symm L p) n]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
L : Type v
inst_3 : CommSemiring L
inst_4 : CharP L p
inst_5 : PerfectRing L p
f : RingHom.{u, v} (PerfectClosure K p) L
x_1 : PerfectClosure K p
n : ℕ
x : K
a :
  Eq (α := L)
    ((⇑(frobenius L p) : (a : L) → L)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
          ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p))) :
      L)
    ((f : (a : PerfectClosure K p) → L)
        ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[n] (mk K p (n, x))) :
      L)
⊢ Eq (α := L)
    ((⇑(frobenius L p) : (a : L) → L)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
          ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p))) :
      L)
    ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : PerfectClosure K p) → L) (mk K p (n, x))) : L)
have a₁ : Eq (α := L)
  ((⇑(frobenius L p) : (a : L) → L)^[n]
      ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
        ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p))) :
    L)
  ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p) : L)
Tactic: rw [← f.map_iterate_frobenius, iterate_frobenius_mk,
      RightInverse.iterate (frobenius_apply_frobeniusEquiv_symm L p) n]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
L : Type v
inst_3 : CommSemiring L
inst_4 : CharP L p
inst_5 : PerfectRing L p
f : RingHom.{u, v} (PerfectClosure K p) L
x_1 : PerfectClosure K p
n : ℕ
x : K
a :
  Eq (α := L)
    ((⇑(frobenius L p) : (a : L) → L)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
          ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p))) :
      L)
    ((f : (a : PerfectClosure K p) → L)
        ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[n] (mk K p (n, x))) :
      L)
a₁ :
  Eq (α := L)
    ((⇑(frobenius L p) : (a : L) → L)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
          ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p))) :
      L)
    ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p) : L)
⊢ Eq (α := L)
    ((⇑(frobenius L p) : (a : L) → L)^[n]
        ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[n]
          ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p))) :
      L)
    ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : PerfectClosure K p) → L) (mk K p (n, x))) : L)
have a₂ : Eq.{v + 1} (α := L)
  ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p) : L)
  ((f : (a : PerfectClosure K p) → L) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p) : L)
Tactic: rw [← f.map_iterate_frobenius, iterate_frobenius_mk,
      RightInverse.iterate (frobenius_apply_frobeniusEquiv_symm L p) n]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 y : ℕ × K
H : R K p x_1 y
n : ℕ
x : K
⊢ R K p ((n, x).1, (n, x).2⁻¹)
    (((n + 1, (frobenius K p : (a : K) → K) x) : ℕ × K).1, (n + 1, (frobenius K p : (a : K) → K) x).2⁻¹)
have simp : R K p (n, x⁻¹) (n + 1, (x ^ p)⁻¹)
Tactic: simp only [frobenius_def]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 y : ℕ × K
H : R K p x_1 y
n : ℕ
x : K
⊢ R K p (n, x⁻¹) (n + 1, (x ^ p)⁻¹)
have rw : R K p (n, x⁻¹) (n + 1, x⁻¹ ^ p)
Tactic: rw [← inv_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (hypothesis)
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
e : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
H : Ne (α := PerfectClosure K p) (mk K p (m, x)) 0
⊢ HMul.hMul (α := PerfectClosure K p) (mk K p (m, x)) (mk K p (m, x))⁻¹ = 1
have this : ¬(⇑(frobenius K p) : (a : K) → K)^[(0, 0).1] (m, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (0, 0).2
Tactic: have := mt (eq_iff _ _ _ _).2 H
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
e : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
H : Ne (α := PerfectClosure K p) (mk K p (m, x)) 0
this : ¬(⇑(frobenius K p) : (a : K) → K)^[(0, 0).1] (m, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (0, 0).2
⊢ HMul.hMul (α := PerfectClosure K p) (mk K p (m, x)) (mk K p (m, x))⁻¹ = 1
have rw : Eq (α := PerfectClosure K p)
  (mk K p
    ((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
      (⇑(frobenius K p) : (a : K) → K)^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
        (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2))
  1
Tactic: rw [mk_inv, mk_mul_mk]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
e : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
H : Ne (α := PerfectClosure K p) (mk K p (m, x)) 0
this : ¬(⇑(frobenius K p) : (a : K) → K)^[(0, 0).1] (m, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (0, 0).2
⊢ Eq (α := PerfectClosure K p)
    (mk K p
      ((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
        (⇑(frobenius K p) : (a : K) → K)^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
          (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2))
    1
have refine : (⇑(frobenius K p) : (a : K) → K)^[(0, 1).1]
    ((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
        (⇑(frobenius K p) : (a : K) → K)^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
          (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2).2 =
  (⇑(frobenius K p) :
        (a : K) →
          K)^[((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
          (⇑(frobenius K p) : (a : K) → K)^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
            (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2).1]
    (0, 1).2
Tactic: refine (eq_iff K p _ _).2 ?_
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
e : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
H : Ne (α := PerfectClosure K p) (mk K p (m, x)) 0
this : ¬(⇑(frobenius K p) : (a : K) → K)^[(0, 0).1] (m, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] (0, 0).2
⊢ (⇑(frobenius K p) : (a : K) → K)^[(0, 1).1]
      ((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
          (⇑(frobenius K p) : (a : K) → K)^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
            (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2).2 =
    (⇑(frobenius K p) :
          (a : K) →
            K)^[((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
            (⇑(frobenius K p) : (a : K) → K)^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
              (⇑(frobenius K p) : (a : K) → K)^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2).1]
      (0, 1).2
have simp : ∀ (this : ¬x = 0), (⇑(frobenius K p) : (a : K) → K)^[m] (x * x⁻¹) = 1
Tactic: simp only [iterate_map_one, iterate_map_zero, iterate_zero_apply, ← iterate_map_mul] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
e : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
H : Ne (α := PerfectClosure K p) (mk K p (m, x)) 0
this : ¬x = 0
⊢ (⇑(frobenius K p) : (a : K) → K)^[m] (x * x⁻¹) = 1
have rw : Eq (α := K) ((⇑(frobenius K p) : (a : K) → K)^[m] 1) 1
Tactic: rw [mul_inv_cancel₀ this, iterate_map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
e : PerfectClosure K p
x_1 : ℕ × K
m : ℕ
x : K
H : Ne (α := PerfectClosure K p) (mk K p (m, x)) 0
this : ¬x = 0
rw : Eq (α := K) ((⇑(frobenius K p) : (a : K) → K)^[m] 1) 1
⊢ (⇑(frobenius K p) : (a : K) → K)^[m] (x * x⁻¹) = 1
have rw₁ : Eq.{u + 1} (α := K) 1 1
Tactic: rw [mul_inv_cancel₀ this, iterate_map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.PerfectClosure (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
⊢ Eq.{u + 1} (α := ℕ × K) ((0, 0).1, (0, 0).2⁻¹) (0, 0)
have rw : Eq.{u + 1} (α := ℕ × K) ((0, 0).1, 0) (0, 0)
Tactic: rw [inv_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
σ τ : p.Gal
h :
  ∀ (x : p.SplittingField),
    Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x →
      Eq (α := p.SplittingField) ((σ : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
        ((τ : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
⊢ σ = τ
have fun : ∀ (x : p.SplittingField),
  Eq (α := Subalgebra F p.SplittingField)
    (AlgHom.equalizer (↑σ : p.SplittingField →ₐ[F] p.SplittingField) (↑τ : p.SplittingField →ₐ[F] p.SplittingField)) ⊤
Tactic: refine
    AlgEquiv.ext fun x =>
      (AlgHom.mem_equalizer σ.toAlgHom τ.toAlgHom x).mp
        ((SetLike.ext_iff.mp ?_ x).mpr Algebra.mem_top)
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
σ τ : p.Gal
h :
  ∀ (x : p.SplittingField),
    Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x →
      Eq (α := p.SplittingField) ((σ : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
        ((τ : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
x : p.SplittingField
⊢ Eq (α := Subalgebra F p.SplittingField)
    (AlgHom.equalizer (↑σ : p.SplittingField →ₐ[F] p.SplittingField) (↑τ : p.SplittingField →ₐ[F] p.SplittingField)) ⊤
have rwa : LE.le (α := Subalgebra F p.SplittingField) ⊤
  (AlgHom.equalizer (↑σ : p.SplittingField →ₐ[F] p.SplittingField) (↑τ : p.SplittingField →ₐ[F] p.SplittingField))
Tactic: rwa [eq_top_iff, ← SplittingField.adjoin_rootSet, Algebra.adjoin_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.PolynomialGaloisGroup (goal)
Goal:
F : Type u_1
inst : Field F
p : F[X]
σ τ : p.Gal
h :
  ∀ (x : p.SplittingField),
    Membership.mem (γ := Set p.SplittingField) (p.rootSet p.SplittingField) x →
      Eq (α := p.SplittingField) ((σ : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
        ((τ : (a : p.SplittingField) → p.SplittingField) x : p.SplittingField)
x : p.SplittingField
rwa :
  LE.le (α := Subalgebra F p.SplittingField) ⊤
    (AlgHom.equalizer (↑σ : p.SplittingField →ₐ[F] p.SplittingField) (↑τ : p.SplittingField →ₐ[F] p.SplittingField))
⊢ Eq (α := Subalgebra F p.SplittingField)
    (AlgHom.equalizer (↑σ : p.SplittingField →ₐ[F] p.SplittingField) (↑τ : p.SplittingField →ₐ[F] p.SplittingField)) ⊤
have rwa₁ : LE.le (α := Subalgebra F p.SplittingField) (Algebra.adjoin F (p.rootSet p.SplittingField))
  (AlgHom.equalizer (↑σ : p.SplittingField →ₐ[F] p.SplittingField) (↑τ : p.SplittingField →ₐ[F] p.SplittingField))
Tactic: rwa [eq_top_iff, ← SplittingField.adjoin_rootSet, Algebra.adjoin_le_iff]