ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>y : PrimeSpectrum ↑Γ(X, U)<VAR>hy : hU.fromSpec.val.base y ∈ U<GOAL>(Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.germ ((fun x => ⟨↑x, ⋯⟩) ⟨y, hy⟩) = StructureSheaf.toStalk (↑Γ(X, U)) y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NonUnitalCommRing α<VAR>a✝ b✝ c k a b x y : α<VAR>hab : k ∣ a - b<VAR>hxy : k ∣ x - y<GOAL>k ∣ a * x - b * y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NonUnitalCommRing α<VAR>a✝ b✝ c k a b x y : α<VAR>hab : k ∣ a - b<VAR>hxy : k ∣ x - y<GOAL>a * x - b * y = a * (x - y) + (a - b) * y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NonUnitalCommRing α<VAR>a✝ b✝ c k a b x y : α<VAR>hab : k ∣ a - b<VAR>hxy : k ∣ x - y<GOAL>a * x - b * y = a * x - a * y + (a * y - b * y)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a : X ⟶ Y<GOAL>a - 0 = a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a : X ⟶ Y<GOAL>prod.lift a 0 ≫ σ = a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a : X ⟶ Y<GOAL>prod.lift (a ≫ 𝟙 Y) (a ≫ 0) ≫ σ = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x✝ : α<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x : Set α<VAR>y : Set β<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>hy : y ⊆ f '' x<GOAL>x ∩ f ⁻¹' minimals s y = minimals r (x ∩ f ⁻¹' y)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>x y z : α<GOAL>x ∈ s.ordConnectedComponent x ↔ x ∈ s
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>proj : Z → B<VAR>e : Pretrivialization F proj<VAR>x : Z<VAR>inst✝ : Nonempty F<GOAL>Injective toPartialEquiv
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>proj : Z → B<VAR>e✝ : Pretrivialization F proj<VAR>x : Z<VAR>inst✝ : Nonempty F<VAR>e e' : Pretrivialization F proj<VAR>h : e.toPartialEquiv = e'.toPartialEquiv<GOAL>e.baseSet = e'.baseSet
<VAR>X : RelCat<VAR>x y : X<GOAL>𝟙 X x y ↔ x = y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↥(pbo f)<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x = RingHom.comp ((specStalkEquiv 𝒜 f x f_deg hm).hom ≫ (Proj.stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv) (algebraMap (A⁰_ f) ↑((Spec.structureSheaf (A⁰_ f)).presheaf.stalk ((toSpec 𝒜 f).val.base x)))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↥(pbo f)<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>StructureSheaf.toStalk (A⁰_ f) ((toSpec 𝒜 f).val.base x) ≫ (specStalkEquiv 𝒜 f x ?f_deg ?hm).hom ≫ (Proj.stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv = RingHom.comp ((specStalkEquiv 𝒜 f x f_deg hm).hom ≫ (Proj.stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv) (algebraMap (A⁰_ f) ↑((Spec.structureSheaf (A⁰_ f)).presheaf.stalk ((toSpec 𝒜 f).val.base x)))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↥(pbo f)<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>ℕ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↥(pbo f)<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>f ∈ 𝒜 ?m
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↥(pbo f)<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>0 < ?m
<VAR>m : ℕ∞<VAR>hm : m ≠ 0<GOAL>↑m * ℵ₀ = ℵ₀
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<GOAL>Nat.card ↥(Stab w) = 1 ∨ Nat.card ↥(Stab w) = 2
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<GOAL>Nat.card ↑↑(Stab (mk w.embedding)) = 1 ∨ Nat.card ↑↑(Stab (mk w.embedding)) = 2
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ n<VAR>α a : K<VAR>hn : 0 < n<VAR>e : α ^ n = a<GOAL>X ^ n - C a = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ n<VAR>α a : K<VAR>hn : 0 < n<VAR>e : α ^ n = a<GOAL>(Multiset.map ((fun a => X - C a) ∘ fun x => ζ ^ x * α) (Multiset.range n)).prod = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>M : ModuleCat R<VAR>inst✝ : Flat R ↑M<VAR>C : ShortComplex (ModuleCat R)<VAR>hC : C.Exact<GOAL>(C.map (tensorLeft M)).Exact
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>M : ModuleCat R<VAR>inst✝ : Flat R ↑M<VAR>C : ShortComplex (ModuleCat R)<VAR>hC : Function.Exact ⇑C.f ⇑C.g<GOAL>Function.Exact ⇑(C.map (tensorLeft M)).f ⇑(C.map (tensorLeft M)).g
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝² : Monoid γ<VAR>inst✝¹ : (i : ι) → AddMonoid (β i)<VAR>inst✝ : (i : ι) → DistribMulAction γ (β i)<VAR>h : κ → ι<VAR>h' : ι → κ<VAR>hh' : Function.LeftInverse h' h<VAR>r : γ<VAR>f : Π₀ (i : ι), β i<VAR>i✝ : κ<GOAL>(comapDomain' h hh' (r • f)) i✝ = (r • comapDomain' h hh' f) i✝
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → β<VAR>ι : Sort u_2<VAR>t₁ t₂ : TopologicalSpace α<VAR>t₃ : TopologicalSpace β<GOAL>Continuous f ↔ Continuous f ∧ Continuous f
<VAR>n p : ℕ<VAR>p2 : 2 ≤ p<VAR>a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p<VAR>this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k<VAR>m : ℕ<VAR>m2 : 2 ≤ m<VAR>l : m < p<VAR>x✝ : m ∣ p<VAR>k : ℕ<VAR>e : p = m * k<GOAL>False
<VAR>n p : ℕ<VAR>p2 : 2 ≤ p<VAR>a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p<VAR>this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k<VAR>m : ℕ<VAR>m2 : 2 ≤ m<VAR>l : m < p<VAR>x✝ : m ∣ p<VAR>k : ℕ<VAR>e : p = m * k<VAR>mk : m ≤ k<GOAL>False
<VAR>n p : ℕ<VAR>p2 : 2 ≤ p<VAR>a : ∀ (m : ℕ), 2 ≤ m → m ≤ p.sqrt → ¬m ∣ p<VAR>this : ∀ {m k : ℕ}, m ≤ k → 1 < m → p ≠ m * k<VAR>m : ℕ<VAR>m2 : 2 ≤ m<VAR>l : m < p<VAR>x✝ : m ∣ p<VAR>k : ℕ<VAR>e : p = m * k<VAR>km : k ≤ m<GOAL>False
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s : Set α<VAR>hs : (inducedOuterMeasure m P0 m0) s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ t, P t ∧ s ⊆ t ∧ (inducedOuterMeasure m P0 m0) t ≤ (inducedOuterMeasure m P0 m0) s + ε
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s : Set α<VAR>hs : (inducedOuterMeasure m P0 m0) s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>h : (inducedOuterMeasure m P0 m0) s < (inducedOuterMeasure m P0 m0) s + ε<GOAL>∃ t, P t ∧ s ⊆ t ∧ (inducedOuterMeasure m P0 m0) t ≤ (inducedOuterMeasure m P0 m0) s + ε
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s : Set α<VAR>hs : (inducedOuterMeasure m P0 m0) s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>h : ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht < (inducedOuterMeasure m P0 m0) s + ε<GOAL>∃ t, P t ∧ s ⊆ t ∧ (inducedOuterMeasure m P0 m0) t ≤ (inducedOuterMeasure m P0 m0) s + ε
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s : Set α<VAR>hs : (inducedOuterMeasure m P0 m0) s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>h : ∃ i, ∃ (h : P i) (_ : s ⊆ i), m i ⋯ < (inducedOuterMeasure m P0 m0) s + ε<GOAL>∃ t, P t ∧ s ⊆ t ∧ (inducedOuterMeasure m P0 m0) t ≤ (inducedOuterMeasure m P0 m0) s + ε
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>s : Set α<VAR>hs : (inducedOuterMeasure m P0 m0) s ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>t : Set α<VAR>h1t : P t<VAR>h2t : s ⊆ t<VAR>h3t : m t ⋯ < (inducedOuterMeasure m P0 m0) s + ε<GOAL>∃ t, P t ∧ s ⊆ t ∧ (inducedOuterMeasure m P0 m0) t ≤ (inducedOuterMeasure m P0 m0) s + ε
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>inst✝ : LinearOrderedSemiring α<VAR>H₁ H₂ : FloorSemiring α<GOAL>H₁ = H₂
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>inst✝ : LinearOrderedSemiring α<VAR>H₁ H₂ : FloorSemiring α<VAR>this : FloorSemiring.ceil = FloorSemiring.ceil<GOAL>H₁ = H₂
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x y : R<GOAL>star x < y ↔ x < star y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>|⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)| ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>|⟪x, y⟫_ℝ| / (‖x‖ * ‖y‖) ≤ 1
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>C : P.W α → Prop<VAR>ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α), (∀ (i : P.last.B a), C (f i)) → C (P.wMk a f' f)<VAR>a : P.wp.A<VAR>f : P.wp.B a ⟹ α<GOAL>C ⟨a, f⟩
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>C : P.W α → Prop<VAR>ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α), (∀ (i : P.last.B a), C (f i)) → C (P.wMk a f' f)<VAR>a : P.wp.A<VAR>f : P.wp.B a ⟹ α<GOAL>∀ (a : P.A) (f : P.last.B a → P.last.W) (f' : P.WPath (WType.mk a f) ⟹ α), (∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩) → C ⟨WType.mk a f, f'⟩
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>C : P.W α → Prop<VAR>ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α), (∀ (i : P.last.B a), C (f i)) → C ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn f' fun i => (f i).snd⟩<VAR>a✝ : P.wp.A<VAR>f✝ : P.wp.B a✝ ⟹ α<VAR>a : P.A<VAR>f : P.last.B a → P.last.W<VAR>f' : P.WPath (WType.mk a f) ⟹ α<VAR>ih' : ∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩<VAR>ih'' : (∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩) → C ⟨WType.mk a fun i => f i, P.wPathCasesOn (P.wPathDestLeft f') fun i => P.wPathDestRight f' i⟩ := ih a (P.wPathDestLeft f') fun i => ⟨f i, P.wPathDestRight f' i⟩<GOAL>C ⟨WType.mk a f, f'⟩
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>C : P.W α → Prop<VAR>ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α), (∀ (i : P.last.B a), C (f i)) → C ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn f' fun i => (f i).snd⟩<VAR>a✝ : P.wp.A<VAR>f✝ : P.wp.B a✝ ⟹ α<VAR>a : P.A<VAR>f : P.last.B a → P.last.W<VAR>f' : P.WPath (WType.mk a f) ⟹ α<VAR>ih' : ∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩<VAR>ih'' : (∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩) → C ⟨WType.mk a fun i => f i, f'⟩<GOAL>C ⟨WType.mk a f, f'⟩
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : Module.Free R M<VAR>inst✝² : Module.Finite R M<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Module.Finite R L<VAR>I : LieIdeal R L<VAR>x : L<GOAL>x ∈ killingCompl R L I ↔ ∀ y ∈ I, ((killingForm R L) y) x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>h : ⋃₀ 𝔖 = univ<GOAL>UniformContinuous ⇑(toFun 𝔖)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>h : ⋃₀ 𝔖 = univ<GOAL>∀ (i : α), UniformContinuous fun x => (toFun 𝔖) x i
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝⁴ : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>inst✝² : HasProducts A<VAR>inst✝¹ : HasProducts A'<VAR>inst✝ : HasPullbacks C<GOAL>forkMap R P ≫ firstMap R P = forkMap R P ≫ secondMap R P
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝⁴ : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>inst✝² : HasProducts A<VAR>inst✝¹ : HasProducts A'<VAR>inst✝ : HasPullbacks C<GOAL>∀ (j : Discrete (((V : C) × { f // R f }) × (W : C) × { g // R g })), (forkMap R P ≫ firstMap R P) ≫ limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j = (forkMap R P ≫ secondMap R P) ≫ limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝⁴ : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>inst✝² : HasProducts A<VAR>inst✝¹ : HasProducts A'<VAR>inst✝ : HasPullbacks C<VAR>Y : C<VAR>f : Y ⟶ U<VAR>hf : R f<VAR>Z : C<VAR>g : Z ⟶ U<VAR>hg : R g<GOAL>(forkMap R P ≫ firstMap R P) ≫ limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) } = (forkMap R P ≫ secondMap R P) ≫ limit.π (Discrete.functor fun fg => P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) { as := (⟨Y, ⟨f, hf⟩⟩, ⟨Z, ⟨g, hg⟩⟩) }
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝⁴ : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>inst✝² : HasProducts A<VAR>inst✝¹ : HasProducts A'<VAR>inst✝ : HasPullbacks C<VAR>Y : C<VAR>f : Y ⟶ U<VAR>hf : R f<VAR>Z : C<VAR>g : Z ⟶ U<VAR>hg : R g<GOAL>P.map f.op ≫ P.map (pullback.fst f g).op = P.map g.op ≫ P.map (pullback.snd f g).op
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝⁴ : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>inst✝² : HasProducts A<VAR>inst✝¹ : HasProducts A'<VAR>inst✝ : HasPullbacks C<VAR>Y : C<VAR>f : Y ⟶ U<VAR>hf : R f<VAR>Z : C<VAR>g : Z ⟶ U<VAR>hg : R g<GOAL>P.map (pullback.snd f g ≫ g).op = P.map g.op ≫ P.map (pullback.snd f g).op
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x✝ : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>inst✝ : Fintype ι<VAR>i : ι<VAR>m : β i<VAR>x : ι<GOAL>(single i m) x = if h : x = i then ⋯ ▸ m else 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝¹⁸ : SeminormedRing 𝕜<VAR>inst✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>x : E<GOAL>∃ i ∈ s, (s.sup p) x = (p i) x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝¹⁸ : SeminormedRing 𝕜<VAR>inst✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>x : E<VAR>i : ι<VAR>hi : i ∈ s<VAR>hix : (s.sup fun i => ⟨(p i) x, ⋯⟩) = ⟨(p i) x, ⋯⟩<GOAL>∃ i ∈ s, (s.sup p) x = (p i) x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝¹⁸ : SeminormedRing 𝕜<VAR>inst✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>x : E<VAR>i : ι<VAR>hi : i ∈ s<VAR>hix : (s.sup fun i => ⟨(p i) x, ⋯⟩) = ⟨(p i) x, ⋯⟩<GOAL>∃ i ∈ s, ↑(s.sup fun i => ⟨(p i) x, ⋯⟩) = (p i) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b a : α<VAR>s : Multiset α<GOAL>fold op b (a ::ₘ s) = fold op (op a b) s
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field L'<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K L'<VAR>S F E✝ E'✝ : IntermediateField K L<VAR>h : F ≤ E✝<VAR>h' : F ≤ E'✝<VAR>x : L<VAR>E E' : { E // F ≤ E }<GOAL>{ toFun := fun E => extendScalars ⋯, invFun := fun E => ⟨restrictScalars K E, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } E ≤ { toFun := fun E => extendScalars ⋯, invFun := fun E => ⟨restrictScalars K E, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } E' ↔ E ≤ E'
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field L'<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K L'<VAR>S F E✝ E'✝ : IntermediateField K L<VAR>h : F ≤ E✝<VAR>h' : F ≤ E'✝<VAR>x : L<VAR>E E' : { E // F ≤ E }<GOAL>extendScalars ⋯ ≤ extendScalars ⋯ ↔ E ≤ E'
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝²³ : Semiring R₁<VAR>inst✝²² : Semiring R₂<VAR>inst✝²¹ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M₁<VAR>inst✝¹⁹ : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹⁸ : TopologicalSpace M'₁<VAR>inst✝¹⁷ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace M₂<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝¹⁴ : TopologicalSpace M₃<VAR>inst✝¹³ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝¹² : TopologicalSpace M₄<VAR>inst✝¹¹ : AddCommMonoid M₄<VAR>inst✝¹⁰ : Module R₁ M₁<VAR>inst✝⁹ : Module R₁ M'₁<VAR>inst✝⁸ : Module R₂ M₂<VAR>inst✝⁷ : Module R₃ M₃<VAR>inst✝⁶ : RingHomSurjective σ₁₂<VAR>inst✝⁵ : TopologicalSpace R₁<VAR>inst✝⁴ : TopologicalSpace R₂<VAR>inst✝³ : ContinuousSMul R₁ M₁<VAR>inst✝² : ContinuousAdd M₁<VAR>inst✝¹ : ContinuousSMul R₂ M₂<VAR>inst✝ : ContinuousAdd M₂<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>hf' : DenseRange ⇑f<VAR>s : Submodule R₁ M₁<VAR>hs : s.topologicalClosure = ⊤<GOAL>(Submodule.map (↑f) s).topologicalClosure = ⊤
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝²³ : Semiring R₁<VAR>inst✝²² : Semiring R₂<VAR>inst✝²¹ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M₁<VAR>inst✝¹⁹ : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹⁸ : TopologicalSpace M'₁<VAR>inst✝¹⁷ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace M₂<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝¹⁴ : TopologicalSpace M₃<VAR>inst✝¹³ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝¹² : TopologicalSpace M₄<VAR>inst✝¹¹ : AddCommMonoid M₄<VAR>inst✝¹⁰ : Module R₁ M₁<VAR>inst✝⁹ : Module R₁ M'₁<VAR>inst✝⁸ : Module R₂ M₂<VAR>inst✝⁷ : Module R₃ M₃<VAR>inst✝⁶ : RingHomSurjective σ₁₂<VAR>inst✝⁵ : TopologicalSpace R₁<VAR>inst✝⁴ : TopologicalSpace R₂<VAR>inst✝³ : ContinuousSMul R₁ M₁<VAR>inst✝² : ContinuousAdd M₁<VAR>inst✝¹ : ContinuousSMul R₂ M₂<VAR>inst✝ : ContinuousAdd M₂<VAR>f : M₁ →SL[σ₁₂] M₂<VAR>hf' : DenseRange ⇑f<VAR>s : Submodule R₁ M₁<VAR>hs : ↑s.topologicalClosure = ↑⊤<GOAL>↑(Submodule.map (↑f) s).topologicalClosure = ↑⊤