ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>Z : Type u_3<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : TopologicalSpace Z<VAR>proj : Z → B<VAR>inst✝ : Nonempty F<VAR>h : IsHomeomorphicTrivialFiberBundle F proj<GOAL>Function.Surjective proj
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>Z : Type u_3<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : Nonempty F<VAR>e : Z ≃ₜ B × F<VAR>h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ⇑e)<GOAL>Function.Surjective (Prod.fst ∘ ⇑e)
<VAR>K✝ : Type u<VAR>inst✝² : Field K✝<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n : ℕ<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ n<VAR>α a : R<VAR>hn : 0 < n<VAR>e : α ^ n = a<VAR>K : Type u_1 := FractionRing R<VAR>i : R →+* K := algebraMap R K<GOAL>X ^ n - C a = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))
<VAR>K✝ : Type u<VAR>inst✝² : Field K✝<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n : ℕ<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ n<VAR>α a : R<VAR>hn : 0 < n<VAR>e : α ^ n = a<VAR>K : Type u_1 := FractionRing R<VAR>i : R →+* K := algebraMap R K<VAR>h : Function.Injective ⇑(algebraMap R K)<GOAL>X ^ n - C a = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))
<VAR>K✝ : Type u<VAR>inst✝² : Field K✝<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n : ℕ<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ n<VAR>α a : R<VAR>hn : 0 < n<VAR>e : α ^ n = a<VAR>K : Type u_1 := FractionRing R<VAR>i : R →+* K := algebraMap R K<VAR>h : Function.Injective ⇑(algebraMap R K)<GOAL>Polynomial.map i (X ^ n - C a) = Polynomial.map i (∏ i ∈ Finset.range n, (X - C (ζ ^ i * α)))
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>h : x + ↑m ≤ f x<VAR>n : ℕ<GOAL>x + ↑m * (↑n + 1) ≤ (f ^ (n + 1)) x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : 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>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>inst✝¹⁶ : Module R M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : Module R M₂<VAR>inst✝¹³ : AddCommMonoid N₂<VAR>inst✝¹² : Module R N₂<VAR>inst✝¹¹ : DecidableEq n<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : DecidableEq m<VAR>inst✝⁸ : Fintype m<VAR>b₁✝ : Basis n R M₁<VAR>b₂✝ : Basis m R M₂<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>inst✝⁷ : AddCommMonoid M₁'<VAR>inst✝⁶ : Module R M₁'<VAR>inst✝⁵ : AddCommMonoid M₂'<VAR>inst✝⁴ : Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>f : M₁' →ₗ[R] M₁<GOAL>(toMatrix₂ b₁' b₂) (B ∘ₗ f) = ((toMatrix b₁' b₁) f)ᵀ * (toMatrix₂ b₁ b₂) B
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : 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>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>inst✝¹⁶ : Module R M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : Module R M₂<VAR>inst✝¹³ : AddCommMonoid N₂<VAR>inst✝¹² : Module R N₂<VAR>inst✝¹¹ : DecidableEq n<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : DecidableEq m<VAR>inst✝⁸ : Fintype m<VAR>b₁✝ : Basis n R M₁<VAR>b₂✝ : Basis m R M₂<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>inst✝⁷ : AddCommMonoid M₁'<VAR>inst✝⁶ : Module R M₁'<VAR>inst✝⁵ : AddCommMonoid M₂'<VAR>inst✝⁴ : Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>f : M₁' →ₗ[R] M₁<GOAL>((toMatrix b₁' b₁) f)ᵀ * (toMatrix₂ b₁ b₂) B * (toMatrix b₂ b₂) id = ((toMatrix b₁' b₁) f)ᵀ * (toMatrix₂ b₁ b₂) B
<VAR>P : Type u_1<VAR>inst✝¹ : BooleanAlgebra P<VAR>x : P<VAR>I : Ideal P<VAR>inst✝ : I.IsProper<VAR>h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I<GOAL>I.IsPrime
<VAR>P : Type u_1<VAR>inst✝¹ : BooleanAlgebra P<VAR>x : P<VAR>I : Ideal P<VAR>inst✝ : I.IsProper<VAR>h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I<GOAL>∀ {x y : P}, x ⊓ y ∈ I → x ∉ I → y ∈ I
<VAR>P : Type u_1<VAR>inst✝¹ : BooleanAlgebra P<VAR>x✝ : P<VAR>I : Ideal P<VAR>inst✝ : I.IsProper<VAR>h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I<VAR>x y : P<VAR>hxy : x ⊓ y ∈ I<VAR>hxI : x ∉ I<GOAL>y ∈ I
<VAR>P : Type u_1<VAR>inst✝¹ : BooleanAlgebra P<VAR>x✝ : P<VAR>I : Ideal P<VAR>inst✝ : I.IsProper<VAR>h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I<VAR>x y : P<VAR>hxy : x ⊓ y ∈ I<VAR>hxI : x ∉ I<VAR>hxcI : xᶜ ∈ I<GOAL>y ∈ I
<VAR>P : Type u_1<VAR>inst✝¹ : BooleanAlgebra P<VAR>x✝ : P<VAR>I : Ideal P<VAR>inst✝ : I.IsProper<VAR>h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I<VAR>x y : P<VAR>hxy : x ⊓ y ∈ I<VAR>hxI : x ∉ I<VAR>hxcI : xᶜ ∈ I<VAR>ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I<GOAL>y ∈ I
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>inst✝ : CompleteSpace E<VAR>f₁ f₂ : v.FunSpace<VAR>n : ℕ<VAR>d : ℝ<VAR>h : ∀ (t : ↑(Icc v.tMin v.tMax)), dist (f₁.toFun t) (f₂.toFun t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d<VAR>t : ↑(Icc v.tMin v.tMax)<GOAL>dist (f₁.next.toFun t) (f₂.next.toFun t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ (n + 1) / ↑(n + 1)! * d
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>v : PicardLindelof E<VAR>f : v.FunSpace<VAR>inst✝ : CompleteSpace E<VAR>f₁ f₂ : v.FunSpace<VAR>n : ℕ<VAR>d : ℝ<VAR>t : ↑(Icc v.tMin v.tMax)<VAR>h : ∀ (t : ↑(Icc v.tMin v.tMax)), ‖f₁.toFun t - f₂.toFun t‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * d<GOAL>‖∫ (x : ℝ) in Ι ↑v.t₀ ↑t, f₁.vComp x - f₂.vComp x ∂volume‖ ≤ (↑v.L * |↑t - ↑v.t₀|) ^ (n + 1) / ↑(n + 1)! * d
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P Q R : C<VAR>f✝ : P ⟶ Q<VAR>g✝ : Q ⟶ R<VAR>A B A' B' : C<VAR>f : A ⟶ B<VAR>g : A' ⟶ B'<VAR>e : Arrow.mk f ≅ Arrow.mk g<VAR>a✝ : StrongMono f<GOAL>StrongMono g
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P Q R : C<VAR>f✝ : P ⟶ Q<VAR>g✝ : Q ⟶ R<VAR>A B A' B' : C<VAR>f : A ⟶ B<VAR>g : A' ⟶ B'<VAR>e : Arrow.mk f ≅ Arrow.mk g<VAR>a✝ : StrongMono g<GOAL>StrongMono f
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<GOAL>Submodule.span R ↑(invSubmonoid M S) = ⊤
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<GOAL>⊤ ≤ Submodule.span R ↑(invSubmonoid M S)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>x : S<GOAL>x ∈ Submodule.span R ↑(invSubmonoid M S)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>r : R<VAR>m : ↥M<GOAL>r • ↑((toInvSubmonoid M S) m) ∈ Submodule.span R ↑(invSubmonoid M S)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<GOAL>⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1
<VAR>a b : ℕ<VAR>hb : Odd b<GOAL>J(↑a | b) = J(↑a | b % (4 * a))
<VAR>b : ℕ<VAR>hb : Odd b<GOAL>J(↑0 | b) = J(↑0 | b % (4 * 0))
<VAR>a b : ℕ<VAR>hb : Odd b<VAR>ha₀ : a ≠ 0<GOAL>J(↑a | b) = J(↑a | b % (4 * a))
<VAR>a b : ℕ<VAR>hb : Odd b<VAR>ha₀ : a ≠ 0<VAR>hb' : Odd (b % (4 * a))<GOAL>J(↑a | b) = J(↑a | b % (4 * a))
<VAR>a b : ℕ<VAR>hb : Odd b<VAR>ha₀ : a ≠ 0<VAR>hb' : Odd (b % (4 * a))<VAR>e a' : ℕ<VAR>ha₁' : ¬2 ∣ a'<VAR>ha₂ : a = 2 ^ e * a'<GOAL>J(↑a | b) = J(↑a | b % (4 * a))
<VAR>a b : ℕ<VAR>hb : Odd b<VAR>ha₀ : a ≠ 0<VAR>hb' : Odd (b % (4 * a))<VAR>e a' : ℕ<VAR>ha₁' : ¬2 ∣ a'<VAR>ha₂ : a = 2 ^ e * a'<VAR>ha₁ : Odd a'<GOAL>J(↑a | b) = J(↑a | b % (4 * a))
<VAR>a b : ℕ<VAR>hb : Odd b<VAR>ha₀ : a ≠ 0<VAR>hb' : Odd (b % (4 * a))<VAR>e a' : ℕ<VAR>ha₁' : ¬2 ∣ a'<VAR>ha₂ : a = 2 ^ e * a'<VAR>ha₁ : Odd a'<GOAL>J(↑(2 ^ e * a') | b) = J(↑(2 ^ e * a') | b % (4 * a))
<VAR>a b : ℕ<VAR>hb : Odd b<VAR>ha₀ : a ≠ 0<VAR>hb' : Odd (b % (4 * a))<VAR>e a' : ℕ<VAR>ha₁' : ¬2 ∣ a'<VAR>ha₂ : a = 2 ^ e * a'<VAR>ha₁ : Odd a'<GOAL>χ₈ ↑b ^ e * (qrSign b a' * J(↑b | a')) = χ₈ ↑(b % (4 * a)) ^ e * (qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a'))
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁹ : NontriviallyNormedField R<VAR>inst✝⁸ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁷ : (x : B) → Module R (E x)<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace R F<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝² : (x : B) → TopologicalSpace (E x)<VAR>inst✝¹ : FiberBundle F E<VAR>e : Trivialization F TotalSpace.proj<VAR>inst✝ : Trivialization.IsLinear R e<VAR>b : B<GOAL>Continuous ⇑(Trivialization.linearMapAt R e b)
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁹ : NontriviallyNormedField R<VAR>inst✝⁸ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁷ : (x : B) → Module R (E x)<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace R F<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝² : (x : B) → TopologicalSpace (E x)<VAR>inst✝¹ : FiberBundle F E<VAR>e : Trivialization F TotalSpace.proj<VAR>inst✝ : Trivialization.IsLinear R e<VAR>b : B<GOAL>Continuous fun y => if b ∈ e.baseSet then (↑e { proj := b, snd := y }).2 else 0
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁹ : NontriviallyNormedField R<VAR>inst✝⁸ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁷ : (x : B) → Module R (E x)<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace R F<VAR>inst✝⁴ : TopologicalSpace B<VAR>inst✝³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝² : (x : B) → TopologicalSpace (E x)<VAR>inst✝¹ : FiberBundle F E<VAR>e : Trivialization F TotalSpace.proj<VAR>inst✝ : Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<GOAL>Continuous fun y => (↑e { proj := b, snd := y }).2
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.support.Nodup<GOAL>p.edges.Nodup
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R✝ I J X Y R : Set α<VAR>hR : R ⊆ M.E<VAR>hI : (M ↾ R).Base I<GOAL>M.Basis I (M ↾ R).E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>h : Integrable f μ<VAR>c : ℝ≥0<GOAL>Integrable f (c • μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>h : Integrable f μ<VAR>c : ℝ≥0<GOAL>↑ofNNRealHom.toMonoidWithZeroHom c ≠ ⊤
<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>s : Set (β × γ)<VAR>δ : Type u_5<VAR>mδ : MeasurableSpace δ<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : δ → γ<VAR>hf : MeasurableEmbedding f<VAR>a : α<VAR>t : Set (β × δ)<VAR>ht : MeasurableSet t<GOAL>(((κ ⊗ₖ η).comapRight ⋯) a) t = ((κ ⊗ₖ η.comapRight hf) a) t
<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>s : Set (β × γ)<VAR>δ : Type u_5<VAR>mδ : MeasurableSpace δ<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : δ → γ<VAR>hf : MeasurableEmbedding f<VAR>a : α<VAR>t : Set (β × δ)<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ (fun x => (id x.1, f x.2)) '' t} ∂κ a = ∫⁻ (b : β), ((η.comapRight hf) (a, b)) {c | (b, c) ∈ t} ∂κ a
<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>s : Set (β × γ)<VAR>δ : Type u_5<VAR>mδ : MeasurableSpace δ<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : δ → γ<VAR>hf : MeasurableEmbedding f<VAR>a : α<VAR>t : Set (β × δ)<VAR>ht : MeasurableSet t<GOAL>MeasurableSet ((fun x => (id x.1, f x.2)) '' t)
<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>s : Set (β × γ)<VAR>δ : Type u_5<VAR>mδ : MeasurableSpace δ<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : δ → γ<VAR>hf : MeasurableEmbedding f<VAR>a : α<VAR>t : Set (β × δ)<VAR>ht : MeasurableSet t<VAR>b : β<GOAL>(η (a, b)) {c | (b, c) ∈ (fun x => (id x.1, f x.2)) '' t} = ((η.comapRight hf) (a, b)) {c | (b, c) ∈ t}
<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>s : Set (β × γ)<VAR>δ : Type u_5<VAR>mδ : MeasurableSpace δ<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : δ → γ<VAR>hf : MeasurableEmbedding f<VAR>a : α<VAR>t : Set (β × δ)<VAR>ht : MeasurableSet t<VAR>b : β<GOAL>(η (a, b)) {c | ∃ a b_1, (a, b_1) ∈ t ∧ a = b ∧ f b_1 = c} = ((η.comapRight hf) (a, b)) {c | (b, c) ∈ t}
<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>s : Set (β × γ)<VAR>δ : Type u_5<VAR>mδ : MeasurableSpace δ<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : δ → γ<VAR>hf : MeasurableEmbedding f<VAR>a : α<VAR>t : Set (β × δ)<VAR>ht : MeasurableSet t<VAR>b : β<GOAL>(η (a, b)) {c | ∃ a b_1, (a, b_1) ∈ t ∧ a = b ∧ f b_1 = c} = (η (a, b)) (f '' {c | (b, c) ∈ t})
<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>s : Set (β × γ)<VAR>δ : Type u_5<VAR>mδ : MeasurableSpace δ<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : δ → γ<VAR>hf : MeasurableEmbedding f<VAR>a : α<VAR>t : Set (β × δ)<VAR>ht : MeasurableSet t<VAR>b : β<GOAL>MeasurableSet {c | (b, c) ∈ t}
<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>s : Set (β × γ)<VAR>δ : Type u_5<VAR>mδ : MeasurableSpace δ<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : δ → γ<VAR>hf : MeasurableEmbedding f<VAR>a : α<VAR>t : Set (β × δ)<VAR>ht : MeasurableSet t<VAR>b : β<VAR>x : γ<GOAL>x ∈ {c | ∃ a b_1, (a, b_1) ∈ t ∧ a = b ∧ f b_1 = c} ↔ x ∈ f '' {c | (b, c) ∈ t}
<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>s : Set (β × γ)<VAR>δ : Type u_5<VAR>mδ : MeasurableSpace δ<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : δ → γ<VAR>hf : MeasurableEmbedding f<VAR>a : α<VAR>t : Set (β × δ)<VAR>ht : MeasurableSet t<VAR>b : β<VAR>x : γ<GOAL>(∃ a b_1, (a, b_1) ∈ t ∧ a = b ∧ f b_1 = x) ↔ ∃ x_1, (b, x_1) ∈ t ∧ f x_1 = x
<VAR>R✝ : Type u<VAR>L✝ : Type v<VAR>inst✝⁵ : CommRing R✝<VAR>inst✝⁴ : LieRing L✝<VAR>inst✝³ : LieAlgebra R✝ L✝<VAR>H : LieSubalgebra R✝ L✝<VAR>R : Type u<VAR>L : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>I : LieIdeal R L<VAR>x : L<GOAL>x ∈ (lieIdealSubalgebra R L I).normalizer ↔ x ∈ ⊤
<VAR>R : Type u_1<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R p<VAR>hn : ¬p ∣ n<VAR>this : Algebra (ZMod p) R := ZMod.algebra R p<GOAL>cyclotomic (n * p) R = cyclotomic n R ^ (p - 1)
<VAR>R : Type u_1<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R p<VAR>hn : ¬p ∣ n<VAR>this : Algebra (ZMod p) R := ZMod.algebra R p<GOAL>cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1)
<VAR>R : Type u_1<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R p<VAR>hn : ¬p ∣ n<VAR>this : Algebra (ZMod p) R := ZMod.algebra R p<GOAL>(fun x => cyclotomic n (ZMod p) * x) (cyclotomic (n * p) (ZMod p)) = (fun x => cyclotomic n (ZMod p) * x) (cyclotomic n (ZMod p) ^ (p - 1))
<VAR>R : Type u_1<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R p<VAR>hn : ¬p ∣ n<VAR>this : Algebra (ZMod p) R := ZMod.algebra R p<GOAL>cyclotomic n (ZMod p) * cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) * cyclotomic n (ZMod p) ^ (p - 1)
<VAR>R : Type u_1<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R p<VAR>hn : ¬p ∣ n<VAR>this : Algebra (ZMod p) R := ZMod.algebra R p<GOAL>cyclotomic (n * p) (ZMod p) * cyclotomic n (ZMod p) = (expand (ZMod p) p) (cyclotomic n (ZMod p))
<VAR>R : Type u_1<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R p<VAR>hn : ¬p ∣ n<VAR>this : Algebra (ZMod p) R := ZMod.algebra R p<GOAL>cyclotomic (n * p) (ZMod p) * cyclotomic n (ZMod p) = (expand (ZMod p) p) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹³ : Category.{?u.377006, u_1} C<VAR>inst✝¹² : Category.{?u.377010, u_2} D<VAR>inst✝¹¹ : HasShift C ℤ<VAR>inst✝¹⁰ : HasShift D ℤ<VAR>inst✝⁹ : HasZeroObject C<VAR>inst✝⁸ : HasZeroObject D<VAR>inst✝⁷ : Preadditive C<VAR>inst✝⁶ : Preadditive D<VAR>inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝³ : Pretriangulated C<VAR>inst✝² : Pretriangulated D<VAR>X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C<VAR>u₁₂ : X₁ ⟶ X₂<VAR>u₂₃ : X₂ ⟶ X₃<VAR>u₁₃ : X₁ ⟶ X₃<VAR>comm : u₁₂ ≫ u₂₃ = u₁₃<VAR>v₁₂ : X₂ ⟶ Z₁₂<VAR>w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles<VAR>v₂₃ : X₃ ⟶ Z₂₃<VAR>w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂<VAR>h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles<VAR>v₁₃ : X₃ ⟶ Z₁₃<VAR>w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles<VAR>h : Octahedron comm h₁₂ h₂₃ h₁₃<VAR>F : C ⥤ D<VAR>inst✝¹ : F.CommShift ℤ<VAR>inst✝ : F.IsTriangulated<GOAL>F.map u₁₂ ≫ F.map u₂₃ = F.map u₁₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹³ : Category.{?u.377006, u_1} C<VAR>inst✝¹² : Category.{?u.377010, u_2} D<VAR>inst✝¹¹ : HasShift C ℤ<VAR>inst✝¹⁰ : HasShift D ℤ<VAR>inst✝⁹ : HasZeroObject C<VAR>inst✝⁸ : HasZeroObject D<VAR>inst✝⁷ : Preadditive C<VAR>inst✝⁶ : Preadditive D<VAR>inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝³ : Pretriangulated C<VAR>inst✝² : Pretriangulated D<VAR>X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C<VAR>u₁₂ : X₁ ⟶ X₂<VAR>u₂₃ : X₂ ⟶ X₃<VAR>u₁₃ : X₁ ⟶ X₃<VAR>comm : u₁₂ ≫ u₂₃ = u₁₃<VAR>v₁₂ : X₂ ⟶ Z₁₂<VAR>w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles<VAR>v₂₃ : X₃ ⟶ Z₂₃<VAR>w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂<VAR>h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles<VAR>v₁₃ : X₃ ⟶ Z₁₃<VAR>w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles<VAR>h : Octahedron comm h₁₂ h₂₃ h₁₃<VAR>F : C ⥤ D<VAR>inst✝¹ : F.CommShift ℤ<VAR>inst✝ : F.IsTriangulated<GOAL>F.map (Triangle.mk u₁₂ v₁₂ w₁₂).mor₂ ≫ F.map h.m₁ = F.map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₁ ≫ F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹³ : Category.{?u.377006, u_1} C<VAR>inst✝¹² : Category.{?u.377010, u_2} D<VAR>inst✝¹¹ : HasShift C ℤ<VAR>inst✝¹⁰ : HasShift D ℤ<VAR>inst✝⁹ : HasZeroObject C<VAR>inst✝⁸ : HasZeroObject D<VAR>inst✝⁷ : Preadditive C<VAR>inst✝⁶ : Preadditive D<VAR>inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝³ : Pretriangulated C<VAR>inst✝² : Pretriangulated D<VAR>X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C<VAR>u₁₂ : X₁ ⟶ X₂<VAR>u₂₃ : X₂ ⟶ X₃<VAR>u₁₃ : X₁ ⟶ X₃<VAR>comm : u₁₂ ≫ u₂₃ = u₁₃<VAR>v₁₂ : X₂ ⟶ Z₁₂<VAR>w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles<VAR>v₂₃ : X₃ ⟶ Z₂₃<VAR>w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂<VAR>h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles<VAR>v₁₃ : X₃ ⟶ Z₁₃<VAR>w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles<VAR>h : Octahedron comm h₁₂ h₂₃ h₁₃<VAR>F : C ⥤ D<VAR>inst✝¹ : F.CommShift ℤ<VAR>inst✝ : F.IsTriangulated<GOAL>F.map h.m₁ ≫ F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃ ≫ (F.commShiftIso 1).hom.app (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁ = F.map (Triangle.mk u₁₂ v₁₂ w₁₂).mor₃ ≫ (F.commShiftIso 1).hom.app (Triangle.mk u₁₂ v₁₂ w₁₂).obj₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹³ : Category.{?u.377006, u_1} C<VAR>inst✝¹² : Category.{?u.377010, u_2} D<VAR>inst✝¹¹ : HasShift C ℤ<VAR>inst✝¹⁰ : HasShift D ℤ<VAR>inst✝⁹ : HasZeroObject C<VAR>inst✝⁸ : HasZeroObject D<VAR>inst✝⁷ : Preadditive C<VAR>inst✝⁶ : Preadditive D<VAR>inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝³ : Pretriangulated C<VAR>inst✝² : Pretriangulated D<VAR>X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C<VAR>u₁₂ : X₁ ⟶ X₂<VAR>u₂₃ : X₂ ⟶ X₃<VAR>u₁₃ : X₁ ⟶ X₃<VAR>comm : u₁₂ ≫ u₂₃ = u₁₃<VAR>v₁₂ : X₂ ⟶ Z₁₂<VAR>w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles<VAR>v₂₃ : X₃ ⟶ Z₂₃<VAR>w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂<VAR>h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles<VAR>v₁₃ : X₃ ⟶ Z₁₃<VAR>w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles<VAR>h : Octahedron comm h₁₂ h₂₃ h₁₃<VAR>F : C ⥤ D<VAR>inst✝¹ : F.CommShift ℤ<VAR>inst✝ : F.IsTriangulated<GOAL>F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₂ ≫ F.map h.m₃ = F.map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹³ : Category.{?u.377006, u_1} C<VAR>inst✝¹² : Category.{?u.377010, u_2} D<VAR>inst✝¹¹ : HasShift C ℤ<VAR>inst✝¹⁰ : HasShift D ℤ<VAR>inst✝⁹ : HasZeroObject C<VAR>inst✝⁸ : HasZeroObject D<VAR>inst✝⁷ : Preadditive C<VAR>inst✝⁶ : Preadditive D<VAR>inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝³ : Pretriangulated C<VAR>inst✝² : Pretriangulated D<VAR>X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C<VAR>u₁₂ : X₁ ⟶ X₂<VAR>u₂₃ : X₂ ⟶ X₃<VAR>u₁₃ : X₁ ⟶ X₃<VAR>comm : u₁₂ ≫ u₂₃ = u₁₃<VAR>v₁₂ : X₂ ⟶ Z₁₂<VAR>w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles<VAR>v₂₃ : X₃ ⟶ Z₂₃<VAR>w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂<VAR>h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles<VAR>v₁₃ : X₃ ⟶ Z₁₃<VAR>w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁<VAR>h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles<VAR>h : Octahedron comm h₁₂ h₂₃ h₁₃<VAR>F : C ⥤ D<VAR>inst✝¹ : F.CommShift ℤ<VAR>inst✝ : F.IsTriangulated<GOAL>(F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃ ≫ (F.commShiftIso 1).hom.app (Triangle.mk u₁₃ v₁₃ w₁₃).obj₁) ≫ (shiftFunctor D 1).map (F.map (Triangle.mk u₁₂ v₁₂ w₁₂).mor₁) = F.map h.m₃ ≫ F.map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₃ ≫ (F.commShiftIso 1).hom.app (Triangle.mk u₂₃ v₂₃ w₂₃).obj₁
<VAR>α : Type u_1<VAR>inst✝² : Group α<VAR>inst✝¹ : LinearOrder α<VAR>a✝¹ b✝ : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b c a : α<GOAL>(mabs a)⁻¹ ≤ a
<VAR>α : Type u_1<VAR>inst✝² : Group α<VAR>inst✝¹ : LinearOrder α<VAR>a✝¹ b✝ : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b c a : α<VAR>h : 1 ≤ a<GOAL>(mabs a)⁻¹ ≤ a
<VAR>α : Type u_1<VAR>inst✝² : Group α<VAR>inst✝¹ : LinearOrder α<VAR>a✝¹ b✝ : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b c a : α<VAR>h : a ≤ 1<GOAL>(mabs a)⁻¹ ≤ a