-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem map.isLocalHom : IsLocalHom (map σ f) :=
  ⟨by
    rintro φ ⟨ψ, h⟩
    replace h := congr_arg (constantCoeff σ S) h
    rw [constantCoeff_map] at h
    have : IsUnit (constantCoeff σ S ↑ψ) := isUnit_constantCoeff _ ψ.isUnit
    rw [h] at this
    rcases isUnit_of_map_unit f _ this with ⟨c, hc⟩
    exact isUnit_of_mul_eq_one φ (invOfUnit φ c) (mul_invOfUnit φ c hc.symm)⟩

Proof state:
case intro
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : (constantCoeff σ S) ↑ψ = f ((constantCoeff σ R) φ)
⊢ IsUnit φ

Tactic:
have : IsUnit (constantCoeff σ S ↑ψ) := isUnit_constantCoeff _ ψ.isUnit

Result:
case intro
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : (constantCoeff σ S) ↑ψ = f ((constantCoeff σ R) φ)
this : IsUnit ((constantCoeff σ S) ↑ψ)
⊢ IsUnit φ

Proof state:
case intro
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : ↑ψ = (map σ f) φ
⊢ IsUnit φ

Tactic:
replace h := congr_arg (constantCoeff σ S) h

Result:
case intro
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : (constantCoeff σ S) ↑ψ = (constantCoeff σ S) ((map σ f) φ)
⊢ IsUnit φ

Proof state:
case intro.intro
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : (constantCoeff σ S) ↑ψ = f ((constantCoeff σ R) φ)
this : IsUnit (f ((constantCoeff σ R) φ))
c : Rˣ
hc : ↑c = (constantCoeff σ R) φ
⊢ IsUnit φ

Tactic:
exact isUnit_of_mul_eq_one φ (invOfUnit φ c) (mul_invOfUnit φ c hc.symm)

Result:
no goals

Proof state:
case intro
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : (constantCoeff σ S) ↑ψ = (constantCoeff σ S) ((map σ f) φ)
⊢ IsUnit φ

Tactic:
rw [constantCoeff_map] at h

Result:
case intro
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : (constantCoeff σ S) ↑ψ = f ((constantCoeff σ R) φ)
⊢ IsUnit φ

Proof state:
case intro
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : (constantCoeff σ S) ↑ψ = f ((constantCoeff σ R) φ)
this : IsUnit (f ((constantCoeff σ R) φ))
⊢ IsUnit φ

Tactic:
rcases isUnit_of_map_unit f _ this with ⟨c, hc⟩

Result:
case intro.intro
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : (constantCoeff σ S) ↑ψ = f ((constantCoeff σ R) φ)
this : IsUnit (f ((constantCoeff σ R) φ))
c : Rˣ
hc : ↑c = (constantCoeff σ R) φ
⊢ IsUnit φ

Proof state:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
⊢ ∀ (a : MvPowerSeries σ R), IsUnit ((map σ f) a) → IsUnit a

Tactic:
rintro φ ⟨ψ, h⟩

Result:
case intro
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : ↑ψ = (map σ f) φ
⊢ IsUnit φ

Proof state:
case intro
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : (constantCoeff σ S) ↑ψ = f ((constantCoeff σ R) φ)
this : IsUnit ((constantCoeff σ S) ↑ψ)
⊢ IsUnit φ

Tactic:
rw [h] at this

Result:
case intro
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
f : R →+* S
inst✝ : IsLocalHom f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : (constantCoeff σ S) ↑ψ = f ((constantCoeff σ R) φ)
this : IsUnit (f ((constantCoeff σ R) φ))
⊢ IsUnit φ