-- Mathlib/RingTheory/Valuation/ValExtension.lean
theorem instIsLocalHomValuationInteger {S ΓS: Type*} [CommRing S]
    [LinearOrderedCommGroupWithZero ΓS]
    [Algebra R S] [IsLocalHom (algebraMap R S)] {vS : Valuation S ΓS}
    [IsValExtension vR vS] : IsLocalHom (algebraMap vR.integer vS.integer) where
  map_nonunit r hr

Proof state:
case hx
R : Type u_1
inst✝⁶ : CommRing R
ΓR : Type u_6
inst✝⁵ : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst✝⁴ : CommRing S
inst✝³ : LinearOrderedCommGroupWithZero ΓS
inst✝² : Algebra R S
inst✝¹ : IsLocalHom (algebraMap R S)
vS : Valuation S ΓS
inst✝ : IsValExtension vR vS
r : ↥vR.integer
hr : IsUnit ((algebraMap ↥vR.integer ↥vS.integer) r)
⊢ IsUnit ((algebraMap (↥vR.integer) R) r)

Tactic:
exact (isUnit_map_iff (algebraMap R S) _).mp (hr.map (algebraMap _ S))

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
ΓR : Type u_6
inst✝⁵ : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst✝⁴ : CommRing S
inst✝³ : LinearOrderedCommGroupWithZero ΓS
inst✝² : Algebra R S
inst✝¹ : IsLocalHom (algebraMap R S)
vS : Valuation S ΓS
inst✝ : IsValExtension vR vS
r : ↥vR.integer
hr : IsUnit ((algebraMap ↥vR.integer ↥vS.integer) r)
⊢ IsUnit r

Tactic:
apply (Valuation.integer.integers (v := vR)).isUnit_of_one

Result:
case hx
R : Type u_1
inst✝⁶ : CommRing R
ΓR : Type u_6
inst✝⁵ : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst✝⁴ : CommRing S
inst✝³ : LinearOrderedCommGroupWithZero ΓS
inst✝² : Algebra R S
inst✝¹ : IsLocalHom (algebraMap R S)
vS : Valuation S ΓS
inst✝ : IsValExtension vR vS
r : ↥vR.integer
hr : IsUnit ((algebraMap ↥vR.integer ↥vS.integer) r)
⊢ IsUnit ((algebraMap (↥vR.integer) R) r)

case hvx
R : Type u_1
inst✝⁶ : CommRing R
ΓR : Type u_6
inst✝⁵ : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst✝⁴ : CommRing S
inst✝³ : LinearOrderedCommGroupWithZero ΓS
inst✝² : Algebra R S
inst✝¹ : IsLocalHom (algebraMap R S)
vS : Valuation S ΓS
inst✝ : IsValExtension vR vS
r : ↥vR.integer
hr : IsUnit ((algebraMap ↥vR.integer ↥vS.integer) r)
⊢ vR ((algebraMap (↥vR.integer) R) r) = 1

Proof state:
case hvx
R : Type u_1
inst✝⁶ : CommRing R
ΓR : Type u_6
inst✝⁵ : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst✝⁴ : CommRing S
inst✝³ : LinearOrderedCommGroupWithZero ΓS
inst✝² : Algebra R S
inst✝¹ : IsLocalHom (algebraMap R S)
vS : Valuation S ΓS
inst✝ : IsValExtension vR vS
r : ↥vR.integer
hr : vS ((algebraMap (↥vS.integer) S) ((algebraMap ↥vR.integer ↥vS.integer) r)) = 1
⊢ vR ((algebraMap (↥vR.integer) R) r) = 1

Tactic:
exact (val_map_eq_one_iff vR vS _).mp hr

Result:
no goals

Proof state:
case hvx
R : Type u_1
inst✝⁶ : CommRing R
ΓR : Type u_6
inst✝⁵ : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst✝⁴ : CommRing S
inst✝³ : LinearOrderedCommGroupWithZero ΓS
inst✝² : Algebra R S
inst✝¹ : IsLocalHom (algebraMap R S)
vS : Valuation S ΓS
inst✝ : IsValExtension vR vS
r : ↥vR.integer
hr : IsUnit ((algebraMap ↥vR.integer ↥vS.integer) r)
⊢ vR ((algebraMap (↥vR.integer) R) r) = 1

Tactic:
apply (Valuation.integer.integers (v := vS)).one_of_isUnit at hr

Result:
case hvx
R : Type u_1
inst✝⁶ : CommRing R
ΓR : Type u_6
inst✝⁵ : LinearOrderedCommGroupWithZero ΓR
vR : Valuation R ΓR
S : Type u_9
ΓS : Type u_10
inst✝⁴ : CommRing S
inst✝³ : LinearOrderedCommGroupWithZero ΓS
inst✝² : Algebra R S
inst✝¹ : IsLocalHom (algebraMap R S)
vS : Valuation S ΓS
inst✝ : IsValExtension vR vS
r : ↥vR.integer
hr : vS ((algebraMap (↥vS.integer) S) ((algebraMap ↥vR.integer ↥vS.integer) r)) = 1
⊢ vR ((algebraMap (↥vR.integer) R) r) = 1