Theorem: ECTate.PerfectRing.pth_root_zero (ECTate/FieldTheory/PerfectClosure.lean)

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
⊢ pth_root 0 = 0
Tactic:
rw [pth_root]
State after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
⊢ dite (ringChar R = 0) (fun h => id) (fun h => Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R)) 0 =
    0

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
⊢ dite (ringChar R = 0) (fun h => id) (fun h => Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R)) 0 =
    0
Tactic:
split
State after:
case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ringChar R = 0
⊢ id 0 = 0

case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0 = 0

State before:
case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ringChar R = 0
⊢ id 0 = 0

case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0 = 0
Tactic:
. simp
State after:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0 = 0

State before:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0 = 0
Tactic:
. apply_fun (fun x : R => x ^ ringChar R)
  . simp only [ne_eq]
    rw [Function.surjInv_eq
          (pth_power_bijective_of_char_nonzero (by assumption)).surjective,
        zero_pow]
    rwa [zero_lt_iff]
  . exact (pth_power_bijective_of_char_nonzero (by assumption)).injective
State after:
no goals

State before:
case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ringChar R = 0
⊢ id 0 = 0
Tactic:
simp
State after:
no goals

State before:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0 = 0
Tactic:
apply_fun (fun x : R => x ^ ringChar R)
State after:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ (fun x => x ^ ringChar R) (Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0) =
    (fun x => x ^ ringChar R) 0

case inr.inj
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.Injective fun x => x ^ ringChar R

State before:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ (fun x => x ^ ringChar R) (Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0) =
    (fun x => x ^ ringChar R) 0

case inr.inj
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.Injective fun x => x ^ ringChar R
Tactic:
. simp only [ne_eq]
  rw [Function.surjInv_eq
        (pth_power_bijective_of_char_nonzero (by assumption)).surjective,
      zero_pow]
  rwa [zero_lt_iff]
State after:
case inr.inj
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.Injective fun x => x ^ ringChar R

State before:
case inr.inj
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.Injective fun x => x ^ ringChar R
Tactic:
. exact (pth_power_bijective_of_char_nonzero (by assumption)).injective
State after:
no goals

State before:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ (fun x => x ^ ringChar R) (Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0) =
    (fun x => x ^ ringChar R) 0
Tactic:
simp only [ne_eq]
State after:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0 ^ ringChar R = 0 ^ ringChar R

State before:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0 ^ ringChar R = 0 ^ ringChar R
Tactic:
rw [Function.surjInv_eq
      (pth_power_bijective_of_char_nonzero (by assumption)).surjective,
    zero_pow]
State after:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ 0 < ringChar R

State before:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ 0 < ringChar R
Tactic:
rwa [zero_lt_iff]
State after:
no goals

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ ringChar R ≠ 0
Tactic:
assumption
State after:
no goals

State before:
case inr.inj
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.Injective fun x => x ^ ringChar R
Tactic:
exact (pth_power_bijective_of_char_nonzero (by assumption)).injective
State after:
no goals