ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>h : p.mirror = 0<GOAL>p = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>h : p = 0<GOAL>p.mirror = 0
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M : Matrix m n R<VAR>v : M₁<GOAL>v₂.equivFun.symm ((toLin' M) ⇑(v₁.repr v)) = ∑ j : m, (M *ᵥ ⇑(v₁.repr v)) j • v₂ j
<VAR>a b r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<VAR>x : ℤ<GOAL>x ∈ map castEmbedding (filter (fun x => x ≡ v [MOD r]) (Ioc a b)) ↔ x ∈ filter (fun x => x ≡ ↑v [ZMOD ↑r]) (Ioc ↑a ↑b)
<VAR>a b r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<VAR>x : ℤ<GOAL>(∃ a_1, ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x) ↔ (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : Archimedean 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>a x : 𝕜<VAR>hx : ↑x ≠ ↑a<GOAL>IsOpen {x | (fun x => toIcoMod hp a x = toIocMod hp a x) x}
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝² : Archimedean 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>a x : 𝕜<VAR>hx : ↑x ≠ ↑a<GOAL>IsOpen (⋃ z, Ioo (a + z • p) (a + p + z • p))
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite (IntermediateField F E)<VAR>K : IntermediateField F E<GOAL>∃ α, F⟮α⟯ = K
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite (IntermediateField F E)<VAR>K : IntermediateField F E<VAR>this : FiniteDimensional F E<GOAL>∃ α, F⟮α⟯ = K
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite (IntermediateField F E)<VAR>K : IntermediateField F E<VAR>this : FiniteDimensional F E<VAR>h✝ : Finite F<GOAL>∃ α, F⟮α⟯ = K
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Finite (IntermediateField F E)<VAR>K : IntermediateField F E<VAR>this : FiniteDimensional F E<VAR>h✝ : Infinite F<GOAL>∃ α, F⟮α⟯ = K
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝ : DecidableEq α<VAR>x : Finset α<GOAL>∑ m ∈ x.powerset, (-1) ^ m.card = if x = ∅ then 1 else 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝ : DecidableEq α<VAR>x : Finset α<GOAL>∑ m ∈ range (x.card + 1), x.card.choose m • (-1) ^ m = if x = ∅ then 1 else 0
<VAR>n : ℕ<GOAL>(n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n
<VAR>n : ℕ<GOAL>n * (n + 1) / 2 = n * (n - 1 + 2) / 2
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<GOAL>‖x‖ < 1 ↔ ↑p ∣ x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ x ∈ Ideal.span {↑p ^ 1}<GOAL>‖x‖ < 1 ↔ ↑p ∣ x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ ↑p ∣ x<GOAL>‖x‖ < 1 ↔ ↑p ∣ x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ ↑p ∣ x<GOAL>‖x‖ < 1 ↔ ‖x‖ < ↑p ^ (-↑1 + 1)
<VAR>x : ℝ<GOAL>tan (π / 2 - x) = (tan x)⁻¹
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x✝ y✝ z✝ t✝ : X ⊕ Y<VAR>fA : f ∈ candidates X Y<VAR>x y z t : X ⊕ Y<GOAL>dist (f (x, y)) (f (z, t)) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist (x, y) (z, t)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x✝ y✝ z✝ t✝ : X ⊕ Y<VAR>fA : f ∈ candidates X Y<VAR>x y z t : X ⊕ Y<GOAL>f (x, y) - f (z, t) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist (x, y) (z, t) ∧ f (z, t) - f (x, y) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist (x, y) (z, t)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x✝ y✝ z✝ t✝ : X ⊕ Y<VAR>fA : f ∈ candidates X Y<VAR>x y z t : X ⊕ Y<GOAL>f (z, t) - f (x, y) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist (x, y) (z, t)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x✝ y✝ z✝ t✝ : X ⊕ Y<VAR>fA : f ∈ candidates X Y<VAR>x y z t : X ⊕ Y<GOAL>f (z, t) - f (x, y) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist (z, t) (x, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>c : ℝ<VAR>c_pos : ¬0 < c<GOAL>ball 0 c = Ico 0 c.toNNReal
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G H : OplaxFunctor B C<VAR>η : StrongOplaxNatTrans F G<VAR>θ : StrongOplaxNatTrans G H<VAR>a b c : B<VAR>a' : C<VAR>f : a' ⟶ G.obj a<GOAL>f ◁ (θ.naturality (𝟙 a)).hom ≫ f ◁ θ.app a ◁ H.mapId a = f ◁ G.mapId a ▷ θ.app a ≫ f ◁ (λ_ (θ.app a)).hom ≫ f ◁ (ρ_ (θ.app a)).inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : (s ∩ t).Finite<GOAL>s.encard = t.encard ↔ (s \ t).encard = (t \ s).encard
<VAR>α : Type u_1<VAR>s : Cycle α<VAR>h : s.Nodup<GOAL>s.Nontrivial ↔ ¬s.Subsingleton
<VAR>α : Type u_1<VAR>s : Cycle α<VAR>h : s.Nodup<GOAL>s.Nontrivial ↔ ¬s.length ≤ 1
<VAR>α : Type u_1<VAR>a✝ : List α<VAR>h : Nodup (Quotient.mk'' a✝)<GOAL>Nontrivial (Quotient.mk'' a✝) ↔ ¬length (Quotient.mk'' a✝) ≤ 1
<VAR>α : Type u_1<VAR>a✝ : List α<VAR>h : a✝.Nodup<GOAL>Nontrivial (Quotient.mk'' a✝) ↔ ¬length (Quotient.mk'' a✝) ≤ 1
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : CommSemiring R₁<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H✝ H : B.IsRefl<GOAL>ker B = ⊥ ↔ ker B.flip = ⊥
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : CommSemiring R₁<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H✝ H : B.IsRefl<VAR>h : ker B.flip = ⊥<GOAL>ker B = ⊥
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>hn : n ≠ 0<GOAL>log b (n * b) = log b n + 1
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>hn : n ≠ 0<GOAL>b ^ log b n * b ≤ n * b
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>hn : n ≠ 0<GOAL>n * b < b ^ (log b n + 1) * b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>(𝓝 l).HasBasis p fun i => Iic (𝓟 (s i))
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>(l.lift' (Iic ∘ 𝓟)).HasBasis p fun i => Iic (𝓟 (s i))
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<GOAL>M.Basis' I X ↔ M.Basis I (M.closure X) ∧ I ⊆ X
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<GOAL>M.Basis I (X ∩ M.E) ↔ M.Basis I (M.closure (X ∩ M.E)) ∧ I ⊆ X
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>inst✝ : LinearOrder α<VAR>f : α → β<VAR>a b : α<GOAL>AEMeasurable f (μ.restrict (Ι a b)) ↔ AEMeasurable f (μ.restrict (Ioc a b)) ∧ AEMeasurable f (μ.restrict (Ioc b a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>μ ν : Measure α<VAR>κ : Kernel α β<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((μ + ν).bind ⇑κ) s = (μ.bind ⇑κ + ν.bind ⇑κ) s
<VAR>α : Type u<VAR>s : Set α<VAR>inst✝ : DivisionRing α<GOAL>#(WType (Subfield.Operands s)) ≤ max #↑s ℵ₀
<VAR>α : Type u<VAR>s : Set α<VAR>inst✝ : DivisionRing α<GOAL>max #↑s ℵ₀ = max (lift.{0, u} #(Fin 6 ⊕ ↑s)) ℵ₀
<VAR>α : Type u<VAR>s : Set α<VAR>inst✝ : DivisionRing α<GOAL>∀ (a : Fin 6 ⊕ ↑s), Finite (Subfield.Operands s a)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>d : σ →₀ ℕ<VAR>r : R<VAR>n : ℕ<VAR>hn : d.degree = n<GOAL>((monomial d) r).IsHomogeneous n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>d : σ →₀ ℕ<VAR>r : R<VAR>n : ℕ<VAR>hn : (weight 1) d = n<GOAL>((monomial d) r).IsHomogeneous n
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>inst✝ : (v : V) → Fintype ↑(M.neighborSet v)<GOAL>M.IsPerfectMatching ↔ ∀ (v : V), M.degree v = 1
<VAR>α : Type u<VAR>inst✝² : DecidableEq α<VAR>β : Type v<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nontrivial α<VAR>a : ℤˣ<VAR>h : a = -1<VAR>x y : α<VAR>hxy : x ≠ y<GOAL>sign (swap x y) = a
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g₁ g₂ : Fix F α → β<VAR>h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)<VAR>x : (P F).W α<GOAL>g₁ (Quot.mk Setoid.r x) = g₂ (Quot.mk Setoid.r x)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g₁ g₂ : Fix F α → β<VAR>h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)<VAR>x : (P F).W α<GOAL>∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α), (∀ (i : (P F).last.B a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))) → g₁ (Quot.mk Setoid.r ((P F).wMk a f' f)) = g₂ (Quot.mk Setoid.r ((P F).wMk a f' f))
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g₁ g₂ : Fix F α → β<VAR>h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)<VAR>x : (P F).W α<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f : (P F).last.B a → (P F).W α<VAR>ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))<GOAL>g₁ ⟦(P F).wMk a f' f⟧ = g₂ ⟦(P F).wMk a f' f⟧
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g₁ g₂ : Fix F α → β<VAR>h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)<VAR>x : (P F).W α<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f : (P F).last.B a → (P F).W α<VAR>ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))<GOAL>g₁ (mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩)) = g₂ (mk (abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩))
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g₁ g₂ : Fix F α → β<VAR>h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)<VAR>x : (P F).W α<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f : (P F).last.B a → (P F).W α<VAR>ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))<GOAL>(TypeVec.id ::: g₁) <$$> abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩ = (TypeVec.id ::: g₂) <$$> abs ⟨a, (P F).appendContents f' fun x => ⟦f x⟧⟩
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g₁ g₂ : Fix F α → β<VAR>h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)<VAR>x : (P F).W α<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f : (P F).last.B a → (P F).W α<VAR>ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))<GOAL>abs ⟨a, (TypeVec.id ::: g₁) ⊚ (P F).appendContents f' fun x => ⟦f x⟧⟩ = abs ⟨a, (TypeVec.id ::: g₂) ⊚ (P F).appendContents f' fun x => ⟦f x⟧⟩
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g₁ g₂ : Fix F α → β<VAR>h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)<VAR>x : (P F).W α<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f : (P F).last.B a → (P F).W α<VAR>ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))<GOAL>((TypeVec.id ::: g₁) ⊚ (P F).appendContents f' fun x => ⟦f x⟧) = (TypeVec.id ::: g₂) ⊚ (P F).appendContents f' fun x => ⟦f x⟧
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g₁ g₂ : Fix F α → β<VAR>h : ∀ (x : F (α ::: Fix F α)), (TypeVec.id ::: g₁) <$$> x = (TypeVec.id ::: g₂) <$$> x → g₁ (mk x) = g₂ (mk x)<VAR>x : (P F).W α<VAR>a : (P F).A<VAR>f' : (P F).drop.B a ⟹ α<VAR>f : (P F).last.B a → (P F).W α<VAR>ih : ∀ (i : (P F).last.B a), g₁ (Quot.mk Setoid.r (f i)) = g₂ (Quot.mk Setoid.r (f i))<GOAL>splitFun (TypeVec.id ⊚ f') (g₁ ∘ fun x => ⟦f x⟧) = splitFun (TypeVec.id ⊚ f') (g₂ ∘ fun x => ⟦f x⟧)
<VAR>a x z : ℂ<VAR>hx_re : x.re < 0<VAR>hx_im : 0 < x.im<GOAL>arg =ᶠ[𝓝 x] fun x => Real.arcsin ((-x).im / abs x) + π
<VAR>a x z : ℂ<VAR>hx_re : x.re < 0<VAR>hx_im : 0 < x.im<GOAL>∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im
<VAR>a x z : ℂ<VAR>hx_re : x.re < 0<VAR>hx_im : 0 < x.im<GOAL>IsOpen fun y => y.re < 0 ∧ 0 < y.im
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>inst✝² : Mul α<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : Unique ι<VAR>w : m → α<VAR>v : n → α<VAR>i✝ : m<VAR>j✝ : n<GOAL>vecMulVec w v i✝ j✝ = (col ι w * row ι v) i✝ j✝
<VAR>n₁ n₂ : Int<VAR>d₁ d₂ : Nat<VAR>z₁ : d₁ ≠ 0<VAR>z₂ : d₂ ≠ 0<VAR>num✝ : Int<VAR>den✝ : Nat<VAR>den_nz✝ : den✝ ≠ 0<VAR>reduced✝ : num✝.natAbs.Coprime den✝<VAR>e₁ : normalize n₁ d₁ z₁ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }<GOAL>{ num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } * normalize n₂ d₂ z₂ = normalize (n₁ * n₂) (d₁ * d₂) ⋯
<VAR>n₂ : Int<VAR>d₂ : Nat<VAR>z₂ : d₂ ≠ 0<VAR>num✝ : Int<VAR>den✝ : Nat<VAR>den_nz✝ : den✝ ≠ 0<VAR>reduced✝ : num✝.natAbs.Coprime den✝<VAR>g₁ : Nat<VAR>zg₁ : g₁ ≠ 0<VAR>z₁ : den✝ * g₁ ≠ 0<VAR>e₁ : normalize (num✝ * ↑g₁) (den✝ * g₁) z₁ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }<GOAL>{ num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } * normalize n₂ d₂ z₂ = normalize (num✝ * ↑g₁ * n₂) (den✝ * g₁ * d₂) ⋯
<VAR>n₂ : Int<VAR>d₂ : Nat<VAR>z₂ : d₂ ≠ 0<VAR>num✝¹ : Int<VAR>den✝¹ : Nat<VAR>den_nz✝¹ : den✝¹ ≠ 0<VAR>reduced✝¹ : num✝¹.natAbs.Coprime den✝¹<VAR>g₁ : Nat<VAR>zg₁ : g₁ ≠ 0<VAR>z₁ : den✝¹ * g₁ ≠ 0<VAR>e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }<VAR>num✝ : Int<VAR>den✝ : Nat<VAR>den_nz✝ : den✝ ≠ 0<VAR>reduced✝ : num✝.natAbs.Coprime den✝<VAR>e₂ : normalize n₂ d₂ z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }<GOAL>{ num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ } * { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } = normalize (num✝¹ * ↑g₁ * n₂) (den✝¹ * g₁ * d₂) ⋯
<VAR>num✝¹ : Int<VAR>den✝¹ : Nat<VAR>den_nz✝¹ : den✝¹ ≠ 0<VAR>reduced✝¹ : num✝¹.natAbs.Coprime den✝¹<VAR>g₁ : Nat<VAR>zg₁ : g₁ ≠ 0<VAR>z₁ : den✝¹ * g₁ ≠ 0<VAR>e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }<VAR>num✝ : Int<VAR>den✝ : Nat<VAR>den_nz✝ : den✝ ≠ 0<VAR>reduced✝ : num✝.natAbs.Coprime den✝<VAR>g₂ : Nat<VAR>zg₂ : g₂ ≠ 0<VAR>z₂ : den✝ * g₂ ≠ 0<VAR>e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }<GOAL>{ num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ } * { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } = normalize (num✝¹ * ↑g₁ * (num✝ * ↑g₂)) (den✝¹ * g₁ * (den✝ * g₂)) ⋯
<VAR>num✝¹ : Int<VAR>den✝¹ : Nat<VAR>den_nz✝¹ : den✝¹ ≠ 0<VAR>reduced✝¹ : num✝¹.natAbs.Coprime den✝¹<VAR>g₁ : Nat<VAR>zg₁ : g₁ ≠ 0<VAR>z₁ : den✝¹ * g₁ ≠ 0<VAR>e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }<VAR>num✝ : Int<VAR>den✝ : Nat<VAR>den_nz✝ : den✝ ≠ 0<VAR>reduced✝ : num✝.natAbs.Coprime den✝<VAR>g₂ : Nat<VAR>zg₂ : g₂ ≠ 0<VAR>z₂ : den✝ * g₂ ≠ 0<VAR>e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }<GOAL>normalize (num✝¹ * num✝) (den✝¹ * den✝) ⋯ = normalize (num✝¹ * ↑g₁ * (num✝ * ↑g₂)) (den✝¹ * g₁ * (den✝ * g₂)) ⋯
<VAR>num✝¹ : Int<VAR>den✝¹ : Nat<VAR>den_nz✝¹ : den✝¹ ≠ 0<VAR>reduced✝¹ : num✝¹.natAbs.Coprime den✝¹<VAR>g₁ : Nat<VAR>zg₁ : g₁ ≠ 0<VAR>z₁ : den✝¹ * g₁ ≠ 0<VAR>e₁ : normalize (num✝¹ * ↑g₁) (den✝¹ * g₁) z₁ = { num := num✝¹, den := den✝¹, den_nz := den_nz✝¹, reduced := reduced✝¹ }<VAR>num✝ : Int<VAR>den✝ : Nat<VAR>den_nz✝ : den✝ ≠ 0<VAR>reduced✝ : num✝.natAbs.Coprime den✝<VAR>g₂ : Nat<VAR>zg₂ : g₂ ≠ 0<VAR>z₂ : den✝ * g₂ ≠ 0<VAR>e₂ : normalize (num✝ * ↑g₂) (den✝ * g₂) z₂ = { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }<GOAL>normalize (num✝¹ * num✝ * ↑(g₁ * g₂)) (den✝¹ * den✝ * (g₁ * g₂)) ⋯ = normalize (num✝¹ * ↑g₁ * (num✝ * ↑g₂)) (den✝¹ * g₁ * (den✝ * g₂)) ⋯
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : TopologicalSemiring A<VAR>inst✝⁶ : ContinuousStar A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : Semiring B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : Algebra R B<VAR>x y : A<VAR>hy : y ∈ elementalStarAlgebra R x<VAR>P : (u : A) → u ∈ elementalStarAlgebra R x → Prop<VAR>self : P x ⋯<VAR>star_self : P (star x) ⋯<VAR>algebraMap : ∀ (r : R), P ((_root_.algebraMap R A) r) ⋯<VAR>add : ∀ (u : A) (hu : u ∈ elementalStarAlgebra R x) (v : A) (hv : v ∈ elementalStarAlgebra R x), P u hu → P v hv → P (u + v) ⋯<VAR>mul : ∀ (u : A) (hu : u ∈ elementalStarAlgebra R x) (v : A) (hv : v ∈ elementalStarAlgebra R x), P u hu → P v hv → P (u * v) ⋯<VAR>closure : ∀ (s : Set A) (hs : s ⊆ ↑(elementalStarAlgebra R x)), (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ _root_.closure s), P v ⋯<GOAL>P y hy
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : TopologicalSemiring A<VAR>inst✝⁶ : ContinuousStar A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : Semiring B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : Algebra R B<VAR>x y✝ : A<VAR>hy✝ : y✝ ∈ elementalStarAlgebra R x<VAR>P : (u : A) → u ∈ elementalStarAlgebra R x → Prop<VAR>self : P x ⋯<VAR>star_self : P (star x) ⋯<VAR>algebraMap : ∀ (r : R), P ((_root_.algebraMap R A) r) ⋯<VAR>add : ∀ (u : A) (hu : u ∈ elementalStarAlgebra R x) (v : A) (hv : v ∈ elementalStarAlgebra R x), P u hu → P v hv → P (u + v) ⋯<VAR>mul : ∀ (u : A) (hu : u ∈ elementalStarAlgebra R x) (v : A) (hv : v ∈ elementalStarAlgebra R x), P u hu → P v hv → P (u * v) ⋯<VAR>closure : ∀ (s : Set A) (hs : s ⊆ ↑(elementalStarAlgebra R x)), (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ _root_.closure s), P v ⋯<VAR>y : A<VAR>hy : y ∈ ↑(adjoin R {x})<GOAL>P y ⋯
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : TopologicalSemiring A<VAR>inst✝⁶ : ContinuousStar A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : Semiring B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : Algebra R B<VAR>x y✝ : A<VAR>hy✝¹ : y✝ ∈ elementalStarAlgebra R x<VAR>P : (u : A) → u ∈ elementalStarAlgebra R x → Prop<VAR>self : P x ⋯<VAR>star_self : P (star x) ⋯<VAR>algebraMap : ∀ (r : R), P ((_root_.algebraMap R A) r) ⋯<VAR>add : ∀ (u : A) (hu : u ∈ elementalStarAlgebra R x) (v : A) (hv : v ∈ elementalStarAlgebra R x), P u hu → P v hv → P (u + v) ⋯<VAR>mul : ∀ (u : A) (hu : u ∈ elementalStarAlgebra R x) (v : A) (hv : v ∈ elementalStarAlgebra R x), P u hu → P v hv → P (u * v) ⋯<VAR>closure : ∀ (s : Set A) (hs : s ⊆ ↑(elementalStarAlgebra R x)), (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ _root_.closure s), P v ⋯<VAR>y : A<VAR>hy✝ : y ∈ ↑(adjoin R {x})<VAR>hy : y ∈ Algebra.adjoin R ({x} ∪ star {x})<GOAL>P y ⋯
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b✝ c d b : α<GOAL>b ≤ ⊤ ⇨ a ↔ b ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β → γ<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>s : Set α<VAR>t : Set β<VAR>x✝ : γ<GOAL>x✝ ∈ image2 f s t ↔ x✝ ∈ ⋃ i ∈ s, ⋃ j ∈ t, {f i j}
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁹ : Category.{u_3, u_1} C<VAR>inst✝⁸ : Category.{u_4, u_2} D<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>inst✝⁶ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁵ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝⁴ : F.PreservesZeroMorphisms<VAR>inst✝³ : S₁.HasLeftHomology<VAR>inst✝² : S₂.HasLeftHomology<VAR>inst✝¹ : F.PreservesLeftHomologyOf S₁<VAR>inst✝ : F.PreservesLeftHomologyOf S₂<GOAL>leftHomologyMap' (F.mapShortComplex.map φ) (F.mapShortComplex.obj S₁).leftHomologyData (F.mapShortComplex.obj S₂).leftHomologyData ≫ leftHomologyMap' (𝟙 (S₂.map F)) (S₂.map F).leftHomologyData (S₂.leftHomologyData.map F) = leftHomologyMap' (𝟙 (S₁.map F)) (S₁.map F).leftHomologyData (S₁.leftHomologyData.map F) ≫ F.map (leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>c : Set (Lifts F E K)<VAR>hc : IsChain (fun x x_1 => x ≤ x_1) c<VAR>t : ↑(insert ⊥ c) → IntermediateField F E := fun i => (↑i).carrier<VAR>t' : ↑(insert ⊥ c) → Subalgebra F E := fun i => (t i).toSubalgebra<GOAL>∃ ub, ∀ a ∈ c, a ≤ ub
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>c : Set (Lifts F E K)<VAR>hc✝ : IsChain (fun x x_1 => x ≤ x_1) c<VAR>t : ↑(insert ⊥ c) → IntermediateField F E := fun i => (↑i).carrier<VAR>t' : ↑(insert ⊥ c) → Subalgebra F E := fun i => (t i).toSubalgebra<VAR>hc : IsChain (fun x x_1 => x ≤ x_1) (insert ⊥ c)<GOAL>∃ ub, ∀ a ∈ c, a ≤ ub