awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : (i : (a : K) → L) y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : (i : (a : K) → L) y2 = x2 ^ p ^ n2
rw :
  HAdd.hAdd (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p (n1 + n2)) : (a : M) → M)
          ((iterateFrobeniusEquiv M p n2 : (a : M) → M) ((j : (a : K) → M) y1 : M) : M) :
        M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p (n1 + n2)) : (a : M) → M)
          (HPow.hPow (α := M) ((j : (a : K) → M) y2 : M) (p ^ n1)) :
        M) =
    HAdd.hAdd (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M) ((j : (a : K) → M) y1 : M) : M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n2) : (a : M) → M) ((j : (a : K) → M) y2 : M) : M)
⊢ liftAux i j p (x1 + x2) = liftAux i j p x1 + liftAux i j p x2

Tactic:
rw [liftAux_apply i j p _ _ _ h1, liftAux_apply i j p _ _ _ h2,
      liftAux_apply i j p (x1 + x2) (n1 + n2) (y1 ^ p ^ n2 + y2 ^ p ^ n1) (by rw [map_add,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, add_pow_expChar_pow]),
      map_add, map_pow, map_pow, map_add, ← iterateFrobeniusEquiv_def]

Premises used: iterateFrobeniusEquiv_def, map_add, map_pow, HPow.hPow, HAdd.hAdd, PerfectRing.liftAux_apply
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : (i : (a : K) → L) y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : (i : (a : K) → L) y2 = x2 ^ p ^ n2
nth_rw :
  HAdd.hAdd (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M)
          ((RingEquiv.symm (iterateFrobeniusEquiv M p n2) : (a : M) → M)
              ((iterateFrobeniusEquiv M p n2 : (a : M) → M) ((j : (a : K) → M) y1 : M) : M) :
            M) :
        M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p (n1 + n2)) : (a : M) → M)
          (HPow.hPow (α := M) ((j : (a : K) → M) y2 : M) (p ^ n1)) :
        M) =
    HAdd.hAdd (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M) ((j : (a : K) → M) y1 : M) : M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n2) : (a : M) → M) ((j : (a : K) → M) y2 : M) : M)
⊢ HAdd.hAdd (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p (n1 + n2)) : (a : M) → M)
          ((iterateFrobeniusEquiv M p n2 : (a : M) → M) ((j : (a : K) → M) y1 : M) : M) :
        M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p (n1 + n2)) : (a : M) → M)
          (HPow.hPow (α := M) ((j : (a : K) → M) y2 : M) (p ^ n1)) :
        M) =
    HAdd.hAdd (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M) ((j : (a : K) → M) y1 : M) : M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n2) : (a : M) → M) ((j : (a : K) → M) y2 : M) : M)

Tactic:
nth_rw 1 [iterateFrobeniusEquiv_symm_add_apply]

Premises used: iterateFrobeniusEquiv_symm_add_apply
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
inst_7 : ExpChar L p
x : L
n : ℕ
y : K
h : (i : (a : K) → L) y = x ^ p ^ n
⊢ Eq.{u_3 + 1} (α := M) ((lift i j p : (a : L) → M) x : M)
    ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M)

Tactic:
liftAux_apply i j p _ _ _ h

Premises used: PerfectRing.liftAux_apply, PerfectRing.liftAux
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
inst_7 : ExpChar L p
x : K
rw : (i : (a : K) → L) x = HPow.hPow (α := L) (β := ℕ) ((i : (a : K) → L) x : L) 1
rw₁ rw₂ : Eq.{u_2 + 1} (α := L) ((i : (a : K) → L) x : L) ((i : (a : K) → L) x : L)
⊢ (i : (a : K) → L) x = HPow.hPow (α := L) ((i : (a : K) → L) x : L) (HPow.hPow (β := ℕ) p 0)

Tactic:
rw [pow_zero, pow_one]

Premises used: pow_zero, pow_one
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
inst_7 : ExpChar L p
x : K
rw :
  Eq (α := M) ((RingEquiv.symm (RingEquiv.refl M) : (a : M) → M) ((j : (a : K) → M) x : M) : M)
    ((j : (a : K) → M) x : M)
