awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x y : ℕ
H : Eq.{u + 1} (α := K) (↑x : K) (↑y : K)
mpr : Eq (α := PerfectClosure K p) (mk K p (0, (↑x : K))) (↑y : PerfectClosure K p)
mpr₁ : Eq (α := PerfectClosure K p) (mk K p (0, (↑x : K))) (mk K p (0, (↑y : K)))
mpr₂ mpr₃ : Eq (α := PerfectClosure K p) (mk K p (0, (↑y : K))) (mk K p (0, (↑y : K)))
⊢ Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) (↑y : PerfectClosure K p)

Tactic:
rw [natCast K p 0, natCast K p 0, H]

Premises used: OfNat.ofNat, PerfectClosure.natCast
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
cast_eq_zero_iff : ∀ (x : ℕ), Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) 0 ↔ p ∣ x
⊢ CharP.{u} (PerfectClosure K p) p

Tactic:
constructor
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ
cast_eq_zero_iff : Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) 0 ↔ Eq.{u + 1} (α := K) (↑x : K) 0
⊢ Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) 0 ↔ p ∣ x

Tactic:
rw [← CharP.cast_eq_zero_iff K]

Premises used: CharP.cast_eq_zero_iff
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ
cast_eq_zero_iff :
  Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) (↑0 : PerfectClosure K p) ↔
    Eq.{u + 1} (α := K) (↑x : K) 0
cast_eq_zero_iff₁ : Eq.{u + 1} (α := K) (↑x : K) (↑0 : K) ↔ Eq.{u + 1} (α := K) (↑x : K) 0
cast_eq_zero_iff₂ cast_eq_zero_iff₃ : Eq.{u + 1} (α := K) (↑x : K) 0 ↔ Eq.{u + 1} (α := K) (↑x : K) 0
⊢ Eq.{u + 1} (α := PerfectClosure K p) (↑x : PerfectClosure K p) 0 ↔ Eq.{u + 1} (α := K) (↑x : K) 0

Tactic:
rw [← Nat.cast_zero, natCast_eq_iff, Nat.cast_zero]

Premises used: PerfectClosure.natCast_eq_iff, Nat.cast_zero
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ × K
⊢ HPow.hPow (α := PerfectClosure K p) (mk K p x) p = mk K p (x.1, x.2 ^ p)

Tactic:
mk_pow K p x p

Premises used: PerfectClosure.mk_pow
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : ℕ × K
⊢ HPow.hPow (α := PerfectClosure K p) (mk K p x) p = mk K p (x.1, x.2 ^ p)

Tactic:
exact mk_pow K p x p

Premises used: PerfectClosure.mk_pow
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : K
⊢ Eq (α := PerfectClosure K p) ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p)
    (mk K p (0, x) : PerfectClosure K p)

Tactic:
rfl

Premises used: PerfectClosure.mk, rfl
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 : PerfectClosure K p
x : ℕ × K
h_1 : IsNilpotent (R := PerfectClosure K p) (mk K p x)
n : ℕ
h : HPow.hPow (α := PerfectClosure K p) (mk K p x) n = 0
rw : HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ n - n + n) = 0
rw₁ : HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ n - n) * HPow.hPow (α := PerfectClosure K p) (mk K p x) n = 0
rw₂ : HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ n - n) * 0 = 0
rw₃ rw₄ : Eq.{u + 1} (α := PerfectClosure K p) 0 0
⊢ HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ n) = 0

Tactic:
rw [← Nat.sub_add_cancel ((n.lt_pow_self (Fact.out : p.Prime).one_lt).le),
        pow_add, h, mul_zero]

Premises used: Nat.lt_pow_self, Nat.Prime.one_lt, pow_add, LT.lt.le, MulZeroClass.mul_zero, Nat.sub_add_cancel, Fact.out
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 : PerfectClosure K p
x : ℕ × K
h_1 : IsNilpotent (R := PerfectClosure K p) (mk K p x)
n : ℕ
h : HPow.hPow (α := PerfectClosure K p) (mk K p x) n = 0
⊢ HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ n) = 0

