ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a b c d : α<GOAL>(a / b)⁻¹ = (c / d)⁻¹ ↔ b / a = d / c
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Ring R<VAR>inst✝¹ : Module R M<VAR>S : Submodule R M<VAR>inst✝ : S.IsPrincipal<GOAL>generator S ∈ S
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Ring R<VAR>inst✝¹ : Module R M<VAR>S : Submodule R M<VAR>inst✝ : S.IsPrincipal<GOAL>generator S ∈ span R {generator S}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f g : Perm α<GOAL>f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f g : Perm α<GOAL>f = g → (g.IsCycle ↔ f.IsCycle)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f : Perm α<GOAL>f.IsCycle ↔ f.IsCycle
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝²⁴ : Category.{u_4, u_1} C<VAR>inst✝²³ : Category.{u_6, u_2} D<VAR>inst✝²² : Category.{u_5, u_3} E<VAR>inst✝²¹ : HasShift C ℤ<VAR>inst✝²⁰ : HasShift D ℤ<VAR>inst✝¹⁹ : HasShift E ℤ<VAR>F : C ⥤ D<VAR>inst✝¹⁸ : F.CommShift ℤ<VAR>G : D ⥤ E<VAR>inst✝¹⁷ : G.CommShift ℤ<VAR>inst✝¹⁶ : HasZeroObject C<VAR>inst✝¹⁵ : HasZeroObject D<VAR>inst✝¹⁴ : HasZeroObject E<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : Preadditive D<VAR>inst✝¹¹ : Preadditive E<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁸ : ∀ (n : ℤ), (shiftFunctor E n).Additive<VAR>inst✝⁷ : Pretriangulated C<VAR>inst✝⁶ : Pretriangulated D<VAR>inst✝⁵ : Pretriangulated E<VAR>H : C ⥤ E<VAR>e : F ⋙ G ≅ H<VAR>inst✝⁴ : H.CommShift ℤ<VAR>inst✝³ : H.IsTriangulated<VAR>inst✝² : F.IsTriangulated<VAR>inst✝¹ : F.mapArrow.EssSurj<VAR>inst✝ : NatTrans.CommShift e.hom ℤ<GOAL>G.IsTriangulated
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝²⁴ : Category.{u_4, u_1} C<VAR>inst✝²³ : Category.{u_6, u_2} D<VAR>inst✝²² : Category.{u_5, u_3} E<VAR>inst✝²¹ : HasShift C ℤ<VAR>inst✝²⁰ : HasShift D ℤ<VAR>inst✝¹⁹ : HasShift E ℤ<VAR>F : C ⥤ D<VAR>inst✝¹⁸ : F.CommShift ℤ<VAR>G : D ⥤ E<VAR>inst✝¹⁷ : G.CommShift ℤ<VAR>inst✝¹⁶ : HasZeroObject C<VAR>inst✝¹⁵ : HasZeroObject D<VAR>inst✝¹⁴ : HasZeroObject E<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : Preadditive D<VAR>inst✝¹¹ : Preadditive E<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁸ : ∀ (n : ℤ), (shiftFunctor E n).Additive<VAR>inst✝⁷ : Pretriangulated C<VAR>inst✝⁶ : Pretriangulated D<VAR>inst✝⁵ : Pretriangulated E<VAR>H : C ⥤ E<VAR>e : F ⋙ G ≅ H<VAR>inst✝⁴ : H.CommShift ℤ<VAR>inst✝³ : H.IsTriangulated<VAR>inst✝² : F.IsTriangulated<VAR>inst✝¹ : F.mapArrow.EssSurj<VAR>inst✝ : NatTrans.CommShift e.hom ℤ<VAR>this : (F ⋙ G).IsTriangulated<GOAL>G.IsTriangulated
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.164135, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<VAR>i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂<GOAL>S₁.LeftHomologyData
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.164135, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<VAR>i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂<VAR>wi : i ≫ S₁.g = 0<GOAL>S₁.LeftHomologyData
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.164135, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<VAR>i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂<VAR>wi : i ≫ S₁.g = 0<VAR>hi : IsLimit (KernelFork.ofι i wi)<GOAL>S₁.LeftHomologyData
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.164135, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<VAR>i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂<VAR>wi : i ≫ S₁.g = 0<VAR>hi : IsLimit (KernelFork.ofι i wi)<VAR>f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)<GOAL>S₁.LeftHomologyData
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.164135, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<VAR>i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂<VAR>wi : i ≫ S₁.g = 0<VAR>hi : IsLimit (KernelFork.ofι i wi)<VAR>f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)<VAR>hf' : f' ≫ i = S₁.f<GOAL>S₁.LeftHomologyData
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.164135, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<VAR>i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂<VAR>wi : i ≫ S₁.g = 0<VAR>hi : IsLimit (KernelFork.ofι i wi)<VAR>f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)<VAR>hf' : f' ≫ i = S₁.f<VAR>hf'' : f' = φ.τ₁ ≫ h.f'<GOAL>S₁.LeftHomologyData
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.164135, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<VAR>i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂<VAR>wi : i ≫ S₁.g = 0<VAR>hi : IsLimit (KernelFork.ofι i wi)<VAR>f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)<VAR>hf' : f' ≫ i = S₁.f<VAR>hf'' : f' = φ.τ₁ ≫ h.f'<VAR>wπ : f' ≫ h.π = 0<GOAL>S₁.LeftHomologyData
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.164135, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<VAR>i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂<VAR>wi : i ≫ S₁.g = 0<VAR>hi : IsLimit (KernelFork.ofι i wi)<VAR>f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)<VAR>hf' : f' ≫ i = S₁.f<VAR>hf'' : f' = φ.τ₁ ≫ h.f'<VAR>wπ : f' ≫ h.π = 0<VAR>hπ : IsColimit (CokernelCofork.ofπ h.π wπ)<GOAL>S₁.LeftHomologyData
<VAR>G H : PGame<VAR>e : G ≡r H<VAR>h : G.Impartial<GOAL>H.Impartial
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsSymm α r<GOAL>s.PartiallyWellOrderedOn r ↔ ∀ t ⊆ s, IsAntichain r t → t.Finite
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsSymm α r<GOAL>(∀ t ⊆ s, IsAntichain r t → t.Finite) → s.PartiallyWellOrderedOn r
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsSymm α r<VAR>hs : ∀ t ⊆ s, IsAntichain r t → t.Finite<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s<GOAL>∃ m n, m < n ∧ r (f m) (f n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsSymm α r<VAR>hs : ∀ t ⊆ s, IsAntichain r t → t.Finite<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s<VAR>H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsSymm α r<VAR>hs : ∀ t ⊆ s, IsAntichain r t → t.Finite<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s<VAR>H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)<VAR>m n : ℕ<VAR>hmn : f m = f n<GOAL>m = n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsSymm α r<VAR>hs : ∀ t ⊆ s, IsAntichain r t → t.Finite<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s<VAR>H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)<GOAL>IsAntichain r (range f)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsSymm α r<VAR>hs : ∀ t ⊆ s, IsAntichain r t → t.Finite<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s<VAR>H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)<VAR>m n : ℕ<VAR>hmn : f m ≠ f n<GOAL>rᶜ (f m) (f n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsSymm α r<VAR>hs : ∀ t ⊆ s, IsAntichain r t → t.Finite<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s<VAR>H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)<VAR>m n : ℕ<VAR>hmn : f m ≠ f n<VAR>h : m < n<GOAL>rᶜ (f m) (f n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsSymm α r<VAR>hs : ∀ t ⊆ s, IsAntichain r t → t.Finite<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s<VAR>H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)<VAR>m n : ℕ<VAR>hmn : f m ≠ f n<VAR>h : n < m<GOAL>rᶜ (f m) (f n)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hPz : P z = 0<GOAL>W'.negDblY P = -(P x ^ 2) ^ 3
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : HasCoequalizers C<VAR>𝒢 : Set C<GOAL>IsCodetecting 𝒢 → IsCoseparating 𝒢
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>f p : R[X]<GOAL>(quotQuotEquivComm I f).symm ((Ideal.Quotient.mk (span {(Ideal.Quotient.mk (Ideal.map C I)) f})) ((Ideal.Quotient.mk (Ideal.map C I)) p)) = (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>p : ℝ≥0∞<VAR>f : α → F<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>hp0 : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
<VAR>a b c : Ordinal.{u}<GOAL>a + b ≤ a ♯ b
<VAR>α : Sort u<VAR>β : Sort v<GOAL>¬Uncountable α ↔ Countable α
<VAR>u : Lean.Level<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<GOAL>(↑(Int.negOfNat 1))⁻¹ = ↑(Int.negOfNat 1)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<GOAL>v.intValuationDef 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>n : ℕ<VAR>f : α → Fin n → σ<VAR>h : Primrec₂ f<VAR>a : α<GOAL>(Vector.ofFn fun i => f a i).get = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>n : ℕ<VAR>f : α → Fin n → σ<VAR>h : Primrec₂ f<VAR>a : α<VAR>i : Fin n<GOAL>(Vector.ofFn fun i => f a i).get i = f a i
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>x y : LocalizedModule S M<VAR>m m' : M<VAR>s s' : ↥S<GOAL>mk m s + mk m' s' = mk m' s' + mk m s
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : ContractibleSpace X<GOAL>(ContinuousMap.id X).Nullhomotopic
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : ContractibleSpace X<VAR>hv : X ≃ₕ Unit<GOAL>(ContinuousMap.id X).Nullhomotopic
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : ContractibleSpace X<VAR>hv : X ≃ₕ Unit<GOAL>(ContinuousMap.id X).Homotopic (const X (hv.invFun ()))
<VAR>x : ℤ[i]<GOAL>toComplex (star x) = (starRingEnd ℂ) (toComplex x)
<VAR>x : ℤ[i]<GOAL>{ re := ↑(star x).re, im := ↑(star x).im } = (starRingEnd ℂ) { re := ↑x.re, im := ↑x.im }
<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₁₂' : I₁₂<VAR>h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂<GOAL>K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ K.D₁ c₁₂ i₁₂ i₁₂' = K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ h ≫ 0
<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₁₂' : I₁₂<VAR>h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂<GOAL>K.d₁ c₁₂ i₁ i₂ i₁₂' = 0
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : AddZeroClass β<VAR>inst✝ : ContinuousAdd β<VAR>l : Filter α<VAR>f g : α → β<VAR>hf : l.ZeroAtFilter f<VAR>hg : l.ZeroAtFilter g<GOAL>l.ZeroAtFilter (f + g)
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>hA : CantorScheme.Disjoint A<VAR>x : ℕ → β<VAR>hx : x ∈ (inducedMap A).fst<VAR>y : ℕ → β<VAR>hy : y ∈ (inducedMap A).fst<VAR>hxy : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩<GOAL>⟨x, hx⟩ = ⟨y, hy⟩
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>hA : CantorScheme.Disjoint A<VAR>x : ℕ → β<VAR>hx : x ∈ (inducedMap A).fst<VAR>y : ℕ → β<VAR>hy : y ∈ (inducedMap A).fst<VAR>hxy : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩<GOAL>res ((fun a => ↑a) ⟨x, hx⟩) = res ((fun a => ↑a) ⟨y, hy⟩)
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>hA : CantorScheme.Disjoint A<VAR>x : ℕ → β<VAR>hx : x ∈ (inducedMap A).fst<VAR>y : ℕ → β<VAR>hy : y ∈ (inducedMap A).fst<VAR>hxy : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩<VAR>n : ℕ<VAR>ih : res x n = res y n<GOAL>res x (n + 1) = res y (n + 1)
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>hA : CantorScheme.Disjoint A<VAR>x : ℕ → β<VAR>hx : x ∈ (inducedMap A).fst<VAR>y : ℕ → β<VAR>hy : y ∈ (inducedMap A).fst<VAR>hxy : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩<VAR>n : ℕ<VAR>ih : res x n = res y n<GOAL>x n = y n ∧ res x n = res y n
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>hA : CantorScheme.Disjoint A<VAR>x : ℕ → β<VAR>hx : x ∈ (inducedMap A).fst<VAR>y : ℕ → β<VAR>hy : y ∈ (inducedMap A).fst<VAR>hxy : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩<VAR>n : ℕ<VAR>ih : res x n = res y n<GOAL>x n = y n
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>x : ℕ → β<VAR>hx : x ∈ (inducedMap A).fst<VAR>y : ℕ → β<VAR>hy : y ∈ (inducedMap A).fst<VAR>hxy : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩<VAR>n : ℕ<VAR>ih : res x n = res y n<VAR>hA : ¬x n = y n<GOAL>¬CantorScheme.Disjoint A
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>x : ℕ → β<VAR>hx : x ∈ (inducedMap A).fst<VAR>y : ℕ → β<VAR>hy : y ∈ (inducedMap A).fst<VAR>hxy : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩<VAR>n : ℕ<VAR>ih : res x n = res y n<VAR>hA : ¬x n = y n<GOAL>∃ x x_1 x_2, ¬x_1 = x_2 ∧ ¬_root_.Disjoint (A (x_1 :: x)) (A (x_2 :: x))
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>x : ℕ → β<VAR>hx : x ∈ (inducedMap A).fst<VAR>y : ℕ → β<VAR>hy : y ∈ (inducedMap A).fst<VAR>hxy : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩<VAR>n : ℕ<VAR>ih : res x n = res y n<VAR>hA : ¬x n = y n<GOAL>¬_root_.Disjoint (A (x n :: res x n)) (A (y n :: res x n))
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>x : ℕ → β<VAR>hx : x ∈ (inducedMap A).fst<VAR>y : ℕ → β<VAR>hy : y ∈ (inducedMap A).fst<VAR>hxy : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩<VAR>n : ℕ<VAR>ih : res x n = res y n<VAR>hA : ¬x n = y n<GOAL>∃ x_1 ∈ A (x n :: res x n), x_1 ∈ A (y n :: res x n)
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>x : ℕ → β<VAR>hx : x ∈ (inducedMap A).fst<VAR>y : ℕ → β<VAR>hy : y ∈ (inducedMap A).fst<VAR>hxy : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩<VAR>n : ℕ<VAR>ih : res x n = res y n<VAR>hA : ¬x n = y n<GOAL>(inducedMap A).snd ⟨x, hx⟩ ∈ A (y n :: res x n)
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>x : ℕ → β<VAR>hx : x ∈ (inducedMap A).fst<VAR>y : ℕ → β<VAR>hy : y ∈ (inducedMap A).fst<VAR>hxy : (inducedMap A).snd ⟨x, hx⟩ = (inducedMap A).snd ⟨y, hy⟩<VAR>n : ℕ<VAR>ih : res x n = res y n<VAR>hA : ¬x n = y n<GOAL>(inducedMap A).snd ⟨y, hy⟩ ∈ A (res y n.succ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y✝ z✝ ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>x y z : ℝ≥0∞<VAR>h : x < y + z<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<VAR>this✝ : NeZero y<VAR>this : NeZero z<GOAL>∃ y' z', y' < y ∧ z' < z ∧ x < y' + z'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y✝ z✝ ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>x y z : ℝ≥0∞<VAR>h : x < y + z<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<VAR>this✝ : NeZero y<VAR>this : NeZero z<VAR>A : Tendsto (fun p => p.1 + p.2) (𝓝[<] y ×ˢ 𝓝[<] z) (𝓝 (y + z))<GOAL>∃ y' z', y' < y ∧ z' < z ∧ x < y' + z'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y✝ z✝ ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>x y z : ℝ≥0∞<VAR>h : x < y + z<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<VAR>this✝ : NeZero y<VAR>this : NeZero z<VAR>A : Tendsto (fun p => p.1 + p.2) (𝓝[<] y ×ˢ 𝓝[<] z) (𝓝 (y + z))<VAR>y' z' : ℝ≥0∞<VAR>hx : x < (y', z').1 + (y', z').2<VAR>hy' : (y', z').1 ∈ Iio y<VAR>hz' : (y', z').2 ∈ Iio z<GOAL>∃ y' z', y' < y ∧ z' < z ∧ x < y' + z'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H✝ : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>p : α → Prop<VAR>f : α →₀ M<VAR>hf : ∀ x ∈ f.support, p x<VAR>H : ∀ (x : α), p x → f x = 0<VAR>x : α<GOAL>f x = 0 x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<VAR>h : a = b<GOAL>a / b = 1
<VAR>d : ℤ<VAR>h₀ : d ≠ 0<VAR>a : Solution₁ d<VAR>ha : a.x = 1<GOAL>a = 1
<VAR>d : ℤ<VAR>h₀ : d ≠ 0<VAR>a : Solution₁ d<VAR>ha : a.x = 1<VAR>prop : d * a.y ^ 2 = a.x ^ 2 - 1<GOAL>a = 1
<VAR>d : ℤ<VAR>h₀ : d ≠ 0<VAR>a : Solution₁ d<VAR>ha : a.x = 1<VAR>prop : a.y = 0<GOAL>a = 1
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>X : C<VAR>Y : T.Algebra<VAR>f : X ⟶ T.forget.obj Y<GOAL>T.map (T.map f ≫ Y.a) ≫ Y.a = T.μ.app X ≫ T.map f ≫ Y.a
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>X : C<VAR>Y : T.Algebra<VAR>f : X ⟶ T.forget.obj Y<GOAL>(fun f => T.η.app X ≫ f.f) ((fun f => { f := T.map f ≫ Y.a, h := ⋯ }) f) = f
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>X : C<VAR>Y : T.Algebra<VAR>f : X ⟶ T.forget.obj Y<GOAL>T.η.app X ≫ T.map f ≫ Y.a = f
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>X : C<VAR>Y : T.Algebra<VAR>f : X ⟶ T.forget.obj Y<GOAL>(𝟭 C).map f ≫ 𝟙 Y.A = f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>C : ℝ<VAR>F : ι → ↥(lp E p)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : ↥(lp E p)<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)<GOAL>‖f‖ ≤ C
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>C : ℝ<VAR>F : ι → ↥(lp E p)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : ↥(lp E p)<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)<VAR>i : ι<VAR>hi : ‖F i‖ ≤ C<GOAL>‖f‖ ≤ C
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>C : ℝ<VAR>F : ι → ↥(lp E p)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : ↥(lp E p)<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)<VAR>i : ι<VAR>hi : ‖F i‖ ≤ C<VAR>hC : 0 ≤ C<GOAL>‖f‖ ≤ C
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>C : ℝ<VAR>i : ι<VAR>hC : 0 ≤ C<VAR>_i : Fact (1 ≤ ⊤)<VAR>F : ι → ↥(lp E ⊤)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : ↥(lp E ⊤)<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)<VAR>hi : ‖F i‖ ≤ C<GOAL>‖f‖ ≤ C
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>C : ℝ<VAR>F : ι → ↥(lp E p)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : ↥(lp E p)<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)<VAR>i : ι<VAR>hi : ‖F i‖ ≤ C<VAR>hC : 0 ≤ C<VAR>hp : p < ⊤<GOAL>‖f‖ ≤ C
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p} ℚ K<GOAL>NumberField.discr K = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p} ℚ K<VAR>this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K<GOAL>NumberField.discr K = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p} ℚ K<VAR>this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K<GOAL>(-1) ^ (↑p ^ 0 * (↑p - 1) / 2) * ↑↑p ^ (↑p ^ 0 * ((↑p - 1) * (0 + 1) - 1)) = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p} ℚ K<VAR>this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K<GOAL>↑↑p ^ (↑p - 1 - 1) = ↑↑p ^ (↑p - 2)
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s μ<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<VAR>hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a<VAR>t : Set Ω<VAR>ht_tail : MeasurableSet t<GOAL>μ t = 0 ∨ μ t = 1
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<VAR>hxy : x < y<GOAL>logb b x < logb b y
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<VAR>hxy : x < y<GOAL>log x < log y
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r x y z✝ : R<VAR>a b c : ℍ[R]<VAR>z : ℤ<GOAL>normSq ↑z = ↑z ^ 2
<VAR>x y : ℂ<GOAL>tan (-x) = -tan x