⊢ Eq.{u_3 + 1} (α := M) ((lift i j p : (a : L) → M) ((i : (a : K) → L) x : L) : M) ((j : (a : K) → M) x : M)

Tactic:
rw [lift_apply i j p _ 0 x (by rw [pow_zero, pow_one]), iterateFrobeniusEquiv_zero]

Premises used: iterateFrobeniusEquiv_zero, PerfectRing.lift_apply, OfNat.ofNat
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
inst_7 : ExpChar L p
x : K
⊢ Eq (α := M) ((RingEquiv.symm (RingEquiv.refl M) : (a : M) → M) ((j : (a : K) → M) x : M) : M)
    ((j : (a : K) → M) x : M)

Tactic:
rfl
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
inst_7 : ExpChar L p
⊢ (lift i j p).comp i = j

Tactic:
RingHom.ext (lift_comp_apply i j p)

Premises used: RingHom.ext, PerfectRing.lift_comp_apply
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommRing K
inst_1 : CommRing L
i : K →+* L
p : ℕ
inst_2 : ExpChar K p
inst_3 : IsPRadical i p
inst_4 : ExpChar L p
inst_5 : PerfectRing L p
x : L
⊢ (lift i i p : (a : L) → L) x = x

Tactic:
liftAux_self_apply i p x

Premises used: PerfectRing.liftAux_self_apply, PerfectRing.liftAux
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommRing K
inst_1 : CommRing L
i : K →+* L
p : ℕ
inst_2 : ExpChar K p
inst_3 : IsPRadical i p
inst_4 : ExpChar L p
inst_5 : PerfectRing L p
⊢ lift i i p = RingHom.id L

Tactic:
RingHom.ext (liftAux_self_apply i p)

Premises used: PerfectRing.liftAux_self_apply, RingHom.ext
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
M : Type u_3
inst : CommRing K
inst_1 : CommRing M
j : K →+* M
p : ℕ
inst_2 : ExpChar M p
inst_3 : ExpChar K p
inst_4 : PerfectRing M p
x : K
⊢ Eq.{u_3 + 1} (α := M) ((lift (RingHom.id K) j p : (a : K) → M) x : M) ((j : (a : K) → M) x : M)

Tactic:
liftAux_id_apply j p x

Premises used: PerfectRing.liftAux_id_apply, PerfectRing.liftAux
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
M : Type u_3
inst : CommRing K
inst_1 : CommRing M
j : K →+* M
p : ℕ
inst_2 : ExpChar M p
inst_3 : ExpChar K p
inst_4 : PerfectRing M p
⊢ lift (RingHom.id K) j p = j

Tactic:
RingHom.ext (liftAux_id_apply j p)

Premises used: PerfectRing.liftAux_id_apply, RingHom.ext
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
inst_7 : ExpChar L p
⊢ lift i (f.comp i) p = f

Tactic:
IsPRadical.injective_comp_of_perfect _ i p (lift_comp i _ p)

Premises used: IsPRadical.injective_comp_of_perfect, PerfectRing.lift_comp
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
inst_7 : ExpChar L p
x : L
⊢ Eq.{u_3 + 1} (α := M) ((lift i (f.comp i) p : (a : L) → M) x : M) ((f : (a : L) → M) x : M)

Tactic:
congr($(comp_lift i f p) x)

Premises used: congrArg, id, DFunLike.coe, PerfectRing.comp_lift
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
inst_7 : ExpChar L p
⊢ (liftEquiv M i p : (a : K →+* M) → L →+* M) j = lift i j p

Tactic:
rfl

Premises used: PerfectRing.lift, rfl
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
inst_7 : ExpChar L p
⊢ (Equiv.symm (liftEquiv M i p) : (a : L →+* M) → K →+* M) f = f.comp i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
M : Type u_3
inst : CommRing K
inst_1 : CommRing M
j : K →+* M
p : ℕ
inst_2 : ExpChar M p
inst_3 : ExpChar K p
inst_4 : PerfectRing M p
⊢ (liftEquiv M (RingHom.id K) p : (a : K →+* M) → K →+* M) j = j

Tactic:
lift_id j p

Premises used: PerfectRing.lift, PerfectRing.lift_id
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
M : Type u_3
inst : CommRing K
inst_1 : CommRing M
p : ℕ
inst_2 : ExpChar M p
inst_3 : ExpChar K p
inst_4 : PerfectRing M p
⊢ Eq (α := (K →+* M) ≃ (K →+* M)) (liftEquiv M (RingHom.id K) p) (Equiv.refl (K →+* M))

Tactic:
Equiv.ext (liftEquiv_id_apply · p)

Premises used: PerfectRing.liftEquiv_id_apply, Equiv.ext
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
inst_9 : ExpChar N p
inst_10 : PerfectRing N p
inst_11 : IsPRadical j p
a :
  ∀ (x : K),
    Eq.{u_4 + 1} (α := N) (((fun (f : L →+* N) ↦ f.comp i) ((lift j k p).comp (lift i j p)) : (a : K) → N) x : N)
      (((fun (f : L →+* N) ↦ f.comp i) (lift i k p) : (a : K) → N) x : N)
⊢ Eq (α := K →+* N) ((fun (f : L →+* N) ↦ f.comp i) ((lift j k p).comp (lift i j p)))
    ((fun (f : L →+* N) ↦ f.comp i) (lift i k p))

Tactic:
ext
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
inst_9 : ExpChar N p
inst_10 : PerfectRing N p
inst_11 : IsPRadical j p
x : K
⊢ Eq.{u_4 + 1} (α := N) (((fun (f : L →+* N) ↦ f.comp i) ((lift j k p).comp (lift i j p)) : (a : K) → N) x : N)
    (((fun (f : L →+* N) ↦ f.comp i) (lift i k p) : (a : K) → N) x : N)

Tactic:
simp
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
inst_9 : ExpChar N p
inst_10 : PerfectRing N p
inst_11 : IsPRadical j p
x : L
⊢ Eq.{u_4 + 1} (α := N) ((lift j k p : (a : M) → N) ((lift i j p : (a : L) → M) x : M) : N)
    ((lift i k p : (a : L) → N) x : N)

Tactic:
congr($(lift_comp_lift i j k p) x)

Premises used: congrArg, PerfectRing.lift_comp_lift, id, DFunLike.coe
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
inst_7 : ExpChar L p
inst_8 : IsPRadical j p
inst_9 : PerfectRing L p
x : L
rw : (lift i i p : (a : L) → L) x = x
rw₁ rw₂ : x = x
⊢ (lift j i p : (a : M) → L) ((lift i j p : (a : L) → M) x : M) = x

Tactic:
rw [lift_comp_lift_apply, lift_self_apply]

Premises used: PerfectRing.lift_comp_lift_apply, PerfectRing.lift_self_apply
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
inst_7 : ExpChar L p
inst_8 : IsPRadical j p
inst_9 : PerfectRing L p
⊢ (lift j i p).comp (lift i j p) = RingHom.id L

Tactic:
RingHom.ext (lift_comp_lift_apply_eq_self i j p)

Premises used: PerfectRing.lift_comp_lift_apply_eq_self, RingHom.ext
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
g : L →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
inst_9 : ExpChar N p
inst_10 : IsPRadical g p
inst_11 : IsPRadical (g.comp i) p
⊢ lift g (lift i j p) p = lift (g.comp i) j p

Tactic:
IsPRadical.injective_comp_of_perfect _ (g.comp i) p ?_

Premises used: IsPRadical.injective_comp_of_perfect, RingHom.comp
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
g : L →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
inst_9 : ExpChar N p
inst_10 : IsPRadical g p
inst_11 : IsPRadical (g.comp i) p
refine :
  Eq (α := K →+* M) ((fun (f : N →+* M) ↦ f.comp (g.comp i)) (lift g (lift i j p) p))
    ((fun (f : N →+* M) ↦ f.comp (g.comp i)) (lift (g.comp i) j p))
⊢ lift g (lift i j p) p = lift (g.comp i) j p

Tactic:
refine IsPRadical.injective_comp_of_perfect _ (g.comp i) p ?_