Tactic:
replace h : mk K p x ^ p ^ n = 0 := by
      rw [← Nat.sub_add_cancel ((n.lt_pow_self (Fact.out : p.Prime).one_lt).le),
        pow_add, h, mul_zero]
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 : PerfectClosure K p
x : ℕ × K
h_1 : IsNilpotent (R := PerfectClosure K p) (mk K p x)
n : ℕ
h : HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ n) = 0
simp :
  ∀ (h : ∃ (z : ℕ), Eq (α := K) ((iterateFrobenius K p z : (a : K) → K) (x.2 ^ p ^ n) : K) (0 : K)),
    ∃ (z : ℕ), Eq (α := K) ((iterateFrobenius K p z : (a : K) → K) x.2 : K) (0 : K)
⊢ Eq (α := PerfectClosure K p) (mk K p x) 0

Tactic:
simp only [zero_def, mk_pow, mk_eq_iff, zero_add, ← coe_iterateFrobenius, map_zero] at h ⊢

Premises used: map_zero, zero_add, coe_iterateFrobenius, PerfectClosure.mk_eq_iff, PerfectClosure.zero_def, PerfectClosure.mk_pow
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 : PerfectClosure K p
x : ℕ × K
h_1 : IsNilpotent (R := PerfectClosure K p) (mk K p x)
n : ℕ
h : ∃ (z : ℕ), Eq (α := K) ((iterateFrobenius K p z : (a : K) → K) (x.2 ^ p ^ n) : K) (0 : K)
obtain :
  ∀ (m : ℕ) (h : Eq (α := K) ((iterateFrobenius K p m : (a : K) → K) (x.2 ^ p ^ n) : K) (0 : K)),
    ∃ (z : ℕ), Eq (α := K) ((iterateFrobenius K p z : (a : K) → K) x.2 : K) (0 : K)
⊢ ∃ (z : ℕ), Eq (α := K) ((iterateFrobenius K p z : (a : K) → K) x.2 : K) (0 : K)

Tactic:
obtain ⟨m, h⟩ := h
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 : PerfectClosure K p
x : ℕ × K
h_1 : IsNilpotent (R := PerfectClosure K p) (mk K p x)
n m : ℕ
h : Eq (α := K) ((iterateFrobenius K p m : (a : K) → K) (x.2 ^ p ^ n) : K) (0 : K)
⊢ Eq (α := K) ((iterateFrobenius K p (n + m) : (a : K) → K) x.2 : K) (0 : K)

Tactic:
simpa only [iterateFrobenius_def, pow_add, pow_mul] using h

Premises used: pow_add, pow_mul, iterateFrobenius_def
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 : PerfectClosure K p
x : ℕ × K
h_1 : IsNilpotent (R := PerfectClosure K p) (mk K p x)
n m : ℕ
h : Eq (α := K) ((iterateFrobenius K p m : (a : K) → K) (x.2 ^ p ^ n) : K) (0 : K)
⊢ ∃ (z : ℕ), Eq (α := K) ((iterateFrobenius K p z : (a : K) → K) x.2 : K) (0 : K)

Tactic:
exact ⟨n + m, by simpa only [iterateFrobenius_def, pow_add, pow_mul] using h⟩
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
f : PerfectClosure K p → PerfectClosure K p :=
  fun (e : PerfectClosure K p) ↦ e.liftOn (fun (x : ℕ × K) ↦ mk K p (x.1 + 1, x.2)) ⋯
⊢ Bijective (β := PerfectClosure K p) fun (x : PerfectClosure K p) ↦
    (frobenius (PerfectClosure K p) p : (a : PerfectClosure K p) → PerfectClosure K p) x

