ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{v}<VAR>x✝ : ∃ a, lift.{u, v} o = succ a<VAR>a : Ordinal.{max v u}<VAR>h : lift.{u, v} o = succ a<VAR>b : Ordinal.{v}<VAR>e : lift.{u, v} b = a<GOAL>lift.{u, v} o = lift.{u, v} (succ b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{v}<VAR>x✝ : ∃ a, o = succ a<VAR>a : Ordinal.{v}<VAR>h : o = succ a<GOAL>lift.{u, v} o = succ (lift.{u, v} a)
<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>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<GOAL>whiskerRight (J.toSheafify P) F ≫ (J.plusCompIso F (J.plusObj P)).hom ≫ J.plusMap (J.plusCompIso F P).hom = J.toSheafify (P ⋙ F)
<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>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<GOAL>whiskerRight (J.toPlus P) F ≫ whiskerRight (J.plusMap (J.toPlus P)) F ≫ (J.plusCompIso F (J.plusObj P)).hom ≫ J.plusMap (J.plusCompIso F P).hom = J.toSheafify (P ⋙ F)
<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>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<GOAL>whiskerRight (J.toPlus P) F ≫ ((J.plusCompIso F P).hom ≫ J.plusMap (whiskerRight (J.toPlus P) F)) ≫ J.plusMap (J.plusCompIso F P).hom = J.toSheafify (P ⋙ F)
<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>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<GOAL>J.toPlus (P ⋙ F) ≫ J.plusMap (J.toPlus (P ⋙ F)) = J.toSheafify (P ⋙ F)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : F →L[𝕜] G<VAR>B : E →L[𝕜] F<VAR>v : G<GOAL>(adjoint (A.comp B)) v = ((adjoint B).comp (adjoint A)) v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : F →L[𝕜] G<VAR>B : E →L[𝕜] F<VAR>v : G<VAR>w : E<GOAL>⟪w, (adjoint (A.comp B)) v⟫_𝕜 = ⟪w, ((adjoint B).comp (adjoint A)) v⟫_𝕜
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a ≠ 0 → ∀ (n : ℕ), a ^ n ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>hf : AEMeasurable f (Measure.map g μ)<VAR>hg : AEMeasurable g μ<GOAL>Measure.map g μ = Measure.map (AEMeasurable.mk g hg) μ
<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<VAR>hodd : p ≠ 2<GOAL>Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)
<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<VAR>hodd : p ≠ 2<GOAL>Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra R B<VAR>f : R →+* S<VAR>g : S →+* T<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsScalarTower R A B<VAR>I : Ideal S<VAR>hf : f.IsIntegral<VAR>x✝ : S ⧸ I<VAR>x : S<VAR>p : R[X]<VAR>p_monic : p.Monic<VAR>hpx : eval₂ f x p = 0<GOAL>(Ideal.quotientMap I f ⋯).IsIntegralElem (Quot.mk Setoid.r x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra R B<VAR>f : R →+* S<VAR>g : S →+* T<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsScalarTower R A B<VAR>I : Ideal S<VAR>hf : f.IsIntegral<VAR>x✝ : S ⧸ I<VAR>x : S<VAR>p : R[X]<VAR>p_monic : p.Monic<VAR>hpx : eval₂ f x p = 0<GOAL>eval₂ (Ideal.quotientMap I f ⋯) (Quot.mk Setoid.r x) (Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p) = 0
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>cR : Type u<VAR>inst✝ : CommRing cR<VAR>s : Set R<VAR>a : R<VAR>h : a ∈ closure s<VAR>b : R<VAR>ih : ∃ L, (∀ l ∈ L, ∀ x ∈ l, x ∈ s ∨ x = -1) ∧ (List.map List.prod L).sum = b<VAR>L1 : List (List R)<VAR>h1 : ∀ l ∈ L1, ∀ x ∈ l, x ∈ s ∨ x = -1<VAR>x✝ : AddGroup.InClosure (Monoid.Closure s) (List.map List.prod L1).sum<GOAL>(List.map (fun x => -x.prod) L1).sum = -(List.map List.prod L1).sum
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>cR : Type u<VAR>inst✝ : CommRing cR<VAR>s : Set R<VAR>a : R<VAR>h : a ∈ closure s<VAR>b : R<VAR>ih✝ : ∃ L, (∀ l ∈ L, ∀ x ∈ l, x ∈ s ∨ x = -1) ∧ (List.map List.prod L).sum = b<VAR>L1 : List (List R)<VAR>h1 : ∀ l ∈ L1, ∀ x ∈ l, x ∈ s ∨ x = -1<VAR>x✝ : AddGroup.InClosure (Monoid.Closure s) (List.map List.prod L1).sum<VAR>hd : List R<VAR>tl : List (List R)<VAR>ih : (List.map (fun x => -x.prod) tl).sum = -(List.map List.prod tl).sum<GOAL>(List.map (fun x => -x.prod) (hd :: tl)).sum = -(List.map List.prod (hd :: tl)).sum
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>cR : Type u<VAR>inst✝ : CommRing cR<VAR>s : Set R<VAR>a : R<VAR>h : a ∈ closure s<VAR>r1 r2 : R<VAR>ih1 : ∃ L, (∀ l ∈ L, ∀ x ∈ l, x ∈ s ∨ x = -1) ∧ (List.map List.prod L).sum = r1<VAR>ih2 : ∃ L, (∀ l ∈ L, ∀ x ∈ l, x ∈ s ∨ x = -1) ∧ (List.map List.prod L).sum = r2<VAR>L1 : List (List R)<VAR>h1 : ∀ l ∈ L1, ∀ x ∈ l, x ∈ s ∨ x = -1<VAR>L2 : List (List R)<VAR>h2 : ∀ l ∈ L2, ∀ x ∈ l, x ∈ s ∨ x = -1<VAR>x✝¹ : AddGroup.InClosure (Monoid.Closure s) (List.map List.prod L1).sum<VAR>x✝ : AddGroup.InClosure (Monoid.Closure s) (List.map List.prod L2).sum<GOAL>(List.map List.prod (L1 ++ L2)).sum = (List.map List.prod L1).sum + (List.map List.prod L2).sum
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero β<VAR>inst✝ : SMulWithZero α β<VAR>s : Set α<VAR>t : Set β<VAR>ht : t.Nonempty<GOAL>0 ⊆ 0 • t
<VAR>l : List ℕ<VAR>a m n : ℕ<VAR>hn : n ≠ 0<GOAL>(n - fib n.greatestFib).greatestFib ≤ n.greatestFib - 2
<VAR>l : List ℕ<VAR>a m n : ℕ<VAR>hn : n ≠ 0<GOAL>n < fib (n.greatestFib + 1)
<VAR>l : List ℕ<VAR>a m n : ℕ<VAR>hn : n ≠ 0<GOAL>n.greatestFib ≠ 0
<VAR>l : List ℕ<VAR>a m n : ℕ<VAR>hn : n ≠ 0<GOAL>n.greatestFib - 1 ≠ 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : AddCommMonoid M''<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>F₂ : BilinForm R M<VAR>ι : Type u_9<VAR>b : Basis ι R M<VAR>x y : M<GOAL>((b.repr x).sum fun i xi => (b.repr y).sum fun j yj => xi • yj • (B (b i)) (b j)) = (B x) y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : AddCommMonoid M''<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>F₂ : BilinForm R M<VAR>ι : Type u_9<VAR>b : Basis ι R M<VAR>x y : M<GOAL>((b.repr x).sum fun i xi => (b.repr y).sum fun j yj => xi • yj • (B (b i)) (b j)) = (B ((Finsupp.total ι M R ⇑b) (b.repr x))) ((Finsupp.total ι M R ⇑b) (b.repr y))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a✝ b✝ c✝ d a b c : G<GOAL>c / a / (c / b) = b / a
<VAR>β : Type v<VAR>inst✝ : NormedField β<VAR>f : ℕ → β<VAR>hf : CauchySeq f<GOAL>IsCauSeq norm f
<VAR>β : Type v<VAR>inst✝ : NormedField β<VAR>f : ℕ → β<VAR>hf : CauchySeq f<VAR>hf1 : (map f atTop).NeBot<VAR>hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s<GOAL>IsCauSeq norm f
<VAR>β : Type v<VAR>inst✝ : NormedField β<VAR>f : ℕ → β<VAR>hf : CauchySeq f<VAR>hf1 : (map f atTop).NeBot<VAR>hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∃ i, ∀ j ≥ i, ‖f j - f i‖ < ε
<VAR>β : Type v<VAR>inst✝ : NormedField β<VAR>f : ℕ → β<VAR>hf : CauchySeq f<VAR>hf1 : (map f atTop).NeBot<VAR>hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>t : Set β<VAR>ht : t ∈ map f atTop<VAR>htsub : t ×ˢ t ⊆ {x | dist x.1 x.2 < ε}<GOAL>∃ i, ∀ j ≥ i, ‖f j - f i‖ < ε
<VAR>β : Type v<VAR>inst✝ : NormedField β<VAR>f : ℕ → β<VAR>hf : CauchySeq f<VAR>hf1 : (map f atTop).NeBot<VAR>hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>t : Set β<VAR>htsub : t ×ˢ t ⊆ {x | dist x.1 x.2 < ε}<VAR>ht : ∃ a, ∀ b ≥ a, f b ∈ t<GOAL>∃ i, ∀ j ≥ i, ‖f j - f i‖ < ε
<VAR>β : Type v<VAR>inst✝ : NormedField β<VAR>f : ℕ → β<VAR>hf : CauchySeq f<VAR>hf1 : (map f atTop).NeBot<VAR>hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>t : Set β<VAR>htsub : t ×ˢ t ⊆ {x | dist x.1 x.2 < ε}<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, f b ∈ t<VAR>j : ℕ<VAR>hj : j ≥ N<GOAL>(f j, f N) ∈ t ×ˢ t
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group G'<VAR>inst✝⁴ : Group G''<VAR>A : Type u_4<VAR>inst✝³ : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝² : Group N<VAR>P : Type u_6<VAR>inst✝¹ : Group P<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>inst✝ : (i : η) → Group (f i)<VAR>p : (i : η) → f i<VAR>hp : p ∈ pi univ fun i => ⊥<GOAL>p = 1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group G'<VAR>inst✝⁴ : Group G''<VAR>A : Type u_4<VAR>inst✝³ : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝² : Group N<VAR>P : Type u_6<VAR>inst✝¹ : Group P<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>inst✝ : (i : η) → Group (f i)<VAR>p : (i : η) → f i<VAR>hp : ∀ i ∈ univ, p i = 1<GOAL>p = 1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group G'<VAR>inst✝⁴ : Group G''<VAR>A : Type u_4<VAR>inst✝³ : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝² : Group N<VAR>P : Type u_6<VAR>inst✝¹ : Group P<VAR>η : Type u_7<VAR>f : η → Type u_8<VAR>inst✝ : (i : η) → Group (f i)<VAR>p : (i : η) → f i<VAR>hp : ∀ i ∈ univ, p i = 1<VAR>j : η<GOAL>p j = 1 j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α<VAR>inst✝⁵ : PseudoEMetricSpace β<VAR>inst✝⁴ : PseudoEMetricSpace γ<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DilationClass F α β<VAR>inst✝¹ : FunLike G β γ<VAR>inst✝ : DilationClass G β γ<VAR>f✝ : F<VAR>g✝ : G<VAR>x✝ y✝ z : α<VAR>s : Set α<VAR>g : β →ᵈ γ<VAR>f : α →ᵈ β<VAR>x y : α<VAR>hα : edist x y ≠ 0 ∧ edist x y ≠ ⊤<GOAL>ratio (g.comp f) = ratio g * ratio f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α<VAR>inst✝⁵ : PseudoEMetricSpace β<VAR>inst✝⁴ : PseudoEMetricSpace γ<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DilationClass F α β<VAR>inst✝¹ : FunLike G β γ<VAR>inst✝ : DilationClass G β γ<VAR>f✝ : F<VAR>g✝ : G<VAR>x✝ y✝ z : α<VAR>s : Set α<VAR>g : β →ᵈ γ<VAR>f : α →ᵈ β<VAR>x y : α<VAR>hα : edist x y ≠ 0 ∧ edist x y ≠ ⊤<VAR>hgf : ↑(ratio (g.comp f)) * edist x y = edist ((g.comp f) x) ((g.comp f) y)<GOAL>ratio (g.comp f) = ratio g * ratio f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁶ : PseudoEMetricSpace α<VAR>inst✝⁵ : PseudoEMetricSpace β<VAR>inst✝⁴ : PseudoEMetricSpace γ<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DilationClass F α β<VAR>inst✝¹ : FunLike G β γ<VAR>inst✝ : DilationClass G β γ<VAR>f✝ : F<VAR>g✝ : G<VAR>x✝ y✝ z : α<VAR>s : Set α<VAR>g : β →ᵈ γ<VAR>f : α →ᵈ β<VAR>x y : α<VAR>hα : edist x y ≠ 0 ∧ edist x y ≠ ⊤<VAR>hgf : ↑(ratio (g.comp f)) = ↑(ratio g) * ↑(ratio f)<GOAL>ratio (g.comp f) = ratio g * ratio f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NonUnitalRing α<VAR>a b c : α<GOAL>a ∣ b - c ↔ a ∣ c - b
<VAR>α : Type u_1<VAR>a✝ b✝ c✝ d : α<VAR>inst✝¹ : MulZeroClass α<VAR>inst✝ : PartialOrder α<VAR>h✝ : CovariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x x_1 => x ≤ x_1<VAR>a : { x // 0 ≤ x }<VAR>b c : α<VAR>h : b ≤ c<GOAL>↑a * b ≤ ↑a * c
<VAR>α : Type u_1<VAR>a✝ b✝ c✝ d : α<VAR>inst✝¹ : MulZeroClass α<VAR>inst✝ : PartialOrder α<VAR>h✝ : CovariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x x_1 => x ≤ x_1<VAR>a : { x // 0 ≤ x }<VAR>b c : α<VAR>h : b ≤ c<VAR>ha : 0 = ↑a<GOAL>↑a * b ≤ ↑a * c
<VAR>α : Type u_1<VAR>a✝ b✝ c✝ d : α<VAR>inst✝¹ : MulZeroClass α<VAR>inst✝ : PartialOrder α<VAR>h✝ : CovariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x x_1 => x ≤ x_1<VAR>a : { x // 0 ≤ x }<VAR>b c : α<VAR>h : b ≤ c<VAR>ha : 0 < ↑a<GOAL>↑a * b ≤ ↑a * c
<VAR>m : ℕ∞<GOAL>1 = m ↔ m = 1
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<GOAL>finInsepDegree F ↥⊥ = finInsepDegree F E
<VAR>A : Type u_1<VAR>inst✝¹ : CanonicallyOrderedAddCommMonoid A<VAR>inst✝ : HasAntidiagonal A<VAR>n : A<VAR>kl : A × A<VAR>hlk : kl ∈ antidiagonal n<GOAL>kl.1 ≤ n
<VAR>A : Type u_1<VAR>inst✝¹ : CanonicallyOrderedAddCommMonoid A<VAR>inst✝ : HasAntidiagonal A<VAR>n : A<VAR>kl : A × A<VAR>hlk : kl ∈ antidiagonal n<GOAL>∃ c, n = kl.1 + c
<VAR>A : Type u_1<VAR>inst✝¹ : CanonicallyOrderedAddCommMonoid A<VAR>inst✝ : HasAntidiagonal A<VAR>n : A<VAR>kl : A × A<VAR>hlk : kl ∈ antidiagonal n<GOAL>n = kl.1 + kl.2
<GOAL>Tendsto (fun n => ∑ i ∈ Finset.range n, 1 / (↑i + 1)) atTop atTop
<GOAL>¬Summable fun i => 1 / (↑i + 1)
<GOAL>∀ (n : ℕ), 0 ≤ 1 / (↑n + 1)
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<GOAL>1 < order P L
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p₁ p₂ p₃ : P<VAR>l₁ l₂ l₃ : L<VAR>h₂₁ : p₂ ∉ l₁<VAR>h₂₂ : p₂ ∈ l₂<VAR>h₂₃ : p₂ ∈ l₃<VAR>h₃₁ : p₃ ∉ l₁<VAR>h₃₂ : p₃ ∈ l₂<VAR>h₃₃ : p₃ ∉ l₃<GOAL>1 < order P L
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p₁ p₂ p₃ : P<VAR>l₁ l₂ l₃ : L<VAR>h₂₁ : p₂ ∉ l₁<VAR>h₂₂ : p₂ ∈ l₂<VAR>h₂₃ : p₂ ∈ l₃<VAR>h₃₁ : p₃ ∉ l₁<VAR>h₃₂ : p₃ ∈ l₂<VAR>h₃₃ : p₃ ∉ l₃<VAR>val✝ : Fintype { p // p ∈ l₂ }<GOAL>1 < order P L
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p₁ p₂ p₃ : P<VAR>l₁ l₂ l₃ : L<VAR>h₂₁ : p₂ ∉ l₁<VAR>h₂₂ : p₂ ∈ l₂<VAR>h₂₃ : p₂ ∈ l₃<VAR>h₃₁ : p₃ ∉ l₁<VAR>h₃₂ : p₃ ∈ l₂<VAR>h₃₃ : p₃ ∉ l₃<VAR>val✝ : Fintype { p // p ∈ l₂ }<GOAL>∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p₁ p₂ p₃ : P<VAR>l₁ l₂ l₃ : L<VAR>h₂₁ : p₂ ∉ l₁<VAR>h₂₂ : p₂ ∈ l₂<VAR>h₂₃ : p₂ ∈ l₃<VAR>h₃₁ : p₃ ∉ l₁<VAR>h₃₂ : p₃ ∈ l₂<VAR>h₃₃ : p₃ ∉ l₃<VAR>val✝ : Fintype { p // p ∈ l₂ }<GOAL>∃ a b c, ¬↑a = ↑b ∧ ¬↑a = ↑c ∧ ¬↑b = ↑c
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>p₁ p₂ p₃ : P<VAR>l₁ l₂ l₃ : L<VAR>h₂₁ : p₂ ∉ l₁<VAR>h₂₂ : p₂ ∈ l₂<VAR>h₂₃ : p₂ ∈ l₃<VAR>h₃₁ : p₃ ∉ l₁<VAR>h₃₂ : p₃ ∈ l₂<VAR>h₃₃ : p₃ ∉ l₃<VAR>val✝ : Fintype { p // p ∈ l₂ }<VAR>h : mkPoint ⋯ ∈ l₁ ∧ mkPoint ⋯ ∈ l₂<GOAL>∃ a b c, ¬↑a = ↑b ∧ ¬↑a = ↑c ∧ ¬↑b = ↑c
<VAR>α : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝¹ : CommMonoid M✝<VAR>s₂ s₁ s : Finset α<VAR>a✝ : α<VAR>g f✝ : α → M✝<VAR>M : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>a b : ℕ<VAR>f : ℕ → ℕ → M<GOAL>∑ i ∈ Ico a b, ∑ j ∈ Ico i b, f i j = ∑ j ∈ Ico a b, ∑ i ∈ Ico a (j + 1), f i j
<VAR>α : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝¹ : CommMonoid M✝<VAR>s₂ s₁ s : Finset α<VAR>a✝ : α<VAR>g f✝ : α → M✝<VAR>M : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>a b : ℕ<VAR>f : ℕ → ℕ → M<GOAL>∑ x ∈ (Ico a b).sigma fun i => Ico i b, f x.fst x.snd = ∑ x ∈ (Ico a b).sigma fun j => Ico a (j + 1), f x.snd x.fst
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s✝ : Set α<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>f : ι → α → F'<VAR>hf : ∀ i ∈ s, Integrable (f i) μ<GOAL>μ[∑ i ∈ s, f i|m] =ᶠ[ae μ] ∑ i ∈ s, μ[f i|m]
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>ι : Type u_5<VAR>f : ι → α → F'<VAR>hf : ∀ i ∈ ∅, Integrable (f i) μ<GOAL>μ[∑ i ∈ ∅, f i|m] =ᶠ[ae μ] ∑ i ∈ ∅, μ[f i|m]
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s✝ : Set α<VAR>ι : Type u_5<VAR>f : ι → α → F'<VAR>i : ι<VAR>s : Finset ι<VAR>his : i ∉ s<VAR>heq : (∀ i ∈ s, Integrable (f i) μ) → μ[∑ i ∈ s, f i|m] =ᶠ[ae μ] ∑ i ∈ s, μ[f i|m]<VAR>hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ<GOAL>μ[∑ i ∈ insert i s, f i|m] =ᶠ[ae μ] ∑ i ∈ insert i s, μ[f i|m]
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>x : S<VAR>hx : IsIntegral R x<GOAL>Injective ⇑(Minpoly.toAdjoin R x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>x : S<VAR>hx : IsIntegral R x<VAR>P₁ : AdjoinRoot (minpoly R x)<VAR>hP₁ : (Minpoly.toAdjoin R x) P₁ = 0<GOAL>P₁ = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>x : S<VAR>hx : IsIntegral R x<VAR>P : R[X]<VAR>hP₁ : (Minpoly.toAdjoin R x) ((AdjoinRoot.mk (minpoly R x)) P) = 0<GOAL>(AdjoinRoot.mk (minpoly R x)) P = 0
<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a b : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>hc' : c ≠ ⊤<GOAL>c * a / (c * b) = a / b
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y : ℝ≥0∞<GOAL>x.toReal = y.toReal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>f : α → α<VAR>g : α → E<VAR>n : ℕ<VAR>x : α<GOAL>dist (birkhoffAverage 𝕜 f g n (f x)) (birkhoffAverage 𝕜 f g n x) = dist (g (f^[n] x)) (g x) / ↑n
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>f : k →+* K<VAR>w : InfinitePlace K<VAR>hφ : w.IsReal<GOAL>(w.comap f).IsReal
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>f : k →+* K<VAR>w : InfinitePlace K<VAR>hφ : w.IsReal<GOAL>ComplexEmbedding.IsReal (w.embedding.comp f)
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<VAR>f : k →+* K<VAR>w : InfinitePlace K<VAR>hφ : ComplexEmbedding.IsReal w.embedding<GOAL>ComplexEmbedding.IsReal (w.embedding.comp f)
<VAR>o : Ordinal.{u_1}<GOAL>(nim o).RightMoves = (Quotient.out o).α
<VAR>o : Ordinal.{u_1}<GOAL>(mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)).RightMoves = (Quotient.out o).α
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<VAR>inst✝ : NormedSpace ℂ E<VAR>hf : TorusIntegrable f c R<GOAL>IntegrableOn (fun θ => (∏ i : Fin n, ↑(R i) * cexp (↑(θ i) * I) * I) • f (torusMap c R θ)) (Icc 0 fun x => 2 * π) volume
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<VAR>inst✝ : NormedSpace ℂ E<VAR>hf : TorusIntegrable f c R<GOAL>AEStronglyMeasurable (fun θ => (∏ i : Fin n, ↑(R i) * cexp (↑(θ i) * I) * I) • f (torusMap c R θ)) (volume.restrict (Icc 0 fun x => 2 * π))