Theorem: pow_ringChar_injective (ECTate/Algebra/CharP/Basic.lean)

State before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
⊢ Function.Injective fun x => x ^ ringChar R
Tactic:
intros x y h
State after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h : (fun x => x ^ ringChar R) x = (fun x => x ^ ringChar R) y
⊢ x = y

State before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h : (fun x => x ^ ringChar R) x = (fun x => x ^ ringChar R) y
⊢ x = y
Tactic:
rw [←sub_eq_zero] at *
State after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝ : (fun x => x ^ ringChar R) x = (fun x => x ^ ringChar R) y
h : (fun x => x ^ ringChar R) x - (fun x => x ^ ringChar R) y = 0
⊢ x - y = 0

State before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝ : (fun x => x ^ ringChar R) x = (fun x => x ^ ringChar R) y
h : (fun x => x ^ ringChar R) x - (fun x => x ^ ringChar R) y = 0
⊢ x - y = 0
Tactic:
rw [←sub_eq_zero] at *
State after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝² : (fun x => x ^ ringChar R) x = (fun x => x ^ ringChar R) y
h✝¹ h✝ : (fun x => x ^ ringChar R) x - (fun x => x ^ ringChar R) y = 0
h : (fun x => x ^ ringChar R) x - (fun x => x ^ ringChar R) y - 0 = 0
⊢ x - y - 0 = 0

State before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝² : (fun x => x ^ ringChar R) x = (fun x => x ^ ringChar R) y
h✝¹ h✝ : (fun x => x ^ ringChar R) x - (fun x => x ^ ringChar R) y = 0
h : (fun x => x ^ ringChar R) x - (fun x => x ^ ringChar R) y - 0 = 0
⊢ x - y - 0 = 0
Tactic:
simp only [sub_zero] at *
State after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝² : x ^ ringChar R = y ^ ringChar R
h✝¹ h✝ h : x ^ ringChar R - y ^ ringChar R = 0
⊢ x - y = 0

State before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝² : x ^ ringChar R = y ^ ringChar R
h✝¹ h✝ h : x ^ ringChar R - y ^ ringChar R = 0
⊢ x - y = 0
Tactic:
rw [← sub_pow_ringChar _ _ hn] at h
State after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝² : x ^ ringChar R = y ^ ringChar R
h✝¹ h✝ : x ^ ringChar R - y ^ ringChar R = 0
h : (x - y) ^ ringChar R = 0
⊢ x - y = 0

State before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝² : x ^ ringChar R = y ^ ringChar R
h✝¹ h✝ : x ^ ringChar R - y ^ ringChar R = 0
h : (x - y) ^ ringChar R = 0
⊢ x - y = 0
Tactic:
exact pow_eq_zero h
State after:
no goals