ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑↑Y<VAR>hU : ↑U ⊆ Set.range ⇑f.base<GOAL>f.c.app (op U) ≫ invApp f ((Opens.map f.base).obj U) = Y.presheaf.map (eqToHom ⋯).op
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑↑Y<VAR>hU : ↑U ⊆ Set.range ⇑f.base<GOAL>(f.c.app (op U) ≫ X.presheaf.map (eqToHom ⋯)) ≫ inv (f.c.app (op ((opensFunctor f).obj ((Opens.map f.base).obj U)))) = Y.presheaf.map (eqToHom ⋯).op
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑↑Y<VAR>hU : ↑U ⊆ Set.range ⇑f.base<GOAL>f.c.app (op U) ≫ X.presheaf.map (eqToHom ⋯) = f.c.app (op U) ≫ ((TopCat.Presheaf.pushforward C f.base).obj X.presheaf).map (eqToHom ⋯).op
<VAR>d : ℤ<VAR>n : ℤ√d<GOAL>↑n.norm = n * star n
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<GOAL>∀ (x : E), ‖LinearMap.id x‖ ≤ 1 * ‖x‖
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝¹ : DecidableRel fun a b => a ∣ b<VAR>inst✝ : DecidableEq (𝓞 K)<GOAL>∃ S₁, S₁.multiplicity < S.multiplicity
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S'✝ : Solution' hζ<VAR>inst✝¹ : DecidableRel fun a b => a ∣ b<VAR>inst✝ : DecidableEq (𝓞 K)<VAR>S' : Solution hζ<VAR>hS' : S'.multiplicity = S.Solution'_descent.multiplicity<GOAL>∃ S₁, S₁.multiplicity < S.multiplicity
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : NormalizationMonoid R<VAR>inst✝¹ : DecidableRel Dvd.dvd<VAR>inst✝ : DecidableEq R<VAR>p x : R<VAR>hp : Irreducible p<VAR>hnorm : normalize p = p<VAR>n : ℕ<VAR>hle : p ^ n ∣ x<VAR>hlt : ¬p ^ (n + 1) ∣ x<VAR>this : DecidableRel fun x x_1 => x ∣ x_1 := fun x x_1 => Classical.propDecidable ((fun x x_2 => x ∣ x_2) x x_1)<VAR>hx0 : ¬x = 0<GOAL>count p (normalizedFactors x) = n
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : NormalizationMonoid R<VAR>inst✝¹ : DecidableRel Dvd.dvd<VAR>inst✝ : DecidableEq R<VAR>p x : R<VAR>hp : Irreducible p<VAR>hnorm : normalize p = p<VAR>n : ℕ<VAR>hle : p ^ n ∣ x<VAR>hlt : ¬p ^ (n + 1) ∣ x<VAR>this : DecidableRel fun x x_1 => x ∣ x_1 := fun x x_1 => Classical.propDecidable ((fun x x_2 => x ∣ x_2) x x_1)<VAR>hx0 : ¬x = 0<GOAL>↑(count p (normalizedFactors x)) = ↑n
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : NormalizationMonoid R<VAR>inst✝¹ : DecidableRel Dvd.dvd<VAR>inst✝ : DecidableEq R<VAR>p x : R<VAR>hp : Irreducible p<VAR>hnorm : normalize p = p<VAR>n : ℕ<VAR>hle : p ^ n ∣ x<VAR>hlt : ¬p ^ (n + 1) ∣ x<VAR>this : DecidableRel fun x x_1 => x ∣ x_1 := fun x x_1 => Classical.propDecidable ((fun x x_2 => x ∣ x_2) x x_1)<VAR>hx0 : ¬x = 0<GOAL>p = normalize p
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : NormalizationMonoid R<VAR>inst✝¹ : DecidableRel Dvd.dvd<VAR>inst✝ : DecidableEq R<VAR>p x : R<VAR>hp : Irreducible p<VAR>hnorm : normalize p = p<VAR>n : ℕ<VAR>hle : p ^ n ∣ x<VAR>hlt : ¬p ^ (n + 1) ∣ x<VAR>this : DecidableRel fun x x_1 => x ∣ x_1 := fun x x_1 => Classical.propDecidable ((fun x x_2 => x ∣ x_2) x x_1)<VAR>hx0 : ¬x = 0<GOAL>↑n = multiplicity p x
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁸ : CommSemiring 𝕜<VAR>inst✝⁷ : TopologicalSpace 𝕜<VAR>inst✝⁶ : ContinuousAdd 𝕜<VAR>inst✝⁵ : ContinuousConstSMul 𝕜 𝕜<VAR>inst✝⁴ : NonUnitalNonAssocSemiring A<VAR>inst✝³ : TopologicalSpace A<VAR>inst✝² : Module 𝕜 A<VAR>inst✝¹ : T2Space 𝕜<VAR>inst✝ : ContinuousMul 𝕜<GOAL>IsClosed (characterSpace 𝕜 A ∪ {0})
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁸ : CommSemiring 𝕜<VAR>inst✝⁷ : TopologicalSpace 𝕜<VAR>inst✝⁶ : ContinuousAdd 𝕜<VAR>inst✝⁵ : ContinuousConstSMul 𝕜 𝕜<VAR>inst✝⁴ : NonUnitalNonAssocSemiring A<VAR>inst✝³ : TopologicalSpace A<VAR>inst✝² : Module 𝕜 A<VAR>inst✝¹ : T2Space 𝕜<VAR>inst✝ : ContinuousMul 𝕜<GOAL>IsClosed (⋂ i, ⋂ i_1, {x | x (i * i_1) = x i * x i_1})
<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>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α<VAR>h : i ∈ s<VAR>f : α → β<GOAL>∏ x ∈ s, f x = (∏ x ∈ s \ {i}, f x) * f i
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C<GOAL>tensor_μ C (X₁, X₂) (Y₁, Y₂) ▷ (Z₁ ⊗ Z₂) ≫ tensor_μ C (X₁ ⊗ Y₁, X₂ ⊗ Y₂) (Z₁, Z₂) ≫ ((α_ X₁ Y₁ Z₁).hom ⊗ (α_ X₂ Y₂ Z₂).hom) = (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫ (X₁ ⊗ X₂) ◁ tensor_μ C (Y₁, Y₂) (Z₁, Z₂) ≫ tensor_μ C (X₁, X₂) (Y₁ ⊗ Z₁, Y₂ ⊗ Z₂)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C<GOAL>((α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ≫ X₁ ◁ (α_ X₂ Y₁ Y₂).inv ≫ X₁ ◁ (β_ X₂ Y₁).hom ▷ Y₂ ≫ X₁ ◁ (α_ Y₁ X₂ Y₂).hom ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).inv) ▷ (Z₁ ⊗ Z₂) ≫ ((α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫ (X₁ ⊗ Y₁) ◁ (α_ (X₂ ⊗ Y₂) Z₁ Z₂).inv ≫ (X₁ ⊗ Y₁) ◁ (β_ (X₂ ⊗ Y₂) Z₁).hom ▷ Z₂ ≫ (X₁ ⊗ Y₁) ◁ (α_ Z₁ (X₂ ⊗ Y₂) Z₂).hom ≫ (α_ (X₁ ⊗ Y₁) Z₁ ((X₂ ⊗ Y₂) ⊗ Z₂)).inv) ≫ ((α_ X₁ Y₁ Z₁).hom ⊗ (α_ X₂ Y₂ Z₂).hom) = (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫ (X₁ ⊗ X₂) ◁ ((α_ Y₁ Y₂ (Z₁ ⊗ Z₂)).hom ≫ Y₁ ◁ (α_ Y₂ Z₁ Z₂).inv ≫ Y₁ ◁ (β_ Y₂ Z₁).hom ▷ Z₂ ≫ Y₁ ◁ (α_ Z₁ Y₂ Z₂).hom ≫ (α_ Y₁ Z₁ (Y₂ ⊗ Z₂)).inv) ≫ (α_ X₁ X₂ ((Y₁ ⊗ Z₁) ⊗ Y₂ ⊗ Z₂)).hom ≫ X₁ ◁ (α_ X₂ (Y₁ ⊗ Z₁) (Y₂ ⊗ Z₂)).inv ≫ X₁ ◁ (β_ X₂ (Y₁ ⊗ Z₁)).hom ▷ (Y₂ ⊗ Z₂) ≫ X₁ ◁ (α_ (Y₁ ⊗ Z₁) X₂ (Y₂ ⊗ Z₂)).hom ≫ (α_ X₁ (Y₁ ⊗ Z₁) (X₂ ⊗ Y₂ ⊗ Z₂)).inv
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C<GOAL>(α_ ((X₁ ⊗ X₂) ⊗ Y₁ ⊗ Y₂) Z₁ Z₂).inv ≫ (α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ▷ Z₁ ▷ Z₂ ≫ (α_ X₁ (X₂ ⊗ Y₁ ⊗ Y₂) Z₁).hom ▷ Z₂ ≫ (α_ X₁ ((X₂ ⊗ Y₁ ⊗ Y₂) ⊗ Z₁) Z₂).hom ≫ X₁ ◁ (α_ X₂ Y₁ Y₂).inv ▷ Z₁ ▷ Z₂ ≫ X₁ ◁ (β_ X₂ Y₁).hom ▷ Y₂ ▷ Z₁ ▷ Z₂ ≫ X₁ ◁ (α_ Y₁ X₂ Y₂).hom ▷ Z₁ ▷ Z₂ ≫ (α_ X₁ ((Y₁ ⊗ X₂ ⊗ Y₂) ⊗ Z₁) Z₂).inv ≫ (α_ X₁ (Y₁ ⊗ X₂ ⊗ Y₂) Z₁).inv ▷ Z₂ ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).inv ▷ Z₁ ▷ Z₂ ≫ (α_ ((X₁ ⊗ Y₁) ⊗ X₂ ⊗ Y₂) Z₁ Z₂).hom ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫ (α_ X₁ Y₁ ((X₂ ⊗ Y₂) ⊗ Z₁ ⊗ Z₂)).hom ≫ X₁ ◁ Y₁ ◁ (α_ (X₂ ⊗ Y₂) Z₁ Z₂).inv ≫ X₁ ◁ Y₁ ◁ (α_ X₂ Y₂ Z₁).hom ▷ Z₂ ≫ X₁ ◁ Y₁ ◁ (α_ X₂ (Y₂ ⊗ Z₁) Z₂).hom ≫ X₁ ◁ Y₁ ◁ X₂ ◁ (β_ Y₂ Z₁).hom ▷ Z₂ ≫ X₁ ◁ Y₁ ◁ (α_ X₂ (Z₁ ⊗ Y₂) Z₂).inv ≫ X₁ ◁ Y₁ ◁ (α_ X₂ Z₁ Y₂).inv ▷ Z₂ ≫ X₁ ◁ Y₁ ◁ (β_ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ≫ X₁ ◁ Y₁ ◁ (α_ Z₁ X₂ Y₂).hom ▷ Z₂ ≫ X₁ ◁ Y₁ ◁ (α_ Z₁ (X₂ ⊗ Y₂) Z₂).hom ≫ (α_ X₁ Y₁ (Z₁ ⊗ (X₂ ⊗ Y₂) ⊗ Z₂)).inv ≫ (α_ (X₁ ⊗ Y₁) Z₁ ((X₂ ⊗ Y₂) ⊗ Z₂)).inv ≫ ((α_ X₁ Y₁ Z₁).hom ⊗ (α_ X₂ Y₂ Z₂).hom) = (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫ (α_ X₁ X₂ ((Y₁ ⊗ Y₂) ⊗ Z₁ ⊗ Z₂)).hom ≫ X₁ ◁ X₂ ◁ (α_ Y₁ Y₂ (Z₁ ⊗ Z₂)).hom ≫ X₁ ◁ X₂ ◁ Y₁ ◁ (α_ Y₂ Z₁ Z₂).inv ≫ X₁ ◁ X₂ ◁ Y₁ ◁ (β_ Y₂ Z₁).hom ▷ Z₂ ≫ X₁ ◁ X₂ ◁ Y₁ ◁ (α_ Z₁ Y₂ Z₂).hom ≫ X₁ ◁ X₂ ◁ (α_ Y₁ Z₁ (Y₂ ⊗ Z₂)).inv ≫ X₁ ◁ (α_ X₂ (Y₁ ⊗ Z₁) (Y₂ ⊗ Z₂)).inv ≫ X₁ ◁ (α_ (X₂ ⊗ Y₁ ⊗ Z₁) Y₂ Z₂).inv ≫ X₁ ◁ (α_ X₂ Y₁ Z₁).inv ▷ Y₂ ▷ Z₂ ≫ X₁ ◁ (β_ X₂ Y₁).hom ▷ Z₁ ▷ Y₂ ▷ Z₂ ≫ X₁ ◁ (α_ Y₁ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ≫ X₁ ◁ (α_ Y₁ (X₂ ⊗ Z₁) Y₂).hom ▷ Z₂ ≫ X₁ ◁ (α_ Y₁ ((X₂ ⊗ Z₁) ⊗ Y₂) Z₂).hom ≫ X₁ ◁ Y₁ ◁ (β_ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ≫ X₁ ◁ (α_ Y₁ ((Z₁ ⊗ X₂) ⊗ Y₂) Z₂).inv ≫ X₁ ◁ (α_ Y₁ (Z₁ ⊗ X₂) Y₂).inv ▷ Z₂ ≫ X₁ ◁ (α_ Y₁ Z₁ X₂).inv ▷ Y₂ ▷ Z₂ ≫ X₁ ◁ (α_ ((Y₁ ⊗ Z₁) ⊗ X₂) Y₂ Z₂).hom ≫ X₁ ◁ (α_ (Y₁ ⊗ Z₁) X₂ (Y₂ ⊗ Z₂)).hom ≫ (α_ X₁ (Y₁ ⊗ Z₁) (X₂ ⊗ Y₂ ⊗ Z₂)).inv
<VAR>R : Type u<VAR>inst✝⁸ : Ring R<VAR>ι : Type v<VAR>inst✝⁷ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁶ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁵ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝⁴ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>x : G i<VAR>H : (of R ι G f i) x = 0<VAR>this : Nonempty ι<VAR>j : ι<VAR>hj : ∀ k ∈ DFinsupp.support ((DirectSum.lof R ι G i) x), k ≤ j<VAR>hxj : (DirectSum.toModule R ι (G j) fun i => totalize G f i j) ((DirectSum.lof R ι G i) x) = 0<VAR>hx0 : ¬x = 0<GOAL>i ∈ DFinsupp.support ((DirectSum.lof R ι G i) x)
<VAR>R : Type u<VAR>inst✝⁸ : Ring R<VAR>ι : Type v<VAR>inst✝⁷ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁶ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁵ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝⁴ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>x : G i<VAR>H : (of R ι G f i) x = 0<VAR>this : Nonempty ι<VAR>j : ι<VAR>hj : ∀ k ∈ DFinsupp.support ((DirectSum.lof R ι G i) x), k ≤ j<VAR>hxj : (DirectSum.toModule R ι (G j) fun i => totalize G f i j) ((DirectSum.lof R ι G i) x) = 0<VAR>hx0 : ¬x = 0<VAR>hij : i ≤ j<GOAL>(f i j hij) x = 0
<VAR>R : Type u<VAR>inst✝⁸ : Ring R<VAR>ι : Type v<VAR>inst✝⁷ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁶ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁵ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝⁴ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>x : G i<VAR>H : (of R ι G f i) x = 0<VAR>this : Nonempty ι<VAR>j : ι<VAR>hj : ∀ k ∈ DFinsupp.support ((DirectSum.lof R ι G i) x), k ≤ j<VAR>hx0 : ¬x = 0<VAR>hij : i ≤ j<VAR>hxj : (totalize G f i j) x = 0<GOAL>(f i j hij) x = 0
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>(smulAux' g z).im = (↑↑g).det * z.im / Complex.normSq (denom g z)
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>(num g z).im * (denom g z).re / Complex.normSq (denom g z) - (num g z).re * (denom g z).im / Complex.normSq (denom g z) = (↑↑g).det * z.im / Complex.normSq (denom g z)
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>↑↑g 0 0 * z.im * (↑↑g 1 0 * z.re + ↑↑g 1 1) / Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) - (↑↑g 0 0 * z.re + ↑↑g 0 1) * (↑↑g 1 0 * z.im) / Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) = (↑↑g).det * z.im / Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1))
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>↑↑g 0 0 * z.im * (↑↑g 1 0 * z.re + ↑↑g 1 1) / Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) - (↑↑g 0 0 * z.re + ↑↑g 0 1) * (↑↑g 1 0 * z.im) / Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) = (↑↑g 0 0 * ↑↑g 1 1 - ↑↑g 0 1 * ↑↑g 1 0) * z.im / Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1))
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>h : 0 < s.length<VAR>x : X<GOAL>x ∈ s ↔ x ∈ (eraseLast s).snoc (last s) ⋯
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>h : 0 < s.length<VAR>x : X<GOAL>x ∈ s ↔ ¬x = last s ∧ x ∈ s ∨ x = last s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>Y Y' : C<VAR>f : G.obj Y ⟶ X<VAR>f' : G.obj Y' ⟶ X<VAR>W : C<VAR>a : W ⟶ Y<VAR>b : W ⟶ Y'<VAR>w : G.map a ≫ f = G.map b ≫ f'<GOAL>liftAux hF α s f ≫ F.map a.op = liftAux hF α s f' ≫ F.map b.op
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>Y Y' : C<VAR>f : G.obj Y ⟶ X<VAR>f' : G.obj Y' ⟶ X<VAR>W : C<VAR>a : W ⟶ Y<VAR>b : W ⟶ Y'<VAR>w : G.map a ≫ f = G.map b ≫ f'<GOAL>∀ (I : GrothendieckTopology.Cover.Arrow ⟨Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) ↑S), ⋯⟩), (liftAux hF α s f ≫ F.map a.op) ≫ F.map I.f.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map I.f.op
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>Y Y' : C<VAR>f : G.obj Y ⟶ X<VAR>f' : G.obj Y' ⟶ X<VAR>W : C<VAR>a : W ⟶ Y<VAR>b : W ⟶ Y'<VAR>w : G.map a ≫ f = G.map b ≫ f'<VAR>T : C<VAR>g : T ⟶ W<VAR>hg : (GrothendieckTopology.Cover.sieve ⟨Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) ↑S), ⋯⟩).arrows g<GOAL>(liftAux hF α s f ≫ F.map a.op) ≫ F.map g.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map g.op
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>Y Y' : C<VAR>f : G.obj Y ⟶ X<VAR>f' : G.obj Y' ⟶ X<VAR>W : C<VAR>a : W ⟶ Y<VAR>b : W ⟶ Y'<VAR>w : G.map a ≫ f = G.map b ≫ f'<VAR>T : C<VAR>g : T ⟶ W<VAR>hg : (GrothendieckTopology.Cover.sieve ⟨Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) ↑S), ⋯⟩).arrows g<VAR>eq₁ : liftAux hF α s f ≫ F.map (g ≫ a).op = s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (𝟙 (G.obj T)).op ≫ α.app (op T)<GOAL>(liftAux hF α s f ≫ F.map a.op) ≫ F.map g.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map g.op
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>Y Y' : C<VAR>f : G.obj Y ⟶ X<VAR>f' : G.obj Y' ⟶ X<VAR>W : C<VAR>a : W ⟶ Y<VAR>b : W ⟶ Y'<VAR>w : G.map a ≫ f = G.map b ≫ f'<VAR>T : C<VAR>g : T ⟶ W<VAR>hg : (GrothendieckTopology.Cover.sieve ⟨Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) ↑S), ⋯⟩).arrows g<VAR>eq₁ : liftAux hF α s f ≫ F.map (g ≫ a).op = s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (𝟙 (G.obj T)).op ≫ α.app (op T)<VAR>eq₂ : liftAux hF α s f' ≫ F.map (g ≫ b).op = s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (𝟙 (G.obj T)).op ≫ α.app (op T)<GOAL>(liftAux hF α s f ≫ F.map a.op) ≫ F.map g.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map g.op
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>Y Y' : C<VAR>f : G.obj Y ⟶ X<VAR>f' : G.obj Y' ⟶ X<VAR>W : C<VAR>a : W ⟶ Y<VAR>b : W ⟶ Y'<VAR>w : G.map a ≫ f = G.map b ≫ f'<VAR>T : C<VAR>g : T ⟶ W<VAR>hg : (GrothendieckTopology.Cover.sieve ⟨Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) ↑S), ⋯⟩).arrows g<VAR>eq₁ : liftAux hF α s f ≫ F.map (a.op ≫ g.op) = s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (𝟙 (op (G.obj T))) ≫ α.app (op T)<VAR>eq₂ : liftAux hF α s f' ≫ F.map (b.op ≫ g.op) = s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ R.map (𝟙 (op (G.obj T))) ≫ α.app (op T)<GOAL>(liftAux hF α s f ≫ F.map a.op) ≫ F.map g.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map g.op
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>Y Y' : C<VAR>f : G.obj Y ⟶ X<VAR>f' : G.obj Y' ⟶ X<VAR>W : C<VAR>a : W ⟶ Y<VAR>b : W ⟶ Y'<VAR>w : G.map a ≫ f = G.map b ≫ f'<VAR>T : C<VAR>g : T ⟶ W<VAR>hg : (GrothendieckTopology.Cover.sieve ⟨Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) ↑S), ⋯⟩).arrows g<VAR>eq₁ : liftAux hF α s f ≫ F.map a.op ≫ F.map g.op = s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ α.app (op T)<VAR>eq₂ : liftAux hF α s f' ≫ F.map b.op ≫ F.map g.op = s.ι { Y := G.obj T, f := G.map g ≫ G.map a ≫ f, hf := hg } ≫ α.app (op T)<GOAL>(liftAux hF α s f ≫ F.map a.op) ≫ F.map g.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map g.op
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f f₁ f₂ : Filter α<VAR>h h₁ h₂ : Set α → Set β<VAR>hh : Monotone h<GOAL>⊥.lift' h = 𝓟 (h ∅)
<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>μ : Measure α<GOAL>∫⁻ (a : α), ↑f a ∂μ = f.lintegral μ
<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>μ : Measure α<GOAL>⨆ g, ⨆ (_ : ↑g ≤ fun a => ↑f a), g.lintegral μ = f.lintegral μ
<GOAL>∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], (algebraMap R T).FiniteType → Algebra.TensorProduct.includeLeftRingHom.FiniteType
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>X : J<VAR>tX : IsTerminal X<VAR>F : J ⥤ C<VAR>j j' : J<VAR>k : j ⟶ j'<GOAL>F.map k ≫ F.map (tX.from j') = F.map (tX.from j) ≫ 𝟙 (F.obj X)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s✝ s : Set G<GOAL>closure s⁻¹ = closure s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<GOAL>AntitoneOn (fun x => x⁻¹) (Set.Ioi 0)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>x✝ : α<GOAL>x✝ = x✝ - 0
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq R<VAR>a : R<GOAL>(C a).degree = if a = 0 then ⊥ else 0
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>h : 0 < x<GOAL>logb b x < 0 ↔ x < 1
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>h : 0 < x<GOAL>logb b x < logb ?m.18267 1 ↔ x < 1
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>h : 0 < x<GOAL>ℝ
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x✝¹ x✝ : MaximalSpectrum R<VAR>asIdeal✝¹ : Ideal R<VAR>IsMaximal✝¹ : asIdeal✝¹.IsMaximal<VAR>asIdeal✝ : Ideal R<VAR>IsMaximal✝ : asIdeal✝.IsMaximal<VAR>h : { asIdeal := asIdeal✝¹, IsMaximal := IsMaximal✝¹ }.toPrimeSpectrum = { asIdeal := asIdeal✝, IsMaximal := IsMaximal✝ }.toPrimeSpectrum<GOAL>{ asIdeal := asIdeal✝¹, IsMaximal := IsMaximal✝¹ } = { asIdeal := asIdeal✝, IsMaximal := IsMaximal✝ }
<VAR>f : ℂ → ℂ := fun s => 2 * (2 * ↑π) ^ (-s)<GOAL>HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1
<VAR>f : ℂ → ℂ := fun s => 2 * (2 * ↑π) ^ (-s)<VAR>this : HasDerivAt (fun s => 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1<GOAL>HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1
<VAR>f : ℂ → ℂ := fun s => 2 * (2 * ↑π) ^ (-s)<VAR>this✝ : HasDerivAt (fun s => 2 * (2 * ↑π) ^ (-s)) (-log (2 * ↑π) / ↑π) 1<VAR>this : HasDerivAt (fun y => 2 * (2 * ↑π) ^ (-y) * Gamma y) (-log (2 * ↑π) / ↑π * Gamma 1 + 2 * (2 * ↑π) ^ (-1) * -↑γ) 1<GOAL>HasDerivAt Gammaℂ (-(↑γ + log (2 * ↑π)) / ↑π) 1
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>N : Type u_4<VAR>inst✝ : CommMonoid N<VAR>s t : Submonoid N<GOAL>s ⊔ t = mrange (s.subtype.coprod t.subtype)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>x₁ x₂ : X<VAR>y₁ y₂ : Y<GOAL>((x₁, y₁) ~ᵢ (x₂, y₂)) ↔ (x₁ ~ᵢ x₂) ∧ (y₁ ~ᵢ y₂)
<VAR>n m : ℕ<VAR>i : Fin (m * n)<GOAL>↑i.rev.modNat = ↑i.modNat.rev
<VAR>n m : ℕ<VAR>i : Fin (m * n)<VAR>H₁ : ↑i % n + 1 ≤ n<GOAL>↑i.rev.modNat = ↑i.modNat.rev
<VAR>n m : ℕ<VAR>i : Fin (m * n)<VAR>H₁ : ↑i % n + 1 ≤ n<VAR>H₂ : ↑i / n < m<GOAL>↑i.rev.modNat = ↑i.modNat.rev
<VAR>n m : ℕ<VAR>i : Fin (m * n)<VAR>H₁ : ↑i % n + 1 ≤ n<VAR>H₂ : ↑i / n < m<GOAL>(m * n - (↑i + 1)) % n = n - (↑i % n + 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>halg : ¬Algebra.IsAlgebraic F E<GOAL>finSepDegree F E * finInsepDegree F E = finrank F E
<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>x y : G<GOAL>map (fun x_1 => x * x_1) (map (fun x => x * y) (𝓝 1 * 𝓝 1)) = map₂ (fun a b => x * (a * b * y)) (𝓝 1) (𝓝 1)
<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>x y : G<GOAL>map₂ (fun a b => x * (a * b * y)) (𝓝 1) (𝓝 1) = map₂ (fun a b => x * a * (b * y)) (𝓝 1) (𝓝 1)
<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>x y : G<GOAL>map₂ (fun a b => x * a * (b * y)) (𝓝 1) (𝓝 1) = 𝓝 x * 𝓝 y