ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝² : (ofArrows X c.inj).hasPullbacks<VAR>inst✝¹ : HasInitial C<VAR>inst✝ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>this : HasCoproduct X<VAR>h : (Pi.lift fun i => F.map (c.inj i).op) = F.map (Pi.lift fun i => (c.inj i).op) ≫ piComparison F fun i => op (X i)<GOAL>(piComparison F fun x => op (X x)) = F.map ((opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Pi.lift fun i => (c.inj i).op) ≫ piComparison F fun i => op (X i)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝² : (ofArrows X c.inj).hasPullbacks<VAR>inst✝¹ : HasInitial C<VAR>inst✝ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>this : HasCoproduct X<VAR>h : (Pi.lift fun i => F.map (c.inj i).op) = F.map (Pi.lift fun i => (c.inj i).op) ≫ piComparison F fun i => op (X i)<VAR>hh : (Pi.lift fun i => (c.inj i).op) = (productIsProduct fun x => op (X x)).lift c.op<GOAL>(piComparison F fun x => op (X x)) = F.map ((opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Pi.lift fun i => (c.inj i).op) ≫ piComparison F fun i => op (X i)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝² : (ofArrows X c.inj).hasPullbacks<VAR>inst✝¹ : HasInitial C<VAR>inst✝ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>this : HasCoproduct X<VAR>h : (Pi.lift fun i => F.map (c.inj i).op) = F.map (Pi.lift fun i => (c.inj i).op) ≫ piComparison F fun i => op (X i)<VAR>hh : (Pi.lift fun i => (c.inj i).op) = (productIsProduct fun x => op (X x)).lift c.op<GOAL>(piComparison F fun x => op (X x)) = F.map ((opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ (hc.desc c).op ≫ (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).hom) ≫ piComparison F fun i => op (X i)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>G'' : Type u_7<VAR>G' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : NormedLatticeAddCommGroup G''<VAR>inst✝ : NormedSpace ℝ G''<VAR>T : Set α → G'' →L[ℝ] G'<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : ↥(simpleFunc G'' 1 μ)<VAR>hfg : f ≤ g<GOAL>setToL1S T f ≤ setToL1S T g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>G'' : Type u_7<VAR>G' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : NormedLatticeAddCommGroup G''<VAR>inst✝ : NormedSpace ℝ G''<VAR>T : Set α → G'' →L[ℝ] G'<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : ↥(simpleFunc G'' 1 μ)<VAR>hfg : 0 ≤ g - f<GOAL>0 ≤ setToL1S T g - setToL1S T f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>G'' : Type u_7<VAR>G' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : NormedLatticeAddCommGroup G''<VAR>inst✝ : NormedSpace ℝ G''<VAR>T : Set α → G'' →L[ℝ] G'<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : ↥(simpleFunc G'' 1 μ)<VAR>hfg : 0 ≤ g - f<GOAL>0 ≤ setToL1S T (g - f)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((structureSheaf R).val.map (iDh i).op) s<GOAL>∃ a' h' iDh', U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h' i) ∧ (∀ i ∈ t, ∀ j ∈ t, a' i * h' j = h' i * a' j) ∧ ∀ i ∈ t, ((structureSheaf R).val.map (iDh' i).op) s = const R (a' i) (h' i) (PrimeSpectrum.basicOpen (h' i)) ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((structureSheaf R).val.map (iDh i).op) s<VAR>fractions_eq : ∀ (i j : ι), IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ = IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩<GOAL>∃ a' h' iDh', U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h' i) ∧ (∀ i ∈ t, ∀ j ∈ t, a' i * h' j = h' i * a' j) ∧ ∀ i ∈ t, ((structureSheaf R).val.map (iDh' i).op) s = const R (a' i) (h' i) (PrimeSpectrum.basicOpen (h' i)) ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((structureSheaf R).val.map (iDh i).op) s<VAR>fractions_eq : ∀ (i j : ι), IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ = IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩<VAR>exists_power : ∀ (i j : ι), ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n<GOAL>∃ a' h' iDh', U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h' i) ∧ (∀ i ∈ t, ∀ j ∈ t, a' i * h' j = h' i * a' j) ∧ ∀ i ∈ t, ((structureSheaf R).val.map (iDh' i).op) s = const R (a' i) (h' i) (PrimeSpectrum.basicOpen (h' i)) ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((structureSheaf R).val.map (iDh i).op) s<VAR>fractions_eq : ∀ (i j : ι), IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ = IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩<VAR>exists_power : ∀ (i j : ι), ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n<VAR>n : ι × ι → ℕ := fun p => ⋯.choose<GOAL>∃ a' h' iDh', U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h' i) ∧ (∀ i ∈ t, ∀ j ∈ t, a' i * h' j = h' i * a' j) ∧ ∀ i ∈ t, ((structureSheaf R).val.map (iDh' i).op) s = const R (a' i) (h' i) (PrimeSpectrum.basicOpen (h' i)) ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((structureSheaf R).val.map (iDh i).op) s<VAR>fractions_eq : ∀ (i j : ι), IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ = IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩<VAR>exists_power : ∀ (i j : ι), ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n<VAR>n : ι × ι → ℕ := fun p => ⋯.choose<VAR>n_spec : ∀ (p : ι × ι), a p.1 * h p.2 * (h p.1 * h p.2) ^ ⋯.choose = h p.1 * a p.2 * (h p.1 * h p.2) ^ ⋯.choose<GOAL>∃ a' h' iDh', U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h' i) ∧ (∀ i ∈ t, ∀ j ∈ t, a' i * h' j = h' i * a' j) ∧ ∀ i ∈ t, ((structureSheaf R).val.map (iDh' i).op) s = const R (a' i) (h' i) (PrimeSpectrum.basicOpen (h' i)) ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((structureSheaf R).val.map (iDh i).op) s<VAR>fractions_eq : ∀ (i j : ι), IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ = IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩<VAR>exists_power : ∀ (i j : ι), ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n<VAR>n : ι × ι → ℕ := fun p => ⋯.choose<VAR>n_spec : ∀ (p : ι × ι), a p.1 * h p.2 * (h p.1 * h p.2) ^ ⋯.choose = h p.1 * a p.2 * (h p.1 * h p.2) ^ ⋯.choose<VAR>N : ℕ := (t ×ˢ t).sup n<GOAL>∃ a' h' iDh', U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h' i) ∧ (∀ i ∈ t, ∀ j ∈ t, a' i * h' j = h' i * a' j) ∧ ∀ i ∈ t, ((structureSheaf R).val.map (iDh' i).op) s = const R (a' i) (h' i) (PrimeSpectrum.basicOpen (h' i)) ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((structureSheaf R).val.map (iDh i).op) s<VAR>fractions_eq : ∀ (i j : ι), IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ = IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩<VAR>exists_power : ∀ (i j : ι), ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n<VAR>n : ι × ι → ℕ := fun p => ⋯.choose<VAR>n_spec : ∀ (p : ι × ι), a p.1 * h p.2 * (h p.1 * h p.2) ^ ⋯.choose = h p.1 * a p.2 * (h p.1 * h p.2) ^ ⋯.choose<VAR>N : ℕ := (t ×ˢ t).sup n<VAR>basic_opens_eq : ∀ (i : ι), PrimeSpectrum.basicOpen (h i ^ (N + 1)) = PrimeSpectrum.basicOpen (h i)<GOAL>∃ a' h' iDh', U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h' i) ∧ (∀ i ∈ t, ∀ j ∈ t, a' i * h' j = h' i * a' j) ∧ ∀ i ∈ t, ((structureSheaf R).val.map (iDh' i).op) s = const R (a' i) (h' i) (PrimeSpectrum.basicOpen (h' i)) ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((structureSheaf R).val.map (iDh i).op) s<VAR>fractions_eq : ∀ (i j : ι), IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ = IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩<VAR>exists_power : ∀ (i j : ι), ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n<VAR>n : ι × ι → ℕ := fun p => ⋯.choose<VAR>n_spec : ∀ (p : ι × ι), a p.1 * h p.2 * (h p.1 * h p.2) ^ ⋯.choose = h p.1 * a p.2 * (h p.1 * h p.2) ^ ⋯.choose<VAR>N : ℕ := (t ×ˢ t).sup n<VAR>basic_opens_eq : ∀ (i : ι), PrimeSpectrum.basicOpen (h i ^ (N + 1)) = PrimeSpectrum.basicOpen (h i)<VAR>i : ι<VAR>a✝ : i ∈ t<GOAL>((structureSheaf R).val.map ((fun i => eqToHom ⋯ ≫ iDh i) i).op) s = const R ((fun i => a i * h i ^ N) i) ((fun i => h i ^ (N + 1)) i) (PrimeSpectrum.basicOpen ((fun i => h i ^ (N + 1)) i)) ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((structureSheaf R).val.map (iDh i).op) s<VAR>fractions_eq : ∀ (i j : ι), IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ = IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩<VAR>exists_power : ∀ (i j : ι), ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n<VAR>n : ι × ι → ℕ := fun p => ⋯.choose<VAR>n_spec : ∀ (p : ι × ι), a p.1 * h p.2 * (h p.1 * h p.2) ^ ⋯.choose = h p.1 * a p.2 * (h p.1 * h p.2) ^ ⋯.choose<VAR>N : ℕ := (t ×ˢ t).sup n<VAR>basic_opens_eq : ∀ (i : ι), PrimeSpectrum.basicOpen (h i ^ (N + 1)) = PrimeSpectrum.basicOpen (h i)<VAR>i : ι<VAR>a✝ : i ∈ t<GOAL>((structureSheaf R).val.map (iDh i).op ≫ (structureSheaf R).val.map (eqToHom ⋯).op) s = const R ((fun i => a i * h i ^ N) i) ((fun i => h i ^ (N + 1)) i) (PrimeSpectrum.basicOpen ((fun i => h i ^ (N + 1)) i)) ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((structureSheaf R).val.map (iDh i).op) s<VAR>fractions_eq : ∀ (i j : ι), IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ = IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩<VAR>exists_power : ∀ (i j : ι), ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n<VAR>n : ι × ι → ℕ := fun p => ⋯.choose<VAR>n_spec : ∀ (p : ι × ι), a p.1 * h p.2 * (h p.1 * h p.2) ^ ⋯.choose = h p.1 * a p.2 * (h p.1 * h p.2) ^ ⋯.choose<VAR>N : ℕ := (t ×ˢ t).sup n<VAR>basic_opens_eq : ∀ (i : ι), PrimeSpectrum.basicOpen (h i ^ (N + 1)) = PrimeSpectrum.basicOpen (h i)<VAR>i : ι<VAR>a✝ : i ∈ t<GOAL>((structureSheaf R).val.map (eqToHom ⋯).op) (((structureSheaf R).val.map (iDh i).op) s) = const R ((fun i => a i * h i ^ N) i) ((fun i => h i ^ (N + 1)) i) (PrimeSpectrum.basicOpen ((fun i => h i ^ (N + 1)) i)) ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((structureSheaf R).val.map (iDh i).op) s<VAR>fractions_eq : ∀ (i j : ι), IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ = IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩<VAR>exists_power : ∀ (i j : ι), ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n<VAR>n : ι × ι → ℕ := fun p => ⋯.choose<VAR>n_spec : ∀ (p : ι × ι), a p.1 * h p.2 * (h p.1 * h p.2) ^ ⋯.choose = h p.1 * a p.2 * (h p.1 * h p.2) ^ ⋯.choose<VAR>N : ℕ := (t ×ˢ t).sup n<VAR>basic_opens_eq : ∀ (i : ι), PrimeSpectrum.basicOpen (h i ^ (N + 1)) = PrimeSpectrum.basicOpen (h i)<VAR>i : ι<VAR>a✝ : i ∈ t<GOAL>const R (a i) (h i) (PrimeSpectrum.basicOpen (h i ^ (N + 1))) ?refine_3.hv = const R ((fun i => a i * h i ^ N) i) ((fun i => h i ^ (N + 1)) i) (PrimeSpectrum.basicOpen ((fun i => h i ^ (N + 1)) i)) ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((structureSheaf R).val.map (iDh i).op) s<VAR>fractions_eq : ∀ (i j : ι), IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ = IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩<VAR>exists_power : ∀ (i j : ι), ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n<VAR>n : ι × ι → ℕ := fun p => ⋯.choose<VAR>n_spec : ∀ (p : ι × ι), a p.1 * h p.2 * (h p.1 * h p.2) ^ ⋯.choose = h p.1 * a p.2 * (h p.1 * h p.2) ^ ⋯.choose<VAR>N : ℕ := (t ×ˢ t).sup n<VAR>basic_opens_eq : ∀ (i : ι), PrimeSpectrum.basicOpen (h i ^ (N + 1)) = PrimeSpectrum.basicOpen (h i)<VAR>i : ι<VAR>a✝ : i ∈ t<GOAL>∀ x ∈ PrimeSpectrum.basicOpen (h i ^ (N + 1)), h i ∈ x.asIdeal.primeCompl
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((structureSheaf R).val.map (iDh i).op) s<VAR>fractions_eq : ∀ (i j : ι), IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ = IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩<VAR>exists_power : ∀ (i j : ι), ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n<VAR>n : ι × ι → ℕ := fun p => ⋯.choose<VAR>n_spec : ∀ (p : ι × ι), a p.1 * h p.2 * (h p.1 * h p.2) ^ ⋯.choose = h p.1 * a p.2 * (h p.1 * h p.2) ^ ⋯.choose<VAR>N : ℕ := (t ×ˢ t).sup n<VAR>basic_opens_eq : ∀ (i : ι), PrimeSpectrum.basicOpen (h i ^ (N + 1)) = PrimeSpectrum.basicOpen (h i)<VAR>i : ι<VAR>a✝ : i ∈ t<GOAL>const R (a i) (h i) (PrimeSpectrum.basicOpen (h i ^ (N + 1))) ⋯ = const R ((fun i => a i * h i ^ N) i) ((fun i => h i ^ (N + 1)) i) (PrimeSpectrum.basicOpen ((fun i => h i ^ (N + 1)) i)) ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((structureSheaf R).val.map (iDh i).op) s<VAR>fractions_eq : ∀ (i j : ι), IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ = IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩<VAR>exists_power : ∀ (i j : ι), ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n<VAR>n : ι × ι → ℕ := fun p => ⋯.choose<VAR>n_spec : ∀ (p : ι × ι), a p.1 * h p.2 * (h p.1 * h p.2) ^ ⋯.choose = h p.1 * a p.2 * (h p.1 * h p.2) ^ ⋯.choose<VAR>N : ℕ := (t ×ˢ t).sup n<VAR>basic_opens_eq : ∀ (i : ι), PrimeSpectrum.basicOpen (h i ^ (N + 1)) = PrimeSpectrum.basicOpen (h i)<VAR>i : ι<VAR>a✝ : i ∈ t<GOAL>a i * (fun i => h i ^ (N + 1)) i = (fun i => a i * h i ^ N) i * h i
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((structureSheaf R).val.map (iDh i).op) s<VAR>fractions_eq : ∀ (i j : ι), IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ = IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩<VAR>exists_power : ∀ (i j : ι), ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n<VAR>n : ι × ι → ℕ := fun p => ⋯.choose<VAR>n_spec : ∀ (p : ι × ι), a p.1 * h p.2 * (h p.1 * h p.2) ^ ⋯.choose = h p.1 * a p.2 * (h p.1 * h p.2) ^ ⋯.choose<VAR>N : ℕ := (t ×ˢ t).sup n<VAR>basic_opens_eq : ∀ (i : ι), PrimeSpectrum.basicOpen (h i ^ (N + 1)) = PrimeSpectrum.basicOpen (h i)<VAR>i : ι<VAR>a✝ : i ∈ t<GOAL>a i * h i ^ (N + 1) = a i * h i ^ N * h i
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((structureSheaf R).val.map (iDh i).op) s<VAR>fractions_eq : ∀ (i j : ι), IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ = IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩<VAR>exists_power : ∀ (i j : ι), ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n<VAR>n : ι × ι → ℕ := fun p => ⋯.choose<VAR>n_spec : ∀ (p : ι × ι), a p.1 * h p.2 * (h p.1 * h p.2) ^ ⋯.choose = h p.1 * a p.2 * (h p.1 * h p.2) ^ ⋯.choose<VAR>N : ℕ := (t ×ˢ t).sup n<VAR>basic_opens_eq : ∀ (i : ι), PrimeSpectrum.basicOpen (h i ^ (N + 1)) = PrimeSpectrum.basicOpen (h i)<VAR>i : ι<VAR>a✝ : i ∈ t<GOAL>a i * (h i ^ N * h i) = a i * h i ^ N * h i
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : InvolutiveInv α<VAR>s t : Set α<VAR>a : α<VAR>ι : Sort u_5<VAR>f : ι → α<GOAL>(range f)⁻¹ = range fun i => (f i)⁻¹
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : InvolutiveInv α<VAR>s t : Set α<VAR>a : α<VAR>ι : Sort u_5<VAR>f : ι → α<GOAL>Inv.inv '' range f = range fun i => (f i)⁻¹
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>S : Type u_1<VAR>inst✝ : Ring S<VAR>n : ℕ<VAR>k : S<GOAL>eval k (descPochhammer S (n + 1)) = eval k (descPochhammer S n) * (k - ↑n)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : FiniteDimensional K L<VAR>f : (L ≃ₐ[K] L) → Lˣ<VAR>x y : L ≃ₐ[K] L<VAR>h : (fun f => ↑f) x = (fun f => ↑f) y<VAR>a✝ : L<GOAL>x a✝ = y a✝
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.oangle (x - y) x).sign = (o.oangle x y).sign
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x y : P.Elements<VAR>f : x ⟶ y<GOAL>yoneda.map (↑f).unop ≫ coconeApp φ x = coconeApp φ y