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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
⊢ Eq (α := HomogeneousLocalization ℬ Q)
    (Quotient.mk''
      { deg := NumDenSameDeg.deg.{u_1, u_2, u_3} (σ := σ) (𝒜 := 𝒜) (x := P) 1,
        num :=
          Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ (NumDenSameDeg.deg.{u_1, u_2, u_3} (σ := σ) (𝒜 := 𝒜) (x := P) 1)) 1 ⋯,
        den :=
          Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ (NumDenSameDeg.deg.{u_1, u_2, u_3} (σ := σ) (𝒜 := 𝒜) (x := P) 1)) 1 ⋯,
        den_mem := ⋯ })
    1

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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
simp :
  Quotient.mk''
      { deg := (x * y).deg,
        num :=
          Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ (x * y).deg)
            (HMul.hMul (α := B) (β := B) ((g : (a : A) → B) (↑x.num : A) : B) ((g : (a : A) → B) (↑y.num : A) : B)) ⋯,
        den :=
          Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ (x * y).deg)
            (HMul.hMul (α := B) (β := B) ((g : (a : A) → B) (↑x.den : A) : B) ((g : (a : A) → B) (↑y.den : A) : B)) ⋯,
        den_mem := ⋯ } =
    mk
      (HMul.hMul (α := NumDenSameDeg ℬ Q)
        { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
          den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ :
          NumDenSameDeg ℬ Q }
        { deg := y.deg, num := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ y.deg) ((g : (a : A) → B) (↑y.num : A)) ⋯,
          den := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ y.deg) ((g : (a : A) → B) (↑y.den : A)) ⋯, den_mem := ⋯ :
          NumDenSameDeg ℬ Q })
⊢ Quotient.map'
      (fun (x : NumDenSameDeg 𝒜 P) ↦
        { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
          den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ })
      ⋯ (HMul.hMul (α := HomogeneousLocalization 𝒜 P) (Quotient.mk'' x) (Quotient.mk'' y)) =
    HMul.hMul (α := HomogeneousLocalization ℬ Q)
      (Quotient.map' (s₁ := Setoid.ker (embedding 𝒜 P))
        (fun (x : NumDenSameDeg 𝒜 P) ↦
          { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ :
            NumDenSameDeg ℬ Q })
        ⋯ (Quotient.mk'' x))
      (Quotient.map' (s₁ := Setoid.ker (embedding 𝒜 P))
        (fun (x : NumDenSameDeg 𝒜 P) ↦
          { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ :
            NumDenSameDeg ℬ Q })
        ⋯ (Quotient.mk'' y))

Tactic:
simp only [← mk_mul, Quotient.map'_mk'', num_mul, map_mul, den_mul]

Premises used: HomogeneousLocalization.NumDenSameDeg.num_mul, HomogeneousLocalization.NumDenSameDeg.den_mul, HomogeneousLocalization.mk_mul, map_mul, Quotient.map'_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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
⊢ Quotient.mk''
      { deg := (x * y).deg,
        num :=
          Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ (x * y).deg)
            (HMul.hMul (α := B) (β := B) ((g : (a : A) → B) (↑x.num : A) : B) ((g : (a : A) → B) (↑y.num : A) : B)) ⋯,
        den :=
          Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ (x * y).deg)
            (HMul.hMul (α := B) (β := B) ((g : (a : A) → B) (↑x.den : A) : B) ((g : (a : A) → B) (↑y.den : A) : B)) ⋯,
        den_mem := ⋯ } =
    mk
      (HMul.hMul (α := NumDenSameDeg ℬ Q)
        { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
          den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ :
          NumDenSameDeg ℬ Q }
        { deg := y.deg, num := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ y.deg) ((g : (a : A) → B) (↑y.num : A)) ⋯,
          den := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ y.deg) ((g : (a : A) → B) (↑y.den : A)) ⋯, den_mem := ⋯ :
          NumDenSameDeg ℬ Q })

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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
simp :
  Eq (α := HomogeneousLocalization ℬ Q)
    (Quotient.mk''
      { deg := 0, num := (Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ 0) 0 ⋯ : ↥(ℬ 0)),
        den := (Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ 0) 1 ⋯ : ↥(ℬ 0)), den_mem := ⋯ })
    0
⊢ Eq (α := HomogeneousLocalization ℬ Q)
    (Quotient.map' (s₁ := Setoid.ker (embedding 𝒜 P))
      (fun (x : NumDenSameDeg 𝒜 P) ↦
        { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
          den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ })
      ⋯ 0)
    0

Tactic:
simp only [← mk_zero (𝒜 := 𝒜), Quotient.map'_mk'', deg_zero,
    num_zero, ZeroMemClass.coe_zero, map_zero, den_zero, map_one]

Premises used: HomogeneousLocalization.mk_zero, map_zero, HomogeneousLocalization.NumDenSameDeg.deg_zero, ZeroMemClass.coe_zero, map_one, Quotient.map'_mk'', HomogeneousLocalization.NumDenSameDeg.num_zero, HomogeneousLocalization.NumDenSameDeg.den_zero
-- 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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
⊢ Eq (α := HomogeneousLocalization ℬ Q)
    (Quotient.mk''
      { deg := 0, num := (Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ 0) 0 ⋯ : ↥(ℬ 0)),
        den := (Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ 0) 1 ⋯ : ↥(ℬ 0)), den_mem := ⋯ })
    0

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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
⊢ Quotient.mk''
      { deg := (x + y).deg,
        num :=
          Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ (x + y).deg)
            (HMul.hMul (α := B) (β := B) ((g : (a : A) → B) (↑x.den : A) : B) ((g : (a : A) → B) (↑y.num : A) : B) +
              HMul.hMul (α := B) (β := B) ((g : (a : A) → B) (↑y.den : A) : B) ((g : (a : A) → B) (↑x.num : A) : B))
            ⋯,
        den :=
          Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ (x + y).deg)
            (HMul.hMul (α := B) (β := B) ((g : (a : A) → B) (↑x.den : A) : B) ((g : (a : A) → B) (↑y.den : A) : B)) ⋯,
        den_mem := ⋯ } =
    mk
      (HAdd.hAdd (α := NumDenSameDeg ℬ Q)
        { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
          den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ :
          NumDenSameDeg ℬ Q }
        { deg := y.deg, num := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ y.deg) ((g : (a : A) → B) (↑y.num : A)) ⋯,
          den := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ y.deg) ((g : (a : A) → B) (↑y.den : A)) ⋯, den_mem := ⋯ :
          NumDenSameDeg ℬ Q })

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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x : NumDenSameDeg 𝒜 P
⊢ Eq (α := HomogeneousLocalization ℬ Q)
    ((map g comap_le : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization ℬ Q) (mk x) :
      HomogeneousLocalization ℬ Q)
    (mk
        { deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.num : A)) ⋯,
          den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((g : (a : A) → B) (↑x.den : A)) ⋯, den_mem := ⋯ } :
      HomogeneousLocalization ℬ Q)

Tactic:
rfl

Premises used: Quot.map, Quotient.map', 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 𝒜
P : Submonoid A
a :
  ∀ (x : HomogeneousLocalization 𝒜 P),
    Eq (α := Localization (M := A) P)
      (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
        (((map (GradedRingHom.id 𝒜) ⋯ : HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒜 P) :
            (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒜 P)
          x))
      (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
        ((RingHom.id (HomogeneousLocalization 𝒜 P) : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒜 P)
          x))
⊢ Eq (α := HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒜 P)
    (map (GradedRingHom.id 𝒜) ⋯ : HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒜 P)
    (RingHom.id (HomogeneousLocalization 𝒜 P) : HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒜 P)

Tactic:
ext x
-- 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 𝒜
P : Submonoid A
x : HomogeneousLocalization 𝒜 P
a :
  ∀ (c : NumDenSameDeg 𝒜 P),
    Eq (α := Localization (M := A) P)
      (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
        (((map (GradedRingHom.id 𝒜) ⋯ : HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒜 P) :
            (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒜 P)
          (mk c)))
      (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
        ((RingHom.id (HomogeneousLocalization 𝒜 P) : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒜 P)
          (mk c)))
⊢ Eq (α := Localization (M := A) P)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      (((map (GradedRingHom.id 𝒜) ⋯ : HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒜 P) :
          (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒜 P)
        x))
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((RingHom.id (HomogeneousLocalization 𝒜 P) : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒜 P) x))

Tactic:
obtain ⟨c, rfl⟩ := x.mk_surjective

Premises used: HomogeneousLocalization.mk_surjective, 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 𝒜
P : Submonoid A
c : NumDenSameDeg 𝒜 P
⊢ Eq (α := Localization (M := A) P)
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      (((map (GradedRingHom.id 𝒜) ⋯ : HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒜 P) :
          (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒜 P)
        (mk c)))
    (val.{u_1, u_2, u_3} (ι := ι) (σ := σ) (𝒜 := 𝒜)
      ((RingHom.id (HomogeneousLocalization 𝒜 P) : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒜 P)
        (mk c)))

Tactic:
simp [map_mk]

Premises used: HomogeneousLocalization.map_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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
P : Submonoid A
Q : Submonoid B
R : Submonoid C
hpq : P ≤ Submonoid.comap f Q
hqr : Q ≤ Submonoid.comap g R
a :
  ∀ (x : HomogeneousLocalization 𝒜 P),
    Eq (α := Localization (M := C) R)
      (val.{u_1, u_6, u_7} (ι := ι) (σ := ψ) (𝒜 := 𝒞)
        ((map (g.comp f) ⋯ : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒞 R) x))
      (val.{u_1, u_6, u_7} (ι := ι) (σ := ψ) (𝒜 := 𝒞)
        ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (map g hqr) (map f hpq) :
            (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒞 R)
          x))
⊢ Eq (α := HomogeneousLocalization 𝒜 P →+* HomogeneousLocalization 𝒞 R) (map (g.comp f) ⋯)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (map g hqr) (map f hpq))

Tactic:
ext x
-- 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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
P : Submonoid A
Q : Submonoid B
R : Submonoid C
hpq : P ≤ Submonoid.comap f Q
hqr : Q ≤ Submonoid.comap g R
x : HomogeneousLocalization 𝒜 P
a :
  ∀ (c : NumDenSameDeg 𝒜 P),
    Eq (α := Localization (M := C) R)
      (val.{u_1, u_6, u_7} (ι := ι) (σ := ψ) (𝒜 := 𝒞)
        ((map (g.comp f) ⋯ : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒞 R) (mk c)))
      (val.{u_1, u_6, u_7} (ι := ι) (σ := ψ) (𝒜 := 𝒞)
        ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (map g hqr) (map f hpq) :
            (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒞 R)
          (mk c)))
⊢ Eq (α := Localization (M := C) R)
    (val.{u_1, u_6, u_7} (ι := ι) (σ := ψ) (𝒜 := 𝒞)
      ((map (g.comp f) ⋯ : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒞 R) x))
    (val.{u_1, u_6, u_7} (ι := ι) (σ := ψ) (𝒜 := 𝒞)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (map g hqr) (map f hpq) :
          (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒞 R)
        x))

Tactic:
obtain ⟨c, rfl⟩ := x.mk_surjective

Premises used: HomogeneousLocalization.mk_surjective, 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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
P : Submonoid A
Q : Submonoid B
R : Submonoid C
hpq : P ≤ Submonoid.comap f Q
hqr : Q ≤ Submonoid.comap g R
c : NumDenSameDeg 𝒜 P
⊢ Eq (α := Localization (M := C) R)
    (val.{u_1, u_6, u_7} (ι := ι) (σ := ψ) (𝒜 := 𝒞)
      ((map (g.comp f) ⋯ : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒞 R) (mk c)))
    (val.{u_1, u_6, u_7} (ι := ι) (σ := ψ) (𝒜 := 𝒞)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (map g hqr) (map f hpq) :
          (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒞 R)
        (mk c)))

Tactic:
simp [map_mk]

Premises used: HomogeneousLocalization.map_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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
P : Submonoid A
Q : Submonoid B
R : Submonoid C
hpq : P ≤ Submonoid.comap f Q
hqr : Q ≤ Submonoid.comap g R
x : HomogeneousLocalization 𝒜 P
⊢ Eq (α := HomogeneousLocalization 𝒞 R)
    ((map g hqr : (a : HomogeneousLocalization ℬ Q) → HomogeneousLocalization 𝒞 R)
        ((map f hpq : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization ℬ Q) x) :
      HomogeneousLocalization 𝒞 R)
    ((map (g.comp f) ⋯ : (a : HomogeneousLocalization 𝒜 P) → HomogeneousLocalization 𝒞 R) x :
      HomogeneousLocalization 𝒞 R)

Tactic:
congr($(map_comp hpq hqr |>.symm) x)

Premises used: congrArg, id, HomogeneousLocalization.map_comp, Eq.symm, DFunLike.coe
-- 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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
f : A
n : ℕ
⊢ Eq.{u_4 + 1} (α := B) ((fun (x : ℕ) ↦ HPow.hPow (α := B) ((g : (a : A) → B) f : B) x) n : B)
    ((g : (a : A) → B) ((fun (x : ℕ) ↦ f ^ x) n) : B)

Tactic:
simp
-- 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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
f : A
n : ℕ
⊢ Membership.mem (γ := Submonoid A) (Submonoid.comap (N := B) g (Submonoid.powers ((g : (a : A) → B) f) : Submonoid B))
    ((fun (x : ℕ) ↦ f ^ x) n)

Tactic:
exact ⟨n, by simp⟩
-- 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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
d : ι
g : 𝒜 →+*ᵍ ℬ
f : A
hf : f ∈ 𝒜 d
n : ℕ
x : A
hx : x ∈ 𝒜 (n • d)
⊢ Eq (α := Away.{u_1, u_4, u_5} (A := B) ℬ ((g : (a : A) → B) f : B))
    ((Away.map g f : (a : Away 𝒜 f) → Away ℬ ((g : (a : A) → B) f)) (Away.mk 𝒜 hf n x hx) :
      Away.{u_1, u_4, u_5} (A := B) ℬ ((g : (a : A) → B) f : B))
    (Away.mk ℬ ⋯ n ((g : (a : A) → B) x) ⋯ : Away.{u_1, u_4, u_5} (A := B) ℬ ((g : (a : A) → B) f : B))

Tactic:
simp [Away.map, Away.mk, HomogeneousLocalization.map_mk]

Premises used: HomogeneousLocalization.map_mk, HomogeneousLocalization.Away.map, HomogeneousLocalization.Away.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 𝒜
f : A
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
HomogeneousLocalization.map_id ..

Premises used: Set.Mem, HomogeneousLocalization.Away.map, HomogeneousLocalization.map_id
-- 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 𝒜
B : Type u_4
τ : Type u_5
inst_6 : CommRing B
inst_7 : SetLike τ B
inst_8 : AddSubgroupClass τ B
ℬ : ι → τ
inst_9 : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst_10 : CommRing C
inst_11 : SetLike ψ C
inst_12 : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst_13 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
s : A
⊢ Eq (α := Away 𝒜 s →+* Away.{u_1, u_6, u_7} (A := C) 𝒞 ((g.comp f : (a : A) → C) s : C)) (Away.map (g.comp f) s)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Away.map g ((f : (a : A) → B) s)) (Away.map f s))

Tactic:
HomogeneousLocalization.map_comp ..

Premises used: Set.Mem, HomogeneousLocalization.Away.map, HomogeneousLocalization.map_comp