ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>x y : α<VAR>h : Inseparable x y<GOAL>𝓝 (x, y) ≤ 𝓤 α
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>x y : α<VAR>h : Inseparable x y<GOAL>𝓝 (y, y) ≤ 𝓤 α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List (Option α)<VAR>x : α<GOAL>x ∈ l.reduceOption ↔ some x ∈ l
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : IsSemisimple R L<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>J : LieIdeal R ↥↑I<VAR>J' : LieIdeal R L := let __spread.0 := Submodule.map ↑I.incl ↑J; { toSubmodule := __spread.0, lie_mem := ⋯ }<GOAL>J = ⊥ ∨ J = ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : IsSemisimple R L<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>J : LieIdeal R ↥↑I<VAR>J' : LieIdeal R L := let __spread.0 := Submodule.map ↑I.incl ↑J; { toSubmodule := __spread.0, lie_mem := ⋯ }<GOAL>¬J = ⊤ → J = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : IsSemisimple R L<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>J : LieIdeal R ↥↑I<VAR>J' : LieIdeal R L := let __spread.0 := Submodule.map ↑I.incl ↑J; { toSubmodule := __spread.0, lie_mem := ⋯ }<VAR>hJ : ¬J = ⊤<GOAL>J = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : IsSemisimple R L<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>J : LieIdeal R ↥↑I<VAR>J' : LieIdeal R L := let __spread.0 := Submodule.map ↑I.incl ↑J; { toSubmodule := __spread.0, lie_mem := ⋯ }<VAR>hJ : ¬J = ⊤<GOAL>J' = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : IsSemisimple R L<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>J : LieIdeal R ↥↑I<VAR>J' : LieIdeal R L := let __spread.0 := Submodule.map ↑I.incl ↑J; { toSubmodule := __spread.0, lie_mem := ⋯ }<VAR>hJ : ¬J = ⊤<GOAL>J' < I
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : IsSemisimple R L<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>J : LieIdeal R ↥↑I<VAR>J' : LieIdeal R L := let __spread.0 := Submodule.map ↑I.incl ↑J; { toSubmodule := __spread.0, lie_mem := ⋯ }<VAR>hJ : ¬J = ⊤<GOAL>J' ≤ I ∧ J' ≠ I
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : IsSemisimple R L<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>J : LieIdeal R ↥↑I<VAR>J' : LieIdeal R L := let __spread.0 := Submodule.map ↑I.incl ↑J; { toSubmodule := __spread.0, lie_mem := ⋯ }<VAR>hJ : ¬J = ⊤<GOAL>J' ≠ I
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : IsSemisimple R L<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>J : LieIdeal R ↥↑I<VAR>J' : LieIdeal R L := let __spread.0 := Submodule.map ↑I.incl ↑J; { toSubmodule := __spread.0, lie_mem := ⋯ }<VAR>hJ : J' = I<GOAL>J = ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : IsSemisimple R L<VAR>I : LieIdeal R L<VAR>hI : IsAtom I<VAR>J : LieIdeal R ↥↑I<VAR>J' : LieIdeal R L := let __spread.0 := Submodule.map ↑I.incl ↑J; { toSubmodule := __spread.0, lie_mem := ⋯ }<VAR>hJ : J' = I<GOAL>⊤ ≤ J
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>h : n < m<VAR>f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<GOAL>∑ i ∈ range (n + 1), ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i)) = 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>h : n < m<VAR>f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<GOAL>∀ i ∈ range (n + 1), f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>h : n < m<VAR>f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>i : ℕ<VAR>h₁ : i ∈ range (n + 1)<GOAL>f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>h : n < m<VAR>f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>i : ℕ<VAR>h₁ : i < n + 1<GOAL>f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>h : n < m<VAR>f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>i : ℕ<VAR>h₁✝ : i < n + 1<VAR>h₁ : i ≤ n<GOAL>f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>h : n < m<VAR>f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>i : ℕ<VAR>h₁✝ : i < n + 1<VAR>h₁ : i ≤ n<VAR>h₂ : i < m<VAR>h₃ : i ≤ m<GOAL>f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>h : n < m<VAR>f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>i : ℕ<VAR>h₁✝ : i < n + 1<VAR>h₁ : i ≤ n<VAR>h₂ : i < m<VAR>h₃ : i ≤ m<VAR>hi₄ : ↑i + 1 ≠ 0<GOAL>f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>h : n < m<VAR>f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>i : ℕ<VAR>h₁✝ : i < n + 1<VAR>h₁ : i ≤ n<VAR>h₂ : i < m<VAR>h₃ : i ≤ m<VAR>hi₄ : ↑i + 1 ≠ 0<VAR>this : ↑(m.choose (i + 1) * (i + 1)) = ↑(m.choose i * (m - i))<GOAL>f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>h : n < m<VAR>f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>i : ℕ<VAR>h₁✝ : i < n + 1<VAR>h₁ : i ≤ n<VAR>h₂ : i < m<VAR>h₃ : i ≤ m<VAR>hi₄ : ↑i + 1 ≠ 0<VAR>this : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)<GOAL>↑(n.choose i) * (↑(m.choose i))⁻¹ - ↑(n.choose (i + 1)) * (↑(m.choose (i + 1)))⁻¹ = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>h : n < m<VAR>f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>i : ℕ<VAR>h₁✝ : i < n + 1<VAR>h₁ : i ≤ n<VAR>h₂ : i < m<VAR>h₃ : i ≤ m<VAR>hi₄ : ↑i + 1 ≠ 0<VAR>this : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)<GOAL>↑(n.choose i) * (↑(m.choose i))⁻¹ - ↑(n.choose (i + 1)) * (↑(m.choose i) * ↑(m - i) * (↑i + 1)⁻¹)⁻¹ = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>h : n < m<VAR>f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>i : ℕ<VAR>h₁✝ : i < n + 1<VAR>h₁ : i ≤ n<VAR>h₂ : i < m<VAR>h₃ : i ≤ m<VAR>hi₄ : ↑i + 1 ≠ 0<VAR>this✝ : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)<VAR>this : ↑(n.choose (i + 1) * (i + 1)) = ↑(n.choose i * (n - i))<GOAL>↑(n.choose i) * (↑(m.choose i))⁻¹ - ↑(n.choose (i + 1)) * (↑(m.choose i) * ↑(m - i) * (↑i + 1)⁻¹)⁻¹ = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>h : n < m<VAR>f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>i : ℕ<VAR>h₁✝ : i < n + 1<VAR>h₁ : i ≤ n<VAR>h₂ : i < m<VAR>h₃ : i ≤ m<VAR>hi₄ : ↑i + 1 ≠ 0<VAR>this✝ : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)<VAR>this : ↑(n.choose (i + 1)) * (↑i + 1) = ↑(n.choose i) * ↑(n - i)<GOAL>↑(n.choose i) * (↑(m.choose i))⁻¹ - ↑(n.choose (i + 1)) * (↑(m.choose i) * ↑(m - i) * (↑i + 1)⁻¹)⁻¹ = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>h : n < m<VAR>f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>i : ℕ<VAR>h₁✝ : i < n + 1<VAR>h₁ : i ≤ n<VAR>h₂ : i < m<VAR>h₃ : i ≤ m<VAR>hi₄ : ↑i + 1 ≠ 0<VAR>this✝ : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)<VAR>this : ↑(n.choose (i + 1)) * (↑i + 1) = ↑(n.choose i) * ↑(n - i)<GOAL>↑(n.choose i) * (↑(m.choose i))⁻¹ - ↑(n.choose i) * ↑(n - i) * (↑i + 1)⁻¹ * (↑(m.choose i) * ↑(m - i) * (↑i + 1)⁻¹)⁻¹ = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>h : n < m<VAR>f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>i : ℕ<VAR>h₁✝ : i < n + 1<VAR>h₁ : i ≤ n<VAR>h₂ : i < m<VAR>h₃ : i ≤ m<VAR>hi₄ : ↑i + 1 ≠ 0<VAR>this✝¹ : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)<VAR>this✝ : ↑(n.choose (i + 1)) * (↑i + 1) = ↑(n.choose i) * ↑(n - i)<VAR>this : ↑m - ↑i ≠ 0<GOAL>↑(n.choose i) * (↑(m.choose i))⁻¹ - ↑(n.choose i) * ↑(n - i) * (↑i + 1)⁻¹ * (↑(m.choose i) * ↑(m - i) * (↑i + 1)⁻¹)⁻¹ = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>m n : ℕ<VAR>h : n < m<VAR>f : ℕ → ℚ := fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>hf : f = fun i => ↑(n.choose i) * (↑(m.choose i))⁻¹<VAR>i : ℕ<VAR>h₁✝ : i < n + 1<VAR>h₁ : i ≤ n<VAR>h₂ : i < m<VAR>h₃ : i ≤ m<VAR>hi₄ : ↑i + 1 ≠ 0<VAR>this✝² : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)<VAR>this✝¹ : ↑(n.choose (i + 1)) * (↑i + 1) = ↑(n.choose i) * ↑(n - i)<VAR>this✝ : ↑m - ↑i ≠ 0<VAR>this : ↑(m.choose i) ≠ 0<GOAL>↑(n.choose i) * (↑(m.choose i))⁻¹ - ↑(n.choose i) * ↑(n - i) * (↑i + 1)⁻¹ * (↑(m.choose i) * ↑(m - i) * (↑i + 1)⁻¹)⁻¹ = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝ : Category.{v₁, u₂} ℰ<VAR>A : C ⥤ ℰ<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x₁ x₂ : P.Elementsᵒᵖ<VAR>f : x₁ ⟶ x₂<GOAL>yoneda.map (↑f.unop).unop ≫ yonedaEquiv.symm (Opposite.unop x₂).snd = yonedaEquiv.symm (Opposite.unop x₁).snd ≫ 𝟙 P
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝ : Category.{v₁, u₂} ℰ<VAR>A : C ⥤ ℰ<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x₁ x₂ : P.Elementsᵒᵖ<VAR>f : x₁ ⟶ x₂<GOAL>yoneda.map (↑f.unop).unop ≫ yonedaEquiv.symm (Opposite.unop x₂).snd = yonedaEquiv.symm (Opposite.unop x₁).snd
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝ : Category.{v₁, u₂} ℰ<VAR>A : C ⥤ ℰ<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x₁ x₂ : P.Elementsᵒᵖ<VAR>f : x₁ ⟶ x₂<GOAL>yonedaEquiv.symm (P.map (↑f.unop) (Opposite.unop x₂).snd) = yonedaEquiv.symm (Opposite.unop x₁).snd
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝ : Category.{v₁, u₂} ℰ<VAR>A : C ⥤ ℰ<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x₁ x₂ : P.Elementsᵒᵖ<VAR>f : x₁ ⟶ x₂<GOAL>P.map (↑f.unop) (Opposite.unop x₂).snd = (Opposite.unop x₁).snd
<VAR>n : ℕ+<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>h : IsCyclotomicExtension {n} ℚ K<GOAL>NrComplexPlaces K = φ ↑n / 2
<VAR>n : ℕ+<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>h : IsCyclotomicExtension {n} ℚ K<VAR>this : NumberField K<GOAL>NrComplexPlaces K = φ ↑n / 2
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : NonarchimedeanGroup G<VAR>H : Type u_2<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalGroup H<VAR>K : Type u_3<VAR>inst✝² : Group K<VAR>inst✝¹ : TopologicalSpace K<VAR>inst✝ : NonarchimedeanGroup K<VAR>U : Set (G × K)<VAR>hU : U ∈ 𝓝 1<GOAL>∃ V W, ↑V ×ˢ ↑W ⊆ U
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : NonarchimedeanGroup G<VAR>H : Type u_2<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalGroup H<VAR>K : Type u_3<VAR>inst✝² : Group K<VAR>inst✝¹ : TopologicalSpace K<VAR>inst✝ : NonarchimedeanGroup K<VAR>U : Set (G × K)<VAR>hU : ∃ t₁ ∈ 𝓝 1, ∃ t₂ ∈ 𝓝 1, t₁ ×ˢ t₂ ⊆ U<GOAL>∃ V W, ↑V ×ˢ ↑W ⊆ U
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : NonarchimedeanGroup G<VAR>H : Type u_2<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalGroup H<VAR>K : Type u_3<VAR>inst✝² : Group K<VAR>inst✝¹ : TopologicalSpace K<VAR>inst✝ : NonarchimedeanGroup K<VAR>U : Set (G × K)<VAR>U₁ : Set G<VAR>hU₁ : U₁ ∈ 𝓝 1<VAR>U₂ : Set K<VAR>hU₂ : U₂ ∈ 𝓝 1<VAR>h : U₁ ×ˢ U₂ ⊆ U<GOAL>∃ V W, ↑V ×ˢ ↑W ⊆ U
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : NonarchimedeanGroup G<VAR>H : Type u_2<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalGroup H<VAR>K : Type u_3<VAR>inst✝² : Group K<VAR>inst✝¹ : TopologicalSpace K<VAR>inst✝ : NonarchimedeanGroup K<VAR>U : Set (G × K)<VAR>U₁ : Set G<VAR>hU₁ : U₁ ∈ 𝓝 1<VAR>U₂ : Set K<VAR>hU₂ : U₂ ∈ 𝓝 1<VAR>h : U₁ ×ˢ U₂ ⊆ U<VAR>V : OpenSubgroup G<VAR>hV : ↑V ⊆ U₁<GOAL>∃ V W, ↑V ×ˢ ↑W ⊆ U
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : NonarchimedeanGroup G<VAR>H : Type u_2<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalGroup H<VAR>K : Type u_3<VAR>inst✝² : Group K<VAR>inst✝¹ : TopologicalSpace K<VAR>inst✝ : NonarchimedeanGroup K<VAR>U : Set (G × K)<VAR>U₁ : Set G<VAR>hU₁ : U₁ ∈ 𝓝 1<VAR>U₂ : Set K<VAR>hU₂ : U₂ ∈ 𝓝 1<VAR>h : U₁ ×ˢ U₂ ⊆ U<VAR>V : OpenSubgroup G<VAR>hV : ↑V ⊆ U₁<VAR>W : OpenSubgroup K<VAR>hW : ↑W ⊆ U₂<GOAL>∃ V W, ↑V ×ˢ ↑W ⊆ U
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : NonarchimedeanGroup G<VAR>H : Type u_2<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalGroup H<VAR>K : Type u_3<VAR>inst✝² : Group K<VAR>inst✝¹ : TopologicalSpace K<VAR>inst✝ : NonarchimedeanGroup K<VAR>U : Set (G × K)<VAR>U₁ : Set G<VAR>hU₁ : U₁ ∈ 𝓝 1<VAR>U₂ : Set K<VAR>hU₂ : U₂ ∈ 𝓝 1<VAR>h : U₁ ×ˢ U₂ ⊆ U<VAR>V : OpenSubgroup G<VAR>hV : ↑V ⊆ U₁<VAR>W : OpenSubgroup K<VAR>hW : ↑W ⊆ U₂<GOAL>∃ W, ↑V ×ˢ ↑W ⊆ U
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : NonarchimedeanGroup G<VAR>H : Type u_2<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalGroup H<VAR>K : Type u_3<VAR>inst✝² : Group K<VAR>inst✝¹ : TopologicalSpace K<VAR>inst✝ : NonarchimedeanGroup K<VAR>U : Set (G × K)<VAR>U₁ : Set G<VAR>hU₁ : U₁ ∈ 𝓝 1<VAR>U₂ : Set K<VAR>hU₂ : U₂ ∈ 𝓝 1<VAR>h : U₁ ×ˢ U₂ ⊆ U<VAR>V : OpenSubgroup G<VAR>hV : ↑V ⊆ U₁<VAR>W : OpenSubgroup K<VAR>hW : ↑W ⊆ U₂<GOAL>↑V ×ˢ ↑W ⊆ U
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : NonarchimedeanGroup G<VAR>H : Type u_2<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalGroup H<VAR>K : Type u_3<VAR>inst✝² : Group K<VAR>inst✝¹ : TopologicalSpace K<VAR>inst✝ : NonarchimedeanGroup K<VAR>U : Set (G × K)<VAR>U₁ : Set G<VAR>hU₁ : U₁ ∈ 𝓝 1<VAR>U₂ : Set K<VAR>hU₂ : U₂ ∈ 𝓝 1<VAR>h : U₁ ×ˢ U₂ ⊆ U<VAR>V : OpenSubgroup G<VAR>hV : ↑V ⊆ U₁<VAR>W : OpenSubgroup K<VAR>hW : ↑W ⊆ U₂<GOAL>∀ x ∈ ↑V, ∀ y ∈ ↑W, (x, y) ∈ U
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : NonarchimedeanGroup G<VAR>H : Type u_2<VAR>inst✝⁵ : Group H<VAR>inst✝⁴ : TopologicalSpace H<VAR>inst✝³ : TopologicalGroup H<VAR>K : Type u_3<VAR>inst✝² : Group K<VAR>inst✝¹ : TopologicalSpace K<VAR>inst✝ : NonarchimedeanGroup K<VAR>U : Set (G × K)<VAR>U₁ : Set G<VAR>hU₁ : U₁ ∈ 𝓝 1<VAR>U₂ : Set K<VAR>hU₂ : U₂ ∈ 𝓝 1<VAR>h : U₁ ×ˢ U₂ ⊆ U<VAR>V : OpenSubgroup G<VAR>hV : ↑V ⊆ U₁<VAR>W : OpenSubgroup K<VAR>hW : ↑W ⊆ U₂<VAR>x : G<VAR>hX : x ∈ ↑V<VAR>y : K<VAR>hY : y ∈ ↑W<GOAL>(x, y) ∈ U
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a : G<VAR>n : ℤ<GOAL>a ^ |n| = 1 ↔ a ^ n = 1
<VAR>x y : SimplexCategory<VAR>f : x ⟶ y<VAR>hyp_f_mono : Mono f<GOAL>x.len ≤ y.len
<VAR>x y : SimplexCategory<VAR>f : x ⟶ y<VAR>hyp_f_mono : Mono f<VAR>f_inj : Function.Injective (Hom.toOrderHom f).toFun<GOAL>x.len ≤ y.len
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>b : β<VAR>s : Multiset α<VAR>t : Multiset β<GOAL>{a} ×ˢ {b} = {(a, b)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝² : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a✝ a : α<VAR>s : Set (β × γ)<VAR>h2s : ((κ ⊗ₖ η) a) s ≠ ⊤<VAR>t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s<GOAL>HasFiniteIntegral (fun b => ((η (a, b)) (Prod.mk b ⁻¹' s)).toReal) (κ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝² : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a✝ a : α<VAR>s : Set (β × γ)<VAR>h2s : ((κ ⊗ₖ η) a) s ≠ ⊤<VAR>t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s<GOAL>∫⁻ (a_1 : β), ENNReal.ofReal ((η (a, a_1)) (Prod.mk a_1 ⁻¹' s)).toReal ∂κ a < ⊤
<VAR>𝕜 : Type u<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : LocallyCompactSpace E<GOAL>LocallyCompactSpace 𝕜
<VAR>𝕜 : Type u<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : LocallyCompactSpace E<VAR>v : E<VAR>hv : v ≠ 0<GOAL>LocallyCompactSpace 𝕜
<VAR>𝕜 : Type u<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : LocallyCompactSpace E<VAR>v : E<VAR>hv : v ≠ 0<VAR>L : 𝕜 → E := fun t => t • v<GOAL>LocallyCompactSpace 𝕜
<VAR>𝕜 : Type u<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>inst✝¹ : Nontrivial E<VAR>inst✝ : LocallyCompactSpace E<VAR>v : E<VAR>hv : v ≠ 0<VAR>L : 𝕜 → E := fun t => t • v<VAR>this : ClosedEmbedding L<GOAL>LocallyCompactSpace 𝕜
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>inst✝² : GroupWithZero G₀<VAR>inst✝¹ : Bornology G₀<VAR>inst✝ : MulAction G₀ α<VAR>s t u : Set α<VAR>S : Set (Set α)<GOAL>Absorbs G₀ (s ∩ t) u ↔ Absorbs G₀ s u ∧ Absorbs G₀ t u
<VAR>Γ✝ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k : ℤ<VAR>Γ : Subgroup SL(2, ℤ)<VAR>f : ℍ → ℂ<VAR>γ : ↥Γ<VAR>z : ℍ<GOAL>(f ∣[k] γ) z = f z ↔ f (γ • z) = (↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k * f z
<VAR>Γ✝ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k : ℤ<VAR>Γ : Subgroup SL(2, ℤ)<VAR>f : ℍ → ℂ<VAR>γ : ↥Γ<VAR>z : ℍ<GOAL>f (↑↑γ • z) * ↑(↑↑↑↑γ).det ^ (k - 1) * denom (↑↑γ) z ^ (-k) = f z ↔ f (γ • z) = (↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k * f z
<VAR>Γ✝ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k : ℤ<VAR>Γ : Subgroup SL(2, ℤ)<VAR>f : ℍ → ℂ<VAR>γ : ↥Γ<VAR>z : ℍ<GOAL>f (↑↑γ • z) * ↑(↑↑↑↑γ).det ^ (k - 1) * denom (↑↑γ) z ^ (-k) = ((↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k)⁻¹ * f (γ • z)
<VAR>Γ✝ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k : ℤ<VAR>Γ : Subgroup SL(2, ℤ)<VAR>f : ℍ → ℂ<VAR>γ : ↥Γ<VAR>z : ℍ<GOAL>(↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteDistribLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>inst✝ : f.NeBot<VAR>a : α<GOAL>a ⊔ limsup u f = limsup (fun x => a ⊔ u x) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteDistribLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>inst✝ : f.NeBot<VAR>a : α<GOAL>⨅ i ∈ f, a ⊔ ⨆ a ∈ i, u a = ⨅ s ∈ f, (⨆ x ∈ s, a) ⊔ ⨆ x ∈ s, u x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : CompleteDistribLattice α<VAR>f : Filter β<VAR>p q : β → Prop<VAR>u : β → α<VAR>inst✝ : f.NeBot<VAR>a : α<VAR>s : Set β<VAR>hs : s ∈ f<GOAL>a = ⨆ x ∈ s, a
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : NonUnitalNonAssocRing α<VAR>inst✝ : IsLeftCancelMulZero α<VAR>x y : α<VAR>h : x * y = 0<VAR>hx : ¬x = 0<GOAL>x = 0 ∨ y = 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<GOAL>(toOpen R (PrimeSpectrum.basicOpen f)) f * const R 1 f (PrimeSpectrum.basicOpen f) ⋯ = 1
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : Semiring R₃<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>f : M →ₗ[R] M<VAR>n m : ℕ<VAR>w : n ≤ m<VAR>x : M<VAR>h : x ∈ (fun n => range (f ^ n)) m<GOAL>x ∈ (fun n => range (f ^ n)) n
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : Semiring R₃<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>x : M<VAR>c : ℕ<VAR>w : n ≤ n + c<VAR>h : x ∈ (fun n => range (f ^ n)) (n + c)<GOAL>x ∈ (fun n => range (f ^ n)) n
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : Semiring R₃<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>x : M<VAR>c : ℕ<VAR>w : n ≤ n + c<VAR>h : ∃ y, (f ^ (n + c)) y = x<GOAL>x ∈ (fun n => range (f ^ n)) n