ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2<VAR>h_max_bi_pos : 0 < b (max_bi b)<VAR>h_max_bi_lt_one : 0 < 1 - b (max_bi b)<VAR>hc_pos : 0 < c<VAR>h₁ : 0 < (1 - b (max_bi b)) / 2<VAR>hc_lt_one : c < 1<VAR>hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖<VAR>hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑x‖<VAR>n : ℕ<VAR>hn' : ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2<VAR>i : α<VAR>hn : ↑n / log ↑n ^ 2 ≤ (1 - b (max_bi b)) / 2 * ↑n<GOAL>↑(r i n) ≤ c * ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>s₁ s₂ : Finset α<GOAL>∀ (x : α), x ∉ s₁ ∩ (s₂ \ s₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>s₁ s₂ : Finset α<GOAL>∀ (x : α), ¬(x ∈ s₁ ∧ x ∈ s₂ ∧ x ∉ s₁)
<VAR>p : ℝ≥0∞<VAR>h : p ≤ 1<VAR>n : ℕ<GOAL>(binomial p h n) 0 = (1 - p) ^ n
<VAR>X : Type u<VAR>α : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>a : X<VAR>l : Filter X<VAR>ha : a ∈ s<VAR>inst✝ : l.NeBot<VAR>hl : l ≤ 𝓟 s<VAR>f g : X → α<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<VAR>ha' : f a ≤ g a<VAR>he : g ≤ᶠ[l] f<GOAL>∃ x ∈ s, f x = g x
<VAR>X : Type u<VAR>α : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>a : X<VAR>l : Filter X<VAR>ha : a ∈ s<VAR>inst✝ : l.NeBot<VAR>hl : l ≤ 𝓟 s<VAR>f g : X → α<VAR>hf : Continuous (s.restrict f)<VAR>hg : Continuous (s.restrict g)<VAR>ha' : f a ≤ g a<VAR>he : g ≤ᶠ[l] f<GOAL>∃ x ∈ s, f x = g x
<VAR>X : Type u<VAR>α : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>a : X<VAR>l : Filter X<VAR>ha : a ∈ s<VAR>inst✝ : l.NeBot<VAR>hl : l ≤ 𝓟 s<VAR>f g : X → α<VAR>hf : Continuous (s.restrict f)<VAR>hg : Continuous (s.restrict g)<VAR>ha' : f a ≤ g a<VAR>he : g ≤ᶠ[l] f<VAR>b : ↑s<VAR>h : s.restrict f b = s.restrict g b<GOAL>∃ x ∈ s, f x = g x
<VAR>a✝ b✝ c : ℕ<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>a : α<VAR>b : ℤ<VAR>nb : ℕ<VAR>num : ℤ<VAR>den : ℕ<VAR>pb : IsNat b nb<VAR>pe' : IsRat (a ^ nb) num den<GOAL>IsRat (a ^ b) num den
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type w<VAR>X✝ : C<VAR>J J₂ : GrothendieckTopology C<VAR>X : C<GOAL>∀ S ∈ ⊥.sieves X, IsSheafFor P S.arrows
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α : Q(Type u)<VAR>sα : Q(CommSemiring «$α»)<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>a a' a₁ a₂ a₃ b b' b₁ b₂ b₃ c : R<GOAL>a₁ + a₂ + (b₁ + b₂) = a₁ + b₁ + (a₂ + b₂)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a b : α<GOAL>⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n : ℕ<VAR>a b : α<GOAL>a + b ≤ ↑⌈a⌉₊ + ↑⌈b⌉₊
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>inst✝ : F.ReflectsMonomorphisms<VAR>α : F ≅ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : Mono (G.map f)<GOAL>Mono f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>inst✝ : F.ReflectsMonomorphisms<VAR>α : F ≅ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : Mono (G.map f)<GOAL>Mono (F.map f)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>inst✝ : F.ReflectsMonomorphisms<VAR>α : F ≅ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : Mono (G.map f)<VAR>this : Mono (G.map f ≫ (α.app Y).inv)<GOAL>Mono (F.map f)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>inst✝ : F.ReflectsMonomorphisms<VAR>α : F ≅ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : Mono (G.map f)<VAR>this : Mono (G.map f ≫ (α.app Y).inv)<GOAL>F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv
<VAR>s : Finset ℕ<VAR>m n p✝ : ℕ<VAR>hm : Squarefree m<VAR>hn : n ≠ 0<VAR>p : ℕ<GOAL>p ∈ (m / m.gcd n).primeFactors ↔ p ∈ m.primeFactors \ n.primeFactors
<VAR>s : Finset ℕ<VAR>m n p✝ : ℕ<VAR>hm : Squarefree m<VAR>hn : n ≠ 0<VAR>p : ℕ<VAR>this : m / m.gcd n ≠ 0<GOAL>p ∈ (m / m.gcd n).primeFactors ↔ p ∈ m.primeFactors \ n.primeFactors
<VAR>s : Finset ℕ<VAR>m n p✝ : ℕ<VAR>hm : Squarefree m<VAR>hn : n ≠ 0<VAR>p : ℕ<VAR>this : m / m.gcd n ≠ 0<GOAL>Prime p ∧ m.gcd n * p ∣ m ↔ (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)
<VAR>s : Finset ℕ<VAR>m n p✝ : ℕ<VAR>hm : Squarefree m<VAR>hn : n ≠ 0<VAR>p : ℕ<VAR>this : m / m.gcd n ≠ 0<VAR>hp : (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)<GOAL>(m.gcd n).Coprime p
<VAR>s : Finset ℕ<VAR>m n p✝ : ℕ<VAR>hm : Squarefree m<VAR>hn : n ≠ 0<VAR>p : ℕ<VAR>this : m / m.gcd n ≠ 0<VAR>hp : (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)<GOAL>¬p ∣ m.gcd n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hsf : support f ⊆ s<GOAL>∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hsf : support f ⊆ s<GOAL>∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hsf : support f ⊆ s<GOAL>∫⁻ (x : α), f x ∂μ = ∫⁻ (a : α), s.indicator f a ∂μ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : Q ⊗[R] N<GOAL>(inverse_of_rightInverse Q hfg hgh) ((lTensor Q g) y) = Submodule.Quotient.mk y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg✝ : Exact ⇑f ⇑g<VAR>hfg : ker g = range f<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : Q ⊗[R] N<GOAL>(inverse_of_rightInverse Q hfg✝ hgh ∘ₗ lTensor Q g) y = (range (lTensor Q f)).mkQ y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg✝ : Exact ⇑f ⇑g<VAR>hfg : ker g = range f<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : Q ⊗[R] N<GOAL>inverse_of_rightInverse Q hfg✝ hgh ∘ₗ lTensor Q g = (range (lTensor Q f)).mkQ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg✝ : Exact ⇑f ⇑g<VAR>hfg : ker g = range f<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : Q ⊗[R] N<GOAL>∀ (x : Q) (y : N), (inverse_of_rightInverse Q hfg✝ hgh ∘ₗ lTensor Q g) (x ⊗ₜ[R] y) = (range (lTensor Q f)).mkQ (x ⊗ₜ[R] y)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg✝ : Exact ⇑f ⇑g<VAR>hfg : ker g = range f<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : Q ⊗[R] N<VAR>n : Q<VAR>q : N<GOAL>(inverse_of_rightInverse Q hfg✝ hgh ∘ₗ lTensor Q g) (n ⊗ₜ[R] q) = (range (lTensor Q f)).mkQ (n ⊗ₜ[R] q)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg✝ : Exact ⇑f ⇑g<VAR>hfg : ker g = range f<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : Q ⊗[R] N<VAR>n : Q<VAR>q : N<GOAL>Submodule.Quotient.mk (n ⊗ₜ[R] h (g q)) = Submodule.Quotient.mk (n ⊗ₜ[R] q)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg✝ : Exact ⇑f ⇑g<VAR>hfg : ker g = range f<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : Q ⊗[R] N<VAR>n : Q<VAR>q : N<GOAL>n ⊗ₜ[R] (h (g q) - q) ∈ range (lTensor Q f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg✝ : Exact ⇑f ⇑g<VAR>hfg : ker g = range f<VAR>hg : Surjective ⇑g<VAR>h : P → N<VAR>hgh : Function.RightInverse h ⇑g<VAR>y : Q ⊗[R] N<VAR>n : Q<VAR>q : N<GOAL>h (g q) - q ∈ range f
<VAR>R : Type u<VAR>inst✝¹⁸ : CommRing R<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>Q : Type w₃<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✝¹¹ : AddCommGroup N<VAR>inst✝¹⁰ : Module R N<VAR>inst✝⁹ : LieRingModule L N<VAR>inst✝⁸ : LieModule R L N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>inst✝⁵ : LieRingModule L P<VAR>inst✝⁴ : LieModule R L P<VAR>inst✝³ : AddCommGroup Q<VAR>inst✝² : Module R Q<VAR>inst✝¹ : LieRingModule L Q<VAR>inst✝ : LieModule R L Q<VAR>f : M →ₗ⁅R,L⁆ N →ₗ[R] P<GOAL>⇑((liftLie R L M N P) f) = ⇑((lift R L M N P) ↑f)
<VAR>R : Type u<VAR>inst✝¹⁸ : CommRing R<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>Q : Type w₃<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✝¹¹ : AddCommGroup N<VAR>inst✝¹⁰ : Module R N<VAR>inst✝⁹ : LieRingModule L N<VAR>inst✝⁸ : LieModule R L N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>inst✝⁵ : LieRingModule L P<VAR>inst✝⁴ : LieModule R L P<VAR>inst✝³ : AddCommGroup Q<VAR>inst✝² : Module R Q<VAR>inst✝¹ : LieRingModule L Q<VAR>inst✝ : LieModule R L Q<VAR>f : M →ₗ⁅R,L⁆ N →ₗ[R] P<GOAL>↑((liftLie R L M N P) f) = (lift R L M N P) ↑f
<VAR>R : Type u<VAR>inst✝¹⁸ : CommRing R<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>P : Type w₂<VAR>Q : Type w₃<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✝¹¹ : AddCommGroup N<VAR>inst✝¹⁰ : Module R N<VAR>inst✝⁹ : LieRingModule L N<VAR>inst✝⁸ : LieModule R L N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>inst✝⁵ : LieRingModule L P<VAR>inst✝⁴ : LieModule R L P<VAR>inst✝³ : AddCommGroup Q<VAR>inst✝² : Module R Q<VAR>inst✝¹ : LieRingModule L Q<VAR>inst✝ : LieModule R L Q<VAR>f : M →ₗ⁅R,L⁆ N →ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>((AlgebraTensorModule.curry ↑((liftLie R L M N P) f)) m) n = ((AlgebraTensorModule.curry ((lift R L M N P) ↑f)) m) n
<VAR>n : ℤ<VAR>help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1<GOAL>χ₈' ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1
<VAR>n : ℤ<VAR>help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1<GOAL>χ₈' ↑(n % ↑8) = if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -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₂<GOAL>comp Q₂ ↑(TensorProduct.lid R M₂) = QuadraticForm.tmul QuadraticMap.sq Q₂
<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.lid R M₂)) = (associatedHom R) (QuadraticForm.tmul QuadraticMap.sq Q₂)
<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.lid R M₂)))) 1) m₂)) 1) m₂' = ((TensorProduct.AlgebraTensorModule.curry (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (QuadraticForm.tmul QuadraticMap.sq Q₂))) 1) m₂)) 1) m₂'
<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.lid R M₂))) (1 ⊗ₜ[R] m₂)) (1 ⊗ₜ[R] m₂') = (((associatedHom R) (QuadraticForm.tmul QuadraticMap.sq Q₂)) (1 ⊗ₜ[R] m₂)) (1 ⊗ₜ[R] m₂')
<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.lid R M₂) ↑(TensorProduct.lid R M₂)) (1 ⊗ₜ[R] m₂)) (1 ⊗ₜ[R] m₂') = (((associated QuadraticMap.sq).tmul (associated Q₂)) (1 ⊗ₜ[R] m₂)) (1 ⊗ₜ[R] m₂')
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some '' Iio a = Iio ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>hG : G.Connected<VAR>hH : H.Connected<GOAL>(G □ H).Connected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>hG : G.Connected<VAR>hH : H.Connected<VAR>this : Nonempty α<GOAL>(G □ H).Connected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>hG : G.Connected<VAR>hH : H.Connected<VAR>this✝ : Nonempty α<VAR>this : Nonempty β<GOAL>(G □ H).Connected
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>inst✝³ : Preadditive C<VAR>inst✝² : CategoryWithHomology C<VAR>inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization<VAR>inst✝ : c.QFactorsThroughHomotopy C<VAR>K L : HomologicalComplex C c<VAR>φ : { as := K } ⟶ { as := L }<GOAL>HomotopyCategory.quasiIso C c φ → IsIso (Qh.map φ)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>inst✝³ : Preadditive C<VAR>inst✝² : CategoryWithHomology C<VAR>inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization<VAR>inst✝ : c.QFactorsThroughHomotopy C<VAR>K L : HomologicalComplex C c<VAR>φ : K ⟶ L<GOAL>HomotopyCategory.quasiIso C c ((HomotopyCategory.quotient C c).map φ) → IsIso (Qh.map ((HomotopyCategory.quotient C c).map φ))
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>inst✝³ : Preadditive C<VAR>inst✝² : CategoryWithHomology C<VAR>inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization<VAR>inst✝ : c.QFactorsThroughHomotopy C<VAR>K L : HomologicalComplex C c<VAR>φ : K ⟶ L<GOAL>IsIso (Q.map φ) → IsIso (Qh.map ((HomotopyCategory.quotient C c).map φ))
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y : ℝ≥0∞<VAR>hx : x ≠ ⊤<VAR>hy : y ≠ ⊤<GOAL>x.toNNReal = y.toNNReal ↔ x = y
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<GOAL>card α = 0 ↔ IsEmpty α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<GOAL>card α = 0 ↔ #α = 0
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<GOAL>card α = 0 ↔ #α = ↑0
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<GOAL>card α = 0 ↔ toPartENat #α = ↑0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C C₁ C₂ C₃ : HomologicalComplex V c<VAR>f : C₁.Hom C₂<VAR>i j : ι<VAR>w : c.Rel i j<GOAL>f.prev j = (C₁.xPrevIso w).hom ≫ f.f i ≫ (C₂.xPrevIso w).inv
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C C₁ C₂ C₃ : HomologicalComplex V c<VAR>f : C₁.Hom C₂<VAR>j : ι<VAR>w : c.Rel (c.prev j) j<GOAL>f.prev j = (C₁.xPrevIso w).hom ≫ f.f (c.prev j) ≫ (C₂.xPrevIso w).inv
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u_3<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>T : Type u_5<VAR>inst✝¹ : AddCommGroup T<VAR>inst✝ : Module (AdicCompletion I R) T<VAR>f g : AdicCompletion I M → N<VAR>h : ∀ (a : AdicCauchySequence I M), f ((mk I M) a) = g ((mk I M) a)<VAR>x : AdicCompletion I M<GOAL>f x = g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>s t : UpperSet α<VAR>a : α<VAR>S : Set (UpperSet α)<GOAL>↑(sInf S).compl = ↑(⨅ s ∈ S, s.compl)
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>x : α ⊕ β<VAR>y : γ ⊕ δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>d : δ<VAR>h : LiftRel r s x y<GOAL>x.isRight = true ↔ y.isRight = true
<VAR>e : ℤˣ<GOAL>‖↑e‖₊ = 1
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>P : R[X]<VAR>hP : P.Monic<VAR>hdeg : 0 < P.natDegree<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a✝ : Nontrivial R<GOAL>(∑ i ∈ range n, P ^ i).Monic
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>P : R[X]<VAR>hP : P.Monic<VAR>hdeg : 0 < P.natDegree<VAR>a✝ : Nontrivial R<VAR>n : ℕ<VAR>hn : n.succ ≠ 0<GOAL>(∑ i ∈ range n.succ, P ^ i).Monic
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>P : R[X]<VAR>hP : P.Monic<VAR>hdeg : 0 < P.natDegree<VAR>a✝ : Nontrivial R<VAR>n : ℕ<VAR>hn : n.succ ≠ 0<GOAL>(P ^ n + ∑ i ∈ range n, P ^ i).Monic
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>P : R[X]<VAR>hP : P.Monic<VAR>hdeg : 0 < P.natDegree<VAR>a✝ : Nontrivial R<VAR>n : ℕ<VAR>hn : n.succ ≠ 0<GOAL>(∑ i ∈ range n, P ^ i).degree < (P ^ n).degree
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>P : R[X]<VAR>hP : P.Monic<VAR>hdeg : 0 < P.natDegree<VAR>a✝ : Nontrivial R<VAR>n : ℕ<VAR>hn : n.succ ≠ 0<GOAL>((range n).sup fun b => (P ^ b).degree) < (P ^ n).degree
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>P : R[X]<VAR>hP : P.Monic<VAR>hdeg : 0 < P.natDegree<VAR>a✝ : Nontrivial R<VAR>n : ℕ<VAR>hn : n.succ ≠ 0<GOAL>∀ b ∈ range n, (P ^ b).degree < (P ^ n).degree
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>P : R[X]<VAR>hP : P.Monic<VAR>hdeg : 0 < P.natDegree<VAR>a✝ : Nontrivial R<VAR>n : ℕ<VAR>hn : n.succ ≠ 0<GOAL>⊥ < (P ^ n).degree
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<GOAL>∀ (x y : B), (fun b => 1 ᵍ⊗ₜ[R] b) (x + y) = (fun b => 1 ᵍ⊗ₜ[R] b) x + (fun b => 1 ᵍ⊗ₜ[R] b) y
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<GOAL>∀ (m : R) (x : B), { toFun := fun b => 1 ᵍ⊗ₜ[R] b, map_add' := ⋯ }.toFun (m • x) = (RingHom.id R) m • { toFun := fun b => 1 ᵍ⊗ₜ[R] b, map_add' := ⋯ }.toFun x
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<GOAL>∀ (x y : B), { toFun := fun b => 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } (x * y) = { toFun := fun b => 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } x * { toFun := fun b => 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } y
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<GOAL>(LinearMap.mul R B).compr₂ { toFun := fun b => 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } = (LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ) ∘ₗ { toFun := fun b => 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ }).compl₂ { toFun := fun b => 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ }