ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>R X✝ Y✝ Z✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>a b : R ⟶ X✝<VAR>X Y Z A : C<VAR>g : Y ⟶ Z<VAR>a₁ a₂ : A ⟶ Y<VAR>h : IsKernelPair g a₁ a₂<VAR>f : X ⟶ Z<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPullback f (a₁ ≫ g)<VAR>s : PullbackCone (pullback.fst f g) (pullback.fst f g)<GOAL>(fun s => pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯) s ≫ (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).snd = s.snd
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>R X✝ Y✝ Z✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>a b : R ⟶ X✝<VAR>X Y Z A : C<VAR>g : Y ⟶ Z<VAR>a₁ a₂ : A ⟶ Y<VAR>h : IsKernelPair g a₁ a₂<VAR>f : X ⟶ Z<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPullback f (a₁ ≫ g)<VAR>s : PullbackCone (pullback.fst f g) (pullback.fst f g)<VAR>m : s.pt ⟶ (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).pt<VAR>hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).π.app j = s.π.app j<GOAL>m = (fun s => pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯) s
<VAR>x✝ y✝ z✝ : PGame<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>zl zr : Type u_1<VAR>zL : zl → PGame<VAR>zR : zr → PGame<VAR>x : PGame := mk xl xr xL xR<VAR>y : PGame := mk yl yr yL yR<VAR>z : PGame := mk zl zr zL zR<GOAL>⟦mk xl xr xL xR * (mk yl yr yL yR + mk zl zr zL zR)⟧ = ⟦mk xl xr xL xR * mk yl yr yL yR⟧ + ⟦mk xl xr xL xR * mk zl zr zL zR⟧
<VAR>x✝ y✝ z✝ : PGame<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>zl zr : Type u_1<VAR>zL : zl → PGame<VAR>zR : zr → PGame<VAR>x : PGame := mk xl xr xL xR<VAR>y : PGame := mk yl yr yL yR<VAR>z : PGame := mk zl zr zL zR<GOAL>(mk xl xr xL xR * (mk yl yr yL yR + mk zl zr zL zR)).LeftMoves ≃ (mk xl xr xL xR * mk yl yr yL yR + mk xl xr xL xR * mk zl zr zL zR).LeftMoves
<VAR>x✝ y✝ z✝ : PGame<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>zl zr : Type u_1<VAR>zL : zl → PGame<VAR>zR : zr → PGame<VAR>x : PGame := mk xl xr xL xR<VAR>y : PGame := mk yl yr yL yR<VAR>z : PGame := mk zl zr zL zR<GOAL>(mk xl xr xL xR * (mk yl yr yL yR + mk zl zr zL zR)).RightMoves ≃ (mk xl xr xL xR * mk yl yr yL yR + mk xl xr xL xR * mk zl zr zL zR).RightMoves
<VAR>x✝ y✝ z✝ : PGame<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>zl zr : Type u_1<VAR>zL : zl → PGame<VAR>zR : zr → PGame<VAR>x : PGame := mk xl xr xL xR<VAR>y : PGame := mk yl yr yL yR<VAR>z : PGame := mk zl zr zL zR<GOAL>∀ (i : (mk xl xr xL xR * (mk yl yr yL yR + mk zl zr zL zR)).LeftMoves), ⟦(mk xl xr xL xR * (mk yl yr yL yR + mk zl zr zL zR)).moveLeft i⟧ = ⟦(mk xl xr xL xR * mk yl yr yL yR + mk xl xr xL xR * mk zl zr zL zR).moveLeft (?refine_1 i)⟧
<VAR>x✝ y✝ z✝ : PGame<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>zl zr : Type u_1<VAR>zL : zl → PGame<VAR>zR : zr → PGame<VAR>x : PGame := mk xl xr xL xR<VAR>y : PGame := mk yl yr yL yR<VAR>z : PGame := mk zl zr zL zR<GOAL>∀ (j : (mk xl xr xL xR * (mk yl yr yL yR + mk zl zr zL zR)).RightMoves), ⟦(mk xl xr xL xR * (mk yl yr yL yR + mk zl zr zL zR)).moveRight j⟧ = ⟦(mk xl xr xL xR * mk yl yr yL yR + mk xl xr xL xR * mk zl zr zL zR).moveRight (?refine_2 j)⟧
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>hp : AffineIndependent k p<VAR>j : ι<VAR>w : ι → kˣ<GOAL>AffineIndependent k fun i => (AffineMap.lineMap (p j) (p i)) ↑(w i)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>j : ι<VAR>hp : LinearIndependent k fun i => p ↑i -ᵥ p j<VAR>w : ι → kˣ<GOAL>LinearIndependent k fun i => (AffineMap.lineMap (p j) (p ↑i)) ↑(w ↑i) -ᵥ (AffineMap.lineMap (p j) (p j)) ↑(w j)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>j : ι<VAR>hp : LinearIndependent k fun i => p ↑i -ᵥ p j<VAR>w : ι → kˣ<GOAL>LinearIndependent k fun i => ↑(w ↑i) • (p ↑i -ᵥ p j)
<VAR>n : ℕ<VAR>c : Composition n<VAR>d : CompositionAsSet n := c.toCompositionAsSet<GOAL>d.blocks = c.blocks
<VAR>n : ℕ<VAR>c : Composition n<VAR>d : CompositionAsSet n := c.toCompositionAsSet<VAR>length_eq : d.blocks.length = c.blocks.length<GOAL>d.blocks = c.blocks
<VAR>n : ℕ<VAR>c : Composition n<VAR>d : CompositionAsSet n := c.toCompositionAsSet<VAR>length_eq : d.blocks.length = c.blocks.length<GOAL>∀ i ≤ d.blocks.length, (take i d.blocks).sum = (take i c.blocks).sum
<VAR>n : ℕ<VAR>c : Composition n<VAR>d : CompositionAsSet n := c.toCompositionAsSet<VAR>length_eq : d.blocks.length = c.blocks.length<VAR>i : ℕ<VAR>hi : i ≤ d.blocks.length<GOAL>(take i d.blocks).sum = (take i c.blocks).sum
<VAR>n : ℕ<VAR>c : Composition n<VAR>d : CompositionAsSet n := c.toCompositionAsSet<VAR>length_eq : d.blocks.length = c.blocks.length<VAR>i : ℕ<VAR>hi : i ≤ d.blocks.length<VAR>i_lt : i < d.boundaries.card<GOAL>(take i d.blocks).sum = (take i c.blocks).sum
<VAR>n : ℕ<VAR>c : Composition n<VAR>d : CompositionAsSet n := c.toCompositionAsSet<VAR>length_eq : d.blocks.length = c.blocks.length<VAR>i : ℕ<VAR>hi : i ≤ d.blocks.length<VAR>i_lt : i < d.boundaries.card<VAR>i_lt' : i < c.boundaries.card<GOAL>(take i d.blocks).sum = (take i c.blocks).sum
<VAR>n : ℕ<VAR>c : Composition n<VAR>d : CompositionAsSet n := c.toCompositionAsSet<VAR>length_eq : d.blocks.length = c.blocks.length<VAR>i : ℕ<VAR>hi : i ≤ d.blocks.length<VAR>i_lt : i < d.boundaries.card<VAR>i_lt' : i < c.boundaries.card<VAR>i_lt'' : i < c.length + 1<GOAL>(take i d.blocks).sum = (take i c.blocks).sum
<VAR>n : ℕ<VAR>c : Composition n<VAR>d : CompositionAsSet n := c.toCompositionAsSet<VAR>length_eq : d.blocks.length = c.blocks.length<VAR>i : ℕ<VAR>hi : i ≤ d.blocks.length<VAR>i_lt : i < d.boundaries.card<VAR>i_lt' : i < c.boundaries.card<VAR>i_lt'' : i < c.length + 1<VAR>A : (d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩ = (c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩<GOAL>(take i d.blocks).sum = (take i c.blocks).sum
<VAR>n : ℕ<VAR>c : Composition n<VAR>d : CompositionAsSet n := c.toCompositionAsSet<VAR>length_eq : d.blocks.length = c.blocks.length<VAR>i : ℕ<VAR>hi : i ≤ d.blocks.length<VAR>i_lt : i < d.boundaries.card<VAR>i_lt' : i < c.boundaries.card<VAR>i_lt'' : i < c.length + 1<VAR>A : (d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩ = (c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩<VAR>B : c.sizeUpTo i = ↑(c.boundary ⟨i, i_lt''⟩)<GOAL>(take i d.blocks).sum = (take i c.blocks).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a \ b ≤ c ↔ a ≤ c ⊔ b
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s✝ : α → α → Prop<VAR>inst✝² : Preorder α<VAR>a✝ : α<VAR>inst✝¹ : PartialOrder β<VAR>f : α → β<VAR>s : Set α<VAR>inst✝ : IsDirected α fun x x_1 => x ≤ x_1<VAR>hf : Monotone f<VAR>hf' : Antitone f<VAR>a b : α<GOAL>f a = f b
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>r r' s✝ : α → α → Prop<VAR>inst✝² : Preorder α<VAR>a✝ : α<VAR>inst✝¹ : PartialOrder β<VAR>f : α → β<VAR>s : Set α<VAR>inst✝ : IsDirected α fun x x_1 => x ≤ x_1<VAR>hf : Monotone f<VAR>hf' : Antitone f<VAR>a b c : α<VAR>hac : a ≤ c<VAR>hbc : b ≤ c<GOAL>f a = f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>p : β → Type u_9<VAR>f : Sigma p → α<VAR>c : α<GOAL>⨆ x, f x ≤ c ↔ ⨆ i, ⨆ j, f ⟨i, j⟩ ≤ c
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a b : ZMod n<VAR>h : n ≤ a.val + b.val<GOAL>a.val + b.val = (a + b).val + n
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>a b : ZMod n<VAR>h : n ≤ a.val + b.val<GOAL>n ≤ a.val % n + b.val % n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<GOAL>Measurable fun a => (condCDF ρ a).measure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<GOAL>∀ (s : Set ℝ), MeasurableSet s → Measurable fun b => (condCDF ρ b).measure s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<GOAL>Measurable fun b => (condCDF ρ b).measure s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<GOAL>(fun s => Measurable fun b => (condCDF ρ b).measure s) ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<GOAL>∀ t ∈ range Iic, (fun s => Measurable fun b => (condCDF ρ b).measure s) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<GOAL>∀ (t : Set ℝ), MeasurableSet t → (fun s => Measurable fun b => (condCDF ρ b).measure s) t → (fun s => Measurable fun b => (condCDF ρ b).measure s) tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<GOAL>∀ (f : ℕ → Set ℝ), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), (fun s => Measurable fun b => (condCDF ρ b).measure s) (f i)) → (fun s => Measurable fun b => (condCDF ρ b).measure s) (⋃ i, f i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<GOAL>(s₁ ∪ s₂).pi t = s₁.pi t ∩ s₂.pi t
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : StrongRankCondition R<VAR>s : Set M<VAR>inst✝ : Fintype ↑s<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<GOAL>Module.rank R ↥(span R s) = ↑s.toFinset.card
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : StrongRankCondition R<VAR>s : Set M<VAR>inst✝ : Fintype ↑s<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>this : Module.rank R ↥(span R s) = #↑s<GOAL>Module.rank R ↥(span R s) = ↑s.toFinset.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : Filter α<VAR>m : α → ℝ≥0∞<VAR>a b : ℝ≥0∞<VAR>hm : Tendsto m f (𝓝 b)<VAR>hb : b ≠ 0 ∨ a ≠ ⊤<VAR>this : a = 0<GOAL>Tendsto (fun b => a * m b) f (𝓝 (a * b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq β<VAR>e : Perm α<VAR>f : α ↪ β<VAR>b : β<VAR>h : b ∉ Set.range ⇑f<GOAL>(e.viaFintypeEmbedding f) b = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>g : α → ℝ≥0∞<VAR>hs : MeasurableSet s<GOAL>essSup (s.piecewise f g) μ = max (essSup f (μ.restrict s)) (essSup g (μ.restrict sᶜ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>g : α → ℝ≥0∞<VAR>hs : MeasurableSet s<GOAL>limsup f (ae μ ⊓ 𝓟 {x | x ∈ s}) ⊔ limsup g (ae μ ⊓ 𝓟 {x | x ∉ s}) = max (limsup f (ae μ ⊓ 𝓟 s)) (limsup g (ae μ ⊓ 𝓟 sᶜ))
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : Disjoint M.E N.E<VAR>I : Set α<VAR>hI : (M.disjointSum N h).Indep I<GOAL>∃ IM IN, M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : Disjoint M.E N.E<VAR>I : Set α<VAR>hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E<GOAL>∃ IM IN, M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : Disjoint M.E N.E<VAR>I : Set α<VAR>hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E<GOAL>I = I ∩ M.E ∪ I ∩ N.E
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>inst✝ : MulOneClass M<VAR>s : Set M<GOAL>(closure s).op = closure (MulOpposite.unop ⁻¹' s)
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>inst✝ : MulOneClass M<VAR>s : Set M<GOAL>sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>inst✝ : MulOneClass M<VAR>s : Set M<VAR>a : Submonoid Mᵐᵒᵖ<GOAL>a ∈ {a | s ⊆ MulOpposite.op ⁻¹' ↑a} ↔ a ∈ {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>μ : Measure E<VAR>s : Set ↑(sphere 0 1)<VAR>r : ↑(Ioi 0)<GOAL>μ (Subtype.val '' (⇑(homeomorphUnitSphereProd E) ⁻¹' s ×ˢ Iio r)) = μ (Ioo 0 ↑r • Subtype.val '' s)
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>μ : Measure E<VAR>s : Set ↑(sphere 0 1)<VAR>r : ↑(Ioi 0)<GOAL>μ ((fun x => ↑((homeomorphUnitSphereProd E).symm x)) '' s ×ˢ Iio r) = μ ((fun x => SMul.smul ↑x.2 ↑x.1) '' s ×ˢ Iio r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ioc a b ∪ Ioc a c = Ioc a (max b c)
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>γ : α → Type u_2<VAR>δ : α → Type u_3<VAR>s : (a : α) → Finset (γ a)<VAR>β : Type u_4<VAR>inst✝ : DecidableEq β<VAR>t : Finset β<VAR>a : α<GOAL>image (fun f => f a) (piFinset fun _i => t) = t
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>γ : α → Type u_2<VAR>δ : α → Type u_3<VAR>s : (a : α) → Finset (γ a)<VAR>β : Type u_4<VAR>inst✝ : DecidableEq β<VAR>a : α<GOAL>image (fun f => f a) (piFinset fun _i => ∅) = ∅
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>γ : α → Type u_2<VAR>δ : α → Type u_3<VAR>s : (a : α) → Finset (γ a)<VAR>β : Type u_4<VAR>inst✝ : DecidableEq β<VAR>t : Finset β<VAR>a : α<VAR>ht : t.Nonempty<GOAL>image (fun f => f a) (piFinset fun _i => t) = t
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : OrderedRing α<VAR>l : Filter β<VAR>f g : β → α<VAR>hf : Tendsto f l atTop<VAR>hg : Tendsto g l atBot<GOAL>Tendsto (fun x => f x * g x) l atBot
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : OrderedRing α<VAR>l : Filter β<VAR>f g : β → α<VAR>hf : Tendsto f l atTop<VAR>hg : Tendsto g l atBot<VAR>this : Tendsto (fun x => f x * (Neg.neg ∘ g) x) l atTop<GOAL>Tendsto (fun x => f x * g x) l atBot
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasPullbacks C<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>g₁ : Y ⟶ W<VAR>inst✝¹ : Epi g₁<VAR>g₂ : W ⟶ Z<VAR>inst✝ : Mono g₂<VAR>hg : g₁ ≫ g₂ = g<VAR>f' : X ⟶ W<VAR>hf : f' ≫ g₂ = f<VAR>t : PullbackCone f g<VAR>ht : IsLimit t<GOAL>Epi t.fst
<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}<GOAL>lift.{u, v} o = 0 ↔ o = 0
<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>H : ∀ a < lift.{u, v} o, succ a < lift.{u, v} o<VAR>a : Ordinal.{v}<VAR>h : a < o<GOAL>lift.{u, v} (succ a) < lift.{u, v} o
<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>H : ∀ a < o, succ a < o<VAR>a : Ordinal.{max u v}<VAR>h : a < lift.{u, v} o<GOAL>succ a < lift.{u, v} o
<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>H : ∀ a < o, succ a < o<VAR>a' : Ordinal.{v}<VAR>h : lift.{u, v} a' < lift.{u, v} o<GOAL>succ (lift.{u, v} a') < lift.{u, v} o
<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>H : ∀ a < o, succ a < o<VAR>a' : Ordinal.{v}<VAR>h : lift.{u, v} a' < lift.{u, v} o<GOAL>succ a' < o
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>i i' j : ι<VAR>rij : c.Rel i j<VAR>rij' : c.Rel i' j<GOAL>eqToHom ⋯ ≫ C.d i' j = C.d i j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>i j : ι<VAR>rij rij' : c.Rel i j<GOAL>eqToHom ⋯ ≫ C.d i j = C.d i j
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (cosZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedCosZeta (↑a) s / s.Gammaℝ)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℤ<GOAL>cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 = s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 / s.Gammaℝ
<VAR>q : ℚ<VAR>x y : ℝ<VAR>m : ℤ<VAR>h : Irrational (x - ↑m)<GOAL>Irrational (x - ↑↑m)
<VAR>R✝ : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M✝ : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁷ : Semiring R✝<VAR>inst✝⁶ : AddCommMonoid M✝<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R✝ M✝<VAR>inst✝³ : Module R✝ M₂<VAR>R : Type u_17<VAR>M : Type u_18<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>c : R<GOAL>IsLinearMap R fun z => c • z
<VAR>R✝ : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M✝ : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁷ : Semiring R✝<VAR>inst✝⁶ : AddCommMonoid M✝<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R✝ M✝<VAR>inst✝³ : Module R✝ M₂<VAR>R : Type u_17<VAR>M : Type u_18<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>c : R<GOAL>∀ (c_1 : R) (x : M), c • c_1 • x = c_1 • c • x
<VAR>R✝ : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M✝ : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁷ : Semiring R✝<VAR>inst✝⁶ : AddCommMonoid M✝<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R✝ M✝<VAR>inst✝³ : Module R✝ M₂<VAR>R : Type u_17<VAR>M : Type u_18<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>c c✝ : R<VAR>x✝ : M<GOAL>c • c✝ • x✝ = c✝ • c • x✝
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>b✝ : Basis ι ℝ E<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι ℝ (ι → ℝ)<GOAL>volume (fundamentalDomain b) = ENNReal.ofReal |(Matrix.of ⇑b).det|
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>b✝ : Basis ι ℝ E<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι ℝ (ι → ℝ)<GOAL>ENNReal.ofReal |(Pi.basisFun ℝ ι).det ⇑b| = ENNReal.ofReal |(Matrix.of ⇑b).transpose.det|
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>α : E<VAR>S : Set E<VAR>K L : IntermediateField F E<VAR>inst✝ : FiniteDimensional F E<VAR>h : ∀ (x : E), finrank F ↥F⟮x⟯ ≤ 1<GOAL>⊥ = ⊤
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>α : E<VAR>S : Set E<VAR>K L : IntermediateField F E<VAR>inst✝ : FiniteDimensional F E<VAR>h : ∀ (x : E), finrank F ↥F⟮x⟯ ≤ 1<GOAL>∀ (x : E), finrank F ↥F⟮x⟯ = 1
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>x y z : L<GOAL>((traceForm R L M) ⁅x, y⁆) z = ((traceForm R L M) x) ⁅y, z⁆
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>x y z : L<GOAL>(trace R M) (φ ⁅x, y⁆ ∘ₗ φ z) = (trace R M) ((φ x * φ y - φ y * φ x) * φ z)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>x y z : L<GOAL>(trace R M) ((φ x * φ y - φ y * φ x) * φ z) = (trace R M) (φ x * (φ y * φ z)) - (trace R M) (φ y * (φ x * φ z))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>x y z : L<GOAL>(trace R M) (φ x * (φ y * φ z)) - (trace R M) (φ y * (φ x * φ z)) = (trace R M) (φ x * (φ y * φ z)) - (trace R M) (φ x * (φ z * φ y))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>x y z : L<GOAL>(trace R M) (φ x * (φ y * φ z)) - (trace R M) (φ x * (φ z * φ y)) = ((traceForm R L M) x) ⁅y, z⁆
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>X : Type u_2<VAR>S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))<GOAL>S = ⊤
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>X : Type u_2<VAR>S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))<VAR>x : FreeAlgebra R X<VAR>hx : x ∈ ⊤<GOAL>x ∈ S
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>X : Type u_2<VAR>S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))<VAR>x : FreeAlgebra R X<GOAL>x ∈ S
<VAR>a b k m n p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>Disjoint a.primeFactors b.primeFactors ↔ a.Coprime b
<VAR>x y : ℂ<GOAL>cos (x * I) = cosh x
<VAR>x y : ℂ<GOAL>cosh (x * I * I) = cosh x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s : Set α<GOAL>insert a s ∈ 𝓝 a ↔ s ∈ 𝓝[≠] a