awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ n) = 0
have rw₃ : Eq.{u + 1} (α := PerfectClosure K p) 0 0
Tactic: rw [← Nat.sub_add_cancel ((n.lt_pow_self (Fact.out : p.Prime).one_lt).le),
        pow_add, h, mul_zero]
-- 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
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
⊢ Eq (α := PerfectClosure K p) (mk K p x) 0
have h₁ : 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]
Cleared hypotheses: h
-- 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
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
⊢ Eq (α := PerfectClosure K p) (mk K p x) 0
have 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)
Tactic: simp only [zero_def, mk_pow, mk_eq_iff, zero_add, ← coe_iterateFrobenius, map_zero] at h ⊢
Cleared hypotheses: h
-- 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
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)
⊢ ∃ (z : ℕ), Eq (α := K) ((iterateFrobenius K p z : (a : K) → K) x.2 : K) (0 : K)
have 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)
Tactic: obtain ⟨m, h⟩ := h
Cleared hypotheses: h
-- 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
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
have 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)
Tactic: refine bijective_iff_has_inverse.mpr ⟨f, fun e ↦ induction_on e fun ⟨n, x⟩ ↦ ?_,
      fun e ↦ induction_on e fun ⟨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
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)
⊢ Bijective (β := PerfectClosure K p) fun (x : PerfectClosure K p) ↦
    (frobenius (PerfectClosure K p) p : (a : PerfectClosure K p) → PerfectClosure K p) x
have 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))
Tactic: refine bijective_iff_has_inverse.mpr ⟨f, fun e ↦ induction_on e fun ⟨n, x⟩ ↦ ?_,
      fun e ↦ induction_on e fun ⟨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
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)
⊢ 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)
have 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)
Tactic: rw [iterate_succ_apply, ← ih, frobenius_mk, mk_succ_pow]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [iterate_succ_apply, ← ih, frobenius_mk, mk_succ_pow]
-- 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
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)
⊢ 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)
have 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)))
Tactic: rw [iterate_succ_apply, ← ih, frobenius_mk, mk_succ_pow]
-- 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
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)))
⊢ 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)
have 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)))
Tactic: rw [iterate_succ_apply, ← ih, frobenius_mk, mk_succ_pow]
-- 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
n : ℕ
x : K
⊢ 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)
have 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)
Tactic: induction n with
  | zero => rfl
  | succ n ih => rw [iterate_succ_apply, ← ih, frobenius_mk, mk_succ_pow]
Cleared hypotheses: 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
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)
⊢ 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)
have 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)
Tactic: induction n with
  | zero => rfl
  | succ n ih => rw [iterate_succ_apply, ← ih, frobenius_mk, mk_succ_pow]
Cleared hypotheses: 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 : K →+* L
⊢ PerfectClosure K p → L
have 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)
Tactic: refine fun e => liftOn e (fun x => (frobeniusEquiv L p).symm^[x.1] (f x.2)) ?_
-- 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
⊢ (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)) ⋯)
have 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)
Tactic: simp only [quot_mk_eq_mk, liftOn_mk, f.map_iterate_frobenius, mk_mul_mk, map_mul,
          iterate_map_mul]
-- 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
⊢ 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)
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]
⊢ 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)
have mk : HMul.hMul (α := 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) =
  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)
Tactic: rw [iterate_add_apply, this _ _, add_comm, 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 :
  HMul.hMul (α := 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) =
    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)
⊢ 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)
have mk₁ : 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)^[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)
Tactic: rw [iterate_add_apply, this _ _, add_comm, 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 :
  HMul.hMul (α := 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) =
    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)
mk₁ :
  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)^[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)
⊢ 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)
have mk₂ : 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 + n]
        ((⇑(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)
Tactic: rw [iterate_add_apply, this _ _, add_comm, 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
⊢ (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)) ⋯)
have 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)
Tactic: simp only [quot_mk_eq_mk, liftOn_mk, f.map_iterate_frobenius, mk_add_mk, map_add,
          iterate_map_add]