ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<VAR>i j : M.ι<GOAL>(∑ j : M.ι, (fun j_1 k => if h : j_1 = j then eqToHom ⋯ else 0) ≫ fun j_1 k => if h : j = k then eqToHom ⋯ else 0) i j = if h : i = j then eqToHom ⋯ else 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<VAR>i j : M.ι<GOAL>((fun j k => if h : j = i then eqToHom ⋯ else 0) ≫ fun j k => if h : i = k then eqToHom ⋯ else 0) i j = if h : i = j then eqToHom ⋯ else 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<VAR>i j : M.ι<GOAL>∀ b ∈ Finset.univ, b ≠ i → ((fun j k => if h : j = b then eqToHom ⋯ else 0) ≫ fun j k => if h : b = k then eqToHom ⋯ else 0) i j = 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<VAR>i j : M.ι<GOAL>i ∉ Finset.univ → ((fun j k => if h : j = i then eqToHom ⋯ else 0) ≫ fun j k => if h : i = k then eqToHom ⋯ else 0) i j = 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<GOAL>((biproduct.desc fun i j k => if h : i = k then eqToHom ⋯ else 0) ≫ biproduct.lift fun i j k => if h : j = i then eqToHom ⋯ else 0) = 𝟙 (⨁ fun i => (embedding C).obj (M.X i))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<GOAL>∀ (j : M.ι), ((biproduct.desc fun i j k => if h : i = k then eqToHom ⋯ else 0) ≫ biproduct.lift fun i j k => if h : j = i then eqToHom ⋯ else 0) ≫ biproduct.π (fun i => (embedding C).obj (M.X i)) j = 𝟙 (⨁ fun i => (embedding C).obj (M.X i)) ≫ biproduct.π (fun i => (embedding C).obj (M.X i)) j
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<VAR>i : M.ι<GOAL>((biproduct.desc fun i j k => if h : i = k then eqToHom ⋯ else 0) ≫ biproduct.lift fun i j k => if h : j = i then eqToHom ⋯ else 0) ≫ biproduct.π (fun i => (embedding C).obj (M.X i)) i = 𝟙 (⨁ fun i => (embedding C).obj (M.X i)) ≫ biproduct.π (fun i => (embedding C).obj (M.X i)) i
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<VAR>i : M.ι<GOAL>∀ (j : M.ι), biproduct.ι (fun i => (embedding C).obj (M.X i)) j ≫ ((biproduct.desc fun i j k => if h : i = k then eqToHom ⋯ else 0) ≫ biproduct.lift fun i j k => if h : j = i then eqToHom ⋯ else 0) ≫ biproduct.π (fun i => (embedding C).obj (M.X i)) i = biproduct.ι (fun i => (embedding C).obj (M.X i)) j ≫ 𝟙 (⨁ fun i => (embedding C).obj (M.X i)) ≫ biproduct.π (fun i => (embedding C).obj (M.X i)) i
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<VAR>i j : M.ι<GOAL>biproduct.ι (fun i => (embedding C).obj (M.X i)) j ≫ ((biproduct.desc fun i j k => if h : i = k then eqToHom ⋯ else 0) ≫ biproduct.lift fun i j k => if h : j = i then eqToHom ⋯ else 0) ≫ biproduct.π (fun i => (embedding C).obj (M.X i)) i = biproduct.ι (fun i => (embedding C).obj (M.X i)) j ≫ 𝟙 (⨁ fun i => (embedding C).obj (M.X i)) ≫ biproduct.π (fun i => (embedding C).obj (M.X i)) i
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<VAR>i j : M.ι<GOAL>((fun j_1 k => if h : j = k then eqToHom ⋯ else 0) ≫ fun j k => if h : j = i then eqToHom ⋯ else 0) = if h : j = i then eqToHom ⋯ else 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<VAR>i j : M.ι<GOAL>((fun j_1 k => if h : j = k then eqToHom ⋯ else 0) ≫ fun j k => if h : j = i then eqToHom ⋯ else 0) PUnit.unit PUnit.unit = (if h : j = i then eqToHom ⋯ else 0) PUnit.unit PUnit.unit
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Preadditive C<VAR>M : Mat_ C<VAR>i j : M.ι<GOAL>(if h : j = i then eqToHom ⋯ else 0) = (if h : j = i then eqToHom ⋯ else 0) PUnit.unit PUnit.unit
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<GOAL>0 < (haarContent K₀).outerMeasure ↑K₀
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<GOAL>1 ≤ (haarContent K₀).outerMeasure ↑K₀
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<GOAL>1 ≤ ⨅ U, ⨅ (hU : IsOpen U), ⨅ (_ : ↑K₀ ⊆ U), (haarContent K₀).innerContent { carrier := U, is_open' := hU }
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>U : Set G<VAR>hU : IsOpen U<VAR>hK₀ : ↑K₀ ⊆ U<GOAL>1 ≤ (fun s => ↑((haarContent K₀).toFun s)) K₀.toCompacts
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s₁ s₂ : Finset ι<VAR>S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)<VAR>S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → α i<GOAL>f ∈ cylinder s₁ S₁ ∩ cylinder s₂ S₂ ↔ f ∈ cylinder (s₁ ∪ s₂) ((fun f j => f ⟨↑j, ⋯⟩) ⁻¹' S₁ ∩ (fun f j => f ⟨↑j, ⋯⟩) ⁻¹' S₂)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s₁ s₂ : Finset ι<VAR>S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)<VAR>S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → α i<GOAL>(fun i => f ↑i) ∈ S₁ ∧ (fun i => f ↑i) ∈ S₂ ↔ (fun i => f ↑i) ∈ (fun f j => f ⟨↑j, ⋯⟩) ⁻¹' S₁ ∧ (fun i => f ↑i) ∈ (fun f j => f ⟨↑j, ⋯⟩) ⁻¹' S₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>sSup ↑s ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>s.max' h ∈ s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : LinearOrderedCommRing S<VAR>n : Type u_3<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>c : ι → R<VAR>A : ι → Matrix n n R<VAR>abv : AbsoluteValue R S<VAR>x : S<VAR>hx : ∀ (k : ι) (i j : n), abv (A k i j) ≤ x<VAR>y : S<VAR>hy : ∀ (k : ι), abv (c k) ≤ y<GOAL>abv (∑ k ∈ s, c k • A k).det ≤ (Fintype.card n).factorial • (s.card • y * x) ^ Fintype.card n
<VAR>a b m n✝ p✝ n p : ℕ<VAR>h : ¬p ∣ n<GOAL>n.factorization p = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Zero α<VAR>s : Finset ι<VAR>f : (i : ι) → i ∈ s → α<VAR>i : ι<VAR>b : α<GOAL>single i b = indicator {i} fun x x => b
<VAR>T : Type u<VAR>inst✝ : Category.{v, u} T<VAR>X Y : T<VAR>i : X ≅ Y<VAR>p : Arrow T<VAR>sq : mk i.hom ⟶ p<GOAL>i.inv ≫ sq.left ≫ p.hom = sq.right
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : CommRing K<VAR>c : σ → K<GOAL>(∏ n : σ, (1 - (X n - C (c n)) ^ (Fintype.card K - 1))).degrees ≤ ∑ s : σ, (Fintype.card K - 1) • {s}
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : CommRing K<VAR>c : σ → K<VAR>s : σ<VAR>x✝ : s ∈ Finset.univ<GOAL>(1 - (X s - C (c s)) ^ (Fintype.card K - 1)).degrees ≤ (Fintype.card K - 1) • {s}
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : CommRing K<VAR>c : σ → K<VAR>s : σ<VAR>x✝ : s ∈ Finset.univ<GOAL>degrees 1 ⊔ ((X s - C (c s)) ^ (Fintype.card K - 1)).degrees ≤ (Fintype.card K - 1) • {s}
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : CommRing K<VAR>c : σ → K<VAR>s : σ<VAR>x✝ : s ∈ Finset.univ<GOAL>((X s - C (c s)) ^ (Fintype.card K - 1)).degrees ≤ (Fintype.card K - 1) • {s}
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : CommRing K<VAR>c : σ → K<VAR>s : σ<VAR>x✝ : s ∈ Finset.univ<GOAL>(X s - C (c s)).degrees ≤ {s}
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : CommRing K<VAR>c : σ → K<VAR>s : σ<VAR>x✝ : s ∈ Finset.univ<GOAL>(X s).degrees ⊔ (C (c s)).degrees ≤ {s}
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : CommRing K<VAR>c : σ → K<VAR>s : σ<VAR>x✝ : s ∈ Finset.univ<GOAL>(X s).degrees ≤ {s}
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Scheme<VAR>f : X.Hom Y<VAR>H : IsOpenImmersion f<VAR>U : Y.Opens<VAR>hU : U ≤ f.opensRange<GOAL>↑(f ''ᵁ f ⁻¹ᵁ U) = ↑U
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<VAR>n : ℤ<GOAL>re ↑n = ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>i✝ : Fin n<VAR>i : Fin n.succ<GOAL>i ∈ Ioi i✝.succ ↔ i ∈ map (succEmb n) (Ioi i✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>i✝ : Fin n<VAR>i : Fin n.succ<GOAL>i✝.succ < i ↔ ∃ a, i✝ < a ∧ (succEmb n) a = i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f✝ g : ι → Set X<VAR>f : Option ι → Set X<GOAL>LocallyFinite f ↔ LocallyFinite (f ∘ some)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f✝ g : ι → Set X<VAR>f : Option ι → Set X<GOAL>LocallyFinite ((f ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧ LocallyFinite ((f ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) ↔ LocallyFinite (f ∘ some)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f✝ g : ι → Set X<VAR>f : Option ι → Set X<GOAL>LocallyFinite ((f ∘ ⇑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ↔ LocallyFinite (f ∘ some)
<VAR>x y : ℂ<GOAL>sin x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)
<VAR>x y : ℂ<VAR>s1 : sin ((x + y) / 2 + (x - y) / 2) = sin ((x + y) / 2) * cos ((x - y) / 2) + cos ((x + y) / 2) * sin ((x - y) / 2)<GOAL>sin x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)
<VAR>x y : ℂ<VAR>s1 : sin ((x + y) / 2 + (x - y) / 2) = sin ((x + y) / 2) * cos ((x - y) / 2) + cos ((x + y) / 2) * sin ((x - y) / 2)<VAR>s2 : sin ((x + y) / 2 - (x - y) / 2) = sin ((x + y) / 2) * cos ((x - y) / 2) - cos ((x + y) / 2) * sin ((x - y) / 2)<GOAL>sin x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)
<VAR>x y : ℂ<VAR>s1 : sin x = sin ((x + y) / 2) * cos ((x - y) / 2) + cos ((x + y) / 2) * sin ((x - y) / 2)<VAR>s2 : sin ((x + y) / 2 - (x - y) / 2) = sin ((x + y) / 2) * cos ((x - y) / 2) - cos ((x + y) / 2) * sin ((x - y) / 2)<GOAL>sin x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)
<VAR>x y : ℂ<VAR>s1 : sin x = sin ((x + y) / 2) * cos ((x - y) / 2) + cos ((x + y) / 2) * sin ((x - y) / 2)<VAR>s2 : sin y = sin ((x + y) / 2) * cos ((x - y) / 2) - cos ((x + y) / 2) * sin ((x - y) / 2)<GOAL>sin x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)
<VAR>d a : ℤ<VAR>b c : ℤ√d<VAR>ha : a ≠ 0<VAR>h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im<GOAL>b.re = c.re ∧ b.im = c.im
<VAR>α : Type u_1<VAR>inst✝² : LinearOrderedAddCommGroup α<VAR>inst✝¹ : DistribMulAction ℚ≥0 α<VAR>inst✝ : PosSMulMono ℚ≥0 α<VAR>q : ℚ≥0<VAR>a : α<GOAL>|q • a| = q • |a|
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t : Cocone F<VAR>X : C<VAR>h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones<VAR>Y : C<VAR>f : X ⟶ Y<VAR>j : J<GOAL>(h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t✝ : Cocone F<VAR>X : C<VAR>h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones<VAR>Y : C<VAR>f : X ⟶ Y<VAR>j : J<VAR>t : ((coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃}).map f ≫ h.hom.app Y) { down := 𝟙 X } = (h.hom.app X ≫ F.cocones.map f) { down := 𝟙 X }<GOAL>(h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t✝ : Cocone F<VAR>X : C<VAR>h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones<VAR>Y : C<VAR>f : X ⟶ Y<VAR>j : J<VAR>t : h.hom.app Y { down := 𝟙 X ≫ f } = F.cocones.map f (h.hom.app X { down := 𝟙 X })<GOAL>(h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t✝ : Cocone F<VAR>X : C<VAR>h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones<VAR>Y : C<VAR>f : X ⟶ Y<VAR>j : J<VAR>t : h.hom.app Y { down := f } = F.cocones.map f (h.hom.app X { down := 𝟙 X })<GOAL>(h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝ : Category.{v₃, u₃} C<VAR>F : J ⥤ C<VAR>t✝ : Cocone F<VAR>X : C<VAR>h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones<VAR>Y : C<VAR>f : X ⟶ Y<VAR>j : J<VAR>t : h.hom.app Y { down := f } = F.cocones.map f (h.hom.app X { down := 𝟙 X })<GOAL>(F.cocones.map f (h.hom.app X { down := 𝟙 X })).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j
<VAR>a b c d m✝ n✝ m n k i : ℤ<VAR>H : m % n = k % n<GOAL>(m + i) % n = (k + i) % n
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r₁ r₂ : R<VAR>h₀ : 0 < r₁<VAR>h : r₁ ≤ r₂<GOAL>log b r₁ ≤ log b r₂
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r₁ r₂ : R<VAR>h₀ : 0 < r₁<VAR>h : r₁ ≤ r₂<VAR>h₁ : r₁ ≤ 1<VAR>h₂ : r₂ ≤ 1<GOAL>log b r₁ ≤ log b r₂
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r₁ r₂ : R<VAR>h₀ : 0 < r₁<VAR>h : r₁ ≤ r₂<VAR>h₁ : r₁ ≤ 1<VAR>h₂ : 1 ≤ r₂<GOAL>log b r₁ ≤ log b r₂
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r₁ r₂ : R<VAR>h₀ : 0 < r₁<VAR>h : r₁ ≤ r₂<VAR>h₁ : 1 ≤ r₁<VAR>h₂ : r₂ ≤ 1<GOAL>log b r₁ ≤ log b r₂
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r₁ r₂ : R<VAR>h₀ : 0 < r₁<VAR>h : r₁ ≤ r₂<VAR>h₁ : 1 ≤ r₁<VAR>h₂ : 1 ≤ r₂<GOAL>log b r₁ ≤ log b r₂
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>h : ¬p = 0<GOAL>p.primPart.IsPrimitive
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>h : ¬p.content = 0<GOAL>p.primPart.IsPrimitive
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>h : ¬p.content = 0<GOAL>p.primPart.content = 1
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>h : ¬p.content = 0<GOAL>p.content * p.primPart.content = p.content * 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f g : A<GOAL>basicOpen 𝒜 (f * g) ≤ basicOpen 𝒜 f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f g : A<GOAL>basicOpen 𝒜 f ⊓ basicOpen 𝒜 g ≤ basicOpen 𝒜 f
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>a * b ≤ b⁻¹ * b ↔ a * b ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ t : Set α<VAR>inst✝¹ : Fintype α<VAR>s : Set α<VAR>inst✝ : Fintype ↑s<GOAL>s.toFinset ⊂ Finset.univ ↔ s ⊂ univ
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Field K<VAR>a b : σ → K<VAR>h : a ≠ b<GOAL>(eval a) (indicator b) = 0
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Field K<VAR>a b : σ → K<VAR>h : a ≠ b<VAR>i : σ<VAR>hi : a i ≠ b i<GOAL>(eval a) (indicator b) = 0
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Field K<VAR>a b : σ → K<VAR>h : a ≠ b<VAR>i : σ<VAR>hi : a i ≠ b i<GOAL>∃ a_1 ∈ Finset.univ, 1 - (a a_1 - b a_1) ^ (Fintype.card K - 1) = 0
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Field K<VAR>a b : σ → K<VAR>h : a ≠ b<VAR>i : σ<VAR>hi : a i ≠ b i<GOAL>1 - (a i - b i) ^ (Fintype.card K - 1) = 0
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Fintype σ<VAR>inst✝ : Field K<VAR>a b : σ → K<VAR>h : a ≠ b<VAR>i : σ<VAR>hi : a i ≠ b i<GOAL>a i - b i ≠ 0
<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✝⁹ : CommSemiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>R₂ : Type u_7<VAR>M₂ : Type u_8<VAR>inst✝⁶ : CommRing R₂<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R₂ M₂<VAR>e : Basis ι R M<VAR>v : ι' → M<VAR>i : ι<VAR>j : ι'<VAR>N : Type u_9<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>b : Basis ι R M<VAR>b' : Basis ι' R M<VAR>c : Basis κ R N<VAR>c' : Basis κ' R N<VAR>f : M →ₗ[R] N<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι'<GOAL>b.toMatrix ⇑b' * b'.toMatrix ⇑b = 1
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y = 0 ↔ o.oangle y x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<GOAL>Fintype.card { a // ¬a.IsDiag } = (Fintype.card α).choose 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<GOAL>Fintype.card { a // ¬a.IsDiag } = (image Sym2.mk univ.offDiag).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<GOAL>∀ (x : Sym2 α), x ∈ filter (fun a => ¬a.IsDiag) (image Sym2.mk (univ ×ˢ univ)) ↔ ¬x.IsDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>x : Sym2 α<GOAL>x ∈ filter (fun a => ¬a.IsDiag) (image Sym2.mk (univ ×ˢ univ)) ↔ ¬x.IsDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>x : Sym2 α<GOAL>(∃ a ∈ univ, Sym2.mk a = x) ∧ ¬x.IsDiag ↔ ¬x.IsDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>x : Sym2 α<VAR>a : α × α<VAR>ha : Quot.mk (Rel α) a = x<GOAL>(∃ a ∈ univ, Sym2.mk a = x) ∧ ¬x.IsDiag ↔ ¬x.IsDiag
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>c : Computation α<GOAL>(HOrElse.hOrElse (empty α) fun x => c) = c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>c : Computation α<GOAL>IsBisimulation fun c₁ c₂ => (HOrElse.hOrElse (empty α) fun x => c₂) = c₁
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>c s' s : Computation α<VAR>h : (HOrElse.hOrElse (empty α) fun x => s) = s'<GOAL>BisimO (fun c₁ c₂ => (HOrElse.hOrElse (empty α) fun x => c₂) = c₁) (HOrElse.hOrElse (empty α) fun x => s).destruct s.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>c s' s✝ : Computation α<VAR>h : (HOrElse.hOrElse (empty α) fun x => s✝) = s'<VAR>s : Computation α<GOAL>(HOrElse.hOrElse (empty α).think fun x => s) = HOrElse.hOrElse (empty α) fun x => s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T1Space α<VAR>s : Closeds α<VAR>t : Set α<VAR>ht : IsAtom t<GOAL>↑(Closeds.closure t) = t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T1Space α<VAR>s : Closeds α<VAR>x : α<VAR>ht : IsAtom {x}<GOAL>↑(Closeds.closure {x}) = {x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>IsPiSystem (⋃ a, {Iic ↑a})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>⋃ a, {Iic ↑a} = Iic '' (Rat.cast '' univ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>x : Set ℝ<GOAL>x ∈ ⋃ a, {Iic ↑a} ↔ x ∈ Iic '' (Rat.cast '' univ)
<VAR>J K : Type v<VAR>inst✝⁶ : SmallCategory J<VAR>inst✝⁵ : SmallCategory K<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>inst✝³ : HasColimitsOfShape J C<VAR>inst✝² : HasColimitsOfShape K C<VAR>inst✝¹ : HasColimitsOfShape (J × K) C<VAR>inst✝ : HasColimitsOfShape (K × J) C<VAR>j : J<VAR>k : K<GOAL>colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k ≫ (colimitUncurryIsoColimitCompColim F.flip).inv ≫ (HasColimit.isoOfNatIso (uncurryObjFlip F)).hom ≫ (HasColimit.isoOfEquivalence (Prod.braiding K J) (NatIso.ofComponents (fun x => Iso.refl ((F.obj x.2).obj x.1)) ⋯)).hom ≫ (colimitUncurryIsoColimitCompColim F).hom = colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j
<VAR>J K : Type v<VAR>inst✝⁶ : SmallCategory J<VAR>inst✝⁵ : SmallCategory K<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>inst✝³ : HasColimitsOfShape J C<VAR>inst✝² : HasColimitsOfShape K C<VAR>inst✝¹ : HasColimitsOfShape (J × K) C<VAR>inst✝ : HasColimitsOfShape (K × J) C<VAR>j : J<VAR>k : K<GOAL>(((colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k ≫ (colimitUncurryIsoColimitCompColim F.flip).inv) ≫ (HasColimit.isoOfNatIso (uncurryObjFlip F)).hom) ≫ (HasColimit.isoOfEquivalence (Prod.braiding K J) (NatIso.ofComponents (fun x => Iso.refl ((F.obj x.2).obj x.1)) ⋯)).hom) ≫ (colimitUncurryIsoColimitCompColim F).hom = colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j
<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∞<GOAL>(range ofNNReal).OrdConnected
<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∞<GOAL>(Iio ⊤).OrdConnected
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>x y z : α<VAR>hu : IsUnit x<GOAL>IsRelPrime (x * y) (x * z) ↔ IsRelPrime y z
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝ : AddGroup A<VAR>s : Set A<VAR>h₁ : IsSubgroup s<VAR>h₂ : ∀ n ∈ s, ∀ (g : Multiplicative A), g * n * g⁻¹ ∈ s<GOAL>IsNormalAddSubgroup s
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p q n : ℕ<VAR>hn : 0 < n<VAR>g g' : R[X]<VAR>H : (expand R n) g = (expand R n) g'<VAR>k : ℕ<GOAL>g.coeff k = g'.coeff k
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>ι : Type u_1<VAR>I J : Ideal R<VAR>coprime : IsCoprime I J<GOAL>(snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime) = factor (I ⊓ J) J ⋯
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>ι : Type u_1<VAR>I J : Ideal R<VAR>coprime : IsCoprime I J<GOAL>((snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime)).comp (Quotient.mk (I ⊓ J)) = (factor (I ⊓ J) J ⋯).comp (Quotient.mk (I ⊓ J))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : IsFiniteMeasure μ<VAR>p : α → Prop<VAR>hp : NullMeasurableSet {a | p a} μ<GOAL>(∀ᵐ (a : α) ∂μ, p a) ↔ μ {a | p a} = μ univ
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>u : κ → UniformSpace β'<VAR>F : ι → β' → α<VAR>k : κ<VAR>hk : UniformEquicontinuous F<GOAL>UniformEquicontinuous F