awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
w : f ^ j * g ^ j ∈ 𝒜 (n + j • e)
⊢ x ^ j ∈ 𝒜 (n + j • e)

Tactic:
rw [hx, mul_pow]

Premises used: mul_pow
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) j ∈ 𝒜 n
w : g ^ j ∈ 𝒜 (j • e)
⊢ f ^ j * g ^ j ∈ 𝒜 (n + j • e)

Tactic:
apply SetLike.mul_mem_graded hb'

Premises used: SetLike.mul_mem_graded
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e_1 : ι
f g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
e : Away 𝒜 x ≃+* ↥(RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x))) :=
  RingEquiv.ofLeftInverse (g :=
    Exists.choose (p := fun (finv : (at Submonoid.powers x) → HomogeneousLocalization 𝒜 (Submonoid.powers x)) ↦
      Function.LeftInverse finv val) ⋯)
    ⋯
refine :
  LE.le.{u_2} (α := Subring (Localization.Away x)) (RingHom.range (R := Away 𝒜 f) (awayMapAux 𝒜 ⋯))
    (RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x)))
⊢ Away 𝒜 f →+* Away 𝒜 x

Tactic:
refine RingHom.comp (e.symm.toRingHom.comp (Subring.inclusion ?_))
    (awayMapAux 𝒜 (f := f) ⟨_, hx⟩).rangeRestrict

Premises used: Subring.inclusion, RingHom.rangeRestrict, RingHom.comp, RingEquiv.toRingHom, Exists.intro, _private.0.HomogeneousLocalization.awayMapAux, RingEquiv.symm
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e_1 : ι
f g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
e : Away 𝒜 x ≃+* ↥(RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x))) :=
  RingEquiv.ofLeftInverse (g :=
    Exists.choose (p := fun (finv : (at Submonoid.powers x) → HomogeneousLocalization 𝒜 (Submonoid.powers x)) ↦
      Function.LeftInverse finv val) ⋯)
    ⋯
⊢ LE.le.{u_2} (α := Subring (Localization.Away x)) (RingHom.range (R := Away 𝒜 f) (awayMapAux 𝒜 ⋯))
    (RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x)))

Tactic:
range_awayMapAux_subset 𝒜 hg hx

Premises used: HomogeneousLocalization.range_awayMapAux_subset, Quotient.liftOn', Set.Mem, setOf, Set.Subset, Set.range, HomogeneousLocalization.val
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e_1 : ι
f g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
e : Away 𝒜 x ≃+* ↥(RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x))) :=
  RingEquiv.ofLeftInverse (g :=
    Exists.choose (p := fun (finv : (at Submonoid.powers x) → HomogeneousLocalization 𝒜 (Submonoid.powers x)) ↦
      Function.LeftInverse finv val) ⋯)
    ⋯
⊢ LE.le.{u_2} (α := Subring (Localization.Away x)) (RingHom.range (R := Away 𝒜 f) (awayMapAux 𝒜 ⋯))
    (RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x)))

Tactic:
exact range_awayMapAux_subset 𝒜 hg hx

Premises used: HomogeneousLocalization.range_awayMapAux_subset
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e_1 : ι
f g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
a : Away 𝒜 f
e : Away 𝒜 x ≃+* ↥(RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x))) :=
  RingEquiv.ofLeftInverse (g :=
    Exists.choose (p := fun (finv : (at Submonoid.powers x) → HomogeneousLocalization 𝒜 (Submonoid.powers x)) ↦
      Function.LeftInverse finv val) ⋯)
    ⋯
convert_2 :
  Eq.{u_2 + 1} (α := Localization.Away x)
    ((↑((e : (a : Away 𝒜 x) → ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range)
            ((e.symm : (a : ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range) → Away 𝒜 x)
              (Subtype.mk (p := fun (x_1 : Localization.Away x) ↦
                Membership.mem (γ := Subring (Localization.Away x))
                  (RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x))) x_1)
                ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away x) a) ⋯))) :
        Localization.Away x) :
      Localization.Away x)
    ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away x) a : Localization.Away x)
⊢ Eq (α := at Submonoid.powers x)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      (Exists.choose (p := fun (finv : (at Submonoid.powers x) → HomogeneousLocalization 𝒜 (Submonoid.powers x)) ↦
        Function.LeftInverse finv val) ⋯
        (↑((Subring.inclusion ⋯ : (a : ↥(awayMapAux 𝒜 ⋯).range) → ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range)
              ((RingHom.rangeRestrict (awayMapAux 𝒜 ⋯) : (a : Away 𝒜 f) → ↥(awayMapAux 𝒜 ⋯).range) a)) :
          Localization.Away x)))
    ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away x) a)

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

