-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
lemma awayMapAux_mk (n a i hi) :
    awayMapAux 𝒜 ⟨_, hx⟩ (mk ⟨n, a, ⟨f ^ i, hi⟩, ⟨i, rfl⟩⟩) =
      Localization.mk (a * g ^ i) ⟨x ^ i, (Submonoid.mem_powers_iff _ _).mpr ⟨i, rfl⟩⟩

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 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ (algebraMap A (Localization.Away x)) f * Localization.mk g ⟨f * g, ⋯⟩ = 1

Tactic:
rw [← Algebra.smul_def, Localization.smul_mk]

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 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ Localization.mk (f • g) ⟨f * g, ⋯⟩ = 1

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 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ x ^ 1 = f * g

Tactic:
simp [hx]

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 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
this : (algebraMap A (Localization.Away x)) f * Localization.mk g ⟨f * g, ⋯⟩ = 1
⊢ Localization.mk (↑a • g ^ i) (⟨f * g, ⋯⟩ ^ i) = Localization.mk (↑a * g ^ i) ⟨x ^ i, ⋯⟩

Tactic:
subst hx

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 𝒜
f g : A
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
this : (algebraMap A (Localization.Away (f * g))) f * Localization.mk g ⟨f * g, ⋯⟩ = 1
⊢ Localization.mk (↑a • g ^ i) (⟨f * g, ⋯⟩ ^ i) = Localization.mk (↑a * g ^ i) ⟨(f * g) ^ i, ⋯⟩

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 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
this : (algebraMap A (Localization.Away x)) f * Localization.mk g ⟨f * g, ⋯⟩ = 1
⊢ (HomogeneousLocalization.awayMapAux 𝒜 ⋯) (mk { deg := n, num := a, den := ⟨f ^ i, hi⟩, den_mem := ⋯ }) =
    Localization.mk (↑a * g ^ i) ⟨x ^ i, ⋯⟩

Tactic:
simp [awayMapAux]

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 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
this : (algebraMap A (Localization.Away x)) f * Localization.mk g ⟨f * g, ⋯⟩ = 1
⊢ (Localization.awayLift (algebraMap A (Localization.Away x)) f ⋯) (Localization.mk ↑a ⟨f ^ i, ⋯⟩) =
    Localization.mk (↑a * g ^ i) ⟨x ^ i, ⋯⟩

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 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ (HomogeneousLocalization.awayMapAux 𝒜 ⋯) (mk { deg := n, num := a, den := ⟨f ^ i, hi⟩, den_mem := ⋯ }) =
    Localization.mk (↑a * g ^ i) ⟨x ^ i, ⋯⟩

Tactic:
have : algebraMap A (Localization.Away x) f *
  (Localization.mk g ⟨f * g, (Submonoid.mem_powers_iff _ _).mpr ⟨1, by simp [hx]⟩⟩) = 1 := by
  rw [← Algebra.smul_def, Localization.smul_mk]
  exact Localization.mk_self ⟨f*g, _⟩

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 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
this : (algebraMap A (Localization.Away x)) f * Localization.mk g ⟨f * g, ⋯⟩ = 1
⊢ (HomogeneousLocalization.awayMapAux 𝒜 ⋯) (mk { deg := n, num := a, den := ⟨f ^ i, hi⟩, den_mem := ⋯ }) =
    Localization.mk (↑a * g ^ i) ⟨x ^ i, ⋯⟩

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 𝒜
f g : A
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
this : (algebraMap A (Localization.Away (f * g))) f * Localization.mk g ⟨f * g, ⋯⟩ = 1
⊢ Localization.mk (↑a • g ^ i) (⟨f * g, ⋯⟩ ^ i) = Localization.mk (↑a * g ^ i) ⟨(f * g) ^ i, ⋯⟩

Tactic:
rfl

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 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
this : (algebraMap A (Localization.Away x)) f * Localization.mk g ⟨f * g, ⋯⟩ = 1
⊢ (Localization.awayLift (algebraMap A (Localization.Away x)) f ⋯) (Localization.mk ↑a ⟨f ^ i, ⋯⟩) =
    Localization.mk (↑a * g ^ i) ⟨x ^ i, ⋯⟩

Tactic:
rw [Localization.awayLift_mk (hv := this), ← Algebra.smul_def,
  Localization.mk_pow, Localization.smul_mk]

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 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
this : (algebraMap A (Localization.Away x)) f * Localization.mk g ⟨f * g, ⋯⟩ = 1
⊢ Localization.mk (↑a • g ^ i) (⟨f * g, ⋯⟩ ^ i) = Localization.mk (↑a * g ^ i) ⟨x ^ i, ⋯⟩

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 𝒜
f g x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ Localization.mk (f • g) ⟨f * g, ⋯⟩ = 1

Tactic:
exact Localization.mk_self ⟨f*g, _⟩

Result:
no goals