Tactic:
bijective_iff_has_inverse.mpr ⟨f, fun e ↦ induction_on e fun ⟨n, x⟩ ↦ ?_,
      fun e ↦ induction_on e fun ⟨n, x⟩ ↦ ?_⟩

Premises used: Iff.mpr, Function.bijective_iff_has_inverse, And.intro, Exists.intro, PerfectClosure.induction_on
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
f : PerfectClosure K p → PerfectClosure K p :=
  fun (e : PerfectClosure K p) ↦ e.liftOn (fun (x : ℕ × K) ↦ mk K p (x.1 + 1, x.2)) ⋯
refine_1 :
  ∀ (e : PerfectClosure K p) (x : ℕ × K) (n : ℕ) (x : K),
    f
        ((fun (x : PerfectClosure K p) ↦
            ((frobenius (PerfectClosure K p) p : (a : PerfectClosure K p) → PerfectClosure K p) x : PerfectClosure K p))
          (mk K p (n, x))) =
      mk K p (n, x)
refine_2 :
  ∀ (e : PerfectClosure K p) (x : ℕ × K) (n : ℕ) (x : K),
    Eq (α := PerfectClosure K p)
      ((fun (x : PerfectClosure K p) ↦
          ((frobenius (PerfectClosure K p) p : (a : PerfectClosure K p) → PerfectClosure K p) x : PerfectClosure K p))
        (f (mk K p (n, x))))
      (mk K p (n, x))
⊢ Bijective (β := PerfectClosure K p) fun (x : PerfectClosure K p) ↦
    (frobenius (PerfectClosure K p) p : (a : PerfectClosure K p) → PerfectClosure K p) x

Tactic:
refine bijective_iff_has_inverse.mpr ⟨f, fun e ↦ induction_on e fun ⟨n, x⟩ ↦ ?_,
      fun e ↦ induction_on e fun ⟨n, x⟩ ↦ ?_⟩

Premises used: Iff.mpr, Function.bijective_iff_has_inverse, And.intro, Exists.intro, PerfectClosure.induction_on
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
f : PerfectClosure K p → PerfectClosure K p :=
  fun (e : PerfectClosure K p) ↦ e.liftOn (fun (x : ℕ × K) ↦ mk K p (x.1 + 1, x.2)) ⋯
e : PerfectClosure K p
x_1 : ℕ × K
n : ℕ
x : K
⊢ f
      ((fun (x : PerfectClosure K p) ↦
          ((frobenius (PerfectClosure K p) p : (a : PerfectClosure K p) → PerfectClosure K p) x : PerfectClosure K p))
        (mk K p (n, x))) =
    mk K p (n, x)

Tactic:
simp only [f, liftOn_mk, frobenius_mk, mk_succ_pow]

Premises used: PerfectClosure.frobenius_mk, PerfectClosure.liftOn_mk, PerfectClosure.mk_succ_pow
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
f : PerfectClosure K p → PerfectClosure K p :=
  fun (e : PerfectClosure K p) ↦ e.liftOn (fun (x : ℕ × K) ↦ mk K p (x.1 + 1, x.2)) ⋯
e : PerfectClosure K p
x_1 : ℕ × K
n : ℕ
x : K
⊢ Eq (α := PerfectClosure K p)
    ((fun (x : PerfectClosure K p) ↦
        ((frobenius (PerfectClosure K p) p : (a : PerfectClosure K p) → PerfectClosure K p) x : PerfectClosure K p))
      (f (mk K p (n, x))))
    (mk K p (n, x))

Tactic:
simp only [f, liftOn_mk, frobenius_mk, mk_succ_pow]

Premises used: PerfectClosure.frobenius_mk, PerfectClosure.liftOn_mk, PerfectClosure.mk_succ_pow
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : K
⊢ Eq (α := PerfectClosure K p)
    ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[0] (mk K p (0, x)))
    ((of K p : (a : K) → PerfectClosure K p) x)

