ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<GOAL>ContinuousOn f s ↔ ∀ (t : Set β), IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>this : ∀ (t : Set β), IsClosed (s.restrict f ⁻¹' t) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s<GOAL>ContinuousOn f s ↔ ∀ (t : Set β), IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s : Set α<VAR>this : ∀ (t : Set β), IsClosed (s.restrict f ⁻¹' t) ↔ ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s<GOAL>(∀ (s_1 : Set β), IsClosed s_1 → IsClosed (s.restrict f ⁻¹' s_1)) ↔ ∀ (t : Set β), IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>f g : ↥(simpleFunc E 1 μ)<GOAL>setToL1S T (f - g) = setToL1S T f - setToL1S T g
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocRing α<VAR>inst✝ : Fintype n<VAR>v : n → α<VAR>A : Matrix m n α<VAR>x✝ : m<GOAL>(-A *ᵥ v) x✝ = (-(A *ᵥ v)) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s✝ : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a✝ : α<VAR>s : Set β<VAR>t : Set γ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>a : α<VAR>u : Set (β × γ)<VAR>hu : MeasurableSet u<GOAL>((κ.restrict hs ⊗ₖ η.restrict ht) a) u = (((κ ⊗ₖ η).restrict ⋯) a) u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s✝ : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a✝ : α<VAR>s : Set β<VAR>t : Set γ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>a : α<VAR>u : Set (β × γ)<VAR>hu : MeasurableSet u<GOAL>∫⁻ (b : β), ((η.restrict ht) (a, b)) {c | (b, c) ∈ u} ∂(κ.restrict hs) a = ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ u ∩ s ×ˢ t} ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s✝ : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a✝ : α<VAR>s : Set β<VAR>t : Set γ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>a : α<VAR>u : Set (β × γ)<VAR>hu : MeasurableSet u<GOAL>∫⁻ (b : β) in s, (η (a, b)) ({c | (b, c) ∈ u} ∩ t) ∂κ a = ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s✝ : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a✝ : α<VAR>s : Set β<VAR>t : Set γ<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>a : α<VAR>u : Set (β × γ)<VAR>hu : MeasurableSet u<VAR>this : ∀ (b : β), (η (a, b)) {c | (b, c) ∈ u ∧ b ∈ s ∧ c ∈ t} = s.indicator (fun b => (η (a, b)) ({c | (b, c) ∈ u} ∩ t)) b<GOAL>∫⁻ (b : β) in s, (η (a, b)) ({c | (b, c) ∈ u} ∩ t) ∂κ a = ∫⁻ (b : β), s.indicator (fun b => (η (a, b)) ({c | (b, c) ∈ u} ∩ t)) b ∂κ a
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : Semiring R<VAR>P : R[X]<VAR>n : ℕ<VAR>hnil : IsNilpotent r<GOAL>IsNilpotent (C r)
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : Semiring R<VAR>P : R[X]<VAR>n m : ℕ<VAR>hm : r ^ m = 0<GOAL>C r ^ m = 0
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>f : R[X]<GOAL>Algebra.adjoin R {root f} = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>f : R[X]<VAR>x : AdjoinRoot f<GOAL>x ∈ Algebra.adjoin R {root f}
<VAR>p : ℕ<VAR>hp : 1 < p<GOAL>padicNorm p ↑p = (↑p)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>μ' : Measure α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>hμ'_le : μ' ≤ c • μ<VAR>f : α → β<VAR>hf : Integrable f μ<GOAL>Integrable f μ'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>μ' : Measure α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>hμ'_le : μ' ≤ c • μ<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<GOAL>Memℒp f 1 μ'
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<GOAL>dist f g = ⨆ x, dist (f x) (g x)
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>h✝ : IsEmpty α<GOAL>dist f g = ⨆ x, dist (f x) (g x)
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>h✝ : Nonempty α<GOAL>dist f g = ⨆ x, dist (f x) (g x)
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>h✝ : Nonempty α<GOAL>BddAbove (range fun x => dist (f x) (g x))
<VAR>α : Type u_1<VAR>R✝ : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝⁴ : Semiring R✝<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R✝ M<VAR>r✝ s : R✝<VAR>x y : M<VAR>R : Type u_9<VAR>inst✝¹ : Ring R<VAR>inst✝ : Module R M<VAR>r : R<VAR>m : M<GOAL>r • m + (1 - r) • m = m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<VAR>hf : Integrable f (μ.restrict s)<VAR>hg : Integrable g (μ.restrict sᶜ)<GOAL>Integrable (s.piecewise f g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<VAR>hf : Memℒp f 1 (μ.restrict s)<VAR>hg : Memℒp g 1 (μ.restrict sᶜ)<GOAL>Memℒp (s.piecewise f g) 1 μ
<VAR>α : Type u_1<VAR>inst✝⁵ : Mul α<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : CovariantClass α α (Function.swap HMul.hMul) LE.le<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>a b : α<GOAL>↑(Iic a * Iic b) ⊆ ↑(Iic (a * b))
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>n : ℕ<VAR>h : p.degree = ↑n<GOAL>p.natDegree = n
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>f : ℕ → β<GOAL>∏ k ∈ range 0, f k = 1
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>f✝ g✝ : X✝ ⟶ Y✝<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>t : Cofork f g<VAR>ht : IsColimit t<VAR>Z : C<VAR>k : t.pt ⟶ Z<GOAL>f ≫ t.π ≫ k = g ≫ t.π ≫ k
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x✝ y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y<GOAL>Perm.sign f = Perm.sign (swap x (f x) * (swap x (f x) * f))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x✝ y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y<VAR>h1 : f (f x) = x<GOAL>Perm.sign (swap x (f x) * (swap x (f x) * f)) = -(-1) ^ f.support.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x✝ y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y<VAR>h1 : f (f x) = x<VAR>h : swap x (f x) * f = 1<GOAL>Perm.sign (swap x (f x) * (swap x (f x) * f)) = -(-1) ^ f.support.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x✝ y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y<VAR>h1 : f (f x) = x<VAR>h : swap x (f x) * f = 1<GOAL>-1 * 1 = -(-1) ^ 2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x✝ y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y<VAR>h1 : ¬f (f x) = x<GOAL>Perm.sign (swap x (f x) * (swap x (f x) * f)) = -(-1) ^ f.support.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x✝ y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y<VAR>h1 : ¬f (f x) = x<VAR>h : (swap x (f x) * f).support.card + 1 = f.support.card<GOAL>Perm.sign (swap x (f x) * (swap x (f x) * f)) = -(-1) ^ f.support.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x✝ y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y<VAR>h1 : ¬f (f x) = x<VAR>h : (swap x (f x) * f).support.card + 1 = f.support.card<VAR>this : (swap x (f x) * f).support.card < f.support.card<GOAL>Perm.sign (swap x (f x) * (swap x (f x) * f)) = -(-1) ^ f.support.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x✝ y : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>x : α<VAR>hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y<VAR>h1 : ¬f (f x) = x<VAR>h : (swap x (f x) * f).support.card + 1 = f.support.card<VAR>this : (swap x (f x) * f).support.card < f.support.card<GOAL>-1 * -(-1) ^ (swap x (f x) * f).support.card = -(-1) ^ ((swap x (f x) * f).support.card + 1)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝³ : AddCommMonoid M₂'<VAR>inst✝² : Module R M₂'<VAR>n : Type w<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>hO : B.iIsOrtho ⇑v<GOAL>B.Nondegenerate ↔ ∀ (i : n), ¬B.IsOrtho (v i) (v i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝³ : AddCommMonoid M₂'<VAR>inst✝² : Module R M₂'<VAR>n : Type w<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>hO : B.iIsOrtho ⇑v<VAR>ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>m : M<VAR>hB : ∀ (n : M), (B m) n = 0<GOAL>m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝³ : AddCommMonoid M₂'<VAR>inst✝² : Module R M₂'<VAR>n : Type w<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>hO : B.iIsOrtho ⇑v<VAR>ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>hB : ∀ (n_1 : M), (B (v.repr.symm vi)) n_1 = 0<GOAL>v.repr.symm vi = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝³ : AddCommMonoid M₂'<VAR>inst✝² : Module R M₂'<VAR>n : Type w<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>hO : B.iIsOrtho ⇑v<VAR>ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>hB : ∀ (n_1 : M), (B (v.repr.symm vi)) n_1 = 0<GOAL>vi = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝³ : AddCommMonoid M₂'<VAR>inst✝² : Module R M₂'<VAR>n : Type w<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>hO : B.iIsOrtho ⇑v<VAR>ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>hB : ∀ (n_1 : M), (B (v.repr.symm vi)) n_1 = 0<VAR>i : n<GOAL>vi i = 0 i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝³ : AddCommMonoid M₂'<VAR>inst✝² : Module R M₂'<VAR>n : Type w<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>hO : B.iIsOrtho ⇑v<VAR>ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>hB : ∀ (n_1 : M), (B (v.repr.symm vi)) n_1 = 0<VAR>i : n<GOAL>vi i = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝³ : AddCommMonoid M₂'<VAR>inst✝² : Module R M₂'<VAR>n : Type w<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>hO : B.iIsOrtho ⇑v<VAR>ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>i : n<VAR>hB : (B (v.repr.symm vi)) (v i) = 0<GOAL>vi i = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝³ : AddCommMonoid M₂'<VAR>inst✝² : Module R M₂'<VAR>n : Type w<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>hO : B.iIsOrtho ⇑v<VAR>ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>i : n<VAR>hB : ∑ x ∈ vi.support, vi x * (B (v x)) (v i) = 0<GOAL>vi i = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝³ : AddCommMonoid M₂'<VAR>inst✝² : Module R M₂'<VAR>n : Type w<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>hO : B.iIsOrtho ⇑v<VAR>ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>i : n<VAR>hB : vi i * (B (v i)) (v i) = 0<GOAL>vi i = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝³ : AddCommMonoid M₂'<VAR>inst✝² : Module R M₂'<VAR>n : Type w<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>hO : B.iIsOrtho ⇑v<VAR>ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>i : n<VAR>hB : ∑ x ∈ vi.support, vi x * (B (v x)) (v i) = 0<GOAL>∀ b ∈ vi.support, b ≠ i → vi b * (B (v b)) (v i) = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝³ : AddCommMonoid M₂'<VAR>inst✝² : Module R M₂'<VAR>n : Type w<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>hO : B.iIsOrtho ⇑v<VAR>ho : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>i : n<VAR>hB : ∑ x ∈ vi.support, vi x * (B (v x)) (v i) = 0<GOAL>i ∉ vi.support → vi i * (B (v i)) (v i) = 0
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>g g' : G<VAR>h : ¬∃ d, g' = g + d<GOAL>(x %ᵒᶠ g) g' = x g'
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>k : A ⟶ S.X₂<VAR>hk : k ≫ S.g = 0<VAR>inst✝ : S.HasLeftHomology<GOAL>h.liftK k hk ≫ h.cyclesIso.inv = S.liftCycles k hk
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>υ : Type u_6<VAR>f : σ → MvPolynomial τ R<VAR>g : τ → MvPolynomial υ R<VAR>i✝ : σ<GOAL>((bind₁ g).comp (bind₁ f)) (X i✝) = (bind₁ fun i => (bind₁ g) (f i)) (X i✝)
<VAR>m n : ℤ<GOAL>Odd (m - n) ↔ (Odd n ↔ Even m)
<VAR>m n a b c✝ d c : ℕ<VAR>h : a ≡ b [MOD n]<GOAL>a * c ≡ b * c [MOD n * c]
<VAR>m n a b c✝ d c : ℕ<VAR>h : a ≡ b [MOD n]<GOAL>c * a ≡ c * b [MOD c * n]
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ a b c : α<GOAL>filter (fun x => x < c) (Ico a b) = Ico a (min b c)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f g : α → β<VAR>a : Multiset α<VAR>l : List (Multiset α)<GOAL>a.Disjoint l.sum ↔ ∀ b ∈ l, a.Disjoint b
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f : X → Z<VAR>g : Y → Z<GOAL>IsOpenMap (Sum.elim f g) ↔ IsOpenMap f ∧ IsOpenMap g
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulRightInvariant<GOAL>MeasurePreserving ?m.126550 ?m.126546 (?m.126476.prod ?m.126477)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i k₁ k₀ : ι<VAR>r₁₀ : c.Rel k₁ k₀<VAR>hk₀ : ∀ (l : ι), ¬c.Rel k₀ l<VAR>hom : (i j : ι) → C.X i ⟶ D.X j<GOAL>(dNext k₀) hom + (prevD k₀) hom = hom k₀ k₁ ≫ D.d k₁ k₀
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i k₁ k₀ : ι<VAR>r₁₀ : c.Rel k₁ k₀<VAR>hk₀ : ∀ (l : ι), ¬c.Rel k₀ l<VAR>hom : (i j : ι) → C.X i ⟶ D.X j<GOAL>¬c.Rel k₀ (c.next k₀)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝¹⁵ : NormedAddCommGroup EB<VAR>inst✝¹⁴ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝¹³ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹² : TopologicalSpace B<VAR>inst✝¹¹ : ChartedSpace HB B<VAR>inst✝¹⁰ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝⁹ : NormedAddCommGroup EM<VAR>inst✝⁸ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝⁷ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝⁴ : (x : B) → AddCommMonoid (E x)<VAR>inst✝³ : (x : B) → Module 𝕜 (E x)<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : VectorPrebundle 𝕜 F E<VAR>ha : IsSmooth IB a<VAR>e✝ e'✝ : Pretrivialization F TotalSpace.proj<VAR>this✝¹ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology<VAR>this✝ : FiberBundle F E := a.toFiberBundle<VAR>this : VectorBundle 𝕜 F E := toVectorBundle a<VAR>e : Pretrivialization F TotalSpace.proj<VAR>he : e ∈ a.toFiberPrebundle.pretrivializationAtlas<VAR>e' : Pretrivialization F TotalSpace.proj<VAR>he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas<GOAL>SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun b => ↑(Trivialization.coordChangeL 𝕜 (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he) (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b)) ((a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he).baseSet ∩ (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he').baseSet)