Theorem: ENatValRing.pth_root_pos_of_pos (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
⊢ v evr.valtn (pth_root evr r) > 0
Tactic:
suffices 0 < evr.valtn (evr.pth_root r ^ evr.residue_char) by
  . simp at this
    exact this.2
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
⊢ 0 < v evr.valtn (pth_root evr r ^ evr.residue_char)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
⊢ 0 < v evr.valtn (pth_root evr r ^ evr.residue_char)
Tactic:
have :
  min (SurjVal.v evr.valtn (pth_root evr r ^ evr.residue_char - r)) (SurjVal.v evr.valtn r) > 0 :=
min_rec' (LT.lt 0) (evr.pth_root_spec.resolve_left hchar r) ha
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
this : min (v evr.valtn (pth_root evr r ^ evr.residue_char - r)) (v evr.valtn r) > 0
⊢ 0 < v evr.valtn (pth_root evr r ^ evr.residue_char)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
this : min (v evr.valtn (pth_root evr r ^ evr.residue_char - r)) (v evr.valtn r) > 0
⊢ 0 < v evr.valtn (pth_root evr r ^ evr.residue_char)
Tactic:
have := this.trans_le (evr.valtn.v_add_ge_min_v (evr.pth_root r ^ evr.residue_char - r) r)
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
this✝ : min (v evr.valtn (pth_root evr r ^ evr.residue_char - r)) (v evr.valtn r) > 0
this : 0 < v evr.valtn (pth_root evr r ^ evr.residue_char - r + r)
⊢ 0 < v evr.valtn (pth_root evr r ^ evr.residue_char)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
this✝ : min (v evr.valtn (pth_root evr r ^ evr.residue_char - r)) (v evr.valtn r) > 0
this : 0 < v evr.valtn (pth_root evr r ^ evr.residue_char - r + r)
⊢ 0 < v evr.valtn (pth_root evr r ^ evr.residue_char)
Tactic:
simpa using this
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
this : 0 < v evr.valtn (pth_root evr r ^ evr.residue_char)
⊢ v evr.valtn (pth_root evr r) > 0
Tactic:
. simp at this
  exact this.2
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
this : 0 < v evr.valtn (pth_root evr r ^ evr.residue_char)
⊢ v evr.valtn (pth_root evr r) > 0
Tactic:
simp at this
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
this : 0 < evr.residue_char ∧ 0 < v evr.valtn (pth_root evr r)
⊢ v evr.valtn (pth_root evr r) > 0

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
this : 0 < evr.residue_char ∧ 0 < v evr.valtn (pth_root evr r)
⊢ v evr.valtn (pth_root evr r) > 0
Tactic:
exact this.2
State after:
no goals