ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group G'<VAR>inst✝⁴ : Group G''<VAR>A : Type u_4<VAR>inst✝³ : AddGroup A<VAR>G₁ : Type u_5<VAR>G₂ : Type u_6<VAR>G₃ : Type u_7<VAR>inst✝² : Group G₁<VAR>inst✝¹ : Group G₂<VAR>inst✝ : Group G₃<VAR>f : G₁ →* G₂<VAR>f_inv : G₂ → G₁<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : G₁ →* G₃<VAR>hg : f.ker ≤ g.ker<VAR>x : G₁<GOAL>f (f_inv (f x)) = f x
<VAR>α : Type u_1<VAR>inst✝ : OrderedRing α<VAR>a : α<GOAL>Pairwise (Disjoint on fun n => Ioo (↑n) (↑n + 1))
<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✝ : CommMonoid β<GOAL>∏ _x ∈ s, 1 = 1
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>γ : LeftHomologyMapData φ h₁ h₂<VAR>inst✝¹ : S₁.HasLeftHomology<VAR>inst✝ : S₂.HasLeftHomology<GOAL>leftHomologyMap φ ≫ h₂.leftHomologyIso.hom = h₁.leftHomologyIso.hom ≫ γ.φH
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsPreimmersion g<VAR>inst✝ : IsPreimmersion (f ≫ g)<GOAL>Embedding ⇑f.val.base
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsPreimmersion g<VAR>inst✝ : IsPreimmersion (f ≫ g)<VAR>h : Embedding ⇑(f ≫ g).val.base<GOAL>Embedding ⇑f.val.base
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsPreimmersion g<VAR>inst✝ : IsPreimmersion (f ≫ g)<VAR>x : ↑↑X.toPresheafedSpace<GOAL>Function.Surjective ⇑(Scheme.Hom.stalkMap f x)
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsPreimmersion g<VAR>inst✝ : IsPreimmersion (f ≫ g)<VAR>x : ↑↑X.toPresheafedSpace<VAR>h : Function.Surjective ⇑(Scheme.Hom.stalkMap (f ≫ g) x)<GOAL>Function.Surjective ⇑(Scheme.Hom.stalkMap f x)
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsPreimmersion g<VAR>inst✝ : IsPreimmersion (f ≫ g)<VAR>x : ↑↑X.toPresheafedSpace<VAR>h : Function.Surjective ⇑(Scheme.Hom.stalkMap g (f.val.base x) ≫ Scheme.Hom.stalkMap f x)<GOAL>Function.Surjective ⇑(Scheme.Hom.stalkMap f x)
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁷ : Ring R<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✝ : StrongRankCondition R<VAR>n : ℕ<VAR>hn : ↑n ≤ Module.rank R M<GOAL>∃ s, s.card = n ∧ LinearIndependent R Subtype.val
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁷ : Ring R<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✝ : StrongRankCondition R<VAR>n : ℕ<VAR>hn : ↑n ≤ Module.rank R M<VAR>this : ∀ (R : Type ?u.181016) (M : Type ?u.181015) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<GOAL>∃ s, s.card = n ∧ LinearIndependent R Subtype.val
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>x : 𝕜<VAR>hx : 0 < x<VAR>p : 𝕜 → Prop<VAR>h : ∀ᶠ (ε : 𝕜) in 𝓝[>] 0, p ε<GOAL>∀ᶠ (ε : 𝕜) in 𝓝[>] 0, p (x * ε)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>x : 𝕜<VAR>hx : 0 < x<VAR>p : 𝕜 → Prop<VAR>h : ∀ᶠ (ε : 𝕜) in 𝓝[>] 0, p ε<GOAL>∀ᶠ (ε : 𝕜) in comap (fun x_1 => x * x_1) (𝓝[>] 0), p (x * ε)
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>α : Type u_7<VAR>β : Type u_8<VAR>m✝ : R<VAR>x✝ : α ⊕ β →₀ M<GOAL>{ toFun := __src✝.toFun, map_add' := ⋯ }.toFun (m✝ • x✝) = (RingHom.id R) m✝ • { toFun := __src✝.toFun, map_add' := ⋯ }.toFun x✝
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B'✝ I J D X : Set α<VAR>e f : α<VAR>hB : M.Base B<VAR>hI : M.Indep I<VAR>hBI : B ⊆ I<VAR>B' : Set α<VAR>hB' : M.Base B'<VAR>hB'I : I ⊆ B'<GOAL>I ⊆ B
<VAR>this : Irrational √↑5<GOAL>Irrational φ
<VAR>this✝ : Irrational √↑5<VAR>this : Irrational (↑1 + √↑5)<GOAL>Irrational φ
<VAR>this✝¹ : Irrational √↑5<VAR>this✝ : Irrational (↑1 + √↑5)<VAR>this : Irrational (↑0.5 * (↑1 + √↑5))<GOAL>Irrational φ
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝ : Nontrivial R<GOAL>nodal s v ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_2<VAR>v : ι → R<VAR>inst✝ : Nontrivial R<GOAL>nodal ∅ v ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝ : Nontrivial R<VAR>h : s.Nonempty<GOAL>nodal s v ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>l : Filter β<VAR>f : β → α<VAR>y : α<GOAL>Tendsto f l (𝓝 y) ↔ Tendsto (fun x => edist (f x) y) l (𝓝 0)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>W : WeierstrassCurve R<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>n : ℤ<GOAL>(W.baseChange B).Φ n = Polynomial.map (↑f) ((W.baseChange A).Φ n)
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>s : Set ℂ<VAR>h₁ : HasDerivWithinAt f f' s x<VAR>h₂ : f x ∈ slitPlane<GOAL>HasDerivWithinAt (fun t => log (f t)) (f' / f x) s x
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>s : Set ℂ<VAR>h₁ : HasDerivWithinAt f f' s x<VAR>h₂ : f x ∈ slitPlane<GOAL>HasDerivWithinAt (fun t => log (f t)) ((f x)⁻¹ * f') s x
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt f (f' x) x<VAR>hgg' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt g (g' x) x<VAR>hg' : ∀ᶠ (x : ℝ) in atBot, g' x ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atBot l<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∃ v ∈ atBot, ∀ y ∈ v, HasDerivAt f (f' y) y<VAR>hgg' : ∃ v ∈ atBot, ∀ y ∈ v, HasDerivAt g (g' y) y<VAR>hg' : ∃ v ∈ atBot, ∀ y ∈ v, g' y ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atBot l<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atBot l<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ atBot<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ atBot<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ atBot<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atBot l<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ atBot<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ atBot<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ atBot<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<VAR>hs : s ∈ atBot<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atBot l<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ atBot<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ atBot<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ atBot<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<VAR>hs : ∃ a, ∀ b ≤ a, b ∈ s<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l✝ : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atBot l✝<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ atBot<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ atBot<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ atBot<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<VAR>l : ℝ<VAR>hl : ∀ b ≤ l, b ∈ s<GOAL>Tendsto (fun x => f x / g x) atBot l✝
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l✝ : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atBot l✝<VAR>s₁ : Set ℝ<VAR>hs₁ : s₁ ∈ atBot<VAR>hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y<VAR>s₂ : Set ℝ<VAR>hs₂ : s₂ ∈ atBot<VAR>hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y<VAR>s₃ : Set ℝ<VAR>hs₃ : s₃ ∈ atBot<VAR>hg' : ∀ y ∈ s₃, g' y ≠ 0<VAR>s : Set ℝ := s₁ ∩ s₂ ∩ s₃<VAR>l : ℝ<VAR>hl : ∀ b ≤ l, b ∈ s<VAR>hl' : Iio l ⊆ s<GOAL>Tendsto (fun x => f x / g x) atBot l✝
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 1 ≤ a<VAR>h : m ≤ n<VAR>ha₀ : 0 < a<GOAL>a ^ m ≤ a ^ n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 1 ≤ a<VAR>h : m ≤ n<VAR>ha₀ : 0 < a<VAR>k : ℕ<VAR>hk : ↑k = n - m<GOAL>a ^ m ≤ a ^ n
<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✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>hP0 : ¬P = ⊥<GOAL>∏ i ∈ s, f i ≤ P ↔ ∃ i ∈ s, f i ≤ P
<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✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → Ideal R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>hP0 : ¬P = ⊥<GOAL>P ∣ ∏ i ∈ s, f i ↔ ∃ i ∈ s, P ∣ f i
<VAR>δ : ℝ<VAR>x : UnitAddCircle<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>x ∈ approxAddOrderOf UnitAddCircle n δ ↔ ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ
<VAR>δ : ℝ<VAR>x : UnitAddCircle<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ) ↔ ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : PartialOrder α<VAR>inst✝⁴ : AddCommSemigroup α<VAR>inst✝³ : Sub α<VAR>inst✝² : OrderedSub α<VAR>a✝ b✝ c✝ d : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a c b : α<GOAL>a + c - (b + c) = a - b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : PartialOrder α<VAR>inst✝⁴ : AddCommSemigroup α<VAR>inst✝³ : Sub α<VAR>inst✝² : OrderedSub α<VAR>a✝ b✝ c✝ d : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a c b : α<GOAL>a ≤ a + c - (b + c) + b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : PartialOrder α<VAR>inst✝⁴ : AddCommSemigroup α<VAR>inst✝³ : Sub α<VAR>inst✝² : OrderedSub α<VAR>a✝ b✝ c✝ d : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a c b : α<GOAL>a + ?a ≤ a + c - (b + c) + b + ?a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : PartialOrder α<VAR>inst✝⁴ : AddCommSemigroup α<VAR>inst✝³ : Sub α<VAR>inst✝² : OrderedSub α<VAR>a✝ b✝ c✝ d : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a c b : α<GOAL>α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : PartialOrder α<VAR>inst✝⁴ : AddCommSemigroup α<VAR>inst✝³ : Sub α<VAR>inst✝² : OrderedSub α<VAR>a✝ b✝ c✝ d : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a c b : α<GOAL>a + ?bc.c ≤ a + c - (b + c) + (b + ?bc.c)
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : LinearOrder α<VAR>a✝ b✝ c✝ d : α<VAR>inst✝⁴ : ExistsAddOfLE α<VAR>inst✝³ : MulPosStrictMono α<VAR>inst✝² : PosMulStrictMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : LinearOrder α<VAR>a✝ b✝ c✝ d : α<VAR>inst✝⁴ : ExistsAddOfLE α<VAR>inst✝³ : MulPosStrictMono α<VAR>inst✝² : PosMulStrictMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<GOAL>(0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : LinearOrder α<VAR>a✝ b✝ c✝ d : α<VAR>inst✝⁴ : ExistsAddOfLE α<VAR>inst✝³ : MulPosStrictMono α<VAR>inst✝² : PosMulStrictMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>or_a : 0 ≤ a ∨ a ≤ 0<GOAL>(0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : LinearOrder α<VAR>a✝ b✝ c✝ d : α<VAR>inst✝⁴ : ExistsAddOfLE α<VAR>inst✝³ : MulPosStrictMono α<VAR>inst✝² : PosMulStrictMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>or_a : 0 ≤ a ∨ a ≤ 0<VAR>or_b : 0 ≤ b ∨ b ≤ 0<GOAL>(0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : LinearOrder α<VAR>a✝ b✝ c✝ d : α<VAR>inst✝⁴ : ExistsAddOfLE α<VAR>inst✝³ : MulPosStrictMono α<VAR>inst✝² : PosMulStrictMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>or_a : 0 ≤ a ∨ a ≤ 0<VAR>or_b : 0 ≤ b ∨ b ≤ 0<VAR>or_c : 0 ≤ c ∨ c ≤ 0<GOAL>(0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>t₁ t₂ : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>x : α<VAR>h₁ : t₁.Bounded o₁ ↑x<VAR>h₂ : t₂.Bounded (↑x) o₂<GOAL>All (fun y => All (fun z => y < z) t₂) t₁
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>t₁ t₂ : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>x : α<VAR>h₁ : t₁.Bounded o₁ ↑x<VAR>h₂ : t₂.Bounded (↑x) o₂<VAR>y : α<VAR>yx : y < x<GOAL>All (fun z => y < z) t₂
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ZMod 2<GOAL>Submodule.map involute.toLinearMap (evenOdd Q n) = evenOdd Q n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n✝ : ℕ<VAR>hx : x ∈ periodicPts f<VAR>n : ℕ<GOAL>minimalPeriod f (f^[n] x) = minimalPeriod f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n✝ : ℕ<VAR>hx : x ∈ periodicPts f<VAR>n : ℕ<GOAL>IsPeriodicPt f (minimalPeriod f x) (f^[n] x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n✝ : ℕ<VAR>hx : x ∈ periodicPts f<VAR>n : ℕ<GOAL>f^[n] x ∈ periodicPts f
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>inst✝¹³ : TopologicalSpace H<VAR>E : Type u_3<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>inst✝¹⁰ : Monoid G<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : SmoothMul I G<VAR>H' : Type u_5<VAR>inst✝⁶ : TopologicalSpace H'<VAR>E' : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>G' : Type u_7<VAR>inst✝³ : Monoid G'<VAR>inst✝² : TopologicalSpace G'<VAR>inst✝¹ : ChartedSpace H' G'<VAR>inst✝ : SmoothMul I' G'<GOAL>Smooth I I fun a => a ^ 0
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>inst✝¹³ : TopologicalSpace H<VAR>E : Type u_3<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>inst✝¹⁰ : Monoid G<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : SmoothMul I G<VAR>H' : Type u_5<VAR>inst✝⁶ : TopologicalSpace H'<VAR>E' : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>G' : Type u_7<VAR>inst✝³ : Monoid G'<VAR>inst✝² : TopologicalSpace G'<VAR>inst✝¹ : ChartedSpace H' G'<VAR>inst✝ : SmoothMul I' G'<GOAL>Smooth I I fun a => 1
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>inst✝¹³ : TopologicalSpace H<VAR>E : Type u_3<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>inst✝¹⁰ : Monoid G<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : SmoothMul I G<VAR>H' : Type u_5<VAR>inst✝⁶ : TopologicalSpace H'<VAR>E' : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>G' : Type u_7<VAR>inst✝³ : Monoid G'<VAR>inst✝² : TopologicalSpace G'<VAR>inst✝¹ : ChartedSpace H' G'<VAR>inst✝ : SmoothMul I' G'<VAR>k : ℕ<GOAL>Smooth I I fun a => a ^ (k + 1)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>K : Ideal S<GOAL>comap f (sInf {J | K ≤ J ∧ J.IsMaximal}) = sInf {J | comap f K ≤ J ∧ J.IsMaximal}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>K : Ideal S<GOAL>comap f (sInf {J | K ≤ J ∧ J.IsMaximal}) ≤ sInf {J | comap f K ≤ J ∧ J.IsMaximal}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>K : Ideal S<GOAL>sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f (sInf {J | K ≤ J ∧ J.IsMaximal})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionRing K<VAR>a b c d : K<VAR>hab : Commute a b<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a⁻¹ - b⁻¹ = (b - a) / (a * b)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<VAR>h : ¬c₁.Rel i₁ (c₁.next i₁)<GOAL>c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂ = 0
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁸ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>inst✝³ : Nontrivial E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝¹ : Countable ↥L<VAR>inst✝ : DiscreteTopology ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h_cpt : IsCompact s<VAR>h : μ F * 2 ^ finrank ℝ E ≤ μ s<GOAL>∃ x, x ≠ 0 ∧ ↑x ∈ s
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁸ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>inst✝³ : Nontrivial E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝¹ : Countable ↥L<VAR>inst✝ : DiscreteTopology ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h_cpt : IsCompact s<VAR>h : μ F * 2 ^ finrank ℝ E ≤ μ s<VAR>h_mes : μ s ≠ 0<GOAL>∃ x, x ≠ 0 ∧ ↑x ∈ s
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁸ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>inst✝³ : Nontrivial E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝¹ : Countable ↥L<VAR>inst✝ : DiscreteTopology ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h_cpt : IsCompact s<VAR>h : μ F * 2 ^ finrank ℝ E ≤ μ s<VAR>h_mes : μ s ≠ 0<VAR>h_nemp : s.Nonempty<GOAL>∃ x, x ≠ 0 ∧ ↑x ∈ s
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁸ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>inst✝³ : Nontrivial E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝¹ : Countable ↥L<VAR>inst✝ : DiscreteTopology ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h_cpt : IsCompact s<VAR>h : μ F * 2 ^ finrank ℝ E ≤ μ s<VAR>h_mes : μ s ≠ 0<VAR>h_nemp : s.Nonempty<VAR>u : ℕ → ℝ≥0 := ⋯.choose<GOAL>∃ x, x ≠ 0 ∧ ↑x ∈ s
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁸ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>inst✝³ : Nontrivial E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝¹ : Countable ↥L<VAR>inst✝ : DiscreteTopology ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h_cpt : IsCompact s<VAR>h : μ F * 2 ^ finrank ℝ E ≤ μ s<VAR>h_mes : μ s ≠ 0<VAR>h_nemp : s.Nonempty<VAR>u : ℕ → ℝ≥0 := ⋯.choose<VAR>K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }<VAR>S : ℕ → ConvexBody E := fun n => (1 + u n) • K<VAR>Z : ℕ → Set E := fun n => ↑(S n) ∩ (↑L \ {0})<GOAL>∃ x, x ≠ 0 ∧ ↑x ∈ s
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁸ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>inst✝³ : Nontrivial E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝¹ : Countable ↥L<VAR>inst✝ : DiscreteTopology ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h_cpt : IsCompact s<VAR>h : μ F * 2 ^ finrank ℝ E ≤ μ s<VAR>h_mes : μ s ≠ 0<VAR>h_nemp : s.Nonempty<VAR>u : ℕ → ℝ≥0 := ⋯.choose<VAR>K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }<VAR>S : ℕ → ConvexBody E := fun n => (1 + u n) • K<VAR>Z : ℕ → Set E := fun n => ↑(S n) ∩ (↑L \ {0})<VAR>h_zero : 0 ∈ K<GOAL>∃ x, x ≠ 0 ∧ ↑x ∈ s