Tactic:
rfl
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : K
n : ℕ
ih :
  Eq (α := PerfectClosure K p)
    ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[n] (mk K p (n, x)))
    ((of K p : (a : K) → PerfectClosure K p) x)
succ :
  Eq (α := PerfectClosure K p)
    ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[n]
        ((frobenius (PerfectClosure K p) p : (a : PerfectClosure K p) → PerfectClosure K p) (mk K p (n + 1, x))) :
      PerfectClosure K p)
    ((of K p : (a : K) → PerfectClosure K p) x : PerfectClosure K p)
succ₁ :
  Eq (α := PerfectClosure K p)
    ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[n]
        ((frobenius (PerfectClosure K p) p : (a : PerfectClosure K p) → PerfectClosure K p) (mk K p (n + 1, x))) :
      PerfectClosure K p)
    ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[n] (mk K p (n, x)) :
      PerfectClosure K p)
succ₂ :
  Eq (α := PerfectClosure K p)
    ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[n]
      (mk K p ((n + 1, x).1, (n + 1, x).2 ^ p)))
    ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[n] (mk K p (n, x)))
succ₃ succ₄ :
  Eq (α := PerfectClosure K p)
    ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[n]
      (mk K p (n, (n + 1, x).2)))
    ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[n] (mk K p (n, x)))
⊢ Eq (α := PerfectClosure K p)
    ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[n + 1] (mk K p (n + 1, x)))
    ((of K p : (a : K) → PerfectClosure K p) x)

Tactic:
rw [iterate_succ_apply, ← ih, frobenius_mk, mk_succ_pow]

Premises used: PerfectClosure.frobenius_mk, PerfectClosure.mk_succ_pow, Function.iterate_succ_apply
-- Module: Mathlib.FieldTheory.PerfectClosure
Goal:
K : Type u
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
n : ℕ
x : K
zero :
  Eq (α := PerfectClosure K p)
    ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[0] (mk K p (0, x)))
    ((of K p : (a : K) → PerfectClosure K p) x)
succ :
  ∀ (n : ℕ)
    (ih :
      Eq (α := PerfectClosure K p)
        ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[n] (mk K p (n, x)))
        ((of K p : (a : K) → PerfectClosure K p) x)),
    Eq (α := PerfectClosure K p)
      ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[n + 1]
        (mk K p (n + 1, x)))
      ((of K p : (a : K) → PerfectClosure K p) x)
⊢ Eq (α := PerfectClosure K p)
    ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[n] (mk K p (n, x)))
    ((of K p : (a : K) → PerfectClosure K p) x)

Tactic:
induction n with
  | zero => rfl
  | succ n ih => rw [iterate_succ_apply, ← ih, frobenius_mk, mk_succ_pow]

Premises used: PerfectClosure.frobenius_mk, PerfectClosure.mk_succ_pow, Function.iterate_succ_apply
-- Module: Mathlib.FieldTheory.PerfectClosure
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
refine :
  ∀ (e : PerfectClosure K p) (x y : ℕ × K),
    R K p x y →
      Eq.{v + 1} (α := L)
        ((fun (x : ℕ × K) ↦ ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[x.1] ((f : (a : K) → L) x.2) : L))
          x)
        ((fun (x : ℕ × K) ↦ ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[x.1] ((f : (a : K) → L) x.2) : L))
          y)
⊢ PerfectClosure K p → L

Tactic:
refine fun e => liftOn e (fun x => (frobeniusEquiv L p).symm^[x.1] (f x.2)) ?_