Premises used: HomogeneousLocalization.range_awayMapAux_subset, Subtype.mk, Exists.intro, Subtype.val, DFunLike.coe, _private.0.HomogeneousLocalization.awayMapAux, RingEquiv.symm, rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e_1 : ι
f g : A
hg : g ∈ 𝒜 e_1
x : A
hx : x = f * g
a : Away 𝒜 f
e : Away 𝒜 x ≃+* ↥(RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x))) :=
  RingEquiv.ofLeftInverse (g :=
    Exists.choose (p := fun (finv : (at Submonoid.powers x) → HomogeneousLocalization 𝒜 (Submonoid.powers x)) ↦
      Function.LeftInverse finv val) ⋯)
    ⋯
convert_2 convert_2₁ :
  Eq.{u_2 + 1} (α := Localization.Away x)
    ((↑(Subtype.mk (p := fun (x_1 : Localization.Away x) ↦
            Membership.mem (γ := Subring (Localization.Away x))
              (RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x))) x_1)
            ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away x) a) ⋯) :
        Localization.Away x) :
      Localization.Away x)
    ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away x) a : Localization.Away x)
⊢ Eq.{u_2 + 1} (α := Localization.Away x)
    ((↑((e : (a : Away 𝒜 x) → ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range)
            ((e.symm : (a : ↥(algebraMap (Away 𝒜 x) (Localization.Away x)).range) → Away 𝒜 x)
              (Subtype.mk (p := fun (x_1 : Localization.Away x) ↦
                Membership.mem (γ := Subring (Localization.Away x))
                  (RingHom.range (R := Away 𝒜 x) (algebraMap (Away 𝒜 x) (Localization.Away x))) x_1)
                ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away x) a) ⋯))) :
        Localization.Away x) :
      Localization.Away x)
    ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away x) a : Localization.Away x)

Tactic:
rw [e.apply_symm_apply]

Premises used: RingEquiv.apply_symm_apply
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : Away 𝒜 f
rw :
  Eq.{u_2 + 1} (α := at Submonoid.powers x)
    ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away x) a : Localization.Away x)
    ((Localization.awayLift (algebraMap A (at Submonoid.powers x)) f ⋯ :
          (a : Localization.Away f) → at Submonoid.powers x)
        (val a) :
      at Submonoid.powers x)
⊢ Eq (α := at Submonoid.powers x)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) a))
    ((Localization.awayLift (algebraMap A (at Submonoid.powers x)) f ⋯ :
        (a : Localization.Away f) → at Submonoid.powers x)
      (val a))

Tactic:
rw [val_awayMap_eq_aux]

Premises used: HomogeneousLocalization.val_awayMap_eq_aux
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : Away 𝒜 f
⊢ Eq.{u_2 + 1} (α := at Submonoid.powers x)
    ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away x) a : Localization.Away x)
    ((Localization.awayLift (algebraMap A (at Submonoid.powers x)) f ⋯ :
          (a : Localization.Away f) → at Submonoid.powers x)
        (val a) :
      at Submonoid.powers x)

Tactic:
rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : ↥(𝒜 0)
a₁ :
  Eq (α := at Submonoid.powers x)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x)
        ((fromZeroRingHom 𝒜 (Submonoid.powers f) : (a : ↥(𝒜 0)) → HomogeneousLocalization 𝒜 (Submonoid.powers f)) a)))
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((fromZeroRingHom 𝒜 (Submonoid.powers x) : (a : ↥(𝒜 0)) → HomogeneousLocalization 𝒜 (Submonoid.powers x)) a))
⊢ Eq (α := Away 𝒜 x)
    ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x)
        ((fromZeroRingHom 𝒜 (Submonoid.powers f) : (a : ↥(𝒜 0)) → HomogeneousLocalization 𝒜 (Submonoid.powers f)) a) :
      Away 𝒜 x)
    ((fromZeroRingHom 𝒜 (Submonoid.powers x) : (a : ↥(𝒜 0)) → HomogeneousLocalization 𝒜 (Submonoid.powers x)) a :
      HomogeneousLocalization 𝒜 (Submonoid.powers x))

Tactic:
ext
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : ↥(𝒜 0)
a₁ :
  Eq (α := at Submonoid.powers x)
    ((Localization.awayLift (algebraMap A (at Submonoid.powers x)) f ⋯ :
          (a : Localization.Away f) → at Submonoid.powers x)
        (Localization.mk (↑a : A)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (↑1 : A) ⋯)) :
      at Submonoid.powers x)
    (Localization.mk (↑a : A)
        (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (↑1 : A) ⋯) :
      at Submonoid.powers x)
