ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>(p * X).degree = p.degree + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Ring β<VAR>h : Antiperiodic f c<VAR>n : ℕ<GOAL>f (x + ↑n * c) = (-1) ^ n * f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>h : s ⊆ t<VAR>ht : autoParam t.Finite _auto✝<GOAL>(t \ s).ncard = t.ncard - s.ncard
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>ha : 0 < a<VAR>s : ℝ<GOAL>Tendsto (fun x => |x| ^ s * rexp (-a * x ^ 2)) (cocompact ℝ) (𝓝 0)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>ha : 0 < a<VAR>s : ℝ<GOAL>Tendsto (fun x => |x| ^ s * rexp (-a * |x| ^ 2)) (cocompact ℝ) (𝓝 0)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>ha : 0 < a<VAR>s : ℝ<GOAL>Tendsto (fun y => y ^ s * rexp (-a * y ^ 2)) atTop (𝓝 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>R₄ : Type u_7<VAR>M₄ : Type u_8<VAR>inst✝³ : CommRing R₄<VAR>inst✝² : IsDomain R₄<VAR>inst✝¹ : AddCommGroup M₄<VAR>inst✝ : Module R₄ M₄<VAR>G : BilinForm R₄ M₄<VAR>x y : M₄<VAR>a : R₄<VAR>ha : a ≠ 0<GOAL>(G (a • x)) y = 0 ↔ (G x) y = 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>R₄ : Type u_7<VAR>M₄ : Type u_8<VAR>inst✝³ : CommRing R₄<VAR>inst✝² : IsDomain R₄<VAR>inst✝¹ : AddCommGroup M₄<VAR>inst✝ : Module R₄ M₄<VAR>G : BilinForm R₄ M₄<VAR>x y : M₄<VAR>a : R₄<VAR>ha : a ≠ 0<GOAL>(a • G x) y = 0 ↔ (G x) y = 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>R₄ : Type u_7<VAR>M₄ : Type u_8<VAR>inst✝³ : CommRing R₄<VAR>inst✝² : IsDomain R₄<VAR>inst✝¹ : AddCommGroup M₄<VAR>inst✝ : Module R₄ M₄<VAR>G : BilinForm R₄ M₄<VAR>x y : M₄<VAR>a : R₄<VAR>ha : a ≠ 0<GOAL>a = 0 → (G x) y = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.Exact<VAR>hR₂ : R₂.Exact<VAR>hR₂' : Mono (R₂.map' 0 1 ⋯ ⋯)<VAR>h₀ : Epi (app' φ 1 ⋯)<VAR>h₁ : Mono (app' φ 2 ⋯)<GOAL>R₂.map' 0 2 ⋯ ⋯ = 0
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>f : M →[L] N<GOAL>f.range = ⊤ ↔ Function.Surjective ⇑f
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S✝ : Set E<VAR>K : IntermediateField F E<VAR>S : Set E<VAR>h : K ≤ adjoin F S<GOAL>restrictScalars F (extendScalars h) = restrictScalars F (adjoin (↥K) S)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S✝ : Set E<VAR>K : IntermediateField F E<VAR>S : Set E<VAR>h : K ≤ adjoin F S<GOAL>adjoin F S = adjoin F (↑K ∪ S)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝¹ : Zero M<VAR>inst✝ : SMulZeroClass R M<VAR>f : α → R<VAR>g : α → M<VAR>x : α<VAR>hbf : x ∈ support (f • g)<VAR>hf : g x = 0<GOAL>(f • g) x = 0
<VAR>α β : Type u<VAR>a b : Cardinal.{u_1}<GOAL>ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
<VAR>α β : Type u<VAR>a b : Cardinal.{u_1}<VAR>h : ¬a * b < ℵ₀ ↔ ¬(a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀) := Iff.not mul_lt_aleph0_iff<GOAL>ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>exps : HeightOneSpectrum R → ℤ<VAR>h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0<GOAL>count K v (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ exps v) = exps v
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>exps : HeightOneSpectrum R → ℤ<VAR>h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ exps v = { support := Finite.toFinset h_exps, toFun := exps, mem_support_toFun := ⋯ }.prod fun x x_1 => ↑x.asIdeal ^ x_1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>exps : HeightOneSpectrum R → ℤ<VAR>h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0<GOAL>∏ i ∈ Finite.toFinset h_exps, ↑i.asIdeal ^ exps i = ∏ a ∈ { support := Finite.toFinset h_exps, toFun := exps, mem_support_toFun := ⋯ }.support, ↑a.asIdeal ^ { support := Finite.toFinset h_exps, toFun := exps, mem_support_toFun := ⋯ } a
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>exps : HeightOneSpectrum R → ℤ<VAR>h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0<GOAL>(mulSupport fun v => ↑v.asIdeal ^ exps v) ⊆ ↑(Finite.toFinset h_exps)
<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>‖F_nat 1 a t‖ ≤ rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))
<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (g_nat 1 a t) (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))
<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => (↑n + a) ^ 1 * rexp (-π * (↑n + a ^ 2) * t)) (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))
<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => ↑n * rexp (-π * (↑n + a ^ 2) * t) + a * rexp (-π * (↑n + a ^ 2) * t)) (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))
<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun b => ↑b * rexp (-π * (↑b + a ^ 2) * t)) (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2)
<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun b => a * rexp (-π * (↑b + a ^ 2) * t)) (a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁵ : OrderedRing 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y z : E<VAR>x✝ : z ∈ [x-[𝕜]y]<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>hz : a • x + b • y = z<GOAL>(fun θ => (a + b - θ) • x + θ • y) b = a • x + b • y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a✝ b a : α<VAR>s : Finset α<VAR>x : α<GOAL>x ∈ ↑(insert a s) ↔ x ∈ insert a ↑s
<VAR>a b : Rat<GOAL>{ num := a.num.div ↑(a.num.natAbs.gcd b.den) * b.num.div ↑(b.num.natAbs.gcd a.den), den := a.den / b.num.natAbs.gcd a.den * (b.den / a.num.natAbs.gcd b.den), den_nz := ⋯, reduced := ⋯ } = normalize (a.num * b.num) (a.den * b.den) ⋯
<VAR>a b : Rat<VAR>H1 : a.num.natAbs.gcd b.den ≠ 0<GOAL>{ num := a.num.div ↑(a.num.natAbs.gcd b.den) * b.num.div ↑(b.num.natAbs.gcd a.den), den := a.den / b.num.natAbs.gcd a.den * (b.den / a.num.natAbs.gcd b.den), den_nz := ⋯, reduced := ⋯ } = normalize (a.num * b.num) (a.den * b.den) ⋯
<VAR>a b : Rat<VAR>H1 : a.num.natAbs.gcd b.den ≠ 0<VAR>H2 : b.num.natAbs.gcd a.den ≠ 0<GOAL>{ num := a.num.div ↑(a.num.natAbs.gcd b.den) * b.num.div ↑(b.num.natAbs.gcd a.den), den := a.den / b.num.natAbs.gcd a.den * (b.den / a.num.natAbs.gcd b.den), den_nz := ⋯, reduced := ⋯ } = normalize (a.num * b.num) (a.den * b.den) ⋯
<VAR>a b : Rat<VAR>H1 : a.num.natAbs.gcd b.den ≠ 0<VAR>H2 : b.num.natAbs.gcd a.den ≠ 0<GOAL>normalize (a.num.div ↑(a.num.natAbs.gcd b.den) * b.num.div ↑(b.num.natAbs.gcd a.den) * ↑(a.num.natAbs.gcd b.den * b.num.natAbs.gcd a.den)) (a.den / b.num.natAbs.gcd a.den * (b.den / a.num.natAbs.gcd b.den) * (a.num.natAbs.gcd b.den * b.num.natAbs.gcd a.den)) ⋯ = normalize (a.num * b.num) (a.den * b.den) ⋯
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : AddCommGroup M<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✝² : Module R M'<VAR>inst✝¹ : HasRankNullity.{u, u_1} R<VAR>inst✝ : StrongRankCondition R<VAR>n : ℕ<VAR>v : Fin n → M<VAR>hv : LinearIndependent R v<VAR>h : ↑n < Module.rank R M<GOAL>∃ x, LinearIndependent R (Fin.snoc v x)
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : AddCommGroup M<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✝² : Module R M'<VAR>inst✝¹ : HasRankNullity.{u, u_1} R<VAR>inst✝ : StrongRankCondition R<VAR>n : ℕ<VAR>v : Fin n → M<VAR>hv : LinearIndependent R v<VAR>h : ↑n < Module.rank R M<GOAL>∃ x, LinearIndependent R fun i => Fin.cons x v ((finRotate (n + 1)) i)
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : AddCommGroup M<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✝² : Module R M'<VAR>inst✝¹ : HasRankNullity.{u, u_1} R<VAR>inst✝ : StrongRankCondition R<VAR>n : ℕ<VAR>v : Fin n → M<VAR>hv : LinearIndependent R v<VAR>h : ↑n < Module.rank R M<VAR>x : M<VAR>hx : LinearIndependent R (Fin.cons x v)<GOAL>∃ x, LinearIndependent R fun i => Fin.cons x v ((finRotate (n + 1)) i)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>inst✝⁷ : Fintype l<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix l m α<VAR>D : Matrix l n α<VAR>inst✝ : Invertible A<GOAL>fromBlocks A B C D = fromBlocks 1 0 (C * ⅟A) 1 * fromBlocks A 0 0 (D - C * ⅟A * B) * fromBlocks 1 (⅟A * B) 0 1
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>δ : Type u_1<VAR>inst✝ : Monad m<VAR>f : α × β → δ → m (ForInStep δ)<VAR>key✝ : α<VAR>value✝ : β<VAR>tail✝ : AssocList α β<VAR>tail_ih✝ : ∀ (init : δ), tail✝.forIn init f = List.forIn.loop f tail✝.toList init<VAR>init : δ<GOAL>(fun __do_lift => match __do_lift with | ForInStep.done d => pure d | ForInStep.yield d => tail✝.forIn d f) = fun __do_lift => match __do_lift with | ForInStep.done d => pure d | ForInStep.yield b => List.forIn.loop f tail✝.toList b
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>δ : Type u_1<VAR>inst✝ : Monad m<VAR>f : α × β → δ → m (ForInStep δ)<VAR>key✝ : α<VAR>value✝ : β<VAR>tail✝ : AssocList α β<VAR>tail_ih✝ : ∀ (init : δ), tail✝.forIn init f = List.forIn.loop f tail✝.toList init<VAR>init : δ<VAR>a : ForInStep δ<GOAL>(match a with | ForInStep.done d => pure d | ForInStep.yield d => tail✝.forIn d f) = match a with | ForInStep.done d => pure d | ForInStep.yield b => List.forIn.loop f tail✝.toList b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a h : M<VAR>t : List M<VAR>u : ∀ m ∈ h :: t, IsUnit m<GOAL>IsUnit (h :: t).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a h : M<VAR>t : List M<VAR>u : ∀ m ∈ h :: t, IsUnit m<GOAL>IsUnit (h * t.prod)
<VAR>α : Type u<VAR>c : α<GOAL>(ofFn fun x => c) = replicate 0 c
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t s : Set M<VAR>r : R<GOAL>span R (r • s) ≤ span R s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t s : Set M<VAR>r : R<GOAL>r • s ⊆ ↑(span R s)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t s : Set M<VAR>r : R<VAR>x : M<VAR>hx : x ∈ s<GOAL>(fun x => r • x) x ∈ ↑(span R s)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>υ : Type u_3<VAR>R : Type u_4<VAR>inst✝ : CommSemiring R<GOAL>comap (AlgHom.id R (MvPolynomial σ R)) = id
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>υ : Type u_3<VAR>R : Type u_4<VAR>inst✝ : CommSemiring R<VAR>x : σ → R<GOAL>comap (AlgHom.id R (MvPolynomial σ R)) x = id x
<VAR>x y : ℝ*<VAR>r s : ℝ<VAR>hxr : x.IsSt r<VAR>hys : y.IsSt s<VAR>f : ℝ → ℝ → ℝ<VAR>hf : ContinuousAt (Function.uncurry f) (r, s)<GOAL>IsSt (Germ.map₂ f x y) (f r s)
<VAR>y : ℝ*<VAR>r s : ℝ<VAR>hys : y.IsSt s<VAR>f : ℝ → ℝ → ℝ<VAR>hf : ContinuousAt (Function.uncurry f) (r, s)<VAR>x : ℕ → ℝ<VAR>hxr : (ofSeq x).IsSt r<GOAL>IsSt (Germ.map₂ f (ofSeq x) y) (f r s)
<VAR>r s : ℝ<VAR>f : ℝ → ℝ → ℝ<VAR>hf : ContinuousAt (Function.uncurry f) (r, s)<VAR>x : ℕ → ℝ<VAR>hxr : (ofSeq x).IsSt r<VAR>y : ℕ → ℝ<VAR>hys : (ofSeq y).IsSt s<GOAL>IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
<VAR>r s : ℝ<VAR>f : ℝ → ℝ → ℝ<VAR>hf : ContinuousAt (Function.uncurry f) (r, s)<VAR>x : ℕ → ℝ<VAR>hxr : Tendsto x (↑(hyperfilter ℕ)) (𝓝 r)<VAR>y : ℕ → ℝ<VAR>hys : Tendsto y (↑(hyperfilter ℕ)) (𝓝 s)<GOAL>IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>h1 : a < 0<VAR>h2 : -1 ≤ a<VAR>this : 1 / a ≤ 1 / -1<GOAL>1 / a ≤ -1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddZeroClass M<VAR>f : α → β<VAR>v₁ v₂ : β →₀ M<VAR>hv₁ : Set.InjOn f (f ⁻¹' ↑v₁.support)<VAR>hv₂ : Set.InjOn f (f ⁻¹' ↑v₂.support)<VAR>hv₁₂ : Set.InjOn f (f ⁻¹' ↑(v₁ + v₂).support)<VAR>a✝ : α<GOAL>(comapDomain f (v₁ + v₂) hv₁₂) a✝ = (comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂) a✝
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>f : PointedMap Γ Γ'<VAR>L R : List Γ<GOAL>map f (mk₂ L R) = mk₂ (List.map f.f L) (List.map f.f R)
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R n<VAR>a b c : ℕ<VAR>hab : a = b<VAR>hbc : b = c<VAR>x : ZMod a<GOAL>(ringEquivCongr hbc) ((ringEquivCongr hab) x) = (ringEquivCongr ⋯) x
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R n<VAR>a b c : ℕ<VAR>hab : a = b<VAR>hbc : b = c<VAR>x : ZMod a<GOAL>(ringEquivCongr hbc) ((ringEquivCongr hab) x) = ((ringEquivCongr hab).trans (ringEquivCongr hbc)) x
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m : M<VAR>s : ↥S<GOAL>(fromLocalizedModule S f) (LocalizedModule.mk (s • m) s) = f m
<VAR>B : Type u<VAR>inst✝¹ : Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g h : b ⟶ c<VAR>η : g ⟶ h<VAR>inst✝ : IsIso η<GOAL>inv (f ◁ η) = f ◁ inv η
<VAR>B : Type u<VAR>inst✝¹ : Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g h : b ⟶ c<VAR>η : g ⟶ h<VAR>inst✝ : IsIso η<GOAL>f ◁ η ≫ f ◁ inv η = 𝟙 (f ≫ g)
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>inst✝¹ : DecidableEq F.A<VAR>inst✝ : Inhabited F.M<VAR>ps : Path F<VAR>a : F.A<VAR>f : F.B a → F.M<VAR>i : F.B a<GOAL>iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = iselect ps (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝ : α → β<VAR>inst✝ : Countable ι<VAR>f : ι → Measure α<VAR>s : Set α<GOAL>(sum f) s = ∑' (i : ι), (f i) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝ : α → β<VAR>inst✝ : Countable ι<VAR>f : ι → Measure α<VAR>s : Set α<GOAL>(sum f) s ≤ ∑' (i : ι), (f i) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>f✝ : α → β<VAR>inst✝ : Countable ι<VAR>f : ι → Measure α<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>htm : MeasurableSet t<VAR>ht : ∀ (i : ι), (f i) t = (f i) s<GOAL>(sum f) s ≤ ∑' (i : ι), (f i) s
<VAR>R : Type u_1<VAR>inst✝ : Rack R<VAR>x y : R<GOAL>(x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y
<VAR>R : Type u_1<VAR>inst✝ : Rack R<VAR>x y : R<VAR>h : (op x ◃ op x) ◃ op y = op x ◃ op y<GOAL>(x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y
<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✝ : DecidableEq α<VAR>s : Finset α<VAR>m : Multiset α<VAR>hms : ∀ a ∈ m, a ∈ s<GOAL>∑ a ∈ s, count a m = card m
<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✝ : DecidableEq α<VAR>s : Finset α<VAR>m : Multiset α<VAR>hms : ∀ a ∈ m, a ∈ s<GOAL>∑ x ∈ Finset.filter (fun x => count x m ≠ 0) s, count x m = ∑ a ∈ m.toFinset, count a m
<VAR>m n✝ n : ℕ<VAR>p : Fin n → Prop<VAR>inst✝ : DecidablePred p<GOAL>find p = none ↔ ∀ (i : Fin n), ¬p i
<VAR>m n✝ n : ℕ<VAR>p : Fin n → Prop<VAR>inst✝ : DecidablePred p<GOAL>find p = none ↔ ¬(find p).isSome = true
<VAR>α : Type u_1<VAR>s✝ : HeapNode α<VAR>n : Nat<VAR>res : Heap α<VAR>a : α<VAR>c s : HeapNode α<GOAL>(toHeap.go (node a c s) n res).realSize = (node a c s).realSize + res.realSize
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A T : C<VAR>hT : IsTerminal T<VAR>inst✝ : Mono (hT.from A)<VAR>Z : C<VAR>f g : Z ⟶ A<GOAL>f = g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A T : C<VAR>hT : IsTerminal T<VAR>inst✝ : Mono (hT.from A)<VAR>Z : C<VAR>f g : Z ⟶ A<GOAL>f ≫ hT.from A = g ≫ hT.from A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : IsDomain R₁<VAR>inst✝⁴ : Algebra R₁ K<VAR>inst✝³ : IsFractionRing R₁ K<VAR>I J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R₁ K'<VAR>inst✝ : IsFractionRing R₁ K'<VAR>x : R₁<VAR>hx : x ≠ 0<GOAL>(↑(Ideal.span {x}))⁻¹ * ↑(Ideal.span {x}) = 1
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<VAR>b : n → α<VAR>c : m → α<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Star α<GOAL>Mᴴ.updateRow j (star c) = (M.updateColumn j c)ᴴ
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<VAR>b : n → α<VAR>c : m → α<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Star α<GOAL>((M.map star).updateColumn j (star c))ᵀ = ((M.map star).updateColumn j (star ∘ c))ᵀ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>h : Disjoint s t<VAR>hs : autoParam s.Finite _auto✝<VAR>ht : autoParam t.Finite _auto✝<GOAL>(s ∪ t).ncard = s.ncard + t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>h : Disjoint s t<VAR>hs : autoParam s.Finite _auto✝<VAR>ht : autoParam t.Finite _auto✝<GOAL>↑(s ∪ t).ncard = ↑s.ncard + ↑t.ncard
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝¹ : Monoid α<VAR>inst✝ : AddMonoid α<VAR>x : Holor α ds<VAR>h : x.CPRankMax1<VAR>h' : CPRankMax (0 + 1) (x + 0)<GOAL>CPRankMax 1 x
<VAR>U : Type u_1<VAR>inst✝² : Quiver U<VAR>V : Type u_2<VAR>inst✝¹ : Quiver V<VAR>φ : U ⥤q V<VAR>W : Type ?u.10354<VAR>inst✝ : Quiver W<VAR>ψ : V ⥤q W<VAR>hφ : φ.IsCovering<GOAL>φ.symmetrify.IsCovering
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<VAR>f g : a ⟶ b<VAR>η : f ≅ g<VAR>h : b ⟶ c<GOAL>η.inv ▷ h ≫ η.hom ▷ h = 𝟙 (g ≫ h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s✝ s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f✝ f₁ f₂ f₃ : α → β<VAR>g✝ g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>f : α → β<VAR>g : γ → α<VAR>s : Set β<GOAL>MapsTo f (range g) s ↔ MapsTo (f ∘ g) univ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>R : Type u_12<VAR>R' : Type u_13<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<VAR>inst✝¹² : Norm E<VAR>inst✝¹¹ : Norm F<VAR>inst✝¹⁰ : Norm G<VAR>inst✝⁹ : SeminormedAddCommGroup E'<VAR>inst✝⁸ : SeminormedAddCommGroup F'<VAR>inst✝⁷ : SeminormedAddCommGroup G'<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedAddCommGroup F''<VAR>inst✝⁴ : NormedAddCommGroup G''<VAR>inst✝³ : SeminormedRing R<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedField 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>l l' : Filter α<VAR>c : 𝕜<VAR>f : α → 𝕜<VAR>hc : c ≠ 0<GOAL>(fun x => c * f x) =Θ[l] g ↔ f =Θ[l] g