ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>C' : Type ?u.89621<VAR>D : Type u_5<VAR>D' : Type ?u.89627<VAR>H : Type u_2<VAR>H' : Type ?u.89633<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.89641, ?u.89621} C'<VAR>inst✝⁵ : Category.{u_6, u_5} D<VAR>inst✝⁴ : Category.{?u.89649, ?u.89627} D'<VAR>inst✝³ : Category.{u_4, u_2} H<VAR>inst✝² : Category.{?u.89657, ?u.89633} H'<VAR>RF RF' RF'' : D ⥤ H<VAR>F F' F'' : C ⥤ H<VAR>e : F ≅ F'<VAR>L : C ⥤ D<VAR>α : F ⟶ L ⋙ RF<VAR>α' : F' ⟶ L ⋙ RF'<VAR>α'' : F'' ⟶ L ⋙ RF''<VAR>α'₂ : F ⟶ L ⋙ RF'<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : F.HasRightDerivedFunctor W<GOAL>L.HasLeftKanExtension F
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<GOAL>W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) = -W.dblU P / W.dblZ P
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<VAR>hPy : P y - W.negY P ≠ 0<GOAL>W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) = -W.dblU P / W.dblZ P
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hPy : P y - W.negY P ≠ 0<VAR>hx : P x / P z ^ 2 = Q x / Q z ^ 2<VAR>hy : ¬P y / P z ^ 3 = W.toAffine.negY (Q x / Q z ^ 2) (Q y / Q z ^ 3)<GOAL>W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) = -W.dblU P / W.dblZ P
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hPy : P y - W.negY P ≠ 0<VAR>hx : P x / P z ^ 2 = Q x / Q z ^ 2<VAR>hy : ¬P y / P z ^ 3 = W.toAffine.negY (Q x / Q z ^ 2) (Q y / Q z ^ 3)<GOAL>(3 * (P x / P z ^ 2) ^ 2 + 2 * W.toAffine.a₂ * (P x / P z ^ 2) + W.toAffine.a₄ - W.toAffine.a₁ * (P y / P z ^ 3)) / (P y / P z ^ 3 - W.negY P / P z ^ 3) = -(W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z ^ 2 + W.a₄ * P z ^ 4)) / (P z * (P y - W.negY P))
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hPy : P y - W.negY P ≠ 0<VAR>hx : P x / P z ^ 2 = Q x / Q z ^ 2<VAR>hy : ¬P y / P z ^ 3 = W.toAffine.negY (Q x / Q z ^ 2) (Q y / Q z ^ 3)<GOAL>((3 * P x ^ 2 * P z ^ 2 + 2 * W.toAffine.a₂ * P x * (P z ^ 2) ^ 2 + W.toAffine.a₄ * ((P z ^ 2) ^ 2 * P z ^ 2)) * P z ^ 3 - (P z ^ 2) ^ 2 * P z ^ 2 * (W.toAffine.a₁ * P y)) * P z ^ 3 * (P z * (P y - W.negY P)) = (3 * P x ^ 2 + 2 * W.a₂ * P x * P z ^ 2 + W.a₄ * P z ^ 4 - W.a₁ * P y * P z) * ((P z ^ 2) ^ 2 * P z ^ 2 * P z ^ 3 * (P y - W.negY P))
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>k : ℕ<GOAL>f ^ k = (aeval f) (X ^ k %ₘ f.charpoly)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>σ : Type u_4<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>S : Subsemigroup M<VAR>g : N →ₙ* P<VAR>f : M →ₙ* N<GOAL>map g f.srange = (g.comp f).srange
<VAR>m n k : ℕ<GOAL>Nat.shiftLeft' false m (n + k) = Nat.shiftLeft' false (Nat.shiftLeft' false m n) k
<VAR>m n✝ k i n : ℕ<GOAL>↑m <<< ↑i = ↑(Nat.shiftLeft' false m (n + i) >>> n)
<VAR>m n✝ k i n : ℕ<GOAL>↑m <<< -[i+1] = ↑(Nat.shiftLeft' false m n >>> (n + i + 1))
<VAR>m n✝ k i n : ℕ<GOAL>Nat.shiftLeft' true m i = Nat.shiftLeft' true m (n + i) >>> n
<VAR>m n✝ k i n : ℕ<GOAL>n ≤ n + i
<VAR>m n✝ k i n : ℕ<GOAL>m >>> i.succ = Nat.shiftLeft' true m n >>> (n + i + 1)
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b c u : αˣ<VAR>a : α<GOAL>a * ↑u = 1 ↔ a = ↑u⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>R : Type u_7<VAR>R₂ : Type u_8<VAR>M : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring R₂<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R₂ M₂<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : TopologicalSpace M₂<VAR>σ : R →+* R₂<VAR>σ' : R₂ →+* R<VAR>inst✝¹ : RingHomInvPair σ σ'<VAR>inst✝ : RingHomInvPair σ' σ<VAR>f : ι → M<VAR>φ : M →SL[σ] M₂<VAR>x : M<VAR>hf : HasSum f x<GOAL>HasSum (fun b => φ (f b)) (φ x)
<VAR>a : ℝ<GOAL>interior {z | z.re ≤ a} = {z | z.re < a}
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Field A<VAR>inst✝² : Ring B<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>hx : IsIntegral A x<VAR>h : x ≠ 0<GOAL>(minpoly A x).coeff 0 ≠ 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Field A<VAR>inst✝² : Ring B<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>hx : IsIntegral A x<VAR>h : (minpoly A x).coeff 0 = 0<GOAL>x = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>β : Type u_2<VAR>m' : MeasurableSpace β<VAR>μ' : Measure β<VAR>s' : Set β<VAR>g : α → β<VAR>e : α ≃ᵐ β<VAR>h : MeasurePreserving (⇑e) μ μ'<GOAL>PreErgodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ PreErgodic f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>β : Type u_2<VAR>m' : MeasurableSpace β<VAR>μ' : Measure β<VAR>s' : Set β<VAR>g : α → β<VAR>e : α ≃ᵐ β<VAR>h : MeasurePreserving (⇑e) μ μ'<VAR>hf : PreErgodic (⇑e ∘ f ∘ ⇑e.symm) μ'<GOAL>⇑e.symm ∘ ⇑e ∘ f ∘ ⇑e.symm = f ∘ ⇑e.symm
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>β : Type u_2<VAR>m' : MeasurableSpace β<VAR>μ' : Measure β<VAR>s' : Set β<VAR>g : α → β<VAR>e : α ≃ᵐ β<VAR>h : MeasurePreserving (⇑e) μ μ'<VAR>hf : PreErgodic f μ<GOAL>⇑e ∘ f = (⇑e ∘ f ∘ ⇑e.symm) ∘ ⇑e
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>G : C<VAR>hG : IsSeparator G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ (h : G ⟶ X), h ≫ f = 0<GOAL>∀ (h : G ⟶ X), h ≫ f = h ≫ 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>G : C<VAR>hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = 0) → f = 0<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g<GOAL>∀ (h : G ⟶ X), h ≫ (f - g) = 0
<VAR>x✝ y z : ℝ<VAR>n : ℕ<VAR>x : ℝ<GOAL>x ^ (-1) = x⁻¹
<VAR>x✝ y z : ℝ<VAR>n : ℕ<VAR>x : ℝ<GOAL>x ^ ↑(-1) = x⁻¹
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>r : ℤ → ℝ := fun n => ↑n + a<VAR>c : ℤ → ℂ := fun n => 1 / 2<GOAL>HasSum (fun n => (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaOdd (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>r : ℤ → ℝ := fun n => ↑n + a<VAR>c : ℤ → ℂ := fun n => 1 / 2<VAR>hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑(r n) * ↑(rexp (-π * r n ^ 2 * t))) (↑(oddKernel (↑a) t) / 2)<GOAL>HasSum (fun n => (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaOdd (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>r : ℤ → ℝ := fun n => ↑n + a<VAR>c : ℤ → ℂ := fun n => 1 / 2<VAR>hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑(r n) * ↑(rexp (-π * r n ^ 2 * t))) (↑(oddKernel (↑a) t) / 2)<VAR>h_sum : Summable fun i => ‖c i‖ / |r i| ^ s.re<GOAL>HasSum (fun n => (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaOdd (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>r : ℤ → ℝ := fun n => ↑n + a<VAR>c : ℤ → ℂ := fun n => 1 / 2<VAR>hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑(r n) * ↑(rexp (-π * r n ^ 2 * t))) (↑(oddKernel (↑a) t) / 2)<VAR>h_sum : Summable fun i => ‖c i‖ / |r i| ^ s.re<VAR>this : HasSum (fun i => (s + 1).Gammaℝ * c i * ↑(SignType.sign (r i)) / ↑|r i| ^ s) (mellin (fun t => ↑(oddKernel (↑a) t)) ((s + 1) / 2) / 2)<GOAL>HasSum (fun n => (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaOdd (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>r : ℤ → ℝ := fun n => ↑n + a<VAR>c : ℤ → ℂ := fun n => 1 / 2<VAR>hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑(r n) * ↑(rexp (-π * r n ^ 2 * t))) (↑(oddKernel (↑a) t) / 2)<VAR>h_sum : Summable fun i => ‖c i‖ / |r i| ^ s.re<VAR>this : HasSum (fun i => (s + 1).Gammaℝ * c i * ↑(SignType.sign (r i)) / ↑|r i| ^ s) (mellin (fun t => ↑(oddKernel (↑a) t)) ((s + 1) / 2) / 2)<VAR>n : ℤ<GOAL>(s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 = (s + 1).Gammaℝ * c n * ↑(SignType.sign (r n)) / ↑|r n| ^ s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : PerfectPairing R M N<VAR>x : M<VAR>f : Dual R M<GOAL>(p.toDualLeft x) (p.toDualRight.symm f) = f x
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M'<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Fintype ι<VAR>e✝ : Basis ι R M<VAR>A : Type u_5<VAR>inst✝³ : CommRing A<VAR>inst✝² : Module A M<VAR>ι' : Type u_6<VAR>inst✝¹ : Fintype ι'<VAR>inst✝ : DecidableEq ι'<VAR>b : Basis ι R M<VAR>v : ι → M<VAR>e : ι' ≃ ι<GOAL>(b.reindex e.symm).det (v ∘ ⇑e) = b.det v
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>ι : Type u_7<VAR>s : Finset ι<VAR>f : ι → R<VAR>g : Γ₀<VAR>hf : ∀ i ∈ s, v (f i) ≤ g<GOAL>v (∑ i ∈ s, f i) ≤ g
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>ι : Type u_7<VAR>s✝ : Finset ι<VAR>f : ι → R<VAR>g : Γ₀<VAR>hf✝ : ∀ i ∈ s✝, v (f i) ≤ g<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : (∀ i ∈ s, v (f i) ≤ g) → v (∑ i ∈ s, f i) ≤ g<VAR>hf : ∀ i ∈ insert a s, v (f i) ≤ g<GOAL>v (∑ i ∈ insert a s, f i) ≤ g
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>ι : Type u_7<VAR>s✝ : Finset ι<VAR>f : ι → R<VAR>g : Γ₀<VAR>hf✝ : ∀ i ∈ s✝, v (f i) ≤ g<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : (∀ i ∈ s, v (f i) ≤ g) → v (∑ i ∈ s, f i) ≤ g<VAR>hf : v (f a) ≤ g ∧ ∀ x ∈ s, v (f x) ≤ g<GOAL>v (∑ i ∈ insert a s, f i) ≤ g
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>ι : Type u_7<VAR>s✝ : Finset ι<VAR>f : ι → R<VAR>g : Γ₀<VAR>hf✝ : ∀ i ∈ s✝, v (f i) ≤ g<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : (∀ i ∈ s, v (f i) ≤ g) → v (∑ i ∈ s, f i) ≤ g<VAR>hf : v (f a) ≤ g ∧ ∀ x ∈ s, v (f x) ≤ g<GOAL>v (f a + ∑ x ∈ s, f x) ≤ g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<VAR>i : 𝒰.J<GOAL>pullback.snd (p1 𝒰 f g) (𝒰.map i) ≫ 𝒰.map i ≫ f = (pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g) ≫ g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<VAR>i : 𝒰.J<GOAL>pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.map i)) (pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g) ⋯ ≫ (gluing 𝒰 f g).ι i = pullback.fst (p1 𝒰 f g) (𝒰.map i)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<VAR>i : 𝒰.J<GOAL>∀ (x : ((gluing 𝒰 f g).openCover.pullbackCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).J), ((gluing 𝒰 f g).openCover.pullbackCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).map x ≫ pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.map i)) (pullback.fst (p1 𝒰 f g) (𝒰.map i) ≫ p2 𝒰 f g) ⋯ ≫ (gluing 𝒰 f g).ι i = ((gluing 𝒰 f g).openCover.pullbackCover (pullback.fst (p1 𝒰 f g) (𝒰.map i))).map x ≫ pullback.fst (p1 𝒰 f g) (𝒰.map i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>x : List α<VAR>hx : x ≠ []<VAR>h : x <+: []<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) '' Ioc b c = Ioc (b - a) (c - a)
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>HasDerivAt negMulLog (-log x - 1) x
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>DifferentiableAt ℝ negMulLog x
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>W : WeierstrassCurve R<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(W.baseChange B).Ψ₂Sq = Polynomial.map (↑f) (W.baseChange A).Ψ₂Sq
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j : JordanDecomposition α<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>(r • j).posPart = r.toNNReal • j.posPart
<VAR>A B : Grp<VAR>f : A ⟶ B<GOAL>(Equiv.symm τ) (fromCoset ⟨↑(MonoidHom.range f), ⋯⟩) = ∞
<VAR>n m : ℕ<VAR>i : Fin (n + 1)<GOAL>(last n).predAbove i.castSucc = i
<VAR>x y : PGame<VAR>k : (x * y).RightMoves<VAR>P : (x * y).RightMoves → Prop<VAR>hl : ∀ (ix : x.LeftMoves) (jy : y.RightMoves), P (toRightMovesMul (Sum.inl (ix, jy)))<VAR>hr : ∀ (jx : x.RightMoves) (iy : y.LeftMoves), P (toRightMovesMul (Sum.inr (jx, iy)))<GOAL>P k
<VAR>x y : PGame<VAR>k : (x * y).RightMoves<VAR>P : (x * y).RightMoves → Prop<VAR>hl : ∀ (ix : x.LeftMoves) (jy : y.RightMoves), P (toRightMovesMul (Sum.inl (ix, jy)))<VAR>hr : ∀ (jx : x.RightMoves) (iy : y.LeftMoves), P (toRightMovesMul (Sum.inr (jx, iy)))<GOAL>P (toRightMovesMul (toRightMovesMul.symm k))
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>e : α ≃ᵢ β<GOAL>CompleteSpace α ↔ CompleteSpace β
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>B : C<VAR>α : Type v<VAR>inst✝² : Nonempty α<VAR>X : α → C<VAR>f : (j : α) → B ⟶ X j<VAR>inst✝¹ : HasWidePushout B X f<VAR>inst✝ : PreservesColimit (wideSpan B X f) (forget C)<VAR>x : (forget C).obj (widePushout B X f)<GOAL>∃ i y, (ι f i) y = x
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>B : C<VAR>α : Type v<VAR>inst✝² : Nonempty α<VAR>X : α → C<VAR>f : (j : α) → B ⟶ X j<VAR>inst✝¹ : HasWidePushout B X f<VAR>inst✝ : PreservesColimit (wideSpan B X f) (forget C)<VAR>y : (forget C).obj B<GOAL>∃ i y_1, (ι f i) y_1 = (head f) y
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>B : C<VAR>α : Type v<VAR>inst✝² : Nonempty α<VAR>X : α → C<VAR>f : (j : α) → B ⟶ X j<VAR>inst✝¹ : HasWidePushout B X f<VAR>inst✝ : PreservesColimit (wideSpan B X f) (forget C)<VAR>i : α<VAR>y : (forget C).obj (X i)<GOAL>∃ i_1 y_1, (ι f i_1) y_1 = (ι f i) y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F (α ::: Fix F α)<GOAL>rec (MvFunctor.map (TypeVec.id ::: mk)) (mk x) = x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F (α ::: Fix F α)<GOAL>((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F (α ::: Fix F α)<GOAL>((TypeVec.id ::: mk) ⊚ (TypeVec.id ::: dest)) <$$> x = TypeVec.id <$$> x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F (α ::: Fix F α)<GOAL>(TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F (α ::: Fix F α)<VAR>this : mk ∘ dest = _root_.id<GOAL>(TypeVec.id ::: mk ∘ dest) <$$> x = TypeVec.id <$$> x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<GOAL>(CoordinateRing.basis W) 1 = (mk W) Y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>s : Finset β<VAR>a₁ a₂ : α<VAR>inst✝ : T2Space α<GOAL>HasProd f a₁ → HasProd f a₂ → a₁ = a₂
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : IsEmpty ι<VAR>o : Orientation R M ι<GOAL>o = positiveOrientation ∨ o = -positiveOrientation
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : IsEmpty ι<VAR>x : M [⋀^ι]→ₗ[R] R<VAR>hx : x ≠ 0<GOAL>rayOfNeZero R x hx = positiveOrientation ∨ rayOfNeZero R x hx = -positiveOrientation
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : IsEmpty ι<VAR>x : M [⋀^ι]→ₗ[R] R<VAR>hx : x ≠ 0<GOAL>rayOfNeZero R x hx = rayOfNeZero R (AlternatingMap.constOfIsEmpty R M ι 1) ⋯ ∨ rayOfNeZero R x hx = rayOfNeZero R (-AlternatingMap.constOfIsEmpty R M ι 1) ⋯
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : IsEmpty ι<VAR>x : M [⋀^ι]→ₗ[R] R<VAR>hx : x ≠ 0<GOAL>SameRay R x (AlternatingMap.constOfIsEmpty R M ι 1) ∨ SameRay R x (-AlternatingMap.constOfIsEmpty R M ι 1)
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : IsEmpty ι<VAR>x : M [⋀^ι]→ₗ[R] R<VAR>hx : x ≠ 0<GOAL>¬LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : IsEmpty ι<VAR>x : M [⋀^ι]→ₗ[R] R<VAR>hx : x ≠ 0<VAR>h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]<VAR>f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : IsEmpty ι<VAR>x : M [⋀^ι]→ₗ[R] R<VAR>hx : x ≠ 0<VAR>h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]<VAR>f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm<VAR>H : LinearIndependent R ![f x, 1]<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : IsEmpty ι<VAR>x : M [⋀^ι]→ₗ[R] R<VAR>hx : x ≠ 0<VAR>h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]<VAR>f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm<VAR>H : ∀ (s : Finset (Fin (Nat.succ 0).succ)) (g : Fin (Nat.succ 0).succ → R), ∑ i ∈ s, g i • ![f x, 1] i = 0 → ∀ i ∈ s, g i = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>a : R<GOAL>(C a * X).degree ≤ 1
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<GOAL>span K (Weight.toLinear K (↥H) L '' {α | α.IsNonZero}) = ⊤
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<GOAL>span K (Weight.toLinear K (↥H) L '' {α | α.IsNonZero}) = span K (range (Weight.toLinear K (↥H) L))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<GOAL>span K (range (Weight.toLinear K (↥H) L)) ≤ span K (Weight.toLinear K (↥H) L '' {α | α.IsNonZero})
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<GOAL>range (Weight.toLinear K (↥H) L) ⊆ insert 0 (Weight.toLinear K (↥H) L '' {α | α.IsNonZero})
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>α : Weight K (↥H) L<GOAL>Weight.toLinear K (↥H) L α ∈ insert 0 (Weight.toLinear K (↥H) L '' {α | α.IsNonZero})
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>α : Weight K (↥H) L<GOAL>α.IsZero ∨ ∃ x, x.IsNonZero ∧ Weight.toLinear K (↥H) L x = Weight.toLinear K (↥H) L α
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>q : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hq : ∀ (i : ι), a i = 0 ∨ 0 < q i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / q i ^ s.re<GOAL>HasSum (fun i => ↑π ^ (-s) * Complex.Gamma s * a i / ↑(q i) ^ s) (mellin F s)
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>q : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hq : ∀ (i : ι), a i = 0 ∨ 0 < q i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / q i ^ s.re<VAR>hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i<GOAL>HasSum (fun i => ↑π ^ (-s) * Complex.Gamma s * a i / ↑(q i) ^ s) (mellin F s)
<VAR>ι : Type u_1<VAR>inst✝ : Countable ι<VAR>a : ι → ℂ<VAR>q : ι → ℝ<VAR>F : ℝ → ℂ<VAR>s : ℂ<VAR>hq : ∀ (i : ι), a i = 0 ∨ 0 < q i<VAR>hs : 0 < s.re<VAR>hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)<VAR>h_sum : Summable fun i => ‖a i‖ / q i ^ s.re<VAR>hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i<VAR>i : ι<GOAL>↑π ^ (-s) * Complex.Gamma s * a i / ↑(q i) ^ s = Complex.Gamma s * a i / ↑(π * q i) ^ s