ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹¹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁸ : NormedAddCommGroup E'<VAR>inst✝⁷ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : InnerProductSpace ℝ F'<VAR>inst✝² : Fintype ι✝<VAR>v✝ : Set E<VAR>A : ι✝ → Submodule 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 E<VAR>ι : Type u_8<VAR>inst✝ : Fintype ι<VAR>card_ι : finrank 𝕜 E = Fintype.card ι<VAR>v : ι → E<VAR>s : Set ι<VAR>hv : Orthonormal 𝕜 (s.restrict v)<VAR>hsv : Injective (s.restrict v)<VAR>hX✝ : Orthonormal 𝕜 Subtype.val<VAR>Y : Finset E<VAR>b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E<VAR>hX : range (s.restrict v) ⊆ ↑Y<VAR>hb₀ : ⇑b₀ = Subtype.val<GOAL>∃ b, ∀ i ∈ s, b i = v i
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹¹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁸ : NormedAddCommGroup E'<VAR>inst✝⁷ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : InnerProductSpace ℝ F'<VAR>inst✝² : Fintype ι✝<VAR>v✝ : Set E<VAR>A : ι✝ → Submodule 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 E<VAR>ι : Type u_8<VAR>inst✝ : Fintype ι<VAR>card_ι : finrank 𝕜 E = Fintype.card ι<VAR>v : ι → E<VAR>s : Set ι<VAR>hv : Orthonormal 𝕜 (s.restrict v)<VAR>hsv : Injective (s.restrict v)<VAR>hX✝ : Orthonormal 𝕜 Subtype.val<VAR>Y : Finset E<VAR>b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E<VAR>hX : range (s.restrict v) ⊆ ↑Y<VAR>hb₀ : ⇑b₀ = Subtype.val<VAR>hιY : Fintype.card ι = Y.card<GOAL>∃ b, ∀ i ∈ s, b i = v i
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹¹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁸ : NormedAddCommGroup E'<VAR>inst✝⁷ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : InnerProductSpace ℝ F'<VAR>inst✝² : Fintype ι✝<VAR>v✝ : Set E<VAR>A : ι✝ → Submodule 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 E<VAR>ι : Type u_8<VAR>inst✝ : Fintype ι<VAR>card_ι : finrank 𝕜 E = Fintype.card ι<VAR>v : ι → E<VAR>s : Set ι<VAR>hv : Orthonormal 𝕜 (s.restrict v)<VAR>hsv : Injective (s.restrict v)<VAR>hX✝ : Orthonormal 𝕜 Subtype.val<VAR>Y : Finset E<VAR>b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E<VAR>hX : range (s.restrict v) ⊆ ↑Y<VAR>hb₀ : ⇑b₀ = Subtype.val<VAR>hιY : Fintype.card ι = Y.card<VAR>hvsY : MapsTo v s ↑Y<GOAL>∃ b, ∀ i ∈ s, b i = v i
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹¹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁸ : NormedAddCommGroup E'<VAR>inst✝⁷ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : InnerProductSpace ℝ F'<VAR>inst✝² : Fintype ι✝<VAR>v✝ : Set E<VAR>A : ι✝ → Submodule 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 E<VAR>ι : Type u_8<VAR>inst✝ : Fintype ι<VAR>card_ι : finrank 𝕜 E = Fintype.card ι<VAR>v : ι → E<VAR>s : Set ι<VAR>hv : Orthonormal 𝕜 (s.restrict v)<VAR>hsv : Injective (s.restrict v)<VAR>hX✝ : Orthonormal 𝕜 Subtype.val<VAR>Y : Finset E<VAR>b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E<VAR>hX : range (s.restrict v) ⊆ ↑Y<VAR>hb₀ : ⇑b₀ = Subtype.val<VAR>hιY : Fintype.card ι = Y.card<VAR>hvsY : MapsTo v s ↑Y<VAR>hsv' : InjOn v s<GOAL>∃ b, ∀ i ∈ s, b i = v i
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹¹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁸ : NormedAddCommGroup E'<VAR>inst✝⁷ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : InnerProductSpace ℝ F'<VAR>inst✝² : Fintype ι✝<VAR>v✝ : Set E<VAR>A : ι✝ → Submodule 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 E<VAR>ι : Type u_8<VAR>inst✝ : Fintype ι<VAR>card_ι : finrank 𝕜 E = Fintype.card ι<VAR>v : ι → E<VAR>s : Set ι<VAR>hv : Orthonormal 𝕜 (s.restrict v)<VAR>hsv : Injective (s.restrict v)<VAR>hX✝ : Orthonormal 𝕜 Subtype.val<VAR>Y : Finset E<VAR>b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E<VAR>hX : range (s.restrict v) ⊆ ↑Y<VAR>hb₀ : ⇑b₀ = Subtype.val<VAR>hιY : Fintype.card ι = Y.card<VAR>hvsY : MapsTo v s ↑Y<VAR>hsv' : InjOn v s<VAR>g : ι ≃ { x // x ∈ Y }<VAR>hg : ∀ i ∈ s, ↑(g i) = v i<GOAL>∃ b, ∀ i ∈ s, b i = v i
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹¹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁸ : NormedAddCommGroup E'<VAR>inst✝⁷ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : InnerProductSpace ℝ F'<VAR>inst✝² : Fintype ι✝<VAR>v✝ : Set E<VAR>A : ι✝ → Submodule 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 E<VAR>ι : Type u_8<VAR>inst✝ : Fintype ι<VAR>card_ι : finrank 𝕜 E = Fintype.card ι<VAR>v : ι → E<VAR>s : Set ι<VAR>hv : Orthonormal 𝕜 (s.restrict v)<VAR>hsv : Injective (s.restrict v)<VAR>hX✝ : Orthonormal 𝕜 Subtype.val<VAR>Y : Finset E<VAR>b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E<VAR>hX : range (s.restrict v) ⊆ ↑Y<VAR>hb₀ : ⇑b₀ = Subtype.val<VAR>hιY : Fintype.card ι = Y.card<VAR>hvsY : MapsTo v s ↑Y<VAR>hsv' : InjOn v s<VAR>g : ι ≃ { x // x ∈ Y }<VAR>hg : ∀ i ∈ s, ↑(g i) = v i<GOAL>∀ i ∈ s, (b₀.reindex g.symm) i = v i
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R M<VAR>f : Dual R M<VAR>m : M<GOAL>(∑ x : ι, f (b x) • b.coord x) m = f m
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>κ : ι → Sort u_1<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝² : CompleteLattice α<VAR>inst✝¹ : CompleteLattice β<VAR>inst✝ : CompleteLattice γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>l u : α → β → γ<VAR>l₁ u₁ : β → γ → α<VAR>l₂ u₂ : α → γ → β<VAR>h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)<VAR>h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)<GOAL>sSup (image2 l s t) = l (sSup s) (sSup t)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>P : RootPairing ι R M N<VAR>i j : ι<GOAL>P.coxeterWeight i j = P.coxeterWeight j i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>f : α ↪ β<VAR>b✝ : ↑(Set.range ⇑f)<VAR>inst✝ : Nonempty α<VAR>b : β<VAR>h : b ∈ Set.range ⇑f<GOAL>(Set.range ⇑f).restrict (invFun ⇑f) ⟨b, h⟩ = f.invOfMemRange ⟨b, h⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>f : α ↪ β<VAR>b✝ : ↑(Set.range ⇑f)<VAR>inst✝ : Nonempty α<VAR>b : β<VAR>h : b ∈ Set.range ⇑f<GOAL>f ((Set.range ⇑f).restrict (invFun ⇑f) ⟨b, h⟩) = f (f.invOfMemRange ⟨b, h⟩)
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>x y1 y2 : ℕ × K<VAR>H : R K p y1 y2<VAR>n : ℕ<VAR>y : K<GOAL>R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 + (⇑(frobenius K p))^[x.1] (n, y).2) (x.1 + (n + 1, (frobenius K p) y).1, (⇑(frobenius K p))^[(n + 1, (frobenius K p) y).1] x.2 + (⇑(frobenius K p))^[x.1] (n + 1, (frobenius K p) y).2)
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>x y1 y2 : ℕ × K<VAR>H : R K p y1 y2<VAR>n : ℕ<VAR>y : K<GOAL>R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 + (⇑(frobenius K p))^[x.1] (n, y).2) (x.1 + (n + 1, (frobenius K p) y).1, (frobenius K p) ((⇑(frobenius K p))^[n] x.2 + (⇑(frobenius K p))^[x.1] y))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α<VAR>xs : List α<VAR>z : Sym2 α<GOAL>z ∈ (x :: xs).sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α<VAR>xs : List α<VAR>z : Sym2 α<GOAL>z = s(x, x) ∨ (∃ a ∈ xs, s(x, a) = z) ∨ z ∈ xs.sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>r : ℝ<GOAL>⟪x, ↑r • y⟫_𝕜 = r • ⟪x, y⟫_𝕜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a : α<VAR>is l : List α<VAR>H : l ~ [] ++ is → (∃ ts', ∃ (_ : ts' ~ []), l = ts' ++ is) ∨ l ∈ is.permutationsAux []<GOAL>l ~ is → l ∈ is.permutations
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b x a : α<VAR>ha : a ∈ maximals r (s ∪ t)<GOAL>a ∈ maximals r s ∪ maximals r t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b x a : α<VAR>ha : a ∈ maximals r (s ∪ t)<VAR>h : a ∈ s<GOAL>a ∈ maximals r s ∪ maximals r t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b x a : α<VAR>ha : a ∈ maximals r (s ∪ t)<VAR>h : a ∈ t<GOAL>a ∈ maximals r s ∪ maximals r t
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : ¬q = 0<GOAL>((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom ∣ q
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : ¬q = 0<GOAL>q / gcd p q ∣ q
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : ¬q = 0<GOAL>(q / gcd p q).leadingCoeff⁻¹ ≠ 0
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>f : C(X, Y)<GOAL>𝓝 f = ⨅ s, ⨅ (_ : IsCompact s), comap (restrict s) (𝓝 (restrict s f))
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Add α<VAR>b c d : WithTop α<VAR>x y : α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>h : b < c<VAR>a : α<GOAL>b + ↑a < c + ↑a
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Add α<VAR>c d : WithTop α<VAR>x y : α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h' h : ↑b < c<GOAL>↑b + ↑a < c + ↑a
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x<VAR>h : LiftProp P g<GOAL>LiftPropOn P g s
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x<VAR>h : LiftPropOn P g univ<GOAL>LiftPropOn P g s
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>ContinuousAt (fun p => p.1 + p.2) (⊤, ⊤)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), ↑x < a.1 + a.2
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>r : ℝ<VAR>x✝ : EReal × EReal<VAR>h : ↑0 < x✝.1 ∧ ↑r < x✝.2<GOAL>↑r < x✝.1 + x✝.2
<VAR>α β : Type u<GOAL>#α ≤ ℵ₀ ↔ Countable α
<VAR>w : List ℕ<VAR>hw : List.Sorted (fun x x_1 => x ≥ x_1) w<VAR>hpos : ∀ x ∈ w, 0 < x<GOAL>(ofRowLens w hw).rowLens.length = w.length
<VAR>w : List ℕ<VAR>hw : List.Sorted (fun x x_1 => x ≥ x_1) w<VAR>hpos : ∀ x ∈ w, 0 < x<GOAL>¬False ∧ ∀ n < w.length, ∃ (h : n < w.length), 0 < w.get ⟨n, ⋯⟩
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : BoundedOrder α<VAR>a b x : α<VAR>h : IsCompl x ⊥<GOAL>x = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>s t u : Finset α<VAR>a b : α<GOAL>_root_.Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>f : C ⟶ D<VAR>hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)<VAR>n : ι<GOAL>(f ≫ nullHomotopicMap' hom).f n = (nullHomotopicMap' fun i j hij => f.f i ≫ hom i j hij).f n
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>f : C ⟶ D<VAR>hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)<VAR>n : ι<GOAL>(nullHomotopicMap fun i j => f.f i ≫ dite (c.Rel j i) (hom i j) fun x => 0).f n = (nullHomotopicMap' fun i j hij => f.f i ≫ hom i j hij).f n
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H✝ : Subgroup G<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>φ : G →* H<VAR>hφ : Function.Surjective ⇑φ<VAR>M : Subgroup H<VAR>hM : IsCoatom M<GOAL>IsCoatom (comap φ M)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H✝ : Subgroup G<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>φ : G →* H<VAR>hφ : Function.Surjective ⇑φ<VAR>M : Subgroup H<VAR>hM✝ : IsCoatom M<VAR>hM : M ≠ ⊤<GOAL>comap φ M ≠ ⊤
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H✝ : Subgroup G<VAR>H : Type u_2<VAR>inst✝ : Group H<VAR>φ : G →* H<VAR>hφ : Function.Surjective ⇑φ<VAR>M : Subgroup H<VAR>hM✝ : IsCoatom M<VAR>hM : ∀ (b : Subgroup H), M < b → b = ⊤<GOAL>∀ (b : Subgroup G), comap φ M < b → b = ⊤
<VAR>R : Type u_2<VAR>K : Type ?u.68264<VAR>L : Type ?u.68267<VAR>S : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra K L<VAR>x : S<VAR>hx : IsIntegral R x<VAR>inst✝ : Nontrivial S<GOAL>(minpolyDiv R x).natDegree < (minpoly R x).natDegree
<VAR>R : Type u_2<VAR>K : Type ?u.68264<VAR>L : Type ?u.68267<VAR>S : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra K L<VAR>x : S<VAR>hx : IsIntegral R x<VAR>inst✝ : Nontrivial S<GOAL>(minpolyDiv R x).natDegree < (minpolyDiv R x).natDegree + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>δ : Type u_5<VAR>mδ : MeasurableSpace δ<VAR>ξ : Kernel γ δ<VAR>inst✝ : IsSFiniteKernel ξ<VAR>η : Kernel β γ<VAR>κ : Kernel α β<GOAL>ξ ∘ₖ η ∘ₖ κ = ξ ∘ₖ (η ∘ₖ κ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f✝ : β → γ<VAR>g : γ → α<VAR>δ : Type u_5<VAR>mδ : MeasurableSpace δ<VAR>ξ : Kernel γ δ<VAR>inst✝ : IsSFiniteKernel ξ<VAR>η : Kernel β γ<VAR>κ : Kernel α β<VAR>a : α<VAR>f : δ → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (b : δ), f b ∂(ξ ∘ₖ η ∘ₖ κ) a = ∫⁻ (b : δ), f b ∂(ξ ∘ₖ (η ∘ₖ κ)) a
<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 : M<VAR>l : List (List M)<GOAL>l.join.prod = (map prod l).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>h : a ∉ s<GOAL>Multiset.fold op b (Multiset.map f (insert a s).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>s t : Set α<VAR>f g✝ : α → M<VAR>a : α<VAR>g : M → N<VAR>hg : g 1 = 1<GOAL>s.mulIndicator (g ∘ f) = g ∘ s.mulIndicator f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>s t : Set α<VAR>f g✝ : α → M<VAR>a : α<VAR>g : M → N<VAR>hg : g 1 = 1<VAR>x✝ : α<GOAL>s.mulIndicator (g ∘ f) x✝ = (g ∘ s.mulIndicator f) x✝
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝¹ : Traversable t<VAR>inst✝ : LawfulTraversable t<VAR>xs : t α<GOAL>FreeMonoid.toList (foldMap FreeMonoid.of xs) = FreeMonoid.toList (List.reverse (foldMap FreeMonoid.of xs)).reverse
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝¹ : Traversable t<VAR>inst✝ : LawfulTraversable t<VAR>xs : t α<GOAL>FreeMonoid.toList (List.reverse (foldMap FreeMonoid.of xs)).reverse = FreeMonoid.toList (List.foldr cons [] (List.reverse (foldMap FreeMonoid.of xs))).reverse
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝¹ : Traversable t<VAR>inst✝ : LawfulTraversable t<VAR>xs : t α<GOAL>FreeMonoid.toList (List.foldr cons [] (List.reverse (foldMap FreeMonoid.of xs))).reverse = (unop ((Foldl.ofFreeMonoid (flip cons)) (foldMap FreeMonoid.of xs)) []).reverse
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝¹ : Traversable t<VAR>inst✝ : LawfulTraversable t<VAR>xs : t α<GOAL>(unop ((Foldl.ofFreeMonoid (flip cons)) (foldMap FreeMonoid.of xs)) []).reverse = toList xs
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝¹ : Traversable t<VAR>inst✝ : LawfulTraversable t<VAR>xs : t α<GOAL>(unop (foldMap (⇑(Foldl.ofFreeMonoid (flip cons)) ∘ FreeMonoid.of) xs) []).reverse = toList xs
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<GOAL>IsZero T.obj₁ ↔ IsIso T.mor₂
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<GOAL>T.mor₁ = 0 ∧ T.mor₃ = 0 ↔ IsIso T.mor₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrderTop α<VAR>a : α<GOAL>Ioi a ⊆ Ici a
<VAR>n m : ℕ<VAR>a b : Fin n<GOAL>a.succ ≤ b.castSucc ↔ a < b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a b x y : R<VAR>n m : ℕ<VAR>H : 1 ≤ a<GOAL>1 ≤ a ^ 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a b x y : R<VAR>n✝ m : ℕ<VAR>H : 1 ≤ a<VAR>n : ℕ<GOAL>1 ≤ a ^ (n + 1)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a b x y : R<VAR>n✝ m : ℕ<VAR>H : 1 ≤ a<VAR>n : ℕ<GOAL>1 ≤ a * a ^ n
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>C (C 4 * X ^ 3 + C (W.a₁ ^ 2 + 4 * W.a₂) * X ^ 2 + C (2 * (2 * W.a₄ + W.a₁ * W.a₃)) * X + C (W.a₃ ^ 2 + 4 * W.a₆)) = (C (C 2) * Y + C (C W.toAffine.a₁ * X + C W.toAffine.a₃)) ^ 2 - 4 * (Y ^ 2 + C (C W.toAffine.a₁ * X + C W.toAffine.a₃) * Y - C (X ^ 3 + C W.toAffine.a₂ * X ^ 2 + C W.toAffine.a₄ * X + C W.toAffine.a₆))
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>4 * C X ^ 3 + (C (C W.a₁) ^ 2 + 4 * C (C W.a₂)) * C X ^ 2 + 2 * (2 * C (C W.a₄) + C (C W.a₁) * C (C W.a₃)) * C X + (C (C W.a₃) ^ 2 + 4 * C (C W.a₆)) = (2 * Y + (C (C W.toAffine.a₁) * C X + C (C W.toAffine.a₃))) ^ 2 - 4 * (Y ^ 2 + (C (C W.toAffine.a₁) * C X + C (C W.toAffine.a₃)) * Y - (C X ^ 3 + C (C W.toAffine.a₂) * C X ^ 2 + C (C W.toAffine.a₄) * C X + C (C W.toAffine.a₆)))
<VAR>x : ℝ<VAR>n : ℕ<GOAL>sqrtTwoAddSeries 0 (n + 1) < 2
<VAR>x : ℝ<VAR>n : ℕ<GOAL>sqrtTwoAddSeries 0 (n + 1) < √(2 ^ 2)
<VAR>x : ℝ<VAR>n : ℕ<GOAL>sqrtTwoAddSeries 0 n < 2 ^ 2 - 2
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring R₂<VAR>inst✝⁷ : Semiring R₃<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : AddCommMonoid M₃<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₃] M₃<VAR>hg : ker g = ⊥<GOAL>ker (g.comp f) = ker f
<VAR>T : ℝ<VAR>x y : AddCircle T<GOAL>(x + y).toCircle = x.toCircle * y.toCircle
<VAR>T : ℝ<VAR>y : AddCircle T<VAR>z✝ : ℝ<GOAL>(↑z✝ + y).toCircle = toCircle ↑z✝ * y.toCircle
<VAR>T z✝¹ z✝ : ℝ<GOAL>(↑z✝¹ + ↑z✝).toCircle = toCircle ↑z✝¹ * toCircle ↑z✝
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>K L : HomotopyCategory C (ComplexShape.up ℤ)<VAR>f : K ⟶ L<GOAL>quasiIso C (ComplexShape.up ℤ) f ↔ (subcategoryAcyclic C).W f
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num = C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>a : α<VAR>s : Seq α<GOAL>join (ret (f a), Seq.map (ret ∘ f) s) = (f a, Seq.map f s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>a : α<VAR>s : Seq α<GOAL>join ((f a, nil), Seq.map ret (Seq.map f s)) = (f a, Seq.map f s)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝⁵ : Monoid M<VAR>inst✝⁴ : MulAction M α<VAR>inst✝³ : Monoid N<VAR>inst✝² : MulAction M N<VAR>inst✝¹ : IsScalarTower M N N<VAR>inst✝ : SMulCommClass M N N<VAR>r : M<VAR>x : N<VAR>n : ℕ<GOAL>(r • x) ^ (n + 1) = r ^ (n + 1) • x ^ (n + 1)
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ : ↥S<VAR>r' : R<VAR>s' : ↥S<VAR>huv : ↑s' * r₁ = r' * ↑s₂<GOAL>(r₁ /ₒ s₁) • (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>f g : E → 𝕝<VAR>x : E<VAR>fa : AnalyticAt 𝕜 f x<VAR>ga : AnalyticAt 𝕜 g x<VAR>g0 : g x ≠ 0<GOAL>AnalyticAt 𝕜 (fun x => f x / g x) x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>f g : E → 𝕝<VAR>x : E<VAR>fa : AnalyticAt 𝕜 f x<VAR>ga : AnalyticAt 𝕜 g x<VAR>g0 : g x ≠ 0<GOAL>AnalyticAt 𝕜 (fun x => f x * (g x)⁻¹) x