ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>h : p a = true<VAR>b : α<GOAL>decide ((b == a) = true ∧ p b = true) = (b == a)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>h : p a = true<VAR>b : α<GOAL>decide (b = a) = true ∧ p b = true ↔ b = a
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{u_6, u_1} C<VAR>inst✝⁵ : Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>a : M<VAR>X : C<GOAL>(F.shiftIso 0 a a ⋯).inv.app X = (F.shift a).map ((shiftFunctorZero C M).inv.app X)
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>Γ : Subgroup SL(2, ℤ)<GOAL>(g • z).im = z.im / Complex.normSq (denom (↑g) z)
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>Γ : Subgroup SL(2, ℤ)<GOAL>z.im = (↑↑↑g).det * z.im
<VAR>x : ℝ<VAR>h : |x| < 1<VAR>term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)<VAR>h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)<GOAL>HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)) (log (1 + x) - log (1 - x))
<VAR>x : ℝ<VAR>h : |x| < 1<VAR>term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)<VAR>h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)<GOAL>HasSum term (log (1 + x) - log (1 - x))
<VAR>x : ℝ<VAR>h : |x| < 1<VAR>term : ℕ → ℝ := fun n => -1 * ((-x) ^ (n + 1) / (↑n + 1)) + x ^ (n + 1) / (↑n + 1)<VAR>h_term_eq_goal : (term ∘ fun x => 2 * x) = fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)<GOAL>∀ x ∉ Set.range fun x => 2 * x, term x = 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → AddCommMonoid (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i : ι), β i<GOAL>f.sum single = f
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → AddCommMonoid (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i : ι), β i<VAR>this : (liftAddHom (singleAddHom β)) f = (AddMonoidHom.id (Π₀ (i : ι), β i)) f<GOAL>f.sum single = f
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → AddCommMonoid (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>f : Π₀ (i : ι), β i<VAR>this : (f.sum fun x => ⇑(singleAddHom β x)) = (AddMonoidHom.id (Π₀ (i : ι), β i)) f<GOAL>f.sum single = f
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S✝<VAR>inst✝ : NonAssocSemiring T<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subsemiring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℝ≥0∞<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha : a ≠ 0<GOAL>padicValInt p (a * ↑p) = padicValInt p a + 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ℤ<VAR>ha : a ≠ 0<GOAL>padicValInt p a + padicValInt p ↑p = padicValInt p a + 1
<VAR>α : Type u_1<VAR>l r : ℕ<GOAL>l + r ≤ 1 → r + l ≤ 1
<VAR>α : Type u_1<VAR>l r : ℕ<GOAL>r + l ≤ 1 → r + l ≤ 1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a b : α i<VAR>x : (a : ι) → α a<GOAL>x ∈ update f i '' Icc a b ↔ x ∈ Icc (update f i a) (update f i b)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a b : α i<VAR>x : (a : ι) → α a<GOAL>x ∈ update f i '' Icc a b ↔ x ∈ univ.pi fun i_1 => Icc (update f i a i_1) (update f i b i_1)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r✝ : R<VAR>e✝ : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>i : σ<VAR>e : ℕ<VAR>r : R<VAR>he : e ≠ 0<VAR>hr : r ≠ 0<GOAL>((monomial (Finsupp.single i e)) r).vars = {i}
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>(mappingConeCompTriangleh f g).mor₂ ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (mappingConeCompTriangle f g).mor₁)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>(mappingConeCompTriangleh f g).mor₂ ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom ≫ (HomotopyCategory.isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)).inv = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (mappingConeCompTriangle f g).mor₁) ≫ (HomotopyCategory.isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)).inv
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>(HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (map (f ≫ g) g f (𝟙 X₃) ⋯) ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).inv = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (map f (f ≫ g) (𝟙 X₁) g ⋯)) ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).inv
<VAR>x y : ℝ<VAR>h : rexp x = 0<GOAL>cexp ↑x = 0
<VAR>x y : ℝ<VAR>h : ↑(cexp ↑x).re = ↑0<GOAL>cexp ↑x = 0
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 < x<GOAL>1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>h✝ h : α ≃ᵢ β<VAR>x : β<VAR>r : ℝ<GOAL>⇑h ⁻¹' Metric.closedBall x r = Metric.closedBall (h.symm x) r
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : Subgroup G<VAR>g : ι → G<VAR>hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ<VAR>hind : H.index = s.card<GOAL>(↑s).PairwiseDisjoint fun x => g x • ↑H
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : Subgroup G<VAR>g : ι → G<VAR>hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ<VAR>hind : H.index = s.card<VAR>this : Fintype (G ⧸ H)<GOAL>(↑s).PairwiseDisjoint fun x => g x • ↑H
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : Subgroup G<VAR>g : ι → G<VAR>hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ<VAR>hind : H.index = s.card<VAR>this : Fintype (G ⧸ H)<GOAL>Function.Bijective fun x => ↑(g ↑x)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : Subgroup G<VAR>g : ι → G<VAR>hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ<VAR>hind : H.index = s.card<VAR>this : Fintype (G ⧸ H)<GOAL>(Function.Surjective fun x => ↑(g ↑x)) ∧ Fintype.card { x // x ∈ s } = Fintype.card (G ⧸ H)
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁶ : Category.{max v u, w} D<VAR>inst✝⁵ : ConcreteCategory D<VAR>inst✝⁴ : PreservesLimits (forget D)<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝ : (forget D).ReflectsIsomorphisms<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<GOAL>Presheaf.IsSheaf J (J.plusObj P)
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁶ : Category.{max v u, w} D<VAR>inst✝⁵ : ConcreteCategory D<VAR>inst✝⁴ : PreservesLimits (forget D)<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝ : (forget D).ReflectsIsomorphisms<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<GOAL>∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer (J.plusObj P))
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁶ : Category.{max v u, w} D<VAR>inst✝⁵ : ConcreteCategory D<VAR>inst✝⁴ : PreservesLimits (forget D)<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝ : (forget D).ReflectsIsomorphisms<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<GOAL>IsIso (S.toMultiequalizer (J.plusObj P))
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁶ : Category.{max v u, w} D<VAR>inst✝⁵ : ConcreteCategory D<VAR>inst✝⁴ : PreservesLimits (forget D)<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝ : (forget D).ReflectsIsomorphisms<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<GOAL>IsIso ((forget D).map (S.toMultiequalizer (J.plusObj P)))
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁶ : Category.{max v u, w} D<VAR>inst✝⁵ : ConcreteCategory D<VAR>inst✝⁴ : PreservesLimits (forget D)<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>inst✝ : (forget D).ReflectsIsomorphisms<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>S : J.Cover X<GOAL>Function.Bijective ((forget D).map (S.toMultiequalizer (J.plusObj P)))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>r R : ℝ<VAR>h0 : 0 < r<VAR>hle : r ≤ R<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hd : ∀ z ∈ (ball c R \ closedBall c r) \ s, DifferentiableAt ℂ f z<VAR>A : Set ℂ := closedBall c R \ ball c r<VAR>hc : ContinuousOn f A<GOAL>(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>R : ℝ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>a : ℝ<VAR>h0 : 0 < rexp a<VAR>hle : rexp a ≤ R<VAR>hd : ∀ z ∈ (ball c R \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z<VAR>A : Set ℂ := closedBall c R \ ball c (rexp a)<VAR>hc : ContinuousOn f A<GOAL>(∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>a : ℝ<VAR>h0 : 0 < rexp a<VAR>b : ℝ<VAR>hle : rexp a ≤ rexp b<VAR>hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z<VAR>A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)<VAR>hc : ContinuousOn f A<GOAL>(∮ (z : ℂ) in C(c, rexp b), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>a : ℝ<VAR>h0 : 0 < rexp a<VAR>b : ℝ<VAR>hle : a ≤ b<VAR>hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z<VAR>A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)<VAR>hc : ContinuousOn f A<GOAL>(∮ (z : ℂ) in C(c, rexp b), (z - c)⁻¹ • f z) = ∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>a : ℝ<VAR>h0 : 0 < rexp a<VAR>b : ℝ<VAR>hle : a ≤ b<VAR>hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z<VAR>A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)<VAR>hc : ContinuousOn f A<GOAL>∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp a) θ)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>a : ℝ<VAR>h0 : 0 < rexp a<VAR>b : ℝ<VAR>hle : a ≤ b<VAR>hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z<VAR>A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)<VAR>hc : ContinuousOn f A<VAR>R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]<VAR>g : ℂ → ℂ := fun x => c + cexp x<GOAL>∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp a) θ)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>a : ℝ<VAR>h0 : 0 < rexp a<VAR>b : ℝ<VAR>hle : a ≤ b<VAR>hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z<VAR>A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)<VAR>hc : ContinuousOn f A<VAR>R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]<VAR>g : ℂ → ℂ := fun x => c + cexp x<VAR>hdg : Differentiable ℂ g<GOAL>∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp a) θ)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>a : ℝ<VAR>h0 : 0 < rexp a<VAR>b : ℝ<VAR>hle : a ≤ b<VAR>hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z<VAR>A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)<VAR>hc : ContinuousOn f A<VAR>R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]<VAR>g : ℂ → ℂ := fun x => c + cexp x<VAR>hdg : Differentiable ℂ g<VAR>hs : (g ⁻¹' s).Countable<GOAL>∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp a) θ)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>a : ℝ<VAR>h0 : 0 < rexp a<VAR>b : ℝ<VAR>hle : a ≤ b<VAR>hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z<VAR>A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)<VAR>hc : ContinuousOn f A<VAR>R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]<VAR>g : ℂ → ℂ := fun x => c + cexp x<VAR>hdg : Differentiable ℂ g<VAR>hs : (g ⁻¹' s).Countable<VAR>h_maps : MapsTo g R A<GOAL>∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp a) θ)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>a : ℝ<VAR>h0 : 0 < rexp a<VAR>b : ℝ<VAR>hle : a ≤ b<VAR>hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z<VAR>A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)<VAR>R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]<VAR>g : ℂ → ℂ := fun x => c + cexp x<VAR>hdg : Differentiable ℂ g<VAR>hs : (g ⁻¹' s).Countable<VAR>h_maps : MapsTo g R A<VAR>hc : ContinuousOn (f ∘ g) R<GOAL>∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp a) θ)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>a : ℝ<VAR>h0 : 0 < rexp a<VAR>b : ℝ<VAR>hle : a ≤ b<VAR>A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)<VAR>R : Set ℂ := [[a, b]] ×ℂ [[0, 2 * π]]<VAR>g : ℂ → ℂ := fun x => c + cexp x<VAR>hdg : Differentiable ℂ g<VAR>hs : (g ⁻¹' s).Countable<VAR>h_maps : MapsTo g R A<VAR>hc : ContinuousOn (f ∘ g) R<VAR>hd : ∀ z ∈ Ioo (min a b) (max a b) ×ℂ Ioo (min 0 (2 * π)) (max 0 (2 * π)) \ g ⁻¹' s, DifferentiableAt ℂ (f ∘ g) z<GOAL>∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp b) θ) = ∫ (θ : ℝ) in 0 ..2 * π, I • f (circleMap c (rexp a) θ)
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>C0 : 0 ≤ C<GOAL>‖f‖ ≤ C ↔ ∀ (x : α), ‖f x‖ ≤ C
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this : 4 = 2 * 2<GOAL>stirlingSeq n ^ 4 / stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Wallis.W n
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this : 4 = 2 * 2<GOAL>((↑n ! / (√(2 * ↑n) * (↑n / rexp 1) ^ n)) ^ 2) ^ 2 / (↑(2 * n)! / (√(2 * ↑(2 * n)) * (↑(2 * n) / rexp 1) ^ (2 * n))) ^ 2 * (↑n / (2 * ↑n + 1)) = 2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this : 4 = 2 * 2<GOAL>(↑n ! ^ 2) ^ 2 / ((√(2 * ↑n) ^ 2) ^ 2 * ((↑n ^ n / rexp 1 ^ n) ^ 2) ^ 2) / (↑(2 * n)! ^ 2 / (√(2 * ↑(2 * n)) ^ 2 * (↑(2 * n) ^ (2 * n) / rexp 1 ^ (2 * n)) ^ 2)) * (↑n / (2 * ↑n + 1)) = 2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this : 4 = 2 * 2<GOAL>(↑n ! ^ 2) ^ 2 / ((2 * ↑n) ^ 2 * ((↑n ^ n / rexp 1 ^ n) ^ 2) ^ 2) / (↑(2 * n)! ^ 2 / (2 * ↑(2 * n) * (↑(2 * n) ^ (2 * n) / rexp 1 ^ (2 * n)) ^ 2)) * (↑n / (2 * ↑n + 1)) = 2 ^ (4 * n) * ↑n ! ^ 4 / (↑(2 * n)! ^ 2 * (2 * ↑n + 1))
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this : 4 = 2 * 2<GOAL>0 ≤ 2 * ↑(2 * n)
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this : 4 = 2 * 2<GOAL>0 ≤ 2 * ↑n
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this : 4 = 2 * 2<GOAL>(↑n ! ^ 2) ^ 2 * rexp (2 * (2 * ↑n)) * (2 * (2 * ↑n) * ((2 * ↑n) ^ (2 * n)) ^ 2) * ↑n * (↑(2 * n)! ^ 2 * (2 * ↑n + 1)) = 2 ^ (4 * n) * ↑n ! ^ 4 * ((2 * ↑n) ^ 2 * ((↑n ^ n) ^ 2) ^ 2 * (↑(2 * n)! ^ 2 * rexp (2 * (2 * ↑n))) * (2 * ↑n + 1))
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<GOAL>count p (n + 1) = count (fun k => p (k + 1)) n + if p 0 then 1 else 0
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>M : Type uM<VAR>ι : Type uι<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>b : Basis ι R M<VAR>a : A<VAR>i : ι<GOAL>(basis A b).repr.symm (Finsupp.single i a) = a ⊗ₜ[R] b.repr.symm (Finsupp.single i 1)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>M : Type uM<VAR>ι : Type uι<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>b : Basis ι R M<VAR>a : A<VAR>i : ι<GOAL>(basisAux A b).invFun (Finsupp.single i a) = a ⊗ₜ[R] b.repr.symm (Finsupp.single i 1)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : ℝ ≃ᵐ ℝ<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<VAR>f' : ℝ → ℝ<VAR>hf' : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x<VAR>g : ℝ → ℝ<VAR>hg : 0 ≤ᶠ[ae volume] g<VAR>hg_int : Integrable g volume<GOAL>(Measure.map (⇑f.symm) (volume.withDensity fun x => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : ℝ ≃ᵐ ℝ<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<VAR>f' : ℝ → ℝ<VAR>hf' : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x<VAR>g : ℝ → ℝ<VAR>hg : 0 ≤ᶠ[ae volume] g<VAR>hg_int : Integrable g volume<GOAL>ENNReal.ofReal (∫ (x : ℝ) in s, |(ContinuousLinearMap.smulRight 1 (f' x)).det| * g (f x)) = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))
<VAR>R S : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower R S M<VAR>inst✝¹ : FormallyUnramified R S<VAR>inst✝ : EssFiniteType R S<VAR>x : M<GOAL>(TensorProduct.AlgebraTensorModule.lift (↑R (lsmul S S M).toLinearMap.flip).flip ∘ₗ sec R S M) x = LinearMap.id x
<VAR>R S : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : Algebra R S<VAR>M : Type u_1<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower R S M<VAR>inst✝¹ : FormallyUnramified R S<VAR>inst✝ : EssFiniteType R S<VAR>x : M<GOAL>(_root_.TensorProduct.lift (↑R (↑R (lsmul S S M).toLinearMap.flip).flip)) ((TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip x)) (elem R S)) = x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : Group H<VAR>inst✝⁸ : MulAction G α<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MulAction H β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>s t✝ : Set α<VAR>μ : Measure α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : MeasurableSMul G α<VAR>inst✝¹ : SMulInvariantMeasure G α μ<VAR>inst✝ : Countable G<VAR>ν : Measure α<VAR>h : IsFundamentalDomain G s μ<VAR>f : α → ℝ≥0∞<VAR>t : Set α<GOAL>∑' (g : G), ∫⁻ (x : α) in t ∩ g⁻¹ • s, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g⁻¹ • (g • t ∩ s), f x ∂μ
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<VAR>i : (Quotient.out o).α<GOAL>typein (fun x x_1 => x < x_1) i < o
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<VAR>i : (Quotient.out o).α<GOAL>typein (fun x x_1 => x < x_1) i < type fun x x_1 => x < x_1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<GOAL>IsCycleOn 1 s ↔ s.Subsingleton
<VAR>d x y : ℤ<GOAL>{ re := x, im := y } * star { re := x, im := y } = ↑x * ↑x - ↑d * ↑y * ↑y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>t : Multiset β<VAR>s₁ s₂ : Multiset α<VAR>t₁ t₂ : Multiset β<VAR>a : α<VAR>b : β<VAR>x : α ⊕ β<GOAL>inr b ∈ s.disjSum t ↔ b ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>t : Multiset β<VAR>s₁ s₂ : Multiset α<VAR>t₁ t₂ : Multiset β<VAR>a : α<VAR>b : β<VAR>x : α ⊕ β<GOAL>(∃ b_1 ∈ t, inr b_1 = inr b) ↔ b ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>t : Multiset β<VAR>s₁ s₂ : Multiset α<VAR>t₁ t₂ : Multiset β<VAR>a : α<VAR>b : β<VAR>x : α ⊕ β<GOAL>¬∃ a ∈ s, inl a = inr b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>t : Multiset β<VAR>s₁ s₂ : Multiset α<VAR>t₁ t₂ : Multiset β<VAR>a✝ : α<VAR>b : β<VAR>x : α ⊕ β<VAR>a : α<VAR>left✝ : a ∈ s<VAR>ha : inl a = inr b<GOAL>False