ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>inst✝² : OrderedCommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>f g✝ : ι → α<VAR>a a₁ a₂ : α<VAR>g : κ → α<VAR>e : ι → κ<VAR>he : Injective e<VAR>hs : ∀ c ∉ Set.range e, 1 ≤ g c<VAR>h : ∀ (i : ι), f i ≤ g (e i)<VAR>hf : HasProd (extend e f 1) a₁<VAR>hg : HasProd g a₂<VAR>c : κ<GOAL>extend e f 1 c ≤ g c
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>b : ℝ<VAR>hb : 1 ≤ b<GOAL>Monotone fun x => b ^ x
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>b : ℝ<VAR>hb✝ : 1 ≤ b<VAR>hb : 1 < b<GOAL>Monotone fun x => b ^ x
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hb : 1 ≤ 1<GOAL>Monotone fun x => 1 ^ x
<VAR>ι : Type u_1<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : Group α<VAR>inst✝¹ : LinearOrderedAddCommGroup β<VAR>inst✝ : GroupSeminormClass F α β<VAR>f : F<VAR>x y : α<GOAL>|f x - f y| ≤ f (x / y)
<VAR>ι : Type u_1<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : Group α<VAR>inst✝¹ : LinearOrderedAddCommGroup β<VAR>inst✝ : GroupSeminormClass F α β<VAR>f : F<VAR>x y : α<GOAL>f x ≤ f y + f (x / y) ∧ f y ≤ f x + f (x / y)
<VAR>n k : ℕ<VAR>hk : k ≤ n<GOAL>n.choose k = n ! / (k ! * (n - k)!)
<VAR>n k : ℕ<VAR>hk : k ≤ n<GOAL>n.choose k = n.choose k * (k ! * (n - k)!) / (k ! * (n - k)!)
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝¹² : AddCommMonoid M<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module S N<VAR>inst✝⁴ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>inst✝¹ : AddCommMonoid Q<VAR>inst✝ : Module S Q<VAR>m : M<GOAL>h.equiv.symm (f m) = 1 ⊗ₜ[R] m
<VAR>C : Type v₁<VAR>inst✝² : Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsCofilteredOrEmpty C<GOAL>F.Initial ↔ (∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) ∧ ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
<VAR>C : Type v₁<VAR>inst✝² : Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsCofilteredOrEmpty C<VAR>hF : F.Initial<GOAL>(∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) ∧ ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
<VAR>C : Type v₁<VAR>inst✝² : Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsCofilteredOrEmpty C<VAR>hF : F.Initial<VAR>h₁ : ∀ (d : Dᵒᵖ), ∃ c, Nonempty (d ⟶ F.op.obj c)<VAR>h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t<GOAL>(∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) ∧ ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>h : sSup S = ⊤<VAR>_i : DistribLattice α := hS.distribLattice_of_sSup_eq_top h<GOAL>ComplementedLattice α
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>h : sSup S = ⊤<VAR>_i : DistribLattice α := hS.distribLattice_of_sSup_eq_top h<VAR>_i₁ : IsAtomistic α<GOAL>ComplementedLattice α
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<GOAL>Measurable fun p => κ.rnDeriv η p.1 p.2
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<GOAL>Measurable fun p => ENNReal.ofReal (κ.rnDerivAux (κ + η) p.1 p.2) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) p.1 p.2)
<VAR>b : Ordinal.{0}<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>h : (e.oadd n a).NF<VAR>d : ω ^ b ∣ (e.oadd n a).repr<GOAL>b ≤ e.repr ∧ ω ^ b ∣ a.repr
<VAR>b : Ordinal.{0}<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>h : (e.oadd n a).NF<VAR>d : ω ^ b ∣ (e.oadd n a).repr<VAR>this : ¬(e.oadd n a).repr = repr 0<GOAL>b ≤ e.repr ∧ ω ^ b ∣ a.repr
<VAR>b : Ordinal.{0}<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>h : (e.oadd n a).NF<VAR>d : ω ^ b ∣ (e.oadd n a).repr<VAR>this : ¬(e.oadd n a).repr = repr 0<VAR>L : b ≤ e.repr<GOAL>b ≤ e.repr ∧ ω ^ b ∣ a.repr
<VAR>b : Ordinal.{0}<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>h : (e.oadd n a).NF<VAR>d : ω ^ b ∣ ω ^ e.repr * ↑↑n + a.repr<VAR>this : ¬(e.oadd n a).repr = repr 0<VAR>L : b ≤ e.repr<GOAL>b ≤ e.repr ∧ ω ^ b ∣ a.repr
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>a : α<GOAL>round (a + 1) = round a + 1
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>hf : f.degree ≤ 1<VAR>hif : 0 < (map i f).degree<GOAL>Splits i f
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>hf : f.degree ≤ 1<VAR>hif : ↑(Nat.succ 0) ≤ (map i f).degree<GOAL>Splits i f
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<GOAL>Prime hζ.subOneIntegralPowerBasis'.gen
<VAR>R : Type u<VAR>S : Type v<VAR>K✝ : Type w<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : IsDomain K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f : L[X]<VAR>hf : Irreducible f<VAR>this : Fact (Irreducible f)<GOAL>∃ g, g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g
<VAR>R : Type u<VAR>S : Type v<VAR>K✝ : Type w<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : IsDomain K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f : L[X]<VAR>hf : Irreducible f<VAR>this : Fact (Irreducible f)<VAR>h : f ≠ 0<GOAL>∃ g, g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g
<VAR>R : Type u<VAR>S : Type v<VAR>K✝ : Type w<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : IsDomain K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f : L[X]<VAR>hf : Irreducible f<VAR>this : Fact (Irreducible f)<VAR>h : f ≠ 0<VAR>h2 : IsIntegral K (AdjoinRoot.root f)<GOAL>∃ g, g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g
<VAR>R : Type u<VAR>S : Type v<VAR>K✝ : Type w<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : IsDomain K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>f : L[X]<VAR>hf : Irreducible f<VAR>this : Fact (Irreducible f)<VAR>h : f ≠ 0<VAR>h2 : IsIntegral K (AdjoinRoot.root f)<VAR>h3 : f * C f.leadingCoeff⁻¹ ∣ Polynomial.map (algebraMap K L) (minpoly K (AdjoinRoot.root f))<GOAL>∃ g, g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g
<VAR>K : Type uK<VAR>V : Type uV<VAR>inst✝⁹ : CommRing K<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module K V<VAR>inst✝⁶ : Free K V<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✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsReflexive R M<VAR>f : Dual R M<VAR>g : Dual R (Dual R M)<VAR>m : M := (evalEquiv R M).symm g<GOAL>f m = g f
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>h : ↑n ≠ 0<GOAL>(W.preΨ' n).coeff ((n ^ 2 - if Even n then 4 else 1) / 2) ≠ 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>h : ↑(2 * n) ≠ 0<GOAL>(W.preΨ' (2 * n)).coeff (((2 * n) ^ 2 - if Even (2 * n) then 4 else 1) / 2) ≠ 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>h : ↑(2 * n + 1) ≠ 0<GOAL>(W.preΨ' (2 * n + 1)).coeff (((2 * n + 1) ^ 2 - if Even (2 * n + 1) then 4 else 1) / 2) ≠ 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : UniformSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_covers : ⋃₀ 𝔖 = univ<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<GOAL>UniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ UniformInducing F
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : UniformSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<GOAL>UniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ UniformInducing F
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : UniformSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>φ : (↑(⋃₀ 𝔖) → α) ≃ᵤ (X → α) := UniformEquiv.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)<GOAL>UniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ UniformInducing F
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : UniformSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>φ : (↑(⋃₀ 𝔖) → α) ≃ᵤ (X → α) := UniformEquiv.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)<GOAL>UniformInducing (⇑φ.symm ∘ F) ↔ UniformInducing F
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<GOAL>preNormEDS b c d 2 = 1
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>s✝ t✝ u : Multiset α<VAR>a b : α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>finj : Injective f<VAR>s t : Multiset α<VAR>l₁ l₂ : List α<GOAL>List.map f (l₁.diff l₂ ++ l₂) = (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>S S₁ S₂ : ShortComplex C<VAR>hS : S.Exact<VAR>A : C<VAR>x₂ : A ⟶ S.X₂<VAR>hx₂ : x₂ ≫ S.g = 0<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>S S₁ S₂ : ShortComplex C<VAR>hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f<VAR>A : C<VAR>x₂ : A ⟶ S.X₂<VAR>hx₂ : x₂ ≫ S.g = 0<GOAL>∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι✝ → Type u_5<VAR>s✝ s₁ s₂ : Finset ι✝<VAR>i : ι✝<VAR>a : α<VAR>f✝ g : ι✝ → α<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → ℤ<VAR>n : ℤ<VAR>hf : ∀ i ∈ s, n ∣ f i<GOAL>(∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι✝ → Type u_5<VAR>s✝ s₁ s₂ : Finset ι✝<VAR>i : ι✝<VAR>a : α<VAR>f✝ g : ι✝ → α<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → ℤ<VAR>hf : ∀ i ∈ s, 0 ∣ f i<GOAL>(∑ i ∈ s, f i) / 0 = ∑ i ∈ s, f i / 0
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι✝ → Type u_5<VAR>s✝ s₁ s₂ : Finset ι✝<VAR>i : ι✝<VAR>a : α<VAR>f✝ g : ι✝ → α<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → ℤ<VAR>n : ℤ<VAR>hf : ∀ i ∈ s, n ∣ f i<VAR>hn : n ≠ 0<GOAL>(∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι✝ → Type u_5<VAR>s✝ s₁ s₂ : Finset ι✝<VAR>i : ι✝<VAR>a : α<VAR>f✝ g : ι✝ → α<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → ℤ<VAR>n : ℤ<VAR>hf : ∀ i ∈ s, n ∣ f i<VAR>hn : n ≠ 0<GOAL>∑ i ∈ s, f i = ∑ i ∈ s, f i / n * n
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι✝ → Type u_5<VAR>s✝¹ s₁ s₂ : Finset ι✝<VAR>i : ι✝<VAR>a : α<VAR>f✝ g : ι✝ → α<VAR>ι : Type u_6<VAR>s✝ : Finset ι<VAR>f : ι → ℤ<VAR>n : ℤ<VAR>hf : ∀ i ∈ s✝, n ∣ f i<VAR>hn : n ≠ 0<VAR>s : ι<VAR>hs : s ∈ s✝<GOAL>f s = f s / n * n
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝¹ : Monoid N<VAR>inst✝ : (i : ι) → DecidableEq (M i)<VAR>i : ι<VAR>p : Pair M i<VAR>hm : p.head = 1<GOAL>(rcons p).prod = of p.head * p.tail.prod
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝¹ : Monoid N<VAR>inst✝ : (i : ι) → DecidableEq (M i)<VAR>i : ι<VAR>p : Pair M i<VAR>hm : ¬p.head = 1<GOAL>(rcons p).prod = of p.head * p.tail.prod
<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 → R<VAR>u v : R<GOAL>addZ (u • P) (v • Q) = (u * v) ^ 2 * addZ P Q
<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 → R<VAR>u v : R<GOAL>u ^ 2 * P x * (v * Q z) ^ 2 - v ^ 2 * Q x * (u * P z) ^ 2 = (u * v) ^ 2 * (P x * Q z ^ 2 - Q x * P z ^ 2)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : RightHomologyMapData φ h₁ h₂<VAR>γ' : RightHomologyMapData φ' h₁ h₂<GOAL>opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : TopologicalSpace α<VAR>f : α → G<VAR>s✝ : Set α<VAR>x✝ : α<VAR>x : G<VAR>s : Set G<GOAL>x ∈ closure s ↔ ∀ U ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ U
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : TopologicalSpace α<VAR>f : α → G<VAR>s✝ : Set α<VAR>x✝ : α<VAR>x : G<VAR>s : Set G<GOAL>(∀ i ∈ 𝓝 1, ∃ y ∈ s, y ∈ {y | y / x ∈ id i}) ↔ ∀ U ∈ 𝓝 1, ∃ y ∈ s, y / x ∈ U
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : DecidableEq α<VAR>s : Finset α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>inst✝ : Fintype α<VAR>h : ∀ (a : α), n ≤ (filter (fun x => a ∈ x) B).card<GOAL>∑ s ∈ B, (univ ∩ s).card = ∑ s ∈ B, s.card
<VAR>α : Type u<VAR>l s : List ℕ<VAR>hs : s ∈ l.ranges<GOAL>Pairwise (fun x x_1 => x ≠ x_1) l.ranges.join
<VAR>α : Type u<VAR>l s : List ℕ<VAR>hs : s ∈ l.ranges<GOAL>Pairwise (fun x x_1 => x ≠ x_1) (range (Nat.sum l))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>f : α ≃. β<GOAL>(f.symm.trans f).symm = (ofSet {b | (f.symm b).isSome = true}).symm
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype l<VAR>inst✝¹ : DecidableEq l<VAR>inst✝ : DecidableEq m<VAR>A : Matrix m n 𝕜<GOAL>‖Aᴴ‖ = ‖A‖
<VAR>𝕜 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>l : Type u_4<VAR>E : Type u_5<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype l<VAR>inst✝¹ : DecidableEq l<VAR>inst✝ : DecidableEq m<VAR>A : Matrix m n 𝕜<GOAL>‖ContinuousLinearMap.adjoint (toContinuousLinearMap ((toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A))‖ = ‖A‖
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hfd : DifferentiableOn ℝ f (Ioo a b)<VAR>g g' : ℝ → ℝ<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hgd : DifferentiableOn ℝ g (Ioo a b)<VAR>h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x<VAR>hI : h a = h b<VAR>h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x<GOAL>∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hfd : DifferentiableOn ℝ f (Ioo a b)<VAR>g g' : ℝ → ℝ<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hgd : DifferentiableOn ℝ g (Ioo a b)<VAR>h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x<VAR>hI : h a = h b<VAR>h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x<VAR>hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x<GOAL>∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hfd : DifferentiableOn ℝ f (Ioo a b)<VAR>g g' : ℝ → ℝ<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hgd : DifferentiableOn ℝ g (Ioo a b)<VAR>h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x<VAR>hI : h a = h b<VAR>h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x<VAR>hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x<VAR>hhc : ContinuousOn h (Icc a b)<GOAL>∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f f' : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hfd : DifferentiableOn ℝ f (Ioo a b)<VAR>g g' : ℝ → ℝ<VAR>hgc : ContinuousOn g (Icc a b)<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hgd : DifferentiableOn ℝ g (Ioo a b)<VAR>h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x<VAR>hI : h a = h b<VAR>h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x<VAR>hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x<VAR>hhc : ContinuousOn h (Icc a b)<VAR>c : ℝ<VAR>cmem : c ∈ Ioo a b<VAR>hc : h' c = 0<GOAL>∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>m : (i : ι) → E i<GOAL>projectiveSeminorm (⨂ₜ[𝕜] (i : ι), m i) ≤ ∏ i : ι, ‖m i‖
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>m : (i : ι) → E i<GOAL>⨅ p, projectiveSeminormAux ↑p ≤ ∏ i : ι, ‖m i‖
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>m : (i : ι) → E i<GOAL>∏ i : ι, ‖m i‖ = projectiveSeminormAux ↑⟨[(1, m)], ?convert_2⟩
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>m : (i : ι) → E i<GOAL>[(1, m)] ∈ (⨂ₜ[𝕜] (i : ι), m i).lifts
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>k : Type u_3<VAR>inst✝¹ : DivisionRing k<VAR>inst✝ : CharZero k<VAR>m n : ℤ<VAR>n_dvd : n ∣ m<GOAL>↑(m / n) = ↑m / ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>k : Type u_3<VAR>inst✝¹ : DivisionRing k<VAR>inst✝ : CharZero k<VAR>m : ℤ<VAR>n_dvd : 0 ∣ m<GOAL>↑(m / 0) = ↑m / ↑0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>k : Type u_3<VAR>inst✝¹ : DivisionRing k<VAR>inst✝ : CharZero k<VAR>m n : ℤ<VAR>n_dvd : n ∣ m<VAR>hn : n ≠ 0<GOAL>↑(m / n) = ↑m / ↑n
<VAR>x a : ℂ<GOAL>a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : CompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : FirstCountableTopology α<VAR>inst✝¹ : OrderTopology α<VAR>f : Filter β<VAR>inst✝ : CountableInterFilter f<VAR>u : β → α<VAR>h : u =ᶠ[f] ⊥<GOAL>limsup u f = ⊥
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : CompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : FirstCountableTopology α<VAR>inst✝¹ : OrderTopology α<VAR>f : Filter β<VAR>inst✝ : CountableInterFilter f<VAR>u : β → α<VAR>h : u =ᶠ[f] ⊥<GOAL>limsup ⊥ f = ⊥
<VAR>h : Decidable ⊤.Dom<GOAL>⊤.toWithTop = ⊤
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeSup α<VAR>a : α<VAR>h : IsEmpty ↑(Ioi a)<GOAL>atTop = comap Subtype.val atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeSup α<VAR>a b : α<VAR>hb : b ∈ Ioi a<GOAL>atTop = comap Subtype.val atTop
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : ProperSpace α<VAR>K s : Set α<VAR>inst✝ : DiscreteTopology ↑s<VAR>hK : IsBounded K<VAR>hs : IsClosed s<GOAL>(K ∩ s).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : ProperSpace α<VAR>K s : Set α<VAR>inst✝ : DiscreteTopology ↑s<VAR>hK : IsBounded K<VAR>hs : IsClosed s<GOAL>IsCompact (closure K ∩ s)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : ProperSpace α<VAR>K s : Set α<VAR>inst✝ : DiscreteTopology ↑s<VAR>hK : IsBounded K<VAR>hs : IsClosed s<GOAL>DiscreteTopology ↑(closure K ∩ s)
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : J ⥤ C<VAR>e : K ≌ J<VAR>inst✝ : HasLimit (e.functor ⋙ F)<VAR>this : HasLimit (e.inverse ⋙ e.functor ⋙ F)<GOAL>HasLimit F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝² : OrderedRing E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : OrderClosedTopology E<VAR>l : E<VAR>f : ℕ → E<VAR>hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)<VAR>hfa : Antitone f<VAR>k : ℕ<GOAL>l ≤ ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝² : OrderedRing E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : OrderClosedTopology E<VAR>l : E<VAR>f : ℕ → E<VAR>hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)<VAR>hfa : Antitone f<VAR>k : ℕ<VAR>ha : Antitone fun n => ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i<GOAL>l ≤ ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<GOAL>xn a1 (2 * n + j) + xn a1 j ≡ 0 [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<GOAL>xn a1 n * xn a1 (n + j) + (Pell.d a1 * yn a1 n * yn a1 (n + j) + xn a1 j) ≡ 0 + 0 [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<GOAL>Pell.d a1 * yn a1 n * yn a1 (n + j) + xn a1 j ≡ 0 [MOD xn a1 n]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n j : ℕ<GOAL>Pell.d a1 * yn a1 n * (xn a1 n * yn a1 j) + (Pell.d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j) ≡ 0 + 0 [MOD xn a1 n]