Premises used: frobeniusEquiv, Nat.iterate, PerfectClosure.liftOn, Prod.fst, Prod.snd, DFunLike.coe, RingEquiv.symm
-- Module: Mathlib.FieldTheory.PerfectClosure
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
e : PerfectClosure K p
n : ℕ
x : K
⊢ Eq.{v + 1} (α := L)
    ((fun (x : ℕ × K) ↦ ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[x.1] ((f : (a : K) → L) x.2) : L))
      (n, x))
    ((fun (x : ℕ × K) ↦ ((⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[x.1] ((f : (a : K) → L) x.2) : L))
      (n + 1, (frobenius K p : (a : K) → K) x))

Tactic:
simp [f.map_frobenius]

Premises used: RingHom.map_frobenius
-- Module: Mathlib.FieldTheory.PerfectClosure
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
mk :
  HMul.hMul (α := 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) =
    HMul.hMul (α := 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)
⊢ (Quot.mk (R K p) (n, x) * Quot.mk (R K p) (m, y)).liftOn
      (fun (x : ℕ × K) ↦ (⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[x.1] ((f : (a : K) → L) x.2)) ⋯ =
    HMul.hMul (α := L)
      (liftOn (Quot.mk (R K p) (n, x))
        (fun (x : ℕ × K) ↦ (⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[x.1] ((f : (a : K) → L) x.2)) ⋯)
      (liftOn (Quot.mk (R K p) (m, y))
        (fun (x : ℕ × K) ↦ (⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[x.1] ((f : (a : K) → L) x.2)) ⋯)

Tactic:
simp only [quot_mk_eq_mk, liftOn_mk, f.map_iterate_frobenius, mk_mul_mk, map_mul,
          iterate_map_mul]

Premises used: PerfectClosure.mk_mul_mk, PerfectClosure.quot_mk_eq_mk, PerfectClosure.liftOn_mk, RingHom.map_iterate_frobenius, iterate_map_mul, map_mul
-- Module: Mathlib.FieldTheory.PerfectClosure
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
⊢ ∀ (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)
-- Module: Mathlib.FieldTheory.PerfectClosure
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
mk :
  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)
⊢ (Quot.mk (R K p) (n, x) + Quot.mk (R K p) (m, y)).liftOn
      (fun (x : ℕ × K) ↦ (⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[x.1] ((f : (a : K) → L) x.2)) ⋯ =
    HAdd.hAdd (α := L)
      (liftOn (Quot.mk (R K p) (n, x))
        (fun (x : ℕ × K) ↦ (⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[x.1] ((f : (a : K) → L) x.2)) ⋯)
      (liftOn (Quot.mk (R K p) (m, y))
        (fun (x : ℕ × K) ↦ (⇑(RingEquiv.symm (frobeniusEquiv L p)) : (a : L) → L)^[x.1] ((f : (a : K) → L) x.2)) ⋯)

Tactic:
simp only [quot_mk_eq_mk, liftOn_mk, f.map_iterate_frobenius, mk_add_mk, map_add,
          iterate_map_add]

Premises used: PerfectClosure.quot_mk_eq_mk, PerfectClosure.liftOn_mk, PerfectClosure.mk_add_mk, RingHom.map_iterate_frobenius, map_add, iterate_map_add
-- Module: Mathlib.FieldTheory.PerfectClosure
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
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))
                      ⋯,
                  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)
⊢ (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

Tactic:
ext ⟨n, x⟩
-- Module: Mathlib.FieldTheory.PerfectClosure
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)
    ((⇑(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)
⊢ 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)

Tactic:
simp only [quot_mk_eq_mk, RingHom.comp_apply, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
      liftOn_mk]

Premises used: PerfectClosure.quot_mk_eq_mk, PerfectClosure.liftOn_mk, OneHom.coe_mk, MonoidHom.coe_mk, RingHom.coe_mk, RingHom.comp_apply
-- Module: Mathlib.FieldTheory.PerfectClosure
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)
    ((⇑(frobenius L p) : (a : L) → L)^[n] ((f : (a : PerfectClosure K p) → L) (mk K p (n, x))) : L)
⊢ 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:
apply (injective_frobenius L p).iterate n

Premises used: injective_frobenius, Function.Injective.iterate