ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_5, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_6, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_4, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F : Sheaf J A<GOAL>((constantSheafAdj J B ht).counit.app ((sheafCompose J U).obj F)).val = ((sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.val.obj (op t)))).symm ≪≫ (presheafToSheaf J B ⋙ sheafToPresheaf J B).mapIso (constComp Cᵒᵖ (F.val.obj (op t)) U)).inv ≫ ((sheafCompose J U).map ((constantSheafAdj J A ht).counit.app F)).val
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ : Type w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>t : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : StrictMono f<VAR>hc : (range f).OrdConnected<GOAL>induced f t = Preorder.topology α
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ : Type w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>t : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : StrictMono f<VAR>hc : (range f).OrdConnected<VAR>a✝ : α<VAR>b✝ : β<VAR>x✝ : α<VAR>h₁ : b✝ < f a✝<VAR>h₂ : ¬b✝ < f x✝<GOAL>∃ y < a✝, b✝ ≤ f y
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ : Type w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>t : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : StrictMono f<VAR>hc : (range f).OrdConnected<VAR>a✝ : α<VAR>b✝ : β<VAR>x✝ : α<VAR>h₁ : f a✝ < b✝<VAR>h₂ : ¬f x✝ < b✝<GOAL>∃ y, a✝ < y ∧ f y ≤ b✝
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' F'' : C ⥤ D<VAR>G G' G'' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>adj3 : F'' ⊣ G''<VAR>f : G ⟶ G'<VAR>g : G' ⟶ G''<GOAL>(adj2.natTransEquiv adj3) g ≫ (adj1.natTransEquiv adj2) f = (adj1.natTransEquiv adj3) (f ≫ g)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' F'' : C ⥤ D<VAR>G G' G'' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>adj3 : F'' ⊣ G''<VAR>f : G ⟶ G'<VAR>g : G' ⟶ G''<GOAL>(adj1.natTransEquiv adj3).symm ((adj2.natTransEquiv adj3) g ≫ (adj1.natTransEquiv adj2) f) = (adj1.natTransEquiv adj3).symm ((adj1.natTransEquiv adj3) (f ≫ g))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' F'' : C ⥤ D<VAR>G G' G'' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>adj3 : F'' ⊣ G''<VAR>f : G ⟶ G'<VAR>g : G' ⟶ G''<VAR>X : D<GOAL>((adj1.natTransEquiv adj3).symm ((adj2.natTransEquiv adj3) g ≫ (adj1.natTransEquiv adj2) f)).app X = ((adj1.natTransEquiv adj3).symm ((adj1.natTransEquiv adj3) (f ≫ g))).app X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' F'' : C ⥤ D<VAR>G G' G'' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>adj3 : F'' ⊣ G''<VAR>f : G ⟶ G'<VAR>g : G' ⟶ G''<VAR>X : D<GOAL>adj1.unit.app (G.obj X) ≫ f.app (F.obj (G.obj X)) ≫ G'.map (adj1.counit.app X) ≫ g.app X = f.app X ≫ g.app X
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : CharP k p<GOAL>Irreducible ↑p
<VAR>p : ℕ<VAR>hp✝ : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : CharP k p<VAR>hp : ¬IsUnit ↑p<GOAL>Irreducible ↑p
<VAR>p : ℕ<VAR>hp✝ : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : CharP k p<VAR>hp : ¬IsUnit ↑p<VAR>a b : 𝕎 k<VAR>hab : ↑p = a * b<GOAL>IsUnit a ∨ IsUnit b
<VAR>p : ℕ<VAR>hp✝ : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : CharP k p<VAR>hp : ¬IsUnit ↑p<VAR>a b : 𝕎 k<VAR>hab : ↑p = a * b<VAR>ha0 : a ≠ 0<VAR>hb0 : b ≠ 0<GOAL>IsUnit a ∨ IsUnit b
<VAR>p : ℕ<VAR>hp✝ : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : CharP k p<VAR>hp : ¬IsUnit ↑p<VAR>b : 𝕎 k<VAR>hb0 : b ≠ 0<VAR>m : ℕ<VAR>a : 𝕎 k<VAR>ha : a.coeff 0 ≠ 0<VAR>hab : ↑p = (⇑verschiebung)^[m] a * b<VAR>ha0 : (⇑verschiebung)^[m] a ≠ 0<GOAL>IsUnit ((⇑verschiebung)^[m] a) ∨ IsUnit b
<VAR>p : ℕ<VAR>hp✝ : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : CharP k p<VAR>hp : ¬IsUnit ↑p<VAR>m : ℕ<VAR>a : 𝕎 k<VAR>ha : a.coeff 0 ≠ 0<VAR>ha0 : (⇑verschiebung)^[m] a ≠ 0<VAR>n : ℕ<VAR>b : 𝕎 k<VAR>hb : b.coeff 0 ≠ 0<VAR>hb0 : (⇑verschiebung)^[n] b ≠ 0<VAR>hab : ↑p = (⇑verschiebung)^[m] a * (⇑verschiebung)^[n] b<GOAL>IsUnit ((⇑verschiebung)^[m] a) ∨ IsUnit ((⇑verschiebung)^[n] b)
<VAR>p : ℕ<VAR>hp✝ : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : CharP k p<VAR>hp : ¬IsUnit ↑p<VAR>a : 𝕎 k<VAR>ha : a.coeff 0 ≠ 0<VAR>b : 𝕎 k<VAR>hb : b.coeff 0 ≠ 0<VAR>n✝ : ℕ<VAR>ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0<VAR>n : ℕ<VAR>hb0 : (⇑verschiebung)^[n + 1] b ≠ 0<VAR>hab : ↑p = (⇑verschiebung)^[n✝ + 1] a * (⇑verschiebung)^[n + 1] b<GOAL>IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n + 1] b)
<VAR>p : ℕ<VAR>hp✝ : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : CharP k p<VAR>hp : ¬IsUnit ↑p<VAR>a : 𝕎 k<VAR>ha : a.coeff 0 ≠ 0<VAR>b : 𝕎 k<VAR>hb : b.coeff 0 ≠ 0<VAR>n✝ : ℕ<VAR>ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0<VAR>n : ℕ<VAR>hb0 : (⇑verschiebung)^[n + 1] b ≠ 0<VAR>hab : ↑p = (⇑verschiebung)^[n✝ + 1 + (n + 1)] ((⇑frobenius)^[n + 1] a * (⇑frobenius)^[n✝ + 1] b)<GOAL>IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n + 1] b)
<VAR>p : ℕ<VAR>hp✝ : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : CharP k p<VAR>hp : ¬IsUnit ↑p<VAR>a : 𝕎 k<VAR>ha : a.coeff 0 ≠ 0<VAR>b : 𝕎 k<VAR>hb : b.coeff 0 ≠ 0<VAR>n✝ : ℕ<VAR>ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0<VAR>n : ℕ<VAR>hb0 : (⇑verschiebung)^[n + 1] b ≠ 0<VAR>hab : (↑p).coeff 1 = ((⇑verschiebung)^[n✝ + 1 + (n + 1)] ((⇑frobenius)^[n + 1] a * (⇑frobenius)^[n✝ + 1] b)).coeff 1<GOAL>IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n + 1] b)
<VAR>p : ℕ<VAR>hp✝ : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : Field k<VAR>inst✝ : CharP k p<VAR>hp : ¬IsUnit ↑p<VAR>a : 𝕎 k<VAR>ha : a.coeff 0 ≠ 0<VAR>b : 𝕎 k<VAR>hb : b.coeff 0 ≠ 0<VAR>n✝ : ℕ<VAR>ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0<VAR>n : ℕ<VAR>hb0 : (⇑verschiebung)^[n + 1] b ≠ 0<VAR>hab : 1 = 0<GOAL>IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n + 1] b)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedAddCommGroup F<VAR>a : ℝ<GOAL>¬IntegrableOn (fun x => x⁻¹) (Ioi a) volume
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>h : a ≠ b<GOAL>∏ᶠ (i : α) (_ : i ∈ {a, b}), f i = f a * f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>h : a ≠ b<GOAL>a ∉ {b}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>h : a ≠ b<GOAL>{b}.Finite
<VAR>a b m n✝¹ p n n✝ : ℕ<VAR>hk : n✝ + 1 ≠ 0<GOAL>(n ^ (n✝ + 1)).primeFactors = n.primeFactors
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>inst✝ : Setoid α<VAR>r : α → α → Prop<VAR>H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂<GOAL>∀ {a b : Quotient inst✝}, r ((Embedding.quotientOut α) a) ((Embedding.quotientOut α) b) ↔ Quotient.lift₂ r H a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>inst✝ : Setoid α<VAR>r : α → α → Prop<VAR>H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂<VAR>x y : Quotient inst✝<VAR>a b : α<GOAL>r ((Embedding.quotientOut α) ⟦a⟧) ((Embedding.quotientOut α) ⟦b⟧) ↔ Quotient.lift₂ r H ⟦a⟧ ⟦b⟧
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝ : IsRefl β s<VAR>f : r ≃r s<GOAL>Cardinal.lift.{max u v, u} (cof r) ≤ Cardinal.lift.{max u v, v} (cof s)
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝ : IsRefl β s<VAR>f : r ≃r s<GOAL>∀ b ∈ Cardinal.lift.{max u v, v} '' {c | ∃ S, (∀ (a : β), ∃ b ∈ S, s a b) ∧ #↑S = c}, sInf (Cardinal.lift.{max u v, u} '' {c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = c}) ≤ b
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝ : IsRefl β s<VAR>f : r ≃r s<VAR>u : Set β<VAR>H : ∀ (a : β), ∃ b ∈ u, s a b<GOAL>sInf (Cardinal.lift.{max u v, u} '' {c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = c}) ≤ Cardinal.lift.{max u v, v} #↑u
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝ : IsRefl β s<VAR>f : r ≃r s<VAR>u : Set β<VAR>H : ∀ (a : β), ∃ b ∈ u, s a b<GOAL>Cardinal.lift.{max u v, v} #↑u ∈ Cardinal.lift.{max u v, u} '' {c | ∃ S, (∀ (a : α), ∃ b ∈ S, r a b) ∧ #↑S = c}
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝ : IsRefl β s<VAR>f : r ≃r s<VAR>u : Set β<VAR>H : ∀ (a : β), ∃ b ∈ u, s a b<VAR>a : α<GOAL>∃ b ∈ ⇑f.symm '' u, r a b
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝ : IsRefl β s<VAR>f : r ≃r s<VAR>u : Set β<VAR>H : ∀ (a : β), ∃ b ∈ u, s a b<VAR>a : α<VAR>b : β<VAR>hb : b ∈ u<VAR>hb' : s (f a) b<GOAL>∃ b ∈ ⇑f.symm '' u, r a b
<VAR>α✝ : Type u_1<VAR>r✝ : α✝ → α✝ → Prop<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝ : IsRefl β s<VAR>f : r ≃r s<VAR>u : Set β<VAR>H : ∀ (a : β), ∃ b ∈ u, s a b<VAR>a : α<VAR>b : β<VAR>hb : b ∈ u<VAR>hb' : s (f a) b<GOAL>s (f a) (f (f.symm b))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>hI : a₂ ≤ b₂<VAR>ha : a₂ < a₁<VAR>hb : b₁ ≤ b₂<GOAL>Icc a₁ b₁ ⊂ Icc a₂ b₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>hI : a₂ ≤ b₂<VAR>ha : a₂ < a₁<VAR>hb : b₁ ≤ b₂<GOAL>Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂
<VAR>x✝ y x : ℝ<GOAL>√(x ^ 2) = |x|
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ : MvPolynomial σ R<GOAL>↑φ = 0 ↔ φ = 0
<VAR>n m : ℕ<GOAL>Pairwise (fun x x_1 => x < x_1) (range' n (m - n))
<VAR>k : Type u<VAR>inst✝ : CommRing k<VAR>G : Grp<VAR>X Y : Rep k ↑G<VAR>f : ↑X.V →ₗ[k] ↑Y.V<VAR>g : ↑G<GOAL>Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f ↔ f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f
<VAR>k : Type u<VAR>inst✝ : CommRing k<VAR>G : Grp<VAR>X Y : Rep k ↑G<VAR>f : ↑X.V →ₗ[k] ↑Y.V<VAR>g : ↑G<GOAL>Y.ρ g ∘ₗ f ∘ₗ ((ρAut X) g).inv = f ↔ f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f
<VAR>k : Type u<VAR>inst✝ : CommRing k<VAR>G : Grp<VAR>X Y : Rep k ↑G<VAR>f : ↑X.V →ₗ[k] ↑Y.V<VAR>g : ↑G<GOAL>f ≫ Y.ρ g = X.ρ g ≫ f ↔ f ∘ₗ X.ρ g = f ≫ Y.ρ g
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>g : G →₀ k<VAR>f : Fin n → G<VAR>r : k<GOAL>(diagonalSucc k G n).inv.hom (g ⊗ₜ[k] single f r) = ((Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => single (a • partialProd f) r) g
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>g : G →₀ k<VAR>f : Fin n → G<VAR>r : k<GOAL>(diagonalSucc k G n).inv.hom (0 ⊗ₜ[k] single f r) = ((Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => single (a • partialProd f) r) 0
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>g : G →₀ k<VAR>f : Fin n → G<VAR>r : k<GOAL>∀ (a : G) (b : k) (f_1 : G →₀ k), a ∉ f_1.support → b ≠ 0 → (diagonalSucc k G n).inv.hom (f_1 ⊗ₜ[k] single f r) = ((Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => single (a • partialProd f) r) f_1 → (diagonalSucc k G n).inv.hom ((single a b + f_1) ⊗ₜ[k] single f r) = ((Finsupp.lift ((Fin (n + 1) → G) →₀ k) k G) fun a => single (a • partialProd f) r) (single a b + f_1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>x✝² : NonAssocSemiring α<VAR>x✝¹ : NonAssocSemiring β<VAR>f : α →+* β<VAR>x✝ y : α<VAR>h : f 1 = 0<VAR>x : α<GOAL>f x = 0
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S✝ : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>S : Subgroupoid C<VAR>T : Subgroupoid D<GOAL>map φ hφ S ≤ T ↔ S ≤ comap φ T
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S✝ : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>S : Subgroupoid C<VAR>T : Subgroupoid D<GOAL>(∀ {c d : D}, (map φ hφ S).arrows c d ⊆ T.arrows c d) ↔ ∀ {c d : C}, S.arrows c d ⊆ (comap φ T).arrows c d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>u : γ → δ<VAR>h : IdentDistrib f g μ ν<VAR>hu : AEMeasurable u (Measure.map f μ)<GOAL>AEMeasurable (u ∘ g) ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>u : γ → δ<VAR>h : IdentDistrib f g μ ν<VAR>hu : AEMeasurable u (Measure.map g ν)<GOAL>AEMeasurable (u ∘ g) ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>u : γ → δ<VAR>h : IdentDistrib f g μ ν<VAR>hu : AEMeasurable u (Measure.map f μ)<GOAL>Measure.map (u ∘ f) μ = Measure.map (u ∘ g) ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>u : γ → δ<VAR>h : IdentDistrib f g μ ν<VAR>hu : AEMeasurable u (Measure.map f μ)<GOAL>AEMeasurable u (Measure.map g ν)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s s' : Set R<GOAL>zeroLocus s ∪ zeroLocus s' = zeroLocus ↑(Ideal.span s ⊓ Ideal.span s')
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s s' : Set R<GOAL>zeroLocus s ∪ zeroLocus s' = zeroLocus ↑(Ideal.span s) ∪ zeroLocus ↑(Ideal.span s')
<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✝¹⁶ : CommRing T<VAR>inst✝¹⁵ : Algebra R S<VAR>inst✝¹⁴ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹⁰ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Algebra R L<VAR>inst✝⁷ : Algebra L F<VAR>inst✝⁶ : Algebra R F<VAR>inst✝⁵ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra A C<VAR>b : Basis ι A B<VAR>z : B<VAR>i : ι<GOAL>(traceMatrix A ⇑b *ᵥ b.equivFun z) i = (trace A B) (z * b i)
<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✝¹⁶ : CommRing T<VAR>inst✝¹⁵ : Algebra R S<VAR>inst✝¹⁴ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹⁰ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Algebra R L<VAR>inst✝⁷ : Algebra L F<VAR>inst✝⁶ : Algebra R F<VAR>inst✝⁵ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra A C<VAR>b : Basis ι A B<VAR>z : B<VAR>i : ι<GOAL>∑ j : ι, of (fun i j => ((traceForm A B) (b i)) (b j)) i j * col (Fin 1) (b.equivFun z) j 0 = (trace A B) (z * b i)
<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✝¹⁶ : CommRing T<VAR>inst✝¹⁵ : Algebra R S<VAR>inst✝¹⁴ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹⁰ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Algebra R L<VAR>inst✝⁷ : Algebra L F<VAR>inst✝⁶ : Algebra R F<VAR>inst✝⁵ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra A C<VAR>b : Basis ι A B<VAR>z : B<VAR>i : ι<GOAL>∑ x : ι, of (fun i j => (trace A B) (b i * b j)) i x * b.equivFun z x = (trace A B) (z * b i)
<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✝¹⁶ : CommRing T<VAR>inst✝¹⁵ : Algebra R S<VAR>inst✝¹⁴ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹⁰ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Algebra R L<VAR>inst✝⁷ : Algebra L F<VAR>inst✝⁶ : Algebra R F<VAR>inst✝⁵ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra A C<VAR>b : Basis ι A B<VAR>z : B<VAR>i : ι<GOAL>∑ x : ι, (trace A B) (b.equivFun z x • (b i * b x)) = (trace A B) (z * b i)
<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✝¹⁶ : CommRing T<VAR>inst✝¹⁵ : Algebra R S<VAR>inst✝¹⁴ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹⁰ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Algebra R L<VAR>inst✝⁷ : Algebra L F<VAR>inst✝⁶ : Algebra R F<VAR>inst✝⁵ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra A C<VAR>b : Basis ι A B<VAR>z : B<VAR>i : ι<GOAL>(trace A B) (∑ x : ι, b.equivFun z x • (b i * b x)) = (trace A B) (z * b i)
<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✝¹⁶ : CommRing T<VAR>inst✝¹⁵ : Algebra R S<VAR>inst✝¹⁴ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹⁰ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Algebra R L<VAR>inst✝⁷ : Algebra L F<VAR>inst✝⁶ : Algebra R F<VAR>inst✝⁵ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra A C<VAR>b : Basis ι A B<VAR>z : B<VAR>i : ι<GOAL>∑ x : ι, b.equivFun z x • (b i * b x) = z * b i
<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✝¹⁶ : CommRing T<VAR>inst✝¹⁵ : Algebra R S<VAR>inst✝¹⁴ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹⁰ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Algebra R L<VAR>inst✝⁷ : Algebra L F<VAR>inst✝⁶ : Algebra R F<VAR>inst✝⁵ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra A C<VAR>b : Basis ι A B<VAR>z : B<VAR>i : ι<GOAL>∑ x : ι, b i * b.equivFun z x • b x = z * b i
<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✝¹⁶ : CommRing T<VAR>inst✝¹⁵ : Algebra R S<VAR>inst✝¹⁴ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹⁰ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Algebra R L<VAR>inst✝⁷ : Algebra L F<VAR>inst✝⁶ : Algebra R F<VAR>inst✝⁵ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra A C<VAR>b : Basis ι A B<VAR>z : B<VAR>i : ι<GOAL>b i * ∑ i : ι, b.equivFun z i • b i = b i * z
<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✝¹⁶ : CommRing T<VAR>inst✝¹⁵ : Algebra R S<VAR>inst✝¹⁴ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹⁰ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Algebra R L<VAR>inst✝⁷ : Algebra L F<VAR>inst✝⁶ : Algebra R F<VAR>inst✝⁵ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : CommRing C<VAR>inst✝ : Algebra A C<VAR>b : Basis ι A B<VAR>z : B<VAR>i : ι<GOAL>∑ i : ι, b.equivFun z i • b i = z
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝¹¹ : Fact (1 ≤ p)<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : Semiring 𝕜<VAR>inst✝⁸ : (i : ι) → SeminormedAddCommGroup (α i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>inst✝⁶ : (i : ι) → Module 𝕜 (α i)<VAR>inst✝⁵ : (i : ι) → Module 𝕜 (β i)<VAR>c : 𝕜<VAR>ι' : Type u_5<VAR>inst✝⁴ : Fintype ι'<VAR>E : Type u_6<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq ι'<VAR>e : ι ≃ ι'<VAR>i : ι<VAR>v : E<GOAL>(LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) ((WithLp.equiv p (ι → E)).symm (Pi.single i v)) = (WithLp.equiv p (ι' → E)).symm (Pi.single (e i) v)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝¹¹ : Fact (1 ≤ p)<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : Semiring 𝕜<VAR>inst✝⁸ : (i : ι) → SeminormedAddCommGroup (α i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>inst✝⁶ : (i : ι) → Module 𝕜 (α i)<VAR>inst✝⁵ : (i : ι) → Module 𝕜 (β i)<VAR>c : 𝕜<VAR>ι' : Type u_5<VAR>inst✝⁴ : Fintype ι'<VAR>E : Type u_6<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq ι'<VAR>e : ι ≃ ι'<VAR>i : ι<VAR>v : E<VAR>x : ι'<GOAL>(LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) ((WithLp.equiv p (ι → E)).symm (Pi.single i v)) x = (WithLp.equiv p (ι' → E)).symm (Pi.single (e i) v) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>x : E<GOAL>gauge (-s) (-x) = gauge s x
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s t r : Set α<VAR>h : Disjoint s t<GOAL>↑(Sum.inr ⁻¹' (⇑(sumSet h) ⁻¹' r)) = r ∩ t
<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>hp₁ : p ≤ 1<GOAL>ConcaveOn ℝ (Ici 0) fun x => x ^ p
<VAR>hp₀ : 0 ≤ 0<VAR>hp₁ : 0 ≤ 1<GOAL>ConcaveOn ℝ (Ici 0) fun x => x ^ 0
<VAR>p : ℝ<VAR>hp₀✝ : 0 ≤ p<VAR>hp₁ : p ≤ 1<VAR>hp₀ : 0 < p<GOAL>ConcaveOn ℝ (Ici 0) fun x => x ^ p
<VAR>hp₀✝ : 0 ≤ 1<VAR>hp₁ : 1 ≤ 1<VAR>hp₀ : 0 < 1<GOAL>ConcaveOn ℝ (Ici 0) fun x => x ^ 1
<VAR>p : ℝ<VAR>hp₀✝ : 0 ≤ p<VAR>hp₁✝ : p ≤ 1<VAR>hp₀ : 0 < p<VAR>hp₁ : p < 1<GOAL>ConcaveOn ℝ (Ici 0) fun x => x ^ p