ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x✝ y✝ z✝ : ℤ<VAR>h✝ : PythagoreanTriple x✝ y✝ z✝<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>h_coprime : x.gcd y = 1<VAR>h_parity : x % 2 = 1<VAR>h_pos : 0 < z<VAR>m n : ℤ<VAR>ht1 : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2<VAR>ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)<VAR>ht3 : m.gcd n = 1<VAR>ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0<VAR>hm : m < 0<GOAL>∃ m n, x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∧ z = m ^ 2 + n ^ 2 ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m
<VAR>B : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} 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>H : Type u₅<VAR>inst✝ : Category.{v₅, u₅} H<VAR>F : B × C ⥤ D<VAR>x✝² x✝¹ : B × C<VAR>x₁ : B<VAR>x₂ : C<VAR>y₁ : B<VAR>y₂ : C<VAR>x✝ : (x₁, x₂) ⟶ (y₁, y₂)<VAR>f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1<VAR>f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2<GOAL>F.map (f₁, 𝟙 x₂) ≫ F.map (𝟙 y₁, f₂) = 𝟙 (F.obj (x₁, x₂)) ≫ F.map (f₁, f₂) ≫ 𝟙 (F.obj (y₁, y₂))
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : RCLike 𝕜<VAR>F : Type u_2<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : Module ℝ F<VAR>inst✝ : IsScalarTower ℝ 𝕜 F<VAR>fr : F →ₗ[ℝ] ℝ<VAR>x : F<GOAL>‖fr.extendTo𝕜' x‖ ^ 2 = re ((starRingEnd 𝕜) (fr.extendTo𝕜' x) * fr.extendTo𝕜' x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : RCLike 𝕜<VAR>F : Type u_2<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : Module ℝ F<VAR>inst✝ : IsScalarTower ℝ 𝕜 F<VAR>fr : F →ₗ[ℝ] ℝ<VAR>x : F<GOAL>re ((starRingEnd 𝕜) (fr.extendTo𝕜' x) * fr.extendTo𝕜' x) = fr ((starRingEnd 𝕜) (fr.extendTo𝕜' x) • x)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : IsKleinFour G<VAR>x : G<GOAL>x * x = 1
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁷ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁶ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : AddCommMonoid N<VAR>inst✝¹³ : AddCommMonoid P<VAR>inst✝¹² : AddCommMonoid Q<VAR>inst✝¹¹ : AddCommMonoid S<VAR>inst✝¹⁰ : AddCommMonoid T<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : Module R S<VAR>inst✝⁴ : Module R T<VAR>inst✝³ : DistribMulAction R' M<VAR>inst✝² : Module R'' M<VAR>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>r s : R''<VAR>x : M ⊗[R] N<VAR>this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n<GOAL>(r + s) • 0 = r • 0 + s • 0
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁷ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁶ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : AddCommMonoid N<VAR>inst✝¹³ : AddCommMonoid P<VAR>inst✝¹² : AddCommMonoid Q<VAR>inst✝¹¹ : AddCommMonoid S<VAR>inst✝¹⁰ : AddCommMonoid T<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : Module R S<VAR>inst✝⁴ : Module R T<VAR>inst✝³ : DistribMulAction R' M<VAR>inst✝² : Module R'' M<VAR>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>r s : R''<VAR>x : M ⊗[R] N<VAR>this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n<VAR>m : M<VAR>n : N<GOAL>(r + s) • m ⊗ₜ[R] n = r • m ⊗ₜ[R] n + s • m ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁷ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁶ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : AddCommMonoid N<VAR>inst✝¹³ : AddCommMonoid P<VAR>inst✝¹² : AddCommMonoid Q<VAR>inst✝¹¹ : AddCommMonoid S<VAR>inst✝¹⁰ : AddCommMonoid T<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : Module R S<VAR>inst✝⁴ : Module R T<VAR>inst✝³ : DistribMulAction R' M<VAR>inst✝² : Module R'' M<VAR>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>r s : R''<VAR>x✝ : M ⊗[R] N<VAR>this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n<VAR>x y : M ⊗[R] N<VAR>ihx : (r + s) • x = r • x + s • x<VAR>ihy : (r + s) • y = r • y + s • y<GOAL>(r + s) • (x + y) = r • (x + y) + s • (x + y)
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁷ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁶ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : AddCommMonoid N<VAR>inst✝¹³ : AddCommMonoid P<VAR>inst✝¹² : AddCommMonoid Q<VAR>inst✝¹¹ : AddCommMonoid S<VAR>inst✝¹⁰ : AddCommMonoid T<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : Module R S<VAR>inst✝⁴ : Module R T<VAR>inst✝³ : DistribMulAction R' M<VAR>inst✝² : Module R'' M<VAR>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>r s : R''<VAR>x✝ : M ⊗[R] N<VAR>this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n<VAR>x y : M ⊗[R] N<VAR>ihx : (r + s) • x = r • x + s • x<VAR>ihy : (r + s) • y = r • y + s • y<GOAL>(r + s) • x + (r + s) • y = r • x + r • y + (s • x + s • y)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F →L[𝕜] G<VAR>x y✝ : E × F<VAR>x✝ : y✝ ∈ EMetric.ball 0 ⊤<GOAL>HasSum (fun n => (f.fpowerSeriesBilinear x (n + 3)) fun x => y✝) ((f (x + y✝).1) (x + y✝).2 - ∑ i ∈ Finset.range 3, (f.fpowerSeriesBilinear x i) fun x => y✝)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F →L[𝕜] G<VAR>x y✝ : E × F<VAR>x✝ : y✝ ∈ EMetric.ball 0 ⊤<GOAL>HasSum (fun n => (f.fpowerSeriesBilinear x (n + 3)) fun x => y✝) ((f x.1) x.2 + (f.deriv₂ (x.1, x.2)) (y✝.1, y✝.2) + (f y✝.1) y✝.2 - ((((∑ x_1 ∈ Finset.range 0, (f.fpowerSeriesBilinear x x_1) fun x => y✝) + (f.fpowerSeriesBilinear x 0) fun x => y✝) + (f.fpowerSeriesBilinear x 1) fun x => y✝) + (f.fpowerSeriesBilinear x 2) fun x => y✝))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝¹ ys : List α<VAR>n✝¹ n✝ : ℕ<VAR>xs✝ : List α<VAR>n : ℕ<VAR>x : α<VAR>xs : List α<GOAL>(List.sym (n + 1) (x :: xs)).length = (x :: xs).length.multichoose (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝¹ ys : List α<VAR>n✝¹ n✝ : ℕ<VAR>xs✝ : List α<VAR>n : ℕ<VAR>x : α<VAR>xs : List α<GOAL>(List.sym n (x :: xs)).length + (List.sym (n + 1) xs).length = (xs.length + 1).multichoose (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs✝¹ ys : List α<VAR>n✝¹ n✝ : ℕ<VAR>xs✝ : List α<VAR>n : ℕ<VAR>x : α<VAR>xs : List α<GOAL>(x :: xs).length.multichoose n + xs.length.multichoose (n + 1) = (xs.length + 1).multichoose (n + 1)
<VAR>m k : ℕ+<GOAL>m.div k * ↑k + ↑(m.mod k) = ↑m
<VAR>m k : ℕ+<GOAL>↑k * m.div k + ↑(m.mod k) = ↑m
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>U : B ⥤ C<VAR>inst✝² : MonadicRightAdjoint U<VAR>R : A ⥤ B<VAR>inst✝¹ : HasReflexiveCoequalizers A<VAR>inst✝ : (R ⋙ U).IsRightAdjoint<VAR>R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)<GOAL>R'.IsRightAdjoint
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>U : B ⥤ C<VAR>inst✝² : MonadicRightAdjoint U<VAR>R : A ⥤ B<VAR>inst✝¹ : HasReflexiveCoequalizers A<VAR>inst✝ : (R ⋙ U).IsRightAdjoint<VAR>R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)<VAR>this : (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint := Adjunction.isRightAdjoint ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight (isoWhiskerLeft R (Monad.comparisonForget (monadicAdjunction U)).symm))<GOAL>R'.IsRightAdjoint
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>U : B ⥤ C<VAR>inst✝² : MonadicRightAdjoint U<VAR>R : A ⥤ B<VAR>inst✝¹ : HasReflexiveCoequalizers A<VAR>inst✝ : (R ⋙ U).IsRightAdjoint<VAR>R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)<VAR>this✝ : (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint := Adjunction.isRightAdjoint ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight (isoWhiskerLeft R (Monad.comparisonForget (monadicAdjunction U)).symm))<VAR>this : (X : (monadicAdjunction U).toMonad.Algebra) → RegularEpi ((monadicAdjunction U).toMonad.adj.counit.app X) := fun X => ⋯.mpr { W := (monadicAdjunction U).toMonad.free.obj ((monadicAdjunction U).toMonad.obj X.A), left := Monad.FreeCoequalizer.topMap X, right := Monad.FreeCoequalizer.bottomMap X, w := ⋯, isColimit := Monad.beckAlgebraCoequalizer X }<GOAL>R'.IsRightAdjoint
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<GOAL>∃ f, (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous f
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<VAR>f : ((n : ℕ) → E n) → (n : ℕ) → E n<VAR>fs : ∀ x ∈ s, f x = x<VAR>frange : range f = s<VAR>hf : LipschitzWith 1 f<GOAL>∃ f, (∀ x ∈ s, f x = x) ∧ range f = s ∧ Continuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>p : ι → Prop<VAR>s : ι → Set β<VAR>f : Filter β<VAR>u : β → α<VAR>hf : f.HasBasis p s<VAR>q : β → Prop<GOAL>blimsup u f q = ⨅ i, ⨅ (_ : p i), ⨆ a ∈ s i, ⨆ (_ : q a), u a
<VAR>m n : ℕ<GOAL>↑((↑m).gcd -[n+1]) = ↑m * (↑m).gcdA -[n+1] + -(↑n + 1) * -(↑m).natAbs.gcdB n.succ
<VAR>m n : ℕ<GOAL>↑((↑m).gcd -[n+1]) = ↑m * (↑m).gcdA -[n+1] + (↑n + 1) * (↑m).natAbs.gcdB n.succ
<VAR>m n : ℕ<GOAL>↑(-[m+1].gcd ↑n) = -(↑m + 1) * -m.succ.gcdA (↑n).natAbs + ↑n * -[m+1].gcdB ↑n
<VAR>m n : ℕ<GOAL>↑(-[m+1].gcd ↑n) = (↑m + 1) * m.succ.gcdA (↑n).natAbs + ↑n * -[m+1].gcdB ↑n
<VAR>m n : ℕ<GOAL>↑(-[m+1].gcd -[n+1]) = -(↑m + 1) * -m.succ.gcdA -[n+1].natAbs + -(↑n + 1) * - -[m+1].natAbs.gcdB n.succ
<VAR>m n : ℕ<GOAL>↑(-[m+1].gcd -[n+1]) = (↑m + 1) * m.succ.gcdA -[n+1].natAbs + (↑n + 1) * -[m+1].natAbs.gcdB n.succ
<VAR>r : ℝ≥0<VAR>p : ℝ<VAR>hr : 0 < r<VAR>hp : p < 0<GOAL>r ≤ p.toNNReal ↔ ↑r ≤ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<GOAL>∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>val✝ : Encodable ι<GOAL>∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>val✝ : Encodable ι<VAR>a : ℝ≥0<VAR>a0 : 0 < a<VAR>aε : a < ε<GOAL>∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ε : ℝ≥0<VAR>hε : ε ≠ 0<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>val✝ : Encodable ι<VAR>a : ℝ≥0<VAR>a0 : 0 < a<VAR>aε : a < ε<VAR>ε' : ι → ℝ<VAR>hε' : ∀ (i : ι), 0 < ε' i<VAR>c : ℝ<VAR>hc : HasSum ε' c<VAR>hcε : c ≤ (fun a => ↑a) a<GOAL>∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>f : α → β<VAR>hl : l.HasBasis p s<VAR>t : Set β<GOAL>t ∈ Filter.map f l ↔ ∃ i, p i ∧ f '' s i ⊆ t
<VAR>α : Type u_1<VAR>inst✝³ : Semifield α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : PosMulReflectLT α<VAR>inst✝ : ZeroLEOneClass α<VAR>a b : α<GOAL>a⁻¹ ≤ 0 ↔ a ≤ 0
<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>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>inst✝⁴ : DecidableEq R<VAR>inst✝³ : DecidableEq (Ideal R)<VAR>inst✝² : NormalizationMonoid R<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>r X : R<VAR>hr : r ≠ 0<VAR>hX : Prime X<GOAL>Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)
<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>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>inst✝⁴ : DecidableEq R<VAR>inst✝³ : DecidableEq (Ideal R)<VAR>inst✝² : NormalizationMonoid R<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>r X : R<VAR>hr : r ≠ 0<VAR>hX : Prime X<VAR>this : multiplicity (span {X}) (span {r}) = multiplicity X r<GOAL>Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)
<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>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>inst✝⁴ : DecidableEq R<VAR>inst✝³ : DecidableEq (Ideal R)<VAR>inst✝² : NormalizationMonoid R<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>r X : R<VAR>hr : r ≠ 0<VAR>hX : Prime X<VAR>this : Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)<GOAL>Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count (normalize X) (normalizedFactors r)
<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>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>inst✝⁴ : DecidableEq R<VAR>inst✝³ : DecidableEq (Ideal R)<VAR>inst✝² : NormalizationMonoid R<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>r X : R<VAR>hr : r ≠ 0<VAR>hX : Prime X<VAR>this : multiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))<GOAL>span {r} ≠ 0
<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>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsPrincipalIdealRing R<VAR>inst✝⁴ : DecidableEq R<VAR>inst✝³ : DecidableEq (Ideal R)<VAR>inst✝² : NormalizationMonoid R<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>r X : R<VAR>hr : r ≠ 0<VAR>hX : Prime X<VAR>this : multiplicity (span {X}) (span {r}) = ↑(Multiset.count (normalize X) (normalizedFactors r))<GOAL>Prime (span {X})
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<GOAL>S.Exact ↔ Epi (imageToKernel S.f S.g ⋯)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<GOAL>Epi (imageToKernel' S.f S.g ⋯) ↔ Epi (imageToKernel S.f S.g ⋯)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<GOAL>Arrow.mk (imageToKernel' S.f S.g ⋯) ≅ Arrow.mk (imageToKernel S.f S.g ⋯)
<VAR>n : ℕ<VAR>c : Char<VAR>s : List Char<GOAL>(leftpad n c { data := s }).length = max n { data := s }.length
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I✝ X R J I : Set α<GOAL>uniqueBaseOn I I = freeOn I
<VAR>q : ℚ<VAR>n d : ℤ<VAR>hd : d ≠ 0<VAR>qdf : q = n /. d<GOAL>∃ c, n = c * q.num ∧ d = c * ↑q.den
<VAR>q : ℚ<VAR>d : ℤ<VAR>hd : d ≠ 0<VAR>qdf : q = 0 /. d<GOAL>∃ c, 0 = c * q.num ∧ d = c * ↑q.den
<VAR>q : ℚ<VAR>n d : ℤ<VAR>hd : d ≠ 0<VAR>qdf : q = n /. d<VAR>hn : n ≠ 0<GOAL>∃ c, n = c * q.num ∧ d = c * ↑q.den
<VAR>q : ℚ<VAR>n d : ℤ<VAR>hd : d ≠ 0<VAR>qdf : q = n /. d<VAR>hn : n ≠ 0<VAR>this : q.num * d = n * ↑q.den<GOAL>∃ c, n = c * q.num ∧ d = c * ↑q.den
<VAR>q : ℚ<VAR>n d : ℤ<VAR>hd : d ≠ 0<VAR>qdf : q = n /. d<VAR>hn : n ≠ 0<VAR>this : q.num * d = n * ↑q.den<VAR>hqdn : q.num ∣ n<GOAL>∃ c, n = c * q.num ∧ d = c * ↑q.den
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>a ⇔ b = a ⊔ b ⇨ a ⊓ b
<VAR>X : Type u<VAR>inst✝⁵ : TopologicalSpace X<VAR>A D E : Type u<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : TopologicalSpace D<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : T1Space A<VAR>inst✝ : CompactSpace D<VAR>π : D → A<VAR>π_cont : Continuous π<VAR>π_surj : Surjective π<VAR>S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}<VAR>C : Set (Set D)<VAR>C_sub : C ⊆ S<VAR>C_chain : IsChain (fun x x_1 => x ⊆ x_1) C<GOAL>∃ s ∈ S, ∀ c ∈ C, s ⊆ c
<VAR>X : Type u<VAR>inst✝⁵ : TopologicalSpace X<VAR>A D E : Type u<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : TopologicalSpace D<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : T1Space A<VAR>inst✝ : CompactSpace D<VAR>π : D → A<VAR>π_cont : Continuous π<VAR>π_surj : Surjective π<VAR>S : Set (Set D) := {E | IsClosed E ∧ π '' E = univ}<VAR>C : Set (Set D)<VAR>C_sub : C ⊆ S<VAR>C_chain : IsChain (fun x x_1 => x ⊆ x_1) C<GOAL>π '' ⋂ c, ↑c = univ
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>∫ (x : ℝ), cexp (-b * (↑x + ↑c * I) ^ 2) = (↑π / b) ^ (1 / 2)
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<GOAL>Tendsto (fun i => ∫ (x : ℝ) in -i..id i, cexp (-b * (↑x + ↑c * I) ^ 2)) atTop (𝓝 ((↑π / b) ^ (1 / 2)))
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<VAR>I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)<VAR>HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)<VAR>I₂ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)<VAR>I₄ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (↑T + ↑y * I) ^ 2)<VAR>I₅ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (-↑T + ↑y * I) ^ 2)<GOAL>Tendsto (fun i => ∫ (x : ℝ) in -i..id i, cexp (-b * (↑x + ↑c * I) ^ 2)) atTop (𝓝 ((↑π / b) ^ (1 / 2)))
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<VAR>I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)<VAR>HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)<VAR>I₂ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)<VAR>I₄ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (↑T + ↑y * I) ^ 2)<VAR>I₅ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (-↑T + ↑y * I) ^ 2)<VAR>C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0<GOAL>Tendsto (fun i => ∫ (x : ℝ) in -i..id i, cexp (-b * (↑x + ↑c * I) ^ 2)) atTop (𝓝 ((↑π / b) ^ (1 / 2)))
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<VAR>I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)<VAR>HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)<VAR>I₂ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)<VAR>I₄ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (↑T + ↑y * I) ^ 2)<VAR>I₅ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (-↑T + ↑y * I) ^ 2)<VAR>C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0<VAR>this : I₁ = fun T => I₂ T + verticalIntegral b c T<GOAL>Tendsto I₁ atTop (𝓝 ((↑π / b) ^ (1 / 2)))
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<VAR>I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)<VAR>HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)<VAR>I₂ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)<VAR>I₄ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (↑T + ↑y * I) ^ 2)<VAR>I₅ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (-↑T + ↑y * I) ^ 2)<VAR>C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0<VAR>this : I₁ = fun T => I₂ T + verticalIntegral b c T<GOAL>Tendsto (fun T => I₂ T + verticalIntegral b c T) atTop (𝓝 ((∫ (x : ℝ), cexp (-b * ↑x ^ 2)) + 0))
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>c : ℝ<VAR>I₁ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)<VAR>HI₁ : I₁ = fun T => ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)<VAR>I₂ : ℝ → ℂ := fun T => ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)<VAR>I₄ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (↑T + ↑y * I) ^ 2)<VAR>I₅ : ℝ → ℂ := fun T => ∫ (y : ℝ) in 0 ..c, cexp (-b * (-↑T + ↑y * I) ^ 2)<VAR>C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0<VAR>this : I₁ = fun T => I₂ T + verticalIntegral b c T<GOAL>Tendsto I₂ atTop (𝓝 (∫ (x : ℝ), cexp (-b * ↑x ^ 2)))
<VAR>s : ℝ<VAR>hs : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp1 : 0 < p<VAR>hp2 : p < 1<GOAL>(1 + s) ^ p < 1 + p * s
<VAR>p : ℝ<VAR>hp1 : 0 < p<VAR>hp2 : p < 1<VAR>hs : -1 ≤ -1<VAR>hs' : -1 ≠ 0<GOAL>(1 + -1) ^ p < 1 + p * -1
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp1 : 0 < p<VAR>hp2 : p < 1<VAR>hs : -1 < s<GOAL>(1 + s) ^ p < 1 + p * s
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp1 : 0 < p<VAR>hp2 : p < 1<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<GOAL>(1 + s) ^ p < 1 + p * s
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp1 : 0 < p<VAR>hp2 : p < 1<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<VAR>hs2 : 0 < 1 + p * s<GOAL>(1 + s) ^ p < 1 + p * s
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp1 : 0 < p<VAR>hp2 : p < 1<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<VAR>hs2 : 0 < 1 + p * s<VAR>hs3 : 1 + s ≠ 1<GOAL>(1 + s) ^ p < 1 + p * s
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp1 : 0 < p<VAR>hp2 : p < 1<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<VAR>hs2 : 0 < 1 + p * s<VAR>hs3 : 1 + s ≠ 1<VAR>hs4 : 1 + p * s ≠ 1<GOAL>(1 + s) ^ p < 1 + p * s
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp1 : 0 < p<VAR>hp2 : p < 1<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<VAR>hs2 : 0 < 1 + p * s<VAR>hs3 : 1 + s ≠ 1<VAR>hs4 : 1 + p * s ≠ 1<GOAL>rexp (log (1 + s) * p) < rexp (log (1 + p * s))
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp1 : 0 < p<VAR>hp2 : p < 1<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<VAR>hs2 : 0 < 1 + p * s<VAR>hs3 : 1 + s ≠ 1<VAR>hs4 : 1 + p * s ≠ 1<GOAL>log (1 + s) * p < log (1 + p * s)
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs'✝ : s ≠ 0<VAR>p : ℝ<VAR>hp1 : 0 < p<VAR>hp2 : p < 1<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<VAR>hs2 : 0 < 1 + p * s<VAR>hs3 : 1 + s ≠ 1<VAR>hs4 : 1 + p * s ≠ 1<VAR>hs' : s < 0<GOAL>log (1 + s) * p < log (1 + p * s)
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs'✝ : s ≠ 0<VAR>p : ℝ<VAR>hp1 : 0 < p<VAR>hp2 : p < 1<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<VAR>hs2 : 0 < 1 + p * s<VAR>hs3 : 1 + s ≠ 1<VAR>hs4 : 1 + p * s ≠ 1<VAR>hs' : s > 0<GOAL>log (1 + s) * p < log (1 + p * s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<VAR>huv : u ~[l] v<VAR>hwv : w =o[l] v<GOAL>u + w ~[l] v
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>L : ListBlank ((k : K) → Option (Γ k))<GOAL>(addBottom L).head.1 = true
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w : V<VAR>p : G.Walk u v<VAR>p' : G.Walk v w<GOAL>↑(p.append p').support = {u} + ↑p.support.tail + ↑p'.support.tail
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>y : NumDenSameDeg 𝒜 x<GOAL>(-Quotient.mk'' y).val = -val (Quotient.mk'' y)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>y : NumDenSameDeg 𝒜 x<GOAL>Localization.mk ↑(-y).num ⟨↑(-y).den, ⋯⟩ = Localization.mk (-↑y.num) ⟨↑y.den, ⋯⟩
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<GOAL>G.dist u v = 1 ↔ G.Adj u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<GOAL>1 ≠ 0