-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
lemma val_awayMap_eq_aux (a) : (awayMap 𝒜 hg hx a).val = awayMapAux 𝒜 ⟨_, hx⟩ a

Proof state:
case convert_2
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e✝ : ι
f g : A
hg : g ∈ 𝒜 e✝
x : A
hx : x = f * g
a : Away 𝒜 f
e : Away 𝒜 x ≃+* ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range := RingEquiv.ofLeftInverse ⋯
⊢ ↑(e (e.symm ⟨(HomogeneousLocalization.awayMapAux 𝒜 ⋯) a, ⋯⟩)) = (HomogeneousLocalization.awayMapAux 𝒜 ⋯) a

Tactic:
rw [e.apply_symm_apply]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e✝ : ι
f g : A
hg : g ∈ 𝒜 e✝
x : A
hx : x = f * g
a : Away 𝒜 f
e : Away 𝒜 x ≃+* ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range := RingEquiv.ofLeftInverse ⋯
⊢ (Exists.choose ⋯ ↑((Subring.inclusion ⋯) ((HomogeneousLocalization.awayMapAux 𝒜 ⋯).rangeRestrict a))).val =
    (HomogeneousLocalization.awayMapAux 𝒜 ⋯) a

Tactic:
convert_to (e (e.symm ⟨awayMapAux 𝒜 (f := f) ⟨_, hx⟩ a,
  range_awayMapAux_subset 𝒜 hg hx ⟨_, rfl⟩⟩)).1 = _

Result:
case convert_2
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e✝ : ι
f g : A
hg : g ∈ 𝒜 e✝
x : A
hx : x = f * g
a : Away 𝒜 f
e : Away 𝒜 x ≃+* ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range := RingEquiv.ofLeftInverse ⋯
⊢ ↑(e (e.symm ⟨(HomogeneousLocalization.awayMapAux 𝒜 ⋯) a, ⋯⟩)) = (HomogeneousLocalization.awayMapAux 𝒜 ⋯) a

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e✝ : ι
f g : A
hg : g ∈ 𝒜 e✝
x : A
hx : x = f * g
a : Away 𝒜 f
e : Away 𝒜 x ≃+* ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range := RingEquiv.ofLeftInverse ⋯
⊢ val ((awayMap 𝒜 hg hx) a) = (HomogeneousLocalization.awayMapAux 𝒜 ⋯) a

Tactic:
dsimp [awayMap]

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e✝ : ι
f g : A
hg : g ∈ 𝒜 e✝
x : A
hx : x = f * g
a : Away 𝒜 f
e : Away 𝒜 x ≃+* ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range := RingEquiv.ofLeftInverse ⋯
⊢ (Exists.choose ⋯ ↑((Subring.inclusion ⋯) ((HomogeneousLocalization.awayMapAux 𝒜 ⋯).rangeRestrict a))).val =
    (HomogeneousLocalization.awayMapAux 𝒜 ⋯) a

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : Away 𝒜 f
⊢ val ((awayMap 𝒜 hg hx) a) = (HomogeneousLocalization.awayMapAux 𝒜 ⋯) a

Tactic:
let e := RingEquiv.ofLeftInverse (f := algebraMap (Away 𝒜 x) (Localization.Away x))
  (h := (val_injective _).hasLeftInverse.choose_spec)

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e✝ : ι
f g : A
hg : g ∈ 𝒜 e✝
x : A
hx : x = f * g
a : Away 𝒜 f
e : Away 𝒜 x ≃+* ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range := RingEquiv.ofLeftInverse ⋯
⊢ val ((awayMap 𝒜 hg hx) a) = (HomogeneousLocalization.awayMapAux 𝒜 ⋯) a