ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<VAR>g : ℕ → A⁰_ f := fun j => (m + m).choose j • if h2 : m + m < j then 0 else if h1 : j ≤ m then HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } else HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }<GOAL>Localization.mk ↑{ deg := m * i + m * i, num := ⟨∑ x ∈ range (m + m + 1), (m + m).choose x • ((proj 𝒜 i) a ^ x * (proj 𝒜 i) b ^ (m + m - x)), ⋯⟩, den := ⟨f ^ (i + i), ⋯⟩, den_mem := ⋯ }.num ⟨↑{ deg := m * i + m * i, num := ⟨∑ x ∈ range (m + m + 1), (m + m).choose x • ((proj 𝒜 i) a ^ x * (proj 𝒜 i) b ^ (m + m - x)), ⋯⟩, den := ⟨f ^ (i + i), ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ = HomogeneousLocalization.val (∑ i ∈ range (m + m + 1), g i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<VAR>g : ℕ → A⁰_ f := fun j => (m + m).choose j • if h2 : m + m < j then 0 else if h1 : j ≤ m then HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } else HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }<GOAL>Localization.mk ↑{ deg := m * i + m * i, num := ⟨∑ x ∈ range (m + m + 1), (m + m).choose x • ((proj 𝒜 i) a ^ x * (proj 𝒜 i) b ^ (m + m - x)), ⋯⟩, den := ⟨f ^ (i + i), ⋯⟩, den_mem := ⋯ }.num ⟨↑{ deg := m * i + m * i, num := ⟨∑ x ∈ range (m + m + 1), (m + m).choose x • ((proj 𝒜 i) a ^ x * (proj 𝒜 i) b ^ (m + m - x)), ⋯⟩, den := ⟨f ^ (i + i), ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ = (algebraMap (A⁰_ f) (Localization.Away f)) (∑ i ∈ range (m + m + 1), g i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<VAR>g : ℕ → A⁰_ f := fun j => (m + m).choose j • if h2 : m + m < j then 0 else if h1 : j ≤ m then HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } else HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }<GOAL>Localization.mk (∑ x ∈ range (m + m + 1), (m + m).choose x • ((proj 𝒜 i) a ^ x * (proj 𝒜 i) b ^ (m + m - x))) ⟨f ^ (i + i), ⋯⟩ = (algebraMap (A⁰_ f) (Localization.Away f)) (∑ i ∈ range (m + m + 1), g i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<VAR>g : ℕ → A⁰_ f := fun j => (m + m).choose j • if h2 : m + m < j then 0 else if h1 : j ≤ m then HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } else HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }<GOAL>∑ i_1 ∈ range (m + m + 1), Localization.mk ((m + m).choose i_1 • ((proj 𝒜 i) a ^ i_1 * (proj 𝒜 i) b ^ (m + m - i_1))) ⟨f ^ (i + i), ⋯⟩ = ∑ x ∈ range (m + m + 1), (algebraMap (A⁰_ f) (Localization.Away f)) (g x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<VAR>g : ℕ → A⁰_ f := fun j => (m + m).choose j • if h2 : m + m < j then 0 else if h1 : j ≤ m then HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } else HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }<GOAL>∀ j ∈ range (m + m + 1), Localization.mk ((m + m).choose j • ((proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m + m - j))) ⟨f ^ (i + i), ⋯⟩ = (algebraMap (A⁰_ f) (Localization.Away f)) (g j)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<VAR>g : ℕ → A⁰_ f := fun j => (m + m).choose j • if h2 : m + m < j then 0 else if h1 : j ≤ m then HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } else HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }<VAR>j : ℕ<VAR>hj : j ∈ range (m + m + 1)<GOAL>Localization.mk ((m + m).choose j • ((proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m + m - j))) ⟨f ^ (i + i), ⋯⟩ = HomogeneousLocalization.val (g j)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<VAR>g : ℕ → A⁰_ f := fun j => (m + m).choose j • if h2 : m + m < j then 0 else if h1 : j ≤ m then HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } else HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }<VAR>j : ℕ<VAR>hj : j ∈ range (m + m + 1)<GOAL>Localization.mk ((m + m).choose j • ((proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m + m - j))) ⟨f ^ (i + i), ⋯⟩ = (m + m).choose j • HomogeneousLocalization.val (if h2 : m + m < j then 0 else if h1 : j ≤ m then HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } else HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ })
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<VAR>g : ℕ → A⁰_ f := fun j => (m + m).choose j • if h2 : m + m < j then 0 else if h1 : j ≤ m then HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } else HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }<VAR>j : ℕ<VAR>hj : j ∈ range (m + m + 1)<VAR>h2 : ¬m + m < j<VAR>h1 : j ≤ m<GOAL>Localization.mk ((m + m).choose j • ((proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m + m - j))) ⟨f ^ (i + i), ⋯⟩ = (m + m).choose j • HomogeneousLocalization.val (HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ })
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<VAR>g : ℕ → A⁰_ f := fun j => (m + m).choose j • if h2 : m + m < j then 0 else if h1 : j ≤ m then HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } else HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }<VAR>j : ℕ<VAR>hj : j ∈ range (m + m + 1)<VAR>h2 : ¬m + m < j<VAR>h1 : ¬j ≤ m<GOAL>Localization.mk ((m + m).choose j • ((proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m + m - j))) ⟨f ^ (i + i), ⋯⟩ = (m + m).choose j • HomogeneousLocalization.val (HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ })
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<VAR>g : ℕ → A⁰_ f := fun j => (m + m).choose j • if h2 : m + m < j then 0 else if h1 : j ≤ m then HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } else HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }<VAR>j : ℕ<VAR>hj : j ∈ range (m + m + 1)<VAR>h2 : ¬m + m < j<VAR>h1 : j ≤ m<GOAL>(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m + m - j) = (proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j) * (proj 𝒜 i) b ^ m
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<VAR>g : ℕ → A⁰_ f := fun j => (m + m).choose j • if h2 : m + m < j then 0 else if h1 : j ≤ m then HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } else HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }<VAR>j : ℕ<VAR>hj : j ∈ range (m + m + 1)<VAR>h2 : ¬m + m < j<VAR>h1 : j ≤ m<GOAL>⟨f ^ (i + i), ⋯⟩ = ⟨f ^ i, ⋯⟩ * ⟨f ^ i, ⋯⟩
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<VAR>g : ℕ → A⁰_ f := fun j => (m + m).choose j • if h2 : m + m < j then 0 else if h1 : j ≤ m then HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } else HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }<VAR>j : ℕ<VAR>hj : j ∈ range (m + m + 1)<VAR>h2 : ¬m + m < j<VAR>h1 : ¬j ≤ m<GOAL>(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m + m - j) = (proj 𝒜 i) a ^ m * ((proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ carrier f_deg q<VAR>hb : b ∈ carrier f_deg q<VAR>i : ℕ<VAR>g : ℕ → A⁰_ f := fun j => (m + m).choose j • if h2 : m + m < j then 0 else if h1 : j ≤ m then HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } else HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } * HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }<VAR>j : ℕ<VAR>hj : j ∈ range (m + m + 1)<VAR>h2 : ¬m + m < j<VAR>h1 : ¬j ≤ m<GOAL>⟨f ^ (i + i), ⋯⟩ = ⟨f ^ i, ⋯⟩ * ⟨f ^ i, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>0 < (sort (fun x x_1 => x ≤ x_1) s).length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>0 < s.card
<VAR>n b f : ℕ<GOAL>∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>a : X<VAR>g : G<GOAL>g • orbit (↥N) a = orbit (↥N) (g • a)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>a : X<VAR>g : G<GOAL>(Set.range fun i => g • i • a) = Set.range fun m => m • g • a
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>a : X<VAR>g : G<VAR>x✝ : X<GOAL>(x✝ ∈ Set.range fun i => g • i • a) ↔ x✝ ∈ Set.range fun m => m • g • a
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>a : X<VAR>g : G<VAR>x✝ : X<GOAL>(∃ y, g • y • a = x✝) ↔ ∃ y, y • g • a = x✝
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>x y : ↑(π C fun x => x ∈ s)<VAR>a : I<VAR>ha : ↑y a = true<VAR>hx : ↑x a = false<GOAL>1 - e (π C fun x => x ∈ s) a ∈ factors C s x
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>x y : ↑(π C fun x => x ∈ s)<VAR>a : I<VAR>ha : ↑y a = true<VAR>hx : ↑x a = false<GOAL>∃ a_1 ∈ s, (if ↑x a_1 = true then e (π C fun x => x ∈ s) a_1 else 1 - e (π C fun x => x ∈ s) a_1) = 1 - e (π C fun x => x ∈ s) a
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>x y : ↑(π C fun x => x ∈ s)<VAR>a : I<VAR>ha : ↑y a = true<VAR>hx : ↑x a = false<GOAL>a ∈ s ∧ (if ↑x a = true then e (π C fun x => x ∈ s) a else 1 - e (π C fun x => x ∈ s) a) = 1 - e (π C fun x => x ∈ s) a
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>s : Finset I<VAR>x y : ↑(π C fun x => x ∈ s)<VAR>a : I<VAR>ha : ↑y a = true<VAR>hx : ↑x a = false<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>n : ℕ<VAR>i : Fin l.length<GOAL>(l.formPerm ^ n) (l.get i) = l.get ⟨(↑i + n) % l.length, ⋯⟩
<VAR>M : Type u_1<VAR>inst✝⁴ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝³ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝² : CommMonoid P<VAR>R : Type u_4<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>inst✝¹ : SMul R M<VAR>inst✝ : IsScalarTower R M M<VAR>c : R<VAR>a : M<VAR>b : ↥S<GOAL>c • mk a b = mk (c • a) b
<VAR>M : Type u_1<VAR>inst✝⁴ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝³ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝² : CommMonoid P<VAR>R : Type u_4<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>inst✝¹ : SMul R M<VAR>inst✝ : IsScalarTower R M M<VAR>c : R<VAR>a : M<VAR>b : ↥S<GOAL>OreLocalization.oreNum (c • 1) b • a /ₒ (OreLocalization.oreDenom (c • 1) b * 1) = c • a /ₒ b
<VAR>M : Type u_1<VAR>inst✝⁴ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝³ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝² : CommMonoid P<VAR>R : Type u_4<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>inst✝¹ : SMul R M<VAR>inst✝ : IsScalarTower R M M<VAR>c : R<VAR>a : M<VAR>b : ↥S<GOAL>(c • 1) • a /ₒ (b * 1) = c • a /ₒ b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>x : C<GOAL>adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) = adj2.unit.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>x : C<GOAL>adj1.unit.app x ≫ G.map ((adj1.leftAdjointUniq adj2).hom.app x) = (adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝⁴ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝³ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝² : CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>A : Type u_5<VAR>inst✝¹ : CommMonoid A<VAR>U : Submonoid A<VAR>R : Type u_6<VAR>inst✝ : CommMonoid R<VAR>j : U.LocalizationMap R<VAR>l : P →* A<VAR>hl : ∀ (w : ↥T), l ↑w ∈ U<VAR>z : N<GOAL>j.toMap (l (k.sec ((f.map hy k) z)).1) * ↑((IsUnit.liftRight ((j.toMap.comp l).restrict T) ⋯) (k.sec ((f.map hy k) z)).2)⁻¹ = j.toMap (l (g (f.sec z).1)) * ↑((IsUnit.liftRight ((j.toMap.comp (l.comp g)).restrict S) ⋯) (f.sec z).2)⁻¹
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝⁴ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝³ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝² : CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>A : Type u_5<VAR>inst✝¹ : CommMonoid A<VAR>U : Submonoid A<VAR>R : Type u_6<VAR>inst✝ : CommMonoid R<VAR>j : U.LocalizationMap R<VAR>l : P →* A<VAR>hl : ∀ (w : ↥T), l ↑w ∈ U<VAR>z : N<GOAL>j.toMap (l (k.sec ((f.map hy k) z)).1) * (j.toMap.comp (l.comp g)) ↑(f.sec z).2 = (j.toMap.comp l) ↑(k.sec ((f.map hy k) z)).2 * j.toMap (l (g (f.sec z).1))
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝⁴ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝³ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝² : CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>A : Type u_5<VAR>inst✝¹ : CommMonoid A<VAR>U : Submonoid A<VAR>R : Type u_6<VAR>inst✝ : CommMonoid R<VAR>j : U.LocalizationMap R<VAR>l : P →* A<VAR>hl : ∀ (w : ↥T), l ↑w ∈ U<VAR>z : N<GOAL>j.toMap (l (k.sec ((f.map hy k) z)).1) * j.toMap (l (g ↑(f.sec z).2)) = j.toMap (l ↑(k.sec ((f.map hy k) z)).2) * j.toMap (l (g (f.sec z).1))
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝⁴ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝³ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝² : CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>A : Type u_5<VAR>inst✝¹ : CommMonoid A<VAR>U : Submonoid A<VAR>R : Type u_6<VAR>inst✝ : CommMonoid R<VAR>j : U.LocalizationMap R<VAR>l : P →* A<VAR>hl : ∀ (w : ↥T), l ↑w ∈ U<VAR>z : N<GOAL>j.toMap (l ((k.sec ((f.map hy k) z)).1 * g ↑(f.sec z).2)) = j.toMap (l (↑(k.sec ((f.map hy k) z)).2 * g (f.sec z).1))
<VAR>u v : ℤ<VAR>h : u * v = -1<GOAL>u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
<VAR>v : ℤ<VAR>h : 1 * v = -1<GOAL>1 = 1 ∧ v = -1 ∨ 1 = -1 ∧ v = 1
<VAR>v : ℤ<VAR>h : -1 * v = -1<GOAL>-1 = 1 ∧ v = -1 ∨ -1 = -1 ∧ v = 1
<VAR>n p : ℕ<GOAL>padicValNat (p + 1 + 1) (n + 1) ≤ log (p + 1 + 1) (n + 1)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q R : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>γ : Q ⟶ R<VAR>hR : Presheaf.IsSheaf J R<GOAL>J.sheafifyMap η ≫ J.sheafifyLift γ hR = J.sheafifyLift (η ≫ γ) hR
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q R : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>γ : Q ⟶ R<VAR>hR : Presheaf.IsSheaf J R<GOAL>J.toSheafify P ≫ J.sheafifyMap η ≫ J.sheafifyLift γ hR = η ≫ γ
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set ℝ<GOAL>volume s = StieltjesFunction.id.measure s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<GOAL>derivative (X ^ 2) = C 2 * X