ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t✝ : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>t : Finset α<VAR>x✝ : t ∈ 𝒜<VAR>hst : t✝ ⊆ t<GOAL>t✝.card ≤ t.card
<VAR>R : Type u_1<VAR>inst✝⁴ : AddCommMonoid R<VAR>inst✝³ : Pow R ℕ<VAR>inst✝² : BinomialRing R<VAR>inst✝¹ : MulOneClass R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<GOAL>multichoose r 1 = r
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>hinj : Function.Injective ⇑φ<VAR>f : R[X]<VAR>hf : f.IsPrimitive<VAR>h_irr : Irreducible (map φ f)<GOAL>Irreducible f
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>hinj : Function.Injective ⇑φ<VAR>f : R[X]<VAR>hf : f.IsPrimitive<VAR>h_irr : Irreducible (map φ f)<VAR>a b : R[X]<VAR>h : f = a * b<GOAL>IsUnit (map φ a) → IsUnit a
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>hinj : Function.Injective ⇑φ<VAR>f : R[X]<VAR>hf : f.IsPrimitive<VAR>h_irr : Irreducible (map φ f)<VAR>a b : R[X]<VAR>h : f = a * b<GOAL>IsUnit (map φ b) → IsUnit b
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>hinj : Function.Injective ⇑φ<VAR>f : R[X]<VAR>hf : f.IsPrimitive<VAR>h_irr : Irreducible (map φ f)<VAR>a b : R[X]<VAR>h : f = a * b<GOAL>a ∣ f
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : IsDomain S<VAR>φ : R →+* S<VAR>hinj : Function.Injective ⇑φ<VAR>f : R[X]<VAR>hf : f.IsPrimitive<VAR>h_irr : Irreducible (map φ f)<VAR>a b : R[X]<VAR>h : f = a * b<GOAL>b ∣ f
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ZMod 2<GOAL>Submodule.comap involute.toLinearMap (evenOdd Q n) = evenOdd Q n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.9082, u_1} C<VAR>X Y Z : C<VAR>inst✝ : HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ pullback f i<VAR>i₂ : V₂ ⟶ pullback f i<GOAL>(i₁ ≫ snd f i) ≫ i = (i₁ ≫ fst f i) ≫ f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.9082, u_1} C<VAR>X Y Z : C<VAR>inst✝ : HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ pullback f i<VAR>i₂ : V₂ ⟶ pullback f i<GOAL>(i₂ ≫ snd f i) ≫ i = (i₂ ≫ fst f i) ≫ f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X Y Z : C<VAR>inst✝ : HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ pullback f i<VAR>i₂ : V₂ ⟶ pullback f i<GOAL>snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i = fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X Y Z : C<VAR>inst✝ : HasPullbacks C<VAR>U V₁ V₂ : C<VAR>f : X ⟶ Y<VAR>i : U ⟶ Y<VAR>i₁ : V₁ ⟶ pullback f i<VAR>i₂ : V₂ ⟶ pullback f i<GOAL>snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i = fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : Nonempty γ<VAR>a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Icc a b)<VAR>ha : a ∈ s<VAR>hab : a ≤ b<VAR>hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty<VAR>S : Set α := s ∩ Icc a b<GOAL>b ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : Nonempty γ<VAR>a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Icc a b)<VAR>hab : a ≤ b<VAR>hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty<VAR>S : Set α := s ∩ Icc a b<VAR>ha : a ∈ S<GOAL>b ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : Nonempty γ<VAR>a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Icc a b)<VAR>hab : a ≤ b<VAR>hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty<VAR>S : Set α := s ∩ Icc a b<VAR>ha : a ∈ S<VAR>Sbd : BddAbove S<GOAL>b ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : Nonempty γ<VAR>a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Icc a b)<VAR>hab : a ≤ b<VAR>hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty<VAR>S : Set α := s ∩ Icc a b<VAR>ha : a ∈ S<VAR>Sbd : BddAbove S<VAR>c : α := sSup (s ∩ Icc a b)<GOAL>b ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : Nonempty γ<VAR>a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Icc a b)<VAR>hab : a ≤ b<VAR>hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty<VAR>S : Set α := s ∩ Icc a b<VAR>ha : a ∈ S<VAR>Sbd : BddAbove S<VAR>c : α := sSup (s ∩ Icc a b)<VAR>c_mem : c ∈ S<GOAL>b ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : Nonempty γ<VAR>a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Icc a b)<VAR>hab : a ≤ b<VAR>hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty<VAR>S : Set α := s ∩ Icc a b<VAR>ha : a ∈ S<VAR>Sbd : BddAbove S<VAR>c : α := sSup (s ∩ Icc a b)<VAR>c_mem : c ∈ S<VAR>c_le : c ≤ b<GOAL>b ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : Nonempty γ<VAR>a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Icc a b)<VAR>hab : a ≤ b<VAR>hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty<VAR>S : Set α := s ∩ Icc a b<VAR>ha : a ∈ S<VAR>Sbd : BddAbove S<VAR>c : α := sSup (s ∩ Icc a b)<VAR>c_mem : c ∈ S<VAR>c_le : c ≤ b<VAR>hc : c = b<GOAL>b ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : Nonempty γ<VAR>a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Icc a b)<VAR>hab : a ≤ b<VAR>hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty<VAR>S : Set α := s ∩ Icc a b<VAR>ha : a ∈ S<VAR>Sbd : BddAbove S<VAR>c : α := sSup (s ∩ Icc a b)<VAR>c_mem : c ∈ S<VAR>c_le : c ≤ b<VAR>hc : c < b<GOAL>b ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : Nonempty γ<VAR>a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Icc a b)<VAR>hab : a ≤ b<VAR>hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty<VAR>S : Set α := s ∩ Icc a b<VAR>ha : a ∈ S<VAR>Sbd : BddAbove S<VAR>c : α := sSup (s ∩ Icc a b)<VAR>c_mem : c ∈ S<VAR>c_le : c ≤ b<VAR>hc : c < b<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : Nonempty γ<VAR>a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Icc a b)<VAR>hab : a ≤ b<VAR>hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty<VAR>S : Set α := s ∩ Icc a b<VAR>ha : a ∈ S<VAR>Sbd : BddAbove S<VAR>c : α := sSup (s ∩ Icc a b)<VAR>c_mem : c ∈ S<VAR>c_le : c ≤ b<VAR>hc : c < b<VAR>x : α<VAR>xs : x ∈ s<VAR>cx : c < x<VAR>xb : x ≤ b<GOAL>False
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : TopologicalSpace E<VAR>f : E → F<VAR>x : E<GOAL>oscillation f x = 0 ↔ ContinuousAt f x
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : TopologicalSpace E<VAR>f : E → F<VAR>x : E<GOAL>oscillationWithin f univ x = 0 ↔ ContinuousWithinAt f univ x
<VAR>α : Type u<VAR>ι : Type v<VAR>inst✝¹ : MetricSpace α<VAR>inst✝ : ProperSpace α<VAR>c : ι → α<VAR>x : α<VAR>r✝ : ℝ<VAR>s : Set α<VAR>r : ι → ℝ<VAR>hr : ∀ (i : ι), 0 < r i<VAR>hs : IsClosed s<VAR>uf : ∀ x ∈ s, {i | x ∈ ball (c i) (r i)}.Finite<VAR>us : s ⊆ ⋃ i, ball (c i) (r i)<GOAL>∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
<VAR>α : Type u<VAR>ι : Type v<VAR>inst✝¹ : MetricSpace α<VAR>inst✝ : ProperSpace α<VAR>c : ι → α<VAR>x : α<VAR>r✝ : ℝ<VAR>s : Set α<VAR>r : ι → ℝ<VAR>hr : ∀ (i : ι), 0 < r i<VAR>hs : IsClosed s<VAR>uf : ∀ x ∈ s, {i | x ∈ ball (c i) (r i)}.Finite<VAR>us : s ⊆ ⋃ i, ball (c i) (r i)<VAR>v : ι → Set α<VAR>hsv : s ⊆ iUnion v<VAR>hvc : ∀ (i : ι), IsClosed (v i)<VAR>hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)<GOAL>∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
<VAR>α : Type u<VAR>ι : Type v<VAR>inst✝¹ : MetricSpace α<VAR>inst✝ : ProperSpace α<VAR>c : ι → α<VAR>x : α<VAR>r✝ : ℝ<VAR>s : Set α<VAR>r : ι → ℝ<VAR>hr : ∀ (i : ι), 0 < r i<VAR>hs : IsClosed s<VAR>uf : ∀ x ∈ s, {i | x ∈ ball (c i) (r i)}.Finite<VAR>us : s ⊆ ⋃ i, ball (c i) (r i)<VAR>v : ι → Set α<VAR>hsv : s ⊆ iUnion v<VAR>hvc : ∀ (i : ι), IsClosed (v i)<VAR>hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)<VAR>this : ∀ (i : ι), ∃ r' ∈ Ioo 0 (r i), v i ⊆ ball (c i) r'<GOAL>∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
<VAR>α : Type u<VAR>ι : Type v<VAR>inst✝¹ : MetricSpace α<VAR>inst✝ : ProperSpace α<VAR>c : ι → α<VAR>x : α<VAR>r✝ : ℝ<VAR>s : Set α<VAR>r : ι → ℝ<VAR>hr : ∀ (i : ι), 0 < r i<VAR>hs : IsClosed s<VAR>uf : ∀ x ∈ s, {i | x ∈ ball (c i) (r i)}.Finite<VAR>us : s ⊆ ⋃ i, ball (c i) (r i)<VAR>v : ι → Set α<VAR>hsv : s ⊆ iUnion v<VAR>hvc : ∀ (i : ι), IsClosed (v i)<VAR>hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)<VAR>r' : ι → ℝ<VAR>hlt : ∀ (i : ι), r' i ∈ Ioo 0 (r i)<VAR>hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)<GOAL>∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>0 ≤ x ↔ ∀ (j : x.RightMoves), ∃ i, 0 ≤ (x.moveRight j).moveLeft i
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>((∀ (i : LeftMoves 0), (∃ i', moveLeft 0 i ≤ x.moveLeft i') ∨ ∃ j, (moveLeft 0 i).moveRight j ≤ x) ∧ ∀ (j : x.RightMoves), (∃ i, 0 ≤ (x.moveRight j).moveLeft i) ∨ ∃ j', moveRight 0 j' ≤ x.moveRight j) ↔ ∀ (j : x.RightMoves), ∃ i, 0 ≤ (x.moveRight j).moveLeft i
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>a : ℤ<VAR>b : ℕ<VAR>hb : ↑b ≠ 0<GOAL>↑(mkRat a b) = ↑a / ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>a : ℤ<VAR>b : ℕ<VAR>hb : ↑b ≠ 0<GOAL>↑↑b ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>h : a ∈ t<GOAL>a ∉ s \ t
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : AddCommMonoid α<VAR>f : κ → α<VAR>s : Finset κ<VAR>i : ι<GOAL>∑ g ∈ piFinset fun x => s, f (g i) = s.card ^ (card ι - 1) • ∑ b ∈ s, f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>p q : α<VAR>hq : Irreducible q<VAR>left✝ : p ≠ 0<VAR>x : α<VAR>hx : ¬IsUnit x<VAR>hx' : q = p * x<GOAL>IsUnit p
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<GOAL>X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ i.castSucc) = X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ i.succ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝³ : DecidableRel f.SameCycle<VAR>inst✝² : DecidableRel g.SameCycle<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<GOAL>(f.cycleOf x).support.Nonempty ↔ f x ≠ x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y : α<VAR>inst✝³ : DecidableRel f.SameCycle<VAR>inst✝² : DecidableRel g.SameCycle<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<GOAL>Nat.succ 0 ≤ (f.cycleOf x).support.card ↔ 2 ≤ (f.cycleOf x).support.card
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<GOAL>Embedding (tensorProductTo R S T)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<GOAL>Inducing (tensorProductTo R S T)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<GOAL>Inducing (tensorProductTo R S T)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<GOAL>∀ U ∈ Set.range basicOpen, IsOpen ↑U
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>f : S ⊗[R] T<GOAL>IsOpen ↑(basicOpen f)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>f : S ⊗[R] T<GOAL>∀ x ∈ ↑(basicOpen f), ∃ t ⊆ ↑(basicOpen f), IsOpen t ∧ x ∈ t
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>f : S ⊗[R] T<VAR>J : PrimeSpectrum (S ⊗[R] T)<VAR>hJ : f ∉ J.asIdeal<GOAL>∃ t ⊆ ↑(basicOpen f), IsOpen t ∧ J ∈ t
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>f : S ⊗[R] T<VAR>J : PrimeSpectrum (S ⊗[R] T)<VAR>hJ : f ∉ J.asIdeal<VAR>t : T<VAR>r : R<VAR>a : S<VAR>ht : r • t ∉ Ideal.comap g J.asIdeal<VAR>e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t<GOAL>∃ t ⊆ ↑(basicOpen f), IsOpen t ∧ J ∈ t
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>f : S ⊗[R] T<VAR>J : PrimeSpectrum (S ⊗[R] T)<VAR>hJ : f ∉ J.asIdeal<VAR>t : T<VAR>r : R<VAR>a : S<VAR>ht : r • t ∉ Ideal.comap g J.asIdeal<VAR>e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t<GOAL>tensorProductTo R S T ⁻¹' (basicOpen a).carrier ×ˢ (basicOpen t).carrier ⊆ ↑(basicOpen f)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>f : S ⊗[R] T<VAR>J : PrimeSpectrum (S ⊗[R] T)<VAR>hJ : f ∉ J.asIdeal<VAR>t : T<VAR>r : R<VAR>a : S<VAR>ht : r • t ∉ Ideal.comap g J.asIdeal<VAR>e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t<GOAL>J ∈ tensorProductTo R S T ⁻¹' (basicOpen a).carrier ×ˢ (basicOpen t).carrier
<VAR>R : Type u_1<VAR>inst✝⁴ : Semiring R<VAR>S : Submonoid R<VAR>inst✝³ : OreSet S<VAR>X : Type u_2<VAR>inst✝² : AddCommMonoid X<VAR>inst✝¹ : Module R X<VAR>T : Type u_3<VAR>inst✝ : Semiring T<VAR>f : R →+* T<VAR>fS : ↥S →* Tˣ<VAR>hf : ∀ (s : ↥S), f ↑s = ↑(fS s)<VAR>r : R<GOAL>(universalHom f fS hf) (numeratorHom r) = f r
<VAR>b : ℕ<GOAL>jacobiSymNat 1 b = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Finite β<VAR>P : Perm β → Prop<VAR>σ : Perm β<VAR>base_one : P 1<VAR>base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ<VAR>induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)<GOAL>P σ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Finite β<VAR>P : Perm β → Prop<VAR>σ : Perm β<VAR>base_one : P 1<VAR>base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ<VAR>induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)<VAR>val✝ : Fintype β<GOAL>P σ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Finite β<VAR>P : Perm β → Prop<VAR>σ : Perm β<VAR>base_one : P 1<VAR>base_cycles : ∀ (σ : Perm β), σ.IsCycle → P σ<VAR>induction_disjoint : ∀ (σ τ : Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)<VAR>val✝ : Fintype β<GOAL>∀ (l : List (Perm β)), (∀ τ ∈ l, τ.IsCycle) → List.Pairwise Disjoint l → P l.prod
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>x y : γ<GOAL>dist x y ≠ 0 ↔ x ≠ y
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ : V<VAR>c : ℝ<VAR>hc : c ≠ 0<VAR>x y : V<GOAL>angle (c • x) (c • y) = angle x y
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ : V<VAR>c : ℝ<VAR>hc : c ≠ 0<VAR>x y : V<VAR>this : c * c ≠ 0<GOAL>angle (c • x) (c • y) = angle x y
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>F : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f✝ : F<VAR>f : R ≃+* S<GOAL>ker ↑f = ⊥
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a b : α<VAR>l : List α<VAR>x : α<VAR>hx : x ∈ (a :: b :: l).getLast?<GOAL>∃ h, x = (a :: b :: l).getLast h
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a b : α<VAR>l : List α<VAR>x : α<VAR>hx : x ∈ (b :: l).getLast?<GOAL>∃ h, x = (a :: b :: l).getLast h
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a b : α<VAR>l : List α<VAR>x : α<VAR>hx : x ∈ (b :: l).getLast?<VAR>w✝ : b :: l ≠ []<VAR>h₂ : x = (b :: l).getLast w✝<GOAL>∃ h, x = (a :: b :: l).getLast h
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a b : α<VAR>l : List α<VAR>x : α<VAR>hx : x ∈ (b :: l).getLast?<VAR>w✝ : b :: l ≠ []<VAR>h₂ : x = (b :: l).getLast w✝<GOAL>x = (a :: b :: l).getLast ⋯
<VAR>a b c : ℕ<GOAL>Fintype.card ↑(Set.Ico a b) = b - a
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>U : Set G<VAR>hU : IsOpen U<VAR>h'U : U.Nonempty<VAR>h : μ U ≠ ⊤<VAR>K : Set G<VAR>hK : IsCompact K<GOAL>μ K < ⊤
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>U : Set G<VAR>hU : IsOpen U<VAR>h'U : (interior U).Nonempty<VAR>h : μ U ≠ ⊤<VAR>K : Set G<VAR>hK : IsCompact K<GOAL>μ K < ⊤
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>U : Set G<VAR>hU : IsOpen U<VAR>h'U : (interior U).Nonempty<VAR>h : μ U ≠ ⊤<VAR>K : Set G<VAR>hK : IsCompact K<VAR>t : Finset G<VAR>hKt : K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' U<GOAL>μ K < ⊤
<VAR>α : Type u_1<VAR>K : Type u_2<VAR>inst✝ : LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<VAR>x : K<GOAL>x ∈ r • Ioo a b ↔ x ∈ Ioo (r • a) (r • b)
<VAR>α : Type u_1<VAR>K : Type u_2<VAR>inst✝ : LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<VAR>x : K<GOAL>(∃ y, (a < y ∧ y < b) ∧ r * y = x) ↔ r * a < x ∧ x < r * b
<VAR>x✝ y✝ z : ℝ<VAR>n : ℕ<VAR>x : ℝ<VAR>hx : x ≠ 0<VAR>y : ℝ<GOAL>x ^ (y - 1) = x ^ y / x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p✝ p : ℝ≥0∞<VAR>f : α →ₛ E<VAR>hf : ∀ (y : E), y ≠ 0 → μ (↑f ⁻¹' {y}) < ⊤<VAR>hp0 : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>Memℒp (↑f) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p✝ p : ℝ≥0∞<VAR>f : α →ₛ E<VAR>hf : ∀ (y : E), y ≠ 0 → μ (↑f ⁻¹' {y}) < ⊤<VAR>hp0 : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>eLpNorm (↑f) p μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p✝ p : ℝ≥0∞<VAR>f : α →ₛ E<VAR>hf : ∀ (y : E), y ≠ 0 → μ (↑f ⁻¹' {y}) < ⊤<VAR>hp0 : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>(∑ y ∈ f.range, ↑‖y‖₊ ^ p.toReal * μ (↑f ⁻¹' {y})) ^ (1 / p.toReal) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p✝ p : ℝ≥0∞<VAR>f : α →ₛ E<VAR>hf : ∀ (y : E), y ≠ 0 → μ (↑f ⁻¹' {y}) < ⊤<VAR>hp0 : ¬p = 0<VAR>hp_top : ¬p = ⊤<VAR>y : E<VAR>x✝ : y ∈ f.range<GOAL>↑‖y‖₊ ^ p.toReal * μ (↑f ⁻¹' {y}) < ⊤
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z x : K<GOAL>‖(starRingEnd K) x + x‖ ^ 2 = re ((starRingEnd K) x + x) ^ 2
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ xs : List α<GOAL>List.filter p l₁ <:+ List.filter p (xs ++ l₁)
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ xs : List α<GOAL>List.filter p l₁ <:+ List.filter p xs ++ List.filter p l₁
<VAR>b x : ℕ<VAR>hb : 1 < b<VAR>z : ℕ<GOAL>clog b (b ^ x) ≤ z ↔ x ≤ z
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>a : α<VAR>b₁ b₂ : β<VAR>h : (a, b₁) = (a, b₂)<GOAL>b₁ = b₂