Premises used: IsPRadical.injective_comp_of_perfect, RingHom.comp
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
g : L →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
inst_9 : ExpChar N p
inst_10 : IsPRadical g p
inst_11 : IsPRadical (g.comp i) p
simp_rw simp_rw₁ : (lift g (lift i j p) p).comp (g.comp i) = (lift (g.comp i) j p).comp (g.comp i)
simp_rw₂ : ((lift g (lift i j p) p).comp g).comp i = (lift (g.comp i) j p).comp (g.comp i)
⊢ Eq (α := K →+* M) ((fun (f : N →+* M) ↦ f.comp (g.comp i)) (lift g (lift i j p) p))
    ((fun (f : N →+* M) ↦ f.comp (g.comp i)) (lift (g.comp i) j p))

Tactic:
simp_rw [← RingHom.comp_assoc _ _ (lift g _ p), lift_comp]

Premises used: RingHom.comp_assoc, PerfectRing.lift, PerfectRing.lift_comp
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
g : L →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
inst_9 : ExpChar N p
inst_10 : IsPRadical g p
inst_11 : IsPRadical (g.comp i) p
x : N
⊢ Eq.{u_3 + 1} (α := M) ((lift g (lift i j p) p : (a : N) → M) x : M) ((lift (g.comp i) j p : (a : N) → M) x : M)

Tactic:
congr($(lift_lift i j g p) x)

Premises used: congrArg, PerfectRing.lift_lift, id, DFunLike.coe
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
g : L →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
inst_9 : ExpChar N p
inst_10 : IsPRadical g p
inst_11 : IsPRadical (g.comp i) p
⊢ Eq (α := N →+* M)
    ((liftEquiv M g p : (a : L →+* M) → N →+* M) ((liftEquiv M i p : (a : K →+* M) → L →+* M) j) : N →+* M)
    ((liftEquiv M (g.comp i) p : (a : K →+* M) → N →+* M) j : N →+* M)

Tactic:
lift_lift i j g p

Premises used: PerfectRing.lift_lift, PerfectRing.lift
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
g : L →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
inst_9 : ExpChar N p
inst_10 : IsPRadical g p
inst_11 : IsPRadical (g.comp i) p
⊢ Eq (α := (K →+* M) ≃ (N →+* M)) (Equiv.trans (liftEquiv M i p) (liftEquiv M g p)) (liftEquiv M (g.comp i) p)

Tactic:
Equiv.ext (liftEquiv_comp_apply i · g p)

Premises used: PerfectRing.liftEquiv_comp_apply, Equiv.ext
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : ExpChar L p
inst_6 : PerfectRing L p
inst_7 : IsPerfectClosure i p
inst_8 : PerfectRing M p
inst_9 : IsPerfectClosure j p
⊢ (equiv i j p).toRingHom = PerfectRing.lift i j p

Tactic:
rfl

Premises used: Function.surjInv, MulEquiv.toMonoidHom, RingEquiv.toRingHom, Classical.choose, PerfectRing.lift, PerfectRing.liftAux, rfl
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : ExpChar L p
inst_6 : PerfectRing L p
inst_7 : IsPerfectClosure i p
inst_8 : PerfectRing M p
inst_9 : IsPerfectClosure j p
⊢ (equiv i j p).symm = equiv j i p

Tactic:
rfl

Premises used: IsPerfectClosure.equiv, Function.surjInv, Classical.choose, Equiv.symm, PerfectRing.liftAux, RingEquiv.symm, rfl
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : ExpChar L p
inst_6 : PerfectRing L p
inst_7 : IsPerfectClosure i p
inst_8 : PerfectRing M p
inst_9 : IsPerfectClosure j p
⊢ (equiv i j p).symm.toRingHom = PerfectRing.lift j i p

Tactic:
rfl

Premises used: Function.surjInv, MulEquiv.toMonoidHom, RingEquiv.toRingHom, Classical.choose, PerfectRing.lift, PerfectRing.liftAux, rfl
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : ExpChar L p
inst_6 : PerfectRing L p
inst_7 : IsPerfectClosure i p
inst_8 : PerfectRing M p
inst_9 : IsPerfectClosure j p
x : L
n : ℕ
y : K
h : (i : (a : K) → L) y = x ^ p ^ n
⊢ Eq.{u_3 + 1} (α := M) ((equiv i j p : (a : L) → M) x : M)
    ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M)

Tactic:
PerfectRing.liftAux_apply i j p _ _ _ h

