ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>q r : ℚ<GOAL>(q - r).num * ↑q.den * ↑r.den = (q.num * ↑r.den - r.num * ↑q.den) * ↑(q - r).den
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp' : p ≠ 2<VAR>n : ℕ<VAR>a : K<VAR>ha : ∀ (b : K), b ^ p ≠ a<GOAL>Irreducible (X ^ p ^ n - C a)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp' : p ≠ 2<VAR>n : ℕ<VAR>a : K<VAR>ha : ∀ (b : K), b ^ p ≠ a<GOAL>∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p ^ n → ∀ (b : K), b ^ p_1 ≠ a
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>hp' : p ≠ 2<VAR>n : ℕ<VAR>a : K<VAR>ha : ∀ (b : K), b ^ p ≠ a<VAR>q : ℕ<VAR>hq : Nat.Prime q<VAR>hq' : q ∣ p ^ n<GOAL>∀ (b : K), b ^ q ≠ a
<VAR>p q : ℕ<VAR>hp0 : p = 0<GOAL>∑ a ∈ Ico 1 (p / 2).succ, a * q / p = (filter (fun x => x.2 * p ≤ x.1 * q) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ)).card
<VAR>p q : ℕ<VAR>hp0 : ¬p = 0<VAR>x : ℕ<VAR>hx : x ∈ Ico 1 (p / 2).succ<GOAL>x * q / p ≤ p / 2 * q / p
<VAR>p q : ℕ<VAR>hp0 : ¬p = 0<VAR>x : ℕ<VAR>hx : x ∈ Ico 1 (p / 2).succ<VAR>this : x ≤ p / 2<GOAL>x * q / p ≤ p / 2 * q / p
<VAR>p q : ℕ<VAR>hp0 : ¬p = 0<GOAL>∑ a ∈ Ico 1 (p / 2).succ, (filter (fun x => x * p ≤ a * q) (Ico 1 (q / 2).succ)).card = (filter (fun x => x.2 * p ≤ x.1 * q) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ)).card
<VAR>p q : ℕ<VAR>hp0 : ¬p = 0<GOAL>((Ico 1 (p / 2).succ).sigma fun a => filter (fun x => x * p ≤ a * q) (Ico 1 (q / 2).succ)).card = (filter (fun x => x.2 * p ≤ x.1 * q) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ)).card
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>r : AdicCauchySequence I R<VAR>x : AdicCauchySequence I M<GOAL>↑r n • Submodule.Quotient.mk (↑x n) = ↑r m • Submodule.Quotient.mk (↑x m)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : H × E<VAR>q : TM<GOAL>p ∈ (chartAt (ModelProd H E) q).target ↔ p.1 ∈ (chartAt H q.proj).target
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : H × E<VAR>q : TM<GOAL>p.1 ∈ (chartAt H q.proj).target ∧ (↑((chartAt H q.proj).prod (PartialEquiv.refl E)).symm p).1 ∈ (chartAt H q.proj).source ↔ p.1 ∈ (chartAt H q.proj).target
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : H × E<VAR>q : TM<GOAL>p.1 ∈ (chartAt H q.proj).target ∧ (↑((chartAt H q.proj).symm.prod (PartialEquiv.refl E).symm) p).1 ∈ (chartAt H q.proj).source ↔ p.1 ∈ (chartAt H q.proj).target
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : OrderTop α<VAR>inst✝ : CompactIccSpace α<GOAL>cocompact α ≤ atBot
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : OrderTop α<VAR>inst✝ : CompactIccSpace α<VAR>x✝ : Set α<VAR>hs : x✝ ∈ atBot<VAR>h✝ : IsEmpty α<GOAL>∃ t, IsCompact t ∧ tᶜ ⊆ x✝
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : OrderTop α<VAR>inst✝ : CompactIccSpace α<VAR>x✝ : Set α<VAR>hs : x✝ ∈ atBot<VAR>h✝ : Nonempty α<GOAL>∃ t, IsCompact t ∧ tᶜ ⊆ x✝
<VAR>S : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>inst✝ : Group G<VAR>a✝ x✝ y✝ a x y b : G<GOAL>b * a * b⁻¹ * (b * x * b⁻¹) = b * y * b⁻¹ * (b * a * b⁻¹) ↔ a * x = y * a
<VAR>S : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>inst✝ : Group G<VAR>a✝ x✝ y✝ a x y b : G<GOAL>b * a * x * b⁻¹ = b * y * a * b⁻¹ ↔ a * x = y * a
<VAR>S : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>inst✝ : Group G<VAR>a✝ x✝ y✝ a x y b : G<GOAL>b * (a * (x * b⁻¹)) = b * (y * (a * b⁻¹)) ↔ a * x = y * a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>inst✝ : DecidableEq β<VAR>b : β<GOAL>(insert b s).sup' ⋯ f = f b ⊔ s.sup' H f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>s : Finset β<VAR>H : s.Nonempty<VAR>f : β → α<VAR>inst✝ : DecidableEq β<VAR>b : β<GOAL>↑((insert b s).sup' ⋯ f) = ↑(f b ⊔ s.sup' H f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Multiset α<VAR>a b : α<VAR>xs : List α<GOAL>s(a, b) ∈ Multiset.sym2 ⟦xs⟧ ↔ a ∈ ⟦xs⟧ ∧ b ∈ ⟦xs⟧
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>hs : Balanced 𝕜 s<VAR>r : 𝕜<VAR>x : E<VAR>θ : ℝ<GOAL>θ ∈ {r_1 | 0 < r_1 ∧ ‖r‖ • x ∈ r_1 • s} ↔ θ ∈ {r_1 | 0 < r_1 ∧ r • x ∈ r_1 • s}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>hs : Balanced 𝕜 s<VAR>r : 𝕜<VAR>x : E<VAR>θ : ℝ<GOAL>θ ∈ {r_1 | 0 < r_1 ∧ ↑‖r‖ • x ∈ r_1 • s} ↔ θ ∈ {r_1 | 0 < r_1 ∧ r • x ∈ r_1 • s}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>hs : Balanced 𝕜 s<VAR>r : 𝕜<VAR>x : E<VAR>θ : ℝ<VAR>hθ : 0 < θ<GOAL>‖↑‖r‖‖ = ‖r‖
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommSemiring R<VAR>q : R[X]<VAR>n : ℕ<VAR>r : R[X]<GOAL>q ^ (n - 1) ∣ derivative (q ^ n * r)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommSemiring R<VAR>q : R[X]<VAR>n : ℕ<VAR>r : R[X]<GOAL>q ^ (n - 1) ∣ C ↑n * q ^ (n - 1) * derivative q * r + q ^ n * derivative r
<VAR>α✝ : Type u_1<VAR>l₁ l₂ : List α✝<VAR>a : α✝<VAR>x✝ : l₁ <:+: l₂<VAR>L₁ L₂ : List α✝<VAR>h : L₁ ++ l₁ ++ L₂ = l₂<GOAL>L₁ ++ l₁ ++ L₂.concat a = l₂.concat a
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>x : ⨁ (i : ι), A i<GOAL>x * 1 = x
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>x : ⨁ (i : ι), A i<GOAL>(mulHom A).flip One.one = AddMonoidHom.id (⨁ (i : ι), A i)
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>x : ⨁ (i : ι), A i<GOAL>∀ (i : ι) (y : A i), ((mulHom A).flip One.one) ((of A i) y) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) y)
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>x : ⨁ (i : ι), A i<VAR>i : ι<VAR>xi : A i<GOAL>((mulHom A).flip ((of A 0) GradedMonoid.GOne.one)) ((of A i) xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)
<VAR>ι : Type u_1<VAR>inst✝³ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → AddCommMonoid (A i)<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GSemiring A<VAR>x : ⨁ (i : ι), A i<VAR>i : ι<VAR>xi : A i<GOAL>(of A (i + 0)) (GradedMonoid.GMul.mul xi GradedMonoid.GOne.one) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p q : R[X]<VAR>inst✝ : DecidableEq R<GOAL>(Multiset.map (fun a => X - C a) p.roots).prod = ∏ a ∈ p.roots.toFinset, (X - C a) ^ rootMultiplicity a p
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>lawful : LawfulMvFunctor F<VAR>α : TypeVec.{u} n<VAR>ι ι' : Type u<VAR>R : ι' → ι' → Prop<VAR>x : F (α ::: ι)<VAR>f g : ι → ι'<VAR>hh : ∀ (x : ι), R (f x) (g x)<VAR>h : ι → { x // uncurry R x } := fun x => ⟨(f x, g x), ⋯⟩<VAR>b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h<VAR>c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹ (fun i => { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) := ofSubtype α.repeatEq ::: _root_.id<GOAL>subtypeVal (α.RelLast' R) ⊚ toSubtype (α.RelLast' R) ⊚ fromAppend1DropLast ⊚ c ⊚ (diagSub ::: h) = ((TypeVec.id ::: f) ⊗' (TypeVec.id ::: g)) ⊚ prod.diag
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>lawful : LawfulMvFunctor F<VAR>α : TypeVec.{u} n<VAR>ι ι' : Type u<VAR>R : ι' → ι' → Prop<VAR>x : F (α ::: ι)<VAR>f g : ι → ι'<VAR>hh : ∀ (x : ι), R (f x) (g x)<VAR>h : ι → { x // uncurry R x } := fun x => ⟨(f x, g x), ⋯⟩<VAR>b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h<VAR>c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹ (fun i => { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) := ofSubtype α.repeatEq ::: _root_.id<GOAL>dropFun (subtypeVal (α.RelLast' R) ⊚ toSubtype (α.RelLast' R) ⊚ fromAppend1DropLast ⊚ c ⊚ (diagSub ::: h)) = dropFun (((TypeVec.id ::: f) ⊗' (TypeVec.id ::: g)) ⊚ prod.diag)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>lawful : LawfulMvFunctor F<VAR>α : TypeVec.{u} n<VAR>ι ι' : Type u<VAR>R : ι' → ι' → Prop<VAR>x : F (α ::: ι)<VAR>f g : ι → ι'<VAR>hh : ∀ (x : ι), R (f x) (g x)<VAR>h : ι → { x // uncurry R x } := fun x => ⟨(f x, g x), ⋯⟩<VAR>b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h<VAR>c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹ (fun i => { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) := ofSubtype α.repeatEq ::: _root_.id<GOAL>lastFun (subtypeVal (α.RelLast' R) ⊚ toSubtype (α.RelLast' R) ⊚ fromAppend1DropLast ⊚ c ⊚ (diagSub ::: h)) = lastFun (((TypeVec.id ::: f) ⊗' (TypeVec.id ::: g)) ⊚ prod.diag)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>lawful : LawfulMvFunctor F<VAR>α : TypeVec.{u} n<VAR>ι ι' : Type u<VAR>R : ι' → ι' → Prop<VAR>x : F (α ::: ι)<VAR>f g : ι → ι'<VAR>hh : ∀ (x : ι), R (f x) (g x)<VAR>h : ι → { x // uncurry R x } := fun x => ⟨(f x, g x), ⋯⟩<VAR>b : α ::: ι ⟹ Subtype_ α.repeatEq ::: { x // uncurry R x } := diagSub ::: h<VAR>c : Subtype_ α.repeatEq ::: { x // uncurry R x } ⟹ (fun i => { x // ofRepeat (α.RelLast' R i.fs x) }) ::: Subtype (uncurry R) := ofSubtype α.repeatEq ::: _root_.id<GOAL>Subtype.val ∘ lastFun c ∘ h = Prod.map f g ∘ lastFun prod.diag
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>↑(hU.fromSpec ⁻¹ᵁ U) = ↑⊤
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>⇑hU.fromSpec.val.base ⁻¹' (⇑hU.fromSpec.val.base '' Set.univ) = Set.univ
<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>(n - m).Coprime m ↔ n.Coprime m
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x✝ y✝ : α<VAR>h : f.IsCycleOn s<VAR>x : α<VAR>hx : x ∈ ⇑g '' s<VAR>y : α<VAR>hy : y ∈ ⇑g '' s<GOAL>(g * f * g⁻¹).SameCycle x y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x✝ y✝ : α<VAR>h : f.IsCycleOn s<VAR>x : α<VAR>hx : x ∈ ⇑g⁻¹ ⁻¹' s<VAR>y : α<VAR>hy : y ∈ ⇑g⁻¹ ⁻¹' s<GOAL>(g * f * g⁻¹).SameCycle x y
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>opcyclesMap' (φ - φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ - opcyclesMap' φ' h₁ h₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>κ : Sort u_6<VAR>r p q : α → α → Prop<VAR>f : ι → Set α<VAR>s t : Set ι<VAR>h₀ : (s ∪ t).PairwiseDisjoint f<VAR>h₁ : ∀ i ∈ s, (f i).Nonempty<VAR>h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i<VAR>i : ι<VAR>hi : i ∈ s<VAR>a : α<VAR>hai : a ∈ f i<GOAL>i ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>κ : Sort u_6<VAR>r p q : α → α → Prop<VAR>f : ι → Set α<VAR>s t : Set ι<VAR>h₀ : (s ∪ t).PairwiseDisjoint f<VAR>h₁ : ∀ i ∈ s, (f i).Nonempty<VAR>h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i<VAR>i : ι<VAR>hi : i ∈ s<VAR>a : α<VAR>hai : a ∈ f i<VAR>j : ι<VAR>hj : j ∈ t<VAR>haj : a ∈ f j<GOAL>i ∈ t
<VAR>K : Type u<VAR>inst✝⁶ : CommRing K<VAR>G₀ : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : CommGroupWithZero G₀<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : MonoidHomClass F R[X] S[X]<VAR>φ : F<VAR>hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰<VAR>hf : Function.Injective ⇑φ<VAR>x y : FractionRing R[X]<VAR>h : (map φ hφ) { toFractionRing := x } = (map φ hφ) { toFractionRing := y }<GOAL>{ toFractionRing := x } = { toFractionRing := y }
<VAR>K : Type u<VAR>inst✝⁶ : CommRing K<VAR>G₀ : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : CommGroupWithZero G₀<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : MonoidHomClass F R[X] S[X]<VAR>φ : F<VAR>hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰<VAR>hf : Function.Injective ⇑φ<VAR>y : FractionRing R[X]<VAR>y✝ : R[X] × ↥R[X]⁰<VAR>h : (map φ hφ) { toFractionRing := Localization.mk y✝.1 y✝.2 } = (map φ hφ) { toFractionRing := y }<GOAL>{ toFractionRing := Localization.mk y✝.1 y✝.2 } = { toFractionRing := y }
<VAR>K : Type u<VAR>inst✝⁶ : CommRing K<VAR>G₀ : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : CommGroupWithZero G₀<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : MonoidHomClass F R[X] S[X]<VAR>φ : F<VAR>hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰<VAR>hf : Function.Injective ⇑φ<VAR>y✝¹ y✝ : R[X] × ↥R[X]⁰<VAR>h : (map φ hφ) { toFractionRing := Localization.mk y✝¹.1 y✝¹.2 } = (map φ hφ) { toFractionRing := Localization.mk y✝.1 y✝.2 }<GOAL>{ toFractionRing := Localization.mk y✝¹.1 y✝¹.2 } = { toFractionRing := Localization.mk y✝.1 y✝.2 }
<VAR>α : Type u_1<VAR>inst✝ : CoheytingAlgebra α<VAR>a✝ b a : α<GOAL>￢∂ a = ⊤
<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✝¹ : SemilatticeSup α<VAR>inst✝ : SemilatticeSup β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<GOAL>IsLUB (l '' {a₁, a₂}) (l a₁ ⊔ l a₂)
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>c : G.Coloring Bool<VAR>u v : α<VAR>p : G.Walk u v<GOAL>Odd p.length ↔ (¬c u = true ↔ c v = true)
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>c : G.Coloring Bool<VAR>u v : α<VAR>p : G.Walk u v<GOAL>¬(c u = true ↔ c v = true) ↔ (¬c u = true ↔ c v = true)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f : CauSeq α abs<VAR>x✝ : f < f<VAR>h : f < f := x✝<GOAL>(f - f).LimZero
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<GOAL>(rightShiftAddEquiv K L n a n' hn').symm 0 = 0
<VAR>α✝ : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α✝ → α✝ → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{u_3}<VAR>α : Type u_3<GOAL>(ord ⟦α⟧).card = ⟦α⟧
<VAR>α✝ : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{u_3}<VAR>α : Type u_3<VAR>r : α → α → Prop<VAR>w✝ : IsWellOrder α r<VAR>e : (#α).ord = type r<GOAL>(ord ⟦α⟧).card = ⟦α⟧
<VAR>r : ℝ<GOAL>r.sign⁻¹ = r.sign
<VAR>r : ℝ<VAR>hn : r.sign = -1<GOAL>r.sign⁻¹ = r.sign
<VAR>r : ℝ<VAR>hz : r.sign = 0<GOAL>r.sign⁻¹ = r.sign
<VAR>r : ℝ<VAR>hp : r.sign = 1<GOAL>r.sign⁻¹ = r.sign
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Dist α<VAR>inst✝ : Dist β<VAR>f g : WithLp 0 (α × β)<GOAL>dist f g = (if dist f.1 g.1 = 0 then 0 else 1) + if dist f.2 g.2 = 0 then 0 else 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : LinearOrderedRing 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>x✝ y✝ : E<VAR>inst✝ : Invertible 2<VAR>x y : E<GOAL>x ∈ [x - y-[𝕜]x + y]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : LinearOrderedRing 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>x✝ y✝ : E<VAR>inst✝ : Invertible 2<VAR>x y : E<GOAL>x = midpoint 𝕜 (x - y) (x + y)
<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>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<GOAL>LinearIndependent 𝕜 v
<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>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<GOAL>∀ (l : ι →₀ 𝕜), (Finsupp.total ι E 𝕜 v) l = 0 → l = 0
<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>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l : ι →₀ 𝕜<VAR>hl : (Finsupp.total ι E 𝕜 v) l = 0<VAR>i : ι<VAR>key : ⟪v i, (Finsupp.total ι E 𝕜 v) l⟫_𝕜 = ⟪v i, 0⟫_𝕜<GOAL>l i = 0 i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>u v : E<GOAL>(reflection (Submodule.span 𝕜 {u})) v = 2 • (⟪u, v⟫_𝕜 / ↑‖u‖ ^ 2) • u - v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>hA' : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ U ⊇ A, IsOpen U ∧ μ U < ⊤ ∧ μ (U \ A) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>hA' : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>U : Set α<VAR>hAU : U ⊇ A<VAR>hUo : IsOpen U<VAR>hU : μ U < μ A + ε<GOAL>∃ U ⊇ A, IsOpen U ∧ μ U < ⊤ ∧ μ (U \ A) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.OuterRegular<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>hA' : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>U : Set α<VAR>hAU : U ⊇ A<VAR>hUo : IsOpen U<VAR>hU : μ U < μ A + ε<GOAL>μ (U \ A) < ε
<VAR>x : ℂ<GOAL>log ((starRingEnd ℂ) x) = if x.arg = π then log x else (starRingEnd ℂ) (log x)
<VAR>x : ℂ<GOAL>↑(Real.log (abs x)) + ↑(if x.arg = π then π else -x.arg) * I = if x.arg = π then ↑(Real.log (abs x)) + ↑x.arg * I else ↑(Real.log (abs x)) + ↑x.arg * (starRingEnd ℂ) I
<VAR>x : ℂ<VAR>hx : ¬x.arg = π<GOAL>↑(Real.log (abs x)) + ↑(-x.arg) * I = ↑(Real.log (abs x)) + ↑x.arg * (starRingEnd ℂ) I
<GOAL>Bornology.cobounded ℤ = atBot ⊔ atTop
<GOAL>comap (fun x => ↑|x|) atTop = comap (Int.cast ∘ abs) atTop
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝³ : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>f f' : 𝕜 → E<VAR>z₀ z₁ : 𝕜<VAR>hcont : ContinuousOn (fun t => f' (z₀ + t • z₁)) (Icc 0 1)<VAR>hderiv : ∀ t ∈ Icc 0 1, HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)<VAR>γ : ℝ → 𝕜 := fun t => z₀ + t • z₁<GOAL>z₁ • ∫ (t : ℝ) in 0 ..1, f' (z₀ + t • z₁) = f (z₀ + z₁) - f z₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝³ : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>f f' : 𝕜 → E<VAR>z₀ z₁ : 𝕜<VAR>hcont : ContinuousOn (fun t => f' (z₀ + t • z₁)) (Icc 0 1)<VAR>hderiv : ∀ t ∈ Icc 0 1, HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)<VAR>γ : ℝ → 𝕜 := fun t => z₀ + t • z₁<VAR>hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1<GOAL>z₁ • ∫ (t : ℝ) in 0 ..1, f' (z₀ + t • z₁) = f (z₀ + z₁) - f z₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝³ : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>f f' : 𝕜 → E<VAR>z₀ z₁ : 𝕜<VAR>hcont : ContinuousOn (fun t => f' (z₀ + t • z₁)) (Icc 0 1)<VAR>hderiv : ∀ t ∈ Icc 0 1, HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)<VAR>γ : ℝ → 𝕜 := fun t => z₀ + t • z₁<VAR>hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1<VAR>hderiv' : ∀ t ∈ [[0, 1]], HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t<GOAL>z₁ • ∫ (t : ℝ) in 0 ..1, f' (z₀ + t • z₁) = f (z₀ + z₁) - f z₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝³ : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>f f' : 𝕜 → E<VAR>z₀ z₁ : 𝕜<VAR>hcont : ContinuousOn (fun t => f' (z₀ + t • z₁)) (Icc 0 1)<VAR>hderiv : ∀ t ∈ Icc 0 1, HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)<VAR>γ : ℝ → 𝕜 := fun t => z₀ + t • z₁<VAR>hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1<VAR>hderiv' : ∀ t ∈ [[0, 1]], HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t<GOAL>z₁ • ∫ (t : ℝ) in 0 ..1, f' (z₀ + t • z₁) = ∫ (y : ℝ) in 0 ..1, z₁ • (f' ∘ γ) y