⊢ Eq (α := at Submonoid.powers x)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x)
        ((fromZeroRingHom 𝒜 (Submonoid.powers f) : (a : ↥(𝒜 0)) → HomogeneousLocalization 𝒜 (Submonoid.powers f)) a)))
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((fromZeroRingHom 𝒜 (Submonoid.powers x) : (a : ↥(𝒜 0)) → HomogeneousLocalization 𝒜 (Submonoid.powers x)) a))

Tactic:
simp only [fromZeroRingHom, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    val_awayMap, val_mk]

Premises used: OneHom.coe_mk, HomogeneousLocalization.val_awayMap, HomogeneousLocalization.val_mk, HomogeneousLocalization.fromZeroRingHom, MonoidHom.coe_mk, RingHom.coe_mk
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : ↥(𝒜 0)
⊢ Eq (α := at Submonoid.powers x)
    ((IsLocalization.lift (g := algebraMap A (at Submonoid.powers x)) ⋯ :
        (a : Localization.Away f) → at Submonoid.powers x)
      ((algebraMap A (Localization.Away f) : (a : A) → Localization.Away f) a.1))
    ((algebraMap A (at Submonoid.powers x) : (a : A) → at Submonoid.powers x) a.1)

Tactic:
IsLocalization.lift_eq _ _

Premises used: IsLocalization.lift_eq
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : ↥(𝒜 0)
⊢ Eq (α := at Submonoid.powers x)
    ((Localization.awayLift (algebraMap A (at Submonoid.powers x)) f ⋯ :
          (a : Localization.Away f) → at Submonoid.powers x)
        (Localization.mk (↑a : A)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (↑1 : A) ⋯)) :
      at Submonoid.powers x)
    (Localization.mk (↑a : A)
        (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (↑1 : A) ⋯) :
      at Submonoid.powers x)

Tactic:
convert! IsLocalization.lift_eq _ _

Premises used: IsLocalization.lift_eq
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
rw :
  Eq.{u_2 + 1} (α := at Submonoid.powers x)
    ((awayMapAux 𝒜 ⋯ : (a : Away 𝒜 f) → Localization.Away x)
        (mk { deg := n, num := a, den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ i) hi, den_mem := ⋯ }) :
      Localization.Away x)
    (Localization.mk ((↑a : A) * g ^ i)
        (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ i) ⋯) :
      at Submonoid.powers x)
rw₁ rw₂ :
  Eq (α := at Submonoid.powers x)
    (Localization.mk ((↑a : A) * g ^ i)
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ i) ⋯))
    (Localization.mk ((↑a : A) * g ^ i)
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ i) ⋯))
⊢ Eq (α := at Submonoid.powers x)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x)
        (mk { deg := n, num := a, den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ i) hi, den_mem := ⋯ })))
    (Localization.mk ((↑a : A) * g ^ i)
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ i) ⋯))

Tactic:
rw [val_awayMap_eq_aux, awayMapAux_mk 𝒜 (hx := hx)]

Premises used: HomogeneousLocalization.val_awayMap_eq_aux, HomogeneousLocalization.awayMapAux_mk
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
a : Away 𝒜 f
⊢ Eq (α := Away 𝒜 x) ((awayMapₐ 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) a : Away 𝒜 x)
    ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) a : Away 𝒜 x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
rw : a * g ^ n ∈ 𝒜 (n • d + n • e)
⊢ a * g ^ n ∈ 𝒜 (n • (d + e))

Tactic:
rw [smul_add]

Premises used: smul_add
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
⊢ a * g ^ n ∈ 𝒜 (n • d + n • e)

Tactic:
mul_mem_graded ha (pow_mem_graded n hg)

Premises used: SetLike.mul_mem_graded, SetLike.pow_mem_graded
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
⊢ a * g ^ n ∈ 𝒜 (n • d + n • e)

Tactic:
exact mul_mem_graded ha (pow_mem_graded n hg)

Premises used: SetLike.mul_mem_graded, SetLike.pow_mem_graded
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
a₁ :
  Eq (α := at Submonoid.powers x)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha)))
    (val (Away.mk 𝒜 ⋯ n (a * g ^ n) ⋯))
⊢ Eq (α := Away 𝒜 x) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha) : Away 𝒜 x)
    (Away.mk 𝒜 ⋯ n (a * g ^ n) ⋯ : Away 𝒜 x)

Tactic:
ext
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
⊢ Eq (α := at Submonoid.powers x)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha)))
    (val (Away.mk 𝒜 ⋯ n (a * g ^ n) ⋯))

Tactic:
val_awayMap_mk ..

Premises used: Localization.mk, Quotient.liftOn', HomogeneousLocalization.Away.mk, Quotient.mk', HomogeneousLocalization.val_awayMap_mk, OreLocalization.oreDiv, HomogeneousLocalization.NumDenSameDeg.embedding, HomogeneousLocalization.val
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : AddCommMonoid ι
inst_4 : DecidableEq ι
𝒜 : ι → σ
inst_5 : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
d : ι
n : ℕ
hf : f ∈ 𝒜 d
a : A
ha : a ∈ 𝒜 (n • d)
⊢ Eq (α := at Submonoid.powers x)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (Away.mk 𝒜 hf n a ha)))
    (val (Away.mk 𝒜 ⋯ n (a * g ^ n) ⋯))

Tactic:
exact val_awayMap_mk ..

Premises used: HomogeneousLocalization.val_awayMap_mk
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
⊢ g ^ d ∈ 𝒜 (d • e)

Tactic:
SetLike.pow_mem_graded d hg

Premises used: SetLike.pow_mem_graded
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
h : e • d = d • e
⊢ g ^ d ∈ 𝒜 (e • d)

Tactic:
convert! SetLike.pow_mem_graded d hg using 2

Premises used: SetLike.pow_mem_graded
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
⊢ e • d = d • e

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
⊢ e • d = d • e

Tactic:
exact mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
toIsLocalizationMap :
  Submonoid.IsLocalizationMap (M := Away 𝒜 f) (N := Away 𝒜 x) (Submonoid.powers (isLocalizationElem hf hg))
    (⇑(algebraMap (Away 𝒜 f) (Away 𝒜 x)) : (a : Away 𝒜 f) → Away 𝒜 x)
⊢ IsLocalization.Away (R := Away 𝒜 f) (isLocalizationElem hf hg) (Away 𝒜 x)

Tactic:
constructor
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
toIsLocalizationMap :
  ∀ (y : ↥(Submonoid.powers (isLocalizationElem hf hg))),
    IsUnit (M := Away 𝒜 x) ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑y : Away 𝒜 f) : Away 𝒜 x)
toIsLocalizationMap₁ :
  ∀ (z : Away 𝒜 x),
    ∃ (x_1 : Away 𝒜 f × ↥(Submonoid.powers (isLocalizationElem hf hg))),
      HMul.hMul (β := Away 𝒜 x) z
          ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) (↑x_1.2 : Away 𝒜 f) : Away 𝒜 x) =
        (algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1.1
toIsLocalizationMap₂ :
  ∀ {x_1 y : Away 𝒜 f},
    Eq (α := Away 𝒜 x) ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) x_1 : Away 𝒜 x)
        ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x) y : Away 𝒜 x) →
      ∃ (c : ↥(Submonoid.powers (isLocalizationElem hf hg))), (↑c : Away 𝒜 f) * x_1 = (↑c : Away 𝒜 f) * y
⊢ Submonoid.IsLocalizationMap (M := Away 𝒜 f) (N := Away 𝒜 x) (Submonoid.powers (isLocalizationElem hf hg))
    (⇑(algebraMap (Away 𝒜 f) (Away 𝒜 x)) : (a : Away 𝒜 f) → Away 𝒜 x)

Tactic:
constructor
-- Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Goal:
A : Type u_2
σ : Type u_3
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := RingHom.toAlgebra (awayMap 𝒜 hg hx)
n : ℕ
toIsLocalizationMap :
  IsUnit
    (HPow.hPow (α := Away 𝒜 x) ((awayMap 𝒜 hg hx : (a : Away 𝒜 f) → Away 𝒜 x) (isLocalizationElem hf hg) : Away 𝒜 x) n)
⊢ IsUnit (M := Away 𝒜 x)
    ((algebraMap (Away 𝒜 f) (Away 𝒜 x) : (a : Away 𝒜 f) → Away 𝒜 x)
        (↑(Subtype.mk (p := fun (x : Away 𝒜 f) ↦
              Membership.mem (γ := Submonoid (Away 𝒜 f)) (Submonoid.powers (isLocalizationElem hf hg)) x)
              ((fun (x : ℕ) ↦ HPow.hPow (α := Away 𝒜 f) (isLocalizationElem hf hg) x) n) ⋯) :
          Away 𝒜 f) :
      Away 𝒜 x)

Tactic:
rw [map_pow, RingHom.algebraMap_toAlgebra]

Premises used: map_pow, RingHom.algebraMap_toAlgebra