Premises used: Function.surjInv, Classical.choose, PerfectRing.liftAux_apply, PerfectRing.liftAux
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : ExpChar L p
inst_6 : PerfectRing L p
inst_7 : IsPerfectClosure i p
inst_8 : PerfectRing M p
inst_9 : IsPerfectClosure j p
x : M
n : ℕ
y : K
h : (j : (a : K) → M) y = x ^ p ^ n
rw :
  Eq.{u_2 + 1} (α := L) ((equiv j i p : (a : M) → L) x : L)
    ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) y : L) : L)
rw₁ rw₂ :
  Eq (α := L) ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) y : L) : L)
    ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) y : L) : L)
⊢ Eq.{u_2 + 1} (α := L) (((equiv i j p).symm : (a : M) → L) x : L)
    ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) y : L) : L)

Tactic:
rw [equiv_symm, equiv_apply j i p _ _ _ h]

Premises used: IsPerfectClosure.equiv_symm, IsPerfectClosure.equiv_apply
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommRing K
inst_1 : CommRing L
i : K →+* L
p : ℕ
inst_2 : ExpChar K p
inst_3 : ExpChar L p
inst_4 : PerfectRing L p
inst_5 : IsPerfectClosure i p
x : L
⊢ (equiv i i p : (a : L) → L) x = x

Tactic:
PerfectRing.liftAux_self_apply i p x

Premises used: Function.surjInv, PerfectRing.liftAux_self_apply, Classical.choose, PerfectRing.liftAux
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommRing K
inst_1 : CommRing L
i : K →+* L
p : ℕ
inst_2 : ExpChar K p
inst_3 : ExpChar L p
inst_4 : PerfectRing L p
inst_5 : IsPerfectClosure i p
⊢ equiv i i p = RingEquiv.refl L

Tactic:
RingEquiv.ext (equiv_self_apply i p)

Premises used: IsPerfectClosure.equiv_self_apply, RingEquiv.ext
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : ExpChar L p
inst_6 : PerfectRing L p
inst_7 : IsPerfectClosure i p
inst_8 : PerfectRing M p
inst_9 : IsPerfectClosure j p
x : K
⊢ Eq.{u_3 + 1} (α := M) ((equiv i j p : (a : L) → M) ((i : (a : K) → L) x : L) : M) ((j : (a : K) → M) x : M)

Tactic:
PerfectRing.lift_comp_apply i j p x

Premises used: Function.surjInv, Classical.choose, PerfectRing.lift_comp_apply, PerfectRing.liftAux
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : ExpChar L p
inst_6 : PerfectRing L p
inst_7 : IsPerfectClosure i p
inst_8 : PerfectRing M p
inst_9 : IsPerfectClosure j p
⊢ RingHom.comp (↑(equiv i j p) : L →+* M) i = j

Tactic:
RingHom.ext (equiv_comp_apply i j p)

Premises used: RingHom.ext, IsPerfectClosure.equiv_comp_apply
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : ExpChar L p
inst_7 : PerfectRing L p
inst_8 : IsPerfectClosure i p
inst_9 : PerfectRing M p
inst_10 : IsPerfectClosure j p
inst_11 : ExpChar N p
inst_12 : PerfectRing N p
inst_13 : IsPerfectClosure k p
x : L
⊢ Eq.{u_4 + 1} (α := N) ((equiv j k p : (a : M) → N) ((equiv i j p : (a : L) → M) x : M) : N)
    ((equiv i k p : (a : L) → N) x : N)

Tactic:
PerfectRing.lift_comp_lift_apply i j k p x

Premises used: PerfectRing.lift_comp_lift_apply, Function.surjInv, Classical.choose, PerfectRing.liftAux
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : ExpChar L p
inst_7 : PerfectRing L p
inst_8 : IsPerfectClosure i p
inst_9 : PerfectRing M p
inst_10 : IsPerfectClosure j p
inst_11 : ExpChar N p
inst_12 : PerfectRing N p
inst_13 : IsPerfectClosure k p
⊢ (equiv i j p).trans (equiv j k p) = equiv i k p

Tactic:
RingEquiv.ext (equiv_comp_equiv_apply i j k p)

Premises used: RingEquiv.ext, IsPerfectClosure.equiv_comp_equiv_apply