ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : CompleteSpace 𝕜<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : TopologicalSpace E<VAR>inst✝¹⁰ : T2Space E<VAR>inst✝⁹ : TopologicalAddGroup E<VAR>inst✝⁸ : Module 𝕜 E<VAR>inst✝⁷ : ContinuousSMul 𝕜 E<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : T2Space F<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : ContinuousSMul 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : E →ₗ[𝕜] F<VAR>hf : ker f = ⊥<VAR>g : E ≃ₗ[𝕜] ↥(range f) := LinearEquiv.ofInjective f ⋯<VAR>this : FiniteDimensional 𝕜 ↥(range f)<GOAL>IsClosed (Set.range ⇑f)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m μ : OuterMeasure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>((restrict s) μ).trim = (restrict s) μ.trim
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m μ : OuterMeasure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<GOAL>((restrict s) μ).trim t ≤ ((restrict s) μ.trim) t
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m μ : OuterMeasure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>((restrict s) μ.trim) t ≤ ((restrict s) μ) t
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a<GOAL>∀ (a : Args), ArgsRel a (Args.P1 y x) → P124 a
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>ih : ∀ (a : Args), TransGen (CutExpand IsOption) (match a with | Args.P1 x y => {y, x} | Args.P24 x₁ x₂ y => {x₁, y, x₂}) {y, x} → P124 a<GOAL>∀ (a : Args), TransGen (CutExpand IsOption) (match a with | Args.P1 x y => {y, x} | Args.P24 x₁ x₂ y => {x₁, y, x₂}) {y, x} → P124 a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : NoetherianSpace α<VAR>s : Closeds α<GOAL>∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : NoetherianSpace α<VAR>s : Closeds α<GOAL>∀ (x : Closeds α), (∀ y < x, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S) → ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ x = sSup S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : NoetherianSpace α<VAR>s : Closeds α<VAR>H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S<GOAL>∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : NoetherianSpace α<VAR>H : ∀ y < ⊥, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S<GOAL>∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ ⊥ = sSup S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : NoetherianSpace α<VAR>s : Closeds α<VAR>H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S<VAR>h₀ : s ≠ ⊥<GOAL>∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>h_dis : (↑I).PairwiseDisjoint id<GOAL>(↑I ∪ ↑(hC.diffFinset₀ hs hI)).PairwiseDisjoint id
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>h_dis : (↑I).PairwiseDisjoint id<GOAL>(↑I).PairwiseDisjoint id ∧ (↑(hC.diffFinset₀ hs hI)).PairwiseDisjoint id ∧ ∀ ⦃i : Set α⦄, i ∈ ↑I → ∀ ⦃j : Set α⦄, j ∈ ↑(hC.diffFinset₀ hs hI) → i ≠ j → Disjoint (id i) (id j)
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>h_dis : (↑I).PairwiseDisjoint id<VAR>u : Set α<VAR>hu : u ∈ ↑I<VAR>v : Set α<VAR>hv : v ∈ ↑(hC.diffFinset₀ hs hI)<VAR>x✝ : u ≠ v<GOAL>Disjoint (id u) (id v)
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>h_dis : (↑I).PairwiseDisjoint id<VAR>u : Set α<VAR>hu : u ∈ ↑I<VAR>v : Set α<VAR>hv : v ∈ ↑(hC.diffFinset₀ hs hI)<VAR>x✝ : u ≠ v<GOAL>Disjoint u v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<GOAL>IsCondKernelCDF (fun p => condCDF ρ p.2) (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<GOAL>IsCondKernelCDF (fun p => stieltjesOfMeasurableRat (fun p r => (preCDF ρ r p.2).toReal) ⋯ ((), p.2)) (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)
<VAR>α : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝¹ : CommMonoid M✝<VAR>s₂ s₁ s : Finset α<VAR>a✝ : α<VAR>g f✝ : α → M✝<VAR>M : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>a b : ℕ<VAR>f : ℕ → ℕ → M<GOAL>∑ i ∈ Ico a b, ∑ j ∈ Ico (i + 1) b, f i j = ∑ j ∈ Ico a b, ∑ i ∈ Ico a j, f i j
<VAR>α : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝¹ : CommMonoid M✝<VAR>s₂ s₁ s : Finset α<VAR>a✝ : α<VAR>g f✝ : α → M✝<VAR>M : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>a b : ℕ<VAR>f : ℕ → ℕ → M<GOAL>∑ x ∈ (Ico a b).sigma fun i => Ico (i + 1) b, f x.fst x.snd = ∑ x ∈ (Ico a b).sigma (Ico a), f x.snd x.fst
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹³ : CommSemiring R✝<VAR>inst✝¹² : NonUnitalRing A✝<VAR>inst✝¹¹ : Module R✝ A✝<VAR>inst✝¹⁰ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁹ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁸ : Semifield R<VAR>inst✝⁷ : Field S<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module S A<VAR>inst✝³ : IsScalarTower S A A<VAR>inst✝² : SMulCommClass S A A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>a : A<VAR>r : R<GOAL>r ∈ quasispectrum R a ↔ r ∈ spectrum R ↑a
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹³ : CommSemiring R✝<VAR>inst✝¹² : NonUnitalRing A✝<VAR>inst✝¹¹ : Module R✝ A✝<VAR>inst✝¹⁰ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁹ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁸ : Semifield R<VAR>inst✝⁷ : Field S<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module S A<VAR>inst✝³ : IsScalarTower S A A<VAR>inst✝² : SMulCommClass S A A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>a : A<VAR>r : R<VAR>this : {0} ⊆ spectrum R ↑a<GOAL>r ∈ quasispectrum R a ↔ r ∈ spectrum R ↑a
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹³ : CommSemiring R✝<VAR>inst✝¹² : NonUnitalRing A✝<VAR>inst✝¹¹ : Module R✝ A✝<VAR>inst✝¹⁰ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁹ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁸ : Semifield R<VAR>inst✝⁷ : Field S<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module S A<VAR>inst✝³ : IsScalarTower S A A<VAR>inst✝² : SMulCommClass S A A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>a : A<VAR>r : R<VAR>this : {0} ⊆ spectrum R ↑a<GOAL>r ∈ quasispectrum R a ↔ r ∈ quasispectrum R ↑a
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹³ : CommSemiring R✝<VAR>inst✝¹² : NonUnitalRing A✝<VAR>inst✝¹¹ : Module R✝ A✝<VAR>inst✝¹⁰ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁹ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁸ : Semifield R<VAR>inst✝⁷ : Field S<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module S A<VAR>inst✝³ : IsScalarTower S A A<VAR>inst✝² : SMulCommClass S A A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>a : A<VAR>r : R<VAR>this : {0} ⊆ spectrum R ↑a<VAR>x : IsUnit r<GOAL>¬IsQuasiregular (-(x.unit⁻¹ • a)) ↔ ¬IsQuasiregular (-(x.unit⁻¹ • ↑a))
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : Filter X<VAR>h : x ∈ s<VAR>o : IsOpen s<VAR>sf : 𝓟 s ≤ f<GOAL>𝓝 x ≤ f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>f : Filter X<VAR>h : x ∈ s<VAR>o : IsOpen s<VAR>sf : 𝓟 s ≤ f<GOAL>⨅ s ∈ {s | x ∈ s ∧ IsOpen s}, 𝓟 s ≤ f
<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>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>hB₀ : B.IsRefl<GOAL>IsCompl W (B.orthogonal W) ↔ Disjoint W (B.orthogonal W)
<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>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>hB₀ : B.IsRefl<VAR>h : Disjoint W (B.orthogonal W)<GOAL>Codisjoint W (B.orthogonal W)
<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>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>hB₀ : B.IsRefl<VAR>h : Disjoint W (B.orthogonal W)<GOAL>W ⊔ B.orthogonal W = ⊤
<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>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>hB₀ : B.IsRefl<VAR>h : Disjoint W (B.orthogonal W)<GOAL>finrank K V ≤ finrank K ↥(W ⊔ B.orthogonal W)
<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>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>W : Submodule K V<VAR>hB₀ : B.IsRefl<VAR>h : Disjoint W (B.orthogonal W)<GOAL>finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤) ≤ finrank K ↥(W ⊔ B.orthogonal W) + finrank K ↥(W ⊓ B.orthogonal W)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : DecidableEq α<VAR>s✝ : Finset α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>s : Finset ι<VAR>f : ι → Finset α<VAR>hs : (↑s).PairwiseDisjoint f<VAR>hf : ∀ i ∈ s, (f i).Nonempty<GOAL>s.card ≤ (s.biUnion f).card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : DecidableEq α<VAR>s✝ : Finset α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>s : Finset ι<VAR>f : ι → Finset α<VAR>hs : (↑s).PairwiseDisjoint f<VAR>hf : ∀ i ∈ s, (f i).Nonempty<GOAL>∑ x ∈ s, 1 ≤ ∑ u ∈ s, (f u).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : DivisionRing β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>ε : α<VAR>ε0 : ε > 0<VAR>K : α<VAR>K0 : K > 0<VAR>i : ℕ<VAR>H : ∀ j ≥ i, K ≤ abv (↑f j)<VAR>j : ℕ<VAR>ij : j ≥ i<GOAL>abv (↑(f.inv hf * f - 1) j) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>S : WSeq (Computation α)<VAR>a : α<VAR>H : ∀ (s : Computation α), s ∈ S → s ~> a<VAR>c : Computation α<VAR>cs : c ∈ S<VAR>ac : a ∈ c<GOAL>a ∈ parallel S
<VAR>α : Type u<VAR>β : Type v<VAR>S : WSeq (Computation α)<VAR>a : α<VAR>H : ∀ (s : Computation α), s ∈ S → s ~> a<VAR>c : Computation α<VAR>cs : c ∈ S<VAR>ac : a ∈ c<VAR>this : c.Terminates<GOAL>a ∈ parallel S
<VAR>α : Type u<VAR>β : Type v<VAR>S : WSeq (Computation α)<VAR>a : α<VAR>H : ∀ (s : Computation α), s ∈ S → s ~> a<VAR>c : Computation α<VAR>cs : c ∈ S<VAR>ac : a ∈ c<VAR>this✝ : c.Terminates<VAR>this : (parallel S).Terminates<GOAL>a ∈ parallel S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝ : MulOneClass M<VAR>s t : Set α<VAR>f✝ g✝ : α → M<VAR>a : α<VAR>f g : α → M<VAR>h : Disjoint (mulSupport f) (mulSupport g)<GOAL>(mulSupport g).mulIndicator (f * g) = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝ : MulOneClass M<VAR>s t : Set α<VAR>f✝ g✝ : α → M<VAR>a : α<VAR>f g : α → M<VAR>h : Disjoint (mulSupport f) (mulSupport g)<VAR>x : α<VAR>hx : x ∈ mulSupport g<GOAL>(f * g) x = g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝ : MulOneClass M<VAR>s t : Set α<VAR>f✝ g✝ : α → M<VAR>a : α<VAR>f g : α → M<VAR>h : Disjoint (mulSupport f) (mulSupport g)<VAR>x : α<VAR>hx : x ∈ mulSupport g<VAR>this : f x = 1<GOAL>(f * g) x = g x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<GOAL>Collinear k ∅
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<GOAL>Module.rank k ↥⊥ ≤ 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>h : f + g ≈ 0<VAR>this : (f + g - 0).LimZero<GOAL>f.norm = g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>h : f + g ≈ 0<VAR>this✝ : (f + g - 0).LimZero<VAR>this : f ≈ -g<GOAL>f.norm = g.norm
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>h : f + g ≈ 0<VAR>this✝¹ : (f + g - 0).LimZero<VAR>this✝ : f ≈ -g<VAR>this : f.norm = (-g).norm<GOAL>f.norm = g.norm
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → F<VAR>R : ℝ<VAR>hR : 0 ≤ R<GOAL>∫ (x : E), f (R⁻¹ • x) ∂μ = R ^ finrank ℝ E • ∫ (x : E), f x ∂μ
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<GOAL>comp Q₁ ↑(TensorProduct.rid R M₁) = Q₁.tmul QuadraticMap.sq
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<GOAL>(associatedHom R) (comp Q₁ ↑(TensorProduct.rid R M₁)) = (associatedHom R) (Q₁.tmul QuadraticMap.sq)
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>m₁ m₁' : M₁<GOAL>((TensorProduct.AlgebraTensorModule.curry (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (comp Q₁ ↑(TensorProduct.rid R M₁)))) m₁) 1)) m₁') 1 = ((TensorProduct.AlgebraTensorModule.curry (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (Q₁.tmul QuadraticMap.sq))) m₁) 1)) m₁') 1
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>m₁ m₁' : M₁<GOAL>(((associatedHom R) (comp Q₁ ↑(TensorProduct.rid R M₁))) (m₁ ⊗ₜ[R] 1)) (m₁' ⊗ₜ[R] 1) = (((associatedHom R) (Q₁.tmul QuadraticMap.sq)) (m₁ ⊗ₜ[R] 1)) (m₁' ⊗ₜ[R] 1)
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>m₁ m₁' : M₁<GOAL>((LinearMap.compl₁₂ ((associatedHom R) Q₁) ↑(TensorProduct.rid R M₁) ↑(TensorProduct.rid R M₁)) (m₁ ⊗ₜ[R] 1)) (m₁' ⊗ₜ[R] 1) = (((associated Q₁).tmul (associated QuadraticMap.sq)) (m₁ ⊗ₜ[R] 1)) (m₁' ⊗ₜ[R] 1)
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>Q₁✝ : QuadraticForm R M₁<VAR>Q₂✝ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>f : Q₁ →qᵢ Q₂<VAR>g : Q₂ →qᵢ Q₁<VAR>h : LeftInverse ⇑g ⇑f<VAR>x : CliffordAlgebra Q₁<GOAL>(map g) ((map f) x) = x
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>Q₁✝ : QuadraticForm R M₁<VAR>Q₂✝ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>f : Q₁ →qᵢ Q₂<VAR>g : Q₂ →qᵢ Q₁<VAR>x : CliffordAlgebra Q₁<VAR>h : g.comp f = QuadraticMap.Isometry.id Q₁<GOAL>(map g) ((map f) x) = x
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{u₂, u₁} C<VAR>inst✝³ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝² : FiberFunctor F<VAR>X A : C<VAR>inst✝¹ : IsConnected A<VAR>u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X<VAR>inst✝ : Mono u<VAR>a : ↑(F.obj A)<VAR>h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X<VAR>b : ↑(F.obj A)<GOAL>∀ (i : ↑(F.obj X)), (F.map (Pi.π (fun x => X) i)) (F.map u b) = (F.map (Pi.π (fun x => X) i)) (F.map (CategoryTheory.PreGaloisCategory.selfProdPermIncl h b) a)
<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✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>s : Finset ι<VAR>f : ι → α → E<VAR>hf : ∀ i ∈ s, Integrable (f i) μ<GOAL>(setToFun μ T hT fun a => ∑ i ∈ s, f i a) = ∑ i ∈ s, setToFun μ T hT (f i)
<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✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>s : Finset ι<VAR>f : ι → α → E<VAR>hf : ∀ i ∈ s, Integrable (f i) μ<VAR>a : α<GOAL>∑ i ∈ s, f i a = (∑ i ∈ s, f i) a
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝³ : CommRing A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<VAR>int : IsIntegral A x<GOAL>2 ≤ (minpoly A x).natDegree ↔ x ∉ (algebraMap A B).range
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝³ : CommRing A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<VAR>int : IsIntegral A x<GOAL>(minpoly A x).natDegree = 1 ↔ (minpoly A x).natDegree < 2
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsCofilteredOrEmpty C<VAR>h₁ : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<VAR>h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'<VAR>d : D<GOAL>IsCofiltered (CostructuredArrow F d)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsCofilteredOrEmpty C<VAR>h₁ : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<VAR>h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'<VAR>d : D<GOAL>IsFiltered (CostructuredArrow F d)ᵒᵖ
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsCofilteredOrEmpty C<VAR>h₁ : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<VAR>h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'<VAR>d : D<GOAL>IsFiltered (StructuredArrow (op d) F.op)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsCofilteredOrEmpty C<VAR>h₁ : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<VAR>h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'<VAR>d : D<GOAL>∀ (d : Dᵒᵖ), ∃ c, Nonempty (d ⟶ F.op.obj c)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsCofilteredOrEmpty C<VAR>h₁ : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<VAR>h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'<VAR>d : D<GOAL>∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring A'<VAR>inst✝⁵ : Algebra ℚ A<VAR>inst✝⁴ : Algebra ℚ A'<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring A'<VAR>inst✝¹ : Algebra ℚ A<VAR>inst✝ : Algebra ℚ A'<VAR>n : ℕ<VAR>f : A →+* A'<VAR>n✝ : ℕ<GOAL>(coeff A' n✝) ((map f) (sin A)) = (coeff A' n✝) (sin A')
<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>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<GOAL>(∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff