awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
refine :
  ∀ (x : ↥(Proj 𝒜)) (hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x),
    ∃ (i : ι), Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x
refine₁ :
  ∀ (x : ↥(Proj 𝒜)) (hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x)
    (H : ∀ (i : ι), x ∉ basicOpen 𝒜 (f i)), False
⊢ Eq.{u + 1} (α := (Proj 𝒜).Opens) (⨆ (i : ι), basicOpen 𝒜 (f i)) ⊤
have refine₂ : ∀ (x : ↥(Proj 𝒜)) (hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x)
  (H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal), False
Tactic: classical
  refine top_le_iff.mp fun x hx ↦ TopologicalSpace.Opens.mem_iSup.mpr ?_
  by_contra! H
  simp only [mem_basicOpen, Decidable.not_not] at H
  refine x.not_irrelevant_le (hf.trans ?_)
  rwa [Ideal.span_le, Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
refine :
  ∀ (x : ↥(Proj 𝒜)) (hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x),
    ∃ (i : ι), Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x
refine₁ :
  ∀ (x : ↥(Proj 𝒜)) (hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x)
    (H : ∀ (i : ι), x ∉ basicOpen 𝒜 (f i)), False
refine₂ :
  ∀ (x : ↥(Proj 𝒜)) (hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x)
    (H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal), False
⊢ Eq.{u + 1} (α := (Proj 𝒜).Opens) (⨆ (i : ι), basicOpen 𝒜 (f i)) ⊤
have refine₃ : ∀ (x : ↥(Proj 𝒜)) (hx : Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) ⊤ x)
  (H : ∀ (i : ι), f i ∈ x.asHomogeneousIdeal), Ideal.span (Set.range f) ≤ x.asHomogeneousIdeal.toSubmodule
Tactic: classical
  refine top_le_iff.mp fun x hx ↦ TopologicalSpace.Opens.mem_iSup.mpr ?_
  by_contra! H
  simp only [mem_basicOpen, Decidable.not_not] at H
  refine x.not_irrelevant_le (hf.trans ?_)
  rwa [Ideal.span_le, Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
⊢ Eq.{u + 1} (α := (Proj 𝒜).Opens) (⨆ (i : ι), basicOpen 𝒜 (f i)) ⊤
have hf₁ : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
Tactic: apply Proj.iSup_basicOpen_eq_top
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
hx : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) x
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f)) x
have h : x = HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A)
Tactic: convert_to x - GradedRing.projZeroRingHom 𝒜 x ∈ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
hx : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) x
h : x = HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A)
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f)) x
have hf₁ : Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
  (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
Tactic: convert_to x - GradedRing.projZeroRingHom 𝒜 x ∈ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
hx : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) x
⊢ x = HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A)
have h : x =
  x -
    (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          0) :
      A)
Tactic: rw [GradedRing.projZeroRingHom_apply, ← GradedRing.proj_apply,
      (HomogeneousIdeal.mem_irrelevant_iff _ _).mp hx, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
hx : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) x
h :
  x =
    x -
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            0) :
        A)
⊢ x = HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A)
have h₁ : x = HSub.hSub (β := A) x ((GradedRing.proj 𝒜 0 : (a : A) → A) x : A)
Tactic: rw [GradedRing.projZeroRingHom_apply, ← GradedRing.proj_apply,
      (HomogeneousIdeal.mem_irrelevant_iff _ _).mp hx, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
hx : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) x
h :
  x =
    x -
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            0) :
        A)
h₁ : x = HSub.hSub (β := A) x ((GradedRing.proj 𝒜 0 : (a : A) → A) x : A)
⊢ x = HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A)
have h₂ : x = x - 0
Tactic: rw [GradedRing.projZeroRingHom_apply, ← GradedRing.proj_apply,
      (HomogeneousIdeal.mem_irrelevant_iff _ _).mp hx, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
hx : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) x
h :
  x =
    x -
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            0) :
        A)
h₁ : x = HSub.hSub (β := A) x ((GradedRing.proj 𝒜 0 : (a : A) → A) x : A)
h₂ : x = x - 0
⊢ x = HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A)
have h₃ : x = x
Tactic: rw [GradedRing.projZeroRingHom_apply, ← GradedRing.proj_apply,
      (HomogeneousIdeal.mem_irrelevant_iff _ _).mp hx, sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (hypothesis)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
have this : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x
Tactic: have := (eq_iff_iff.mp congr(x ∈ $hf)).mpr trivial
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x_1 x : A
hx : x ∈ Set.range f
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
have hf₁ : ∀ (i : ι),
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) (f i) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (f i) : A))
Tactic: obtain ⟨i, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
i : ι
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) (f i) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (f i) : A))
have hf₁ : ∀ (n : ℕ) (hn : f i ∈ 𝒜 n),
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) (f i) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (f i) : A))
Tactic: obtain ⟨n, hn⟩ := hfn i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) (f i) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (f i) : A))
have hf₁ : Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
  (f i -
    (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) (f i) :
              DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          0) :
      A))
Tactic: rw [GradedRing.projZeroRingHom_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (f i -
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) (f i) :
                DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            0) :
        A))
have pos : ∀ (hn' : n = 0),
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (f i -
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) (f i) :
                DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            0) :
        A))
Tactic: by_cases hn' : n = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
pos :
  ∀ (hn' : n = 0),
    Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
      (f i -
        (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) (f i) :
                  DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
                (a : ℕ) → ↥(𝒜 a))
              0) :
          A))
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (f i -
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) (f i) :
                DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            0) :
        A))
have neg : ∀ (hn' : ¬n = 0),
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (f i -
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) (f i) :
                DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            0) :
        A))
Tactic: by_cases hn' : n = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
hn' : n = 0
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (f i -
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) (f i) :
                DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            0) :
        A))
have pos : Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f)) 0
Tactic: rw [DirectSum.decompose_of_mem_same 𝒜 (hn' ▸ hn), sub_self]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
hn' : ¬n = 0
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (f i -
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) (f i) :
                DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            0) :
        A))
have neg : Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f)) (f i)
Tactic: rw [DirectSum.decompose_of_mem_ne 𝒜 hn hn', sub_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
r : ↥(𝒜 0)
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (α := A) (β := A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A)
      ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A) : A))
have h : HSub.hSub (α := A) (β := A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A)
    ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A) : A) =
  0
Tactic: convert! zero_mem (Ideal.span _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
r : ↥(𝒜 0)
⊢ HSub.hSub (α := A) (β := A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A)
      ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A) : A) =
    0
have h : Eq (α := A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A)
  ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A) : A)
Tactic: rw [sub_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x_1 x y : A
hx : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x
hy : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) y
h :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
h_1 :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A))
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) (x + y) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (x + y) : A))
have hf₁ : Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
  (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A) +
    HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A))
Tactic: rw [map_add, add_sub_add_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x_1 x y : A
hx : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x
hy : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) y
hx' :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
hy' :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A))
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) (x * y) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (x * y) : A))
have h : HSub.hSub (β := A) (x * y) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (x * y) : A) =
  x * HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A) +
    HMul.hMul (β := A) (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
      ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A)
Tactic: convert!
      add_mem (Ideal.mul_mem_left _ x hy')
        (Ideal.mul_mem_right (GradedRing.projZeroRingHom 𝒜 y) _ hx') using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x_1 x y : A
hx : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x
hy : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) y
hx' :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
hy' :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A))
⊢ HSub.hSub (β := A) (x * y) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (x * y) : A) =
    x * HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A) +
      HMul.hMul (β := A) (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
        ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A)
have h : x * y -
    HMul.hMul (α := A) (β := A) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A)
      ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A) =
  x * HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A) +
    HMul.hMul (β := A) (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
      ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A)
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
this : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
have hf₁ : ∀ (x : A) (hx : x ∈ Set.range f),
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
Tactic: induction this using Algebra.adjoin_induction with
  | mem x hx =>
    obtain ⟨i, rfl⟩ := hx
    obtain ⟨n, hn⟩ := hfn i
    rw [GradedRing.projZeroRingHom_apply]
    by_cases hn' : n = 0
    · rw [DirectSum.decompose_of_mem_same 𝒜 (hn' ▸ hn), sub_self]
      exact zero_mem _
    · rw [DirectSum.decompose_of_mem_ne 𝒜 hn hn', sub_zero]
      exact Ideal.subset_span ⟨_, rfl⟩
  | algebraMap r =>
    convert! zero_mem (Ideal.span _)
    rw [sub_eq_zero]
    exact (DirectSum.decompose_of_mem_same 𝒜 r.2).symm
  | add x y hx hy _ _ =>
    rw [map_add, add_sub_add_comm]
    exact add_mem ‹_› ‹_›
  | mul x y hx hy hx' hy' =>
    convert!
      add_mem (Ideal.mul_mem_left _ x hy')
        (Ideal.mul_mem_right (GradedRing.projZeroRingHom 𝒜 y) _ hx') using 1
    rw [map_mul]
    ring
Cleared hypotheses: this