ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<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✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<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>k'' : α → G''<VAR>l l' : Filter α<GOAL>(IsBigOWith c l f fun x => -g' x) ↔ IsBigOWith c l f g'
<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>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<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✝⁵ : SeminormedAddGroup E'''<VAR>inst✝⁴ : SeminormedRing R'<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : NormedDivisionRing 𝕜'<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>k'' : α✝ → G''<VAR>l l' : Filter α✝<VAR>α : Type u_17<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : Nonempty α<VAR>f : α → G<VAR>g : α → G'<GOAL>f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.areaForm (o.rightAngleRotation x)) y = -⟪x, y⟫_ℝ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>s✝ : Set α<VAR>f : ι → α<VAR>a✝ : α<VAR>s : Set α<VAR>a : α<VAR>h : a < sSup s<GOAL>∃ b ∈ s, a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>s✝ : Set α<VAR>f : ι → α<VAR>a✝ : α<VAR>s : Set α<VAR>a : α<VAR>h : ∀ b ∈ s, b ≤ a<GOAL>sSup s ≤ a
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I : FractionalIdeal S P<GOAL>1 ≤ I ↔ 1 ∈ I
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>a b : R<GOAL>(addVal R) a ≤ (addVal R) b ↔ a ∣ b
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>a b : R<VAR>hp : Prime (Classical.choose ⋯)<GOAL>(addVal R) a ≤ (addVal R) b ↔ a ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NonUnitalRing α<VAR>a b c : α<VAR>h : a ∣ b<GOAL>a ∣ b + c ↔ a ∣ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NonUnitalRing α<VAR>a b c : α<VAR>h : a ∣ b<GOAL>a ∣ c + b ↔ a ∣ c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>f =ᶠ[ae (μ.restrict t)] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>u : Set E<VAR>u_sep : IsSeparable u<VAR>hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u<GOAL>f =ᶠ[ae (μ.restrict t)] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>u : Set E<VAR>u_sep : IsSeparable u<VAR>hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u<VAR>c : Dual ℝ E<GOAL>(fun x => c (f x)) =ᶠ[ae (μ.restrict t)] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>u : Set E<VAR>u_sep : IsSeparable u<VAR>hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u<VAR>c : Dual ℝ E<GOAL>∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (fun x => c (f x)) s μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>u : Set E<VAR>u_sep : IsSeparable u<VAR>hu : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ u<VAR>c : Dual ℝ E<GOAL>∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, c (f x) ∂μ = 0
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>B : V₁ →ₗ[K] V₂ →ₗ[K] K<VAR>inst✝ : FiniteDimensional K V₁<GOAL>Bijective ⇑B.flip ↔ Bijective ⇑B
<VAR>p : ℤ[X]<VAR>hp : p.IsUnitTrinomial<VAR>h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)<GOAL>Irreducible p
<VAR>p : ℤ[X]<VAR>hp : p.IsUnitTrinomial<VAR>h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)<VAR>q : ℤ[X]<VAR>hq : q ∣ p<VAR>hq' : q ∣ p.mirror<GOAL>IsUnit q
<VAR>p : ℤ[X]<VAR>hp : p.IsUnitTrinomial<VAR>h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)<VAR>q : ℤ[X]<VAR>hq : q ∣ p<VAR>hq' : q ∣ p.mirror<GOAL>¬0 < q.natDegree
<VAR>p : ℤ[X]<VAR>hp : p.IsUnitTrinomial<VAR>h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)<VAR>q : ℤ[X]<VAR>hq : q ∣ p<VAR>hq' : q ∣ p.mirror<VAR>hq'' : 0 < q.natDegree<GOAL>False
<VAR>p : ℤ[X]<VAR>hp : p.IsUnitTrinomial<VAR>h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)<VAR>q : ℤ[X]<VAR>hq : q ∣ p<VAR>hq' : q ∣ p.mirror<VAR>hq'' : 0 < q.degree<GOAL>False
<VAR>p : ℤ[X]<VAR>hp : p.IsUnitTrinomial<VAR>h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)<VAR>q : ℤ[X]<VAR>hq : q ∣ p<VAR>hq' : q ∣ p.mirror<VAR>hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree<GOAL>False
<VAR>p : ℤ[X]<VAR>hp : p.IsUnitTrinomial<VAR>h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)<VAR>q : ℤ[X]<VAR>hq : q ∣ p<VAR>hq' : q ∣ p.mirror<VAR>hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree<VAR>z : ℂ<VAR>hz : (map (algebraMap ℤ ℂ) q).IsRoot z<GOAL>False
<VAR>p : ℤ[X]<VAR>hp : p.IsUnitTrinomial<VAR>h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)<VAR>q : ℤ[X]<VAR>hq : q ∣ p<VAR>hq' : q ∣ p.mirror<VAR>hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree<VAR>z : ℂ<VAR>hz : (aeval z) q = 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : Nonempty β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>m : ι → β<VAR>hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun x x_1 => x ≤ x_1) x (m i)<GOAL>IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun a => s.sup' hs fun i => F i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : Nonempty β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>m : ι → β<VAR>hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun x x_1 => x ≤ x_1) x (m i)<GOAL>∀ᶠ (x : β) in Filter.map (fun a => s.sup' hs fun i => F i a) f, (fun x x_1 => x ≤ x_1) x (s.sup' hs m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : Nonempty β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>m : ι → β<VAR>hm : ∀ i ∈ s, ∀ᶠ (a : α) in f, F i a ≤ m i<GOAL>∀ᶠ (a : α) in f, (s.sup' hs fun i => F i a) ≤ s.sup' hs m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : Nonempty β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>m : ι → β<VAR>hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i<GOAL>∀ᶠ (a : α) in f, (s.sup' hs fun i => F i a) ≤ s.sup' hs m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : Nonempty β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>m : ι → β<VAR>hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i<VAR>a : α<VAR>h : ∀ i ∈ s, F i a ≤ m i<GOAL>(s.sup' hs fun i => F i a) ≤ s.sup' hs m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : Nonempty β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>m : ι → β<VAR>hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i<VAR>a : α<VAR>h : ∀ i ∈ s, F i a ≤ m i<GOAL>∀ b ∈ s, F b a ≤ s.sup' hs m
<VAR>X : Type u_1<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ<VAR>c : ℝ<GOAL>∫ (x : X), (const X c - f) x ∂μ = (μ Set.univ).toReal • c - ∫ (x : X), f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>hι : Countable ι<VAR>s : ι → Set X<VAR>hcomp : ∀ (i : ι), IsCompact (s i)<GOAL>IsSigmaCompact (⋃ i, s i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>hι : Countable ι<VAR>s : ι → Set X<VAR>hcomp : ∀ (i : ι), IsCompact (s i)<VAR>h✝ : IsEmpty ι<GOAL>IsSigmaCompact (⋃ i, s i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>hι : Countable ι<VAR>s : ι → Set X<VAR>hcomp : ∀ (i : ι), IsCompact (s i)<VAR>h✝ : Nonempty ι<GOAL>IsSigmaCompact (⋃ i, s i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>inst✝ : Preorder ι<VAR>l : Filter α<VAR>s : ι → Set α<VAR>hs : l.HasAntitoneBasis s<VAR>t : Set α<GOAL>(∃ i, True ∧ s i ⊆ t) ↔ ∃ i, s i ⊆ t
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y : M<VAR>f : E →ₗ.[R] F<VAR>z : M<VAR>x_fst : E<VAR>x_snd : F<VAR>h : (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph<GOAL>(x_fst, x_snd) ∈ (z • f).graph
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y : M<VAR>f : E →ₗ.[R] F<VAR>z : M<VAR>x_fst : E<VAR>x_snd : F<VAR>h : ∃ y ∈ f.graph, (LinearMap.id.prodMap (z • LinearMap.id)) y = (x_fst, x_snd)<GOAL>(x_fst, x_snd) ∈ (z • f).graph
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y : M<VAR>f : E →ₗ.[R] F<VAR>z : M<VAR>x_fst : E<VAR>x_snd : F<VAR>fst✝ : E<VAR>snd✝ : F<VAR>hx' : (fst✝, snd✝) ∈ f.graph<VAR>h : (LinearMap.id.prodMap (z • LinearMap.id)) (fst✝, snd✝) = (x_fst, x_snd)<GOAL>(x_fst, x_snd) ∈ (z • f).graph
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y : M<VAR>f : E →ₗ.[R] F<VAR>z : M<VAR>x_fst : E<VAR>x_snd : F<VAR>fst✝ : E<VAR>snd✝ : F<VAR>hx' : (fst✝, snd✝) ∈ f.graph<VAR>h : fst✝ = x_fst ∧ z • snd✝ = x_snd<GOAL>(x_fst, x_snd) ∈ (z • f).graph
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y : M<VAR>f : E →ₗ.[R] F<VAR>z : M<VAR>x_fst : E<VAR>x_snd : F<VAR>fst✝ : E<VAR>snd✝ : F<VAR>hx' : ∃ y, ↑y = (fst✝, snd✝).1 ∧ ↑f y = (fst✝, snd✝).2<VAR>h : fst✝ = x_fst ∧ z • snd✝ = x_snd<GOAL>∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(z • f) y = (x_fst, x_snd).2
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>z : M<VAR>x_fst : E<VAR>x_snd : F<VAR>fst✝ : E<VAR>snd✝ : F<VAR>h : fst✝ = x_fst ∧ z • snd✝ = x_snd<VAR>y : ↥f.domain<VAR>hy : ↑y = (fst✝, snd✝).1<VAR>hx' : ↑f y = (fst✝, snd✝).2<GOAL>∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(z • f) y = (x_fst, x_snd).2
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>z : M<VAR>x_fst : E<VAR>x_snd : F<VAR>fst✝ : E<VAR>snd✝ : F<VAR>h : fst✝ = x_fst ∧ z • snd✝ = x_snd<VAR>y : ↥f.domain<VAR>hy : ↑y = (fst✝, snd✝).1<VAR>hx' : ↑f y = (fst✝, snd✝).2<GOAL>↑y = (x_fst, x_snd).1 ∧ ↑(z • f) y = (x_fst, x_snd).2
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y✝ : M<VAR>f : E →ₗ.[R] F<VAR>z : M<VAR>x_fst : E<VAR>x_snd : F<VAR>fst✝ : E<VAR>snd✝ : F<VAR>h : fst✝ = x_fst ∧ z • snd✝ = x_snd<VAR>y : ↥f.domain<VAR>hy : ↑y = (fst✝, snd✝).1<VAR>hx' : ↑f y = (fst✝, snd✝).2<GOAL>↑y = (fst✝, z • snd✝).1 ∧ ↑(z • f) y = (fst✝, z • snd✝).2
<VAR>m n✝ n : ℕ<VAR>x✝ : ℤ<GOAL>x✝ ∈ (Int.castAddHom (ZMod n)).ker ↔ x✝ ∈ AddSubgroup.zmultiples ↑n
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Fintype G<VAR>x : F<GOAL>(minpoly G F x).Monic
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Fintype G<VAR>x : F<GOAL>(prodXSubSMul G F x).Monic
<VAR>q : ℚ<VAR>n₁ n₂ : ℤ<VAR>d₁ d₂ : ℕ<VAR>hd₁ : d₁ ≠ 0<VAR>hd₂ : d₂ ≠ 0<VAR>hnd₁ : n₁.natAbs.Coprime d₁<VAR>hnd₂ : n₂.natAbs.Coprime d₂<VAR>h₁₂ : n₁.natAbs.Coprime d₂<VAR>h₂₁ : n₂.natAbs.Coprime d₁<GOAL>(n₁ * n₂).natAbs.Coprime (d₁ * d₂)
<VAR>q : ℚ<VAR>n₁ n₂ : ℤ<VAR>d₁ d₂ : ℕ<VAR>hd₁ : d₁ ≠ 0<VAR>hd₂ : d₂ ≠ 0<VAR>hnd₁ : n₁.natAbs.Coprime d₁<VAR>hnd₂ : n₂.natAbs.Coprime d₂<VAR>h₁₂ : n₁.natAbs.Coprime d₂<VAR>h₂₁ : n₂.natAbs.Coprime d₁<GOAL>(n₁.natAbs * n₂.natAbs).Coprime (d₁ * d₂)
<VAR>q : ℚ<VAR>n₁ n₂ : ℤ<VAR>d₁ d₂ : ℕ<VAR>hd₁ : d₁ ≠ 0<VAR>hd₂ : d₂ ≠ 0<VAR>hnd₁ : n₁.natAbs.Coprime d₁<VAR>hnd₂ : n₂.natAbs.Coprime d₂<VAR>h₁₂ : n₁.natAbs.Coprime d₂<VAR>h₂₁ : n₂.natAbs.Coprime d₁<GOAL>{ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ } * { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ } = { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }
<VAR>q : ℚ<VAR>n₁ n₂ : ℤ<VAR>d₁ d₂ : ℕ<VAR>hd₁ : d₁ ≠ 0<VAR>hd₂ : d₂ ≠ 0<VAR>hnd₁ : n₁.natAbs.Coprime d₁<VAR>hnd₂ : n₂.natAbs.Coprime d₂<VAR>h₁₂ : n₁.natAbs.Coprime d₂<VAR>h₂₁ : n₂.natAbs.Coprime d₁<GOAL>normalize ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ }.num * { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ }.num) ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ }.den * { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ }.den) ⋯ = { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }
<VAR>q : ℚ<VAR>n₁ n₂ : ℤ<VAR>d₁ d₂ : ℕ<VAR>hd₁ : d₁ ≠ 0<VAR>hd₂ : d₂ ≠ 0<VAR>hnd₁ : n₁.natAbs.Coprime d₁<VAR>hnd₂ : n₂.natAbs.Coprime d₂<VAR>h₁₂ : n₁.natAbs.Coprime d₂<VAR>h₂₁ : n₂.natAbs.Coprime d₁<GOAL>normalize (n₁ * n₂) (d₁ * d₂) ⋯ = { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a b : α<VAR>inst✝ : DecidableEq α<VAR>ha : a ∈ s<GOAL>compress u v a ∈ 𝓒 u v s
<VAR>α : Type u_1<VAR>inst✝³ : GeneralizedBooleanAlgebra α<VAR>inst✝² : DecidableRel Disjoint<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s : Finset α<VAR>u v a b : α<VAR>inst✝ : DecidableEq α<VAR>ha : a ∈ s<GOAL>compress u v a ∈ s ∧ compress u v (compress u v a) ∈ s ∨ compress u v a ∉ s ∧ ∃ b ∈ s, compress u v b = compress u v a
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.30360, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>S.f ≫ 𝟙 S.X₂ = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.30360, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>𝟙 S.X₂ ≫ S.g = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<GOAL>(p * q).natDegree = p.natDegree + q.natDegree
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>α β : A₁ ⟶ A₂<GOAL>A₁.str ≫ F.map (α.f + β.f) = (α.f + β.f) ≫ A₂.str
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<GOAL>A₁.str ≫ F.map 0 = 0 ≫ A₂.str
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>n : ℕ<VAR>α : A₁ ⟶ A₂<GOAL>A₁.str ≫ F.map (n • α.f) = (n • α.f) ≫ A₂.str
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>α : A₁ ⟶ A₂<GOAL>A₁.str ≫ F.map (-α.f) = (-α.f) ≫ A₂.str
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>α β : A₁ ⟶ A₂<GOAL>A₁.str ≫ F.map (α.f - β.f) = (α.f - β.f) ≫ A₂.str
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>r : ℤ<VAR>α : A₁ ⟶ A₂<GOAL>A₁.str ≫ F.map (r • α.f) = (r • α.f) ≫ A₂.str
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>a✝ b✝ c✝ : A₁ ⟶ A₂<GOAL>(a✝ + b✝ + c✝).f = (a✝ + (b✝ + c✝)).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>a✝ : A₁ ⟶ A₂<GOAL>(0 + a✝).f = a✝.f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>a✝ : A₁ ⟶ A₂<GOAL>(a✝ + 0).f = a✝.f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>x✝ : A₁ ⟶ A₂<GOAL>((fun n α => { f := n • α.f, h := ⋯ }) 0 x✝).f = Coalgebra.Hom.f 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>n✝ : ℕ<VAR>x✝ : A₁ ⟶ A₂<GOAL>((fun n α => { f := n • α.f, h := ⋯ }) (n✝ + 1) x✝).f = ((fun n α => { f := n • α.f, h := ⋯ }) n✝ x✝ + x✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>a✝ b✝ : A₁ ⟶ A₂<GOAL>(a✝ - b✝).f = (a✝ + -b✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>a✝ : A₁ ⟶ A₂<GOAL>((fun r α => { f := r • α.f, h := ⋯ }) 0 a✝).f = Coalgebra.Hom.f 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>n✝ : ℕ<VAR>a✝ : A₁ ⟶ A₂<GOAL>↑(n✝ + 1) • a✝.f = ({ f := ↑n✝ • a✝.f, h := ⋯ } + a✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>n✝ : ℕ<VAR>a✝ : A₁ ⟶ A₂<GOAL>n✝ • a✝.f + a✝.f = ({ f := n✝ • a✝.f, h := ⋯ } + a✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>n✝ : ℕ<VAR>a✝ : A₁ ⟶ A₂<GOAL>((fun r α => { f := r • α.f, h := ⋯ }) (Int.negSucc n✝) a✝).f = (-(fun r α => { f := r • α.f, h := ⋯ }) (↑n✝.succ) a✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>a✝ : A₁ ⟶ A₂<GOAL>(-a✝ + a✝).f = Coalgebra.Hom.f 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>A₁ A₂ : Coalgebra F<VAR>a✝ b✝ : A₁ ⟶ A₂<GOAL>(a✝ + b✝).f = (b✝ + a✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>P✝ Q✝ R✝ : Coalgebra F<VAR>f✝ f'✝ : P✝ ⟶ Q✝<VAR>g✝ : Q✝ ⟶ R✝<GOAL>((f✝ + f'✝) ≫ g✝).f = (f✝ ≫ g✝ + f'✝ ≫ g✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>P✝ Q✝ R✝ : Coalgebra F<VAR>f✝ : P✝ ⟶ Q✝<VAR>g✝ g'✝ : Q✝ ⟶ R✝<GOAL>(f✝ ≫ (g✝ + g'✝)).f = (f✝ ≫ g✝ + f✝ ≫ g'✝).f