ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : Group G'<VAR>inst✝⁵ : Group G''<VAR>A : Type u_4<VAR>inst✝⁴ : AddGroup A<VAR>M : Type u_5<VAR>S : Type u_6<VAR>inst✝³ : DivInvMonoid M<VAR>inst✝² : SetLike S M<VAR>hSM : SubgroupClass S M<VAR>H✝ K✝ : S<VAR>inst✝¹ : SetLike S G<VAR>inst✝ : SubgroupClass S G<VAR>H K L : S<VAR>h : ↑H ⊆ ↑K ∪ ↑L<GOAL>H ≤ K ∨ H ≤ L
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : Group G'<VAR>inst✝⁵ : Group G''<VAR>A : Type u_4<VAR>inst✝⁴ : AddGroup A<VAR>M : Type u_5<VAR>S : Type u_6<VAR>inst✝³ : DivInvMonoid M<VAR>inst✝² : SetLike S M<VAR>hSM : SubgroupClass S M<VAR>H✝ K✝ : S<VAR>inst✝¹ : SetLike S G<VAR>inst✝ : SubgroupClass S G<VAR>H K L : S<VAR>h : ↑H ⊆ ↑K ∪ ↑L<GOAL>(∃ x ∈ H, x ∉ K) → H ≤ L
<VAR>R : Type uR<VAR>S✝ : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁷ : CommSemiring E✝<VAR>inst✝¹⁶ : Semiring K<VAR>inst✝¹⁵ : SMul F✝ E✝<VAR>inst✝¹⁴ : Algebra E✝ K<VAR>inst✝¹³ : CommSemiring F✝<VAR>inst✝¹² : Algebra F✝ K<VAR>inst✝¹¹ : IsScalarTower F✝ E✝ K<VAR>L✝ : Subalgebra F✝ K<VAR>F : Type u_4<VAR>E : Type u_5<VAR>L : Type u_6<VAR>L' : Type u_7<VAR>inst✝¹⁰ : CommSemiring F<VAR>inst✝⁹ : CommSemiring L<VAR>inst✝⁸ : CommSemiring L'<VAR>inst✝⁷ : Semiring E<VAR>inst✝⁶ : Algebra F L<VAR>inst✝⁵ : Algebra L E<VAR>inst✝⁴ : Algebra F L'<VAR>inst✝³ : Algebra L' E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : IsScalarTower F L E<VAR>inst✝ : IsScalarTower F L' E<VAR>i : L ≃ₐ[F] L'<VAR>hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i<VAR>S : Set E<GOAL>Subalgebra.restrictScalars F (adjoin L S) = Subalgebra.restrictScalars F (adjoin L' S)
<VAR>R : Type uR<VAR>S✝ : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁷ : CommSemiring E✝<VAR>inst✝¹⁶ : Semiring K<VAR>inst✝¹⁵ : SMul F✝ E✝<VAR>inst✝¹⁴ : Algebra E✝ K<VAR>inst✝¹³ : CommSemiring F✝<VAR>inst✝¹² : Algebra F✝ K<VAR>inst✝¹¹ : IsScalarTower F✝ E✝ K<VAR>L✝ : Subalgebra F✝ K<VAR>F : Type u_4<VAR>E : Type u_5<VAR>L : Type u_6<VAR>L' : Type u_7<VAR>inst✝¹⁰ : CommSemiring F<VAR>inst✝⁹ : CommSemiring L<VAR>inst✝⁸ : CommSemiring L'<VAR>inst✝⁷ : Semiring E<VAR>inst✝⁶ : Algebra F L<VAR>inst✝⁵ : Algebra L E<VAR>inst✝⁴ : Algebra F L'<VAR>inst✝³ : Algebra L' E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : IsScalarTower F L E<VAR>inst✝ : IsScalarTower F L' E<VAR>i : L ≃ₐ[F] L'<VAR>hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i<VAR>S : Set E<GOAL>(Subalgebra.restrictScalars F (adjoin L S)).toSubsemiring = (Subalgebra.restrictScalars F (adjoin L' S)).toSubsemiring
<VAR>R : Type uR<VAR>S✝ : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>F✝ : Type u_1<VAR>E✝ : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁷ : CommSemiring E✝<VAR>inst✝¹⁶ : Semiring K<VAR>inst✝¹⁵ : SMul F✝ E✝<VAR>inst✝¹⁴ : Algebra E✝ K<VAR>inst✝¹³ : CommSemiring F✝<VAR>inst✝¹² : Algebra F✝ K<VAR>inst✝¹¹ : IsScalarTower F✝ E✝ K<VAR>L✝ : Subalgebra F✝ K<VAR>F : Type u_4<VAR>E : Type u_5<VAR>L : Type u_6<VAR>L' : Type u_7<VAR>inst✝¹⁰ : CommSemiring F<VAR>inst✝⁹ : CommSemiring L<VAR>inst✝⁸ : CommSemiring L'<VAR>inst✝⁷ : Semiring E<VAR>inst✝⁶ : Algebra F L<VAR>inst✝⁵ : Algebra L E<VAR>inst✝⁴ : Algebra F L'<VAR>inst✝³ : Algebra L' E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : IsScalarTower F L E<VAR>inst✝ : IsScalarTower F L' E<VAR>i : L ≃ₐ[F] L'<VAR>hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i<VAR>S : Set E<GOAL>closure (Set.range ⇑(algebraMap L E) ∪ S) = closure (Set.range ⇑(algebraMap L' E) ∪ S)
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>M' : Type u_3<VAR>N✝ : Type u_4<VAR>N' : Type u_5<VAR>P✝ : Type u_6<VAR>P' : Type u_7<VAR>inst✝¹⁹ : Semiring R✝<VAR>inst✝¹⁸ : AddCommMonoid M✝<VAR>inst✝¹⁷ : AddCommMonoid M'<VAR>inst✝¹⁶ : AddCommMonoid N✝<VAR>inst✝¹⁵ : AddCommMonoid N'<VAR>inst✝¹⁴ : AddCommMonoid P✝<VAR>inst✝¹³ : AddCommMonoid P'<VAR>inst✝¹² : Module R✝ M✝<VAR>inst✝¹¹ : Module R✝ M'<VAR>inst✝¹⁰ : Module R✝ N✝<VAR>inst✝⁹ : Module R✝ N'<VAR>inst✝⁸ : Module R✝ P✝<VAR>inst✝⁷ : Module R✝ P'<VAR>f : M✝ →ₗ[R✝] N✝<VAR>g : N✝ →ₗ[R✝] P✝<VAR>R : Type u_8<VAR>M : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>Q : Submodule R N<GOAL>Exact ⇑Q.subtype ⇑Q.mkQ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>c1✝ : Computation (WSeq α)<VAR>c2✝ : Computation (WSeq β)<VAR>h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝<VAR>S : WSeq α → WSeq β → Prop := fun s t => ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h✝ : S s t<VAR>c1 : Computation (WSeq α)<VAR>c2 : Computation (WSeq β)<VAR>h : Computation.LiftRel (LiftRel R) c1 c2<GOAL>Computation.LiftRel (LiftRelO R S) (flatten c1).destruct (flatten c2).destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>c1✝ : Computation (WSeq α)<VAR>c2✝ : Computation (WSeq β)<VAR>h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝<VAR>S : WSeq α → WSeq β → Prop := fun s t => ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h✝ : S s t<VAR>c1 : Computation (WSeq α)<VAR>c2 : Computation (WSeq β)<VAR>h : Computation.LiftRel (LiftRel R) c1 c2<GOAL>Computation.LiftRel (LiftRelO R S) (c1 >>= destruct) (c2 >>= destruct)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>c1✝ : Computation (WSeq α)<VAR>c2✝ : Computation (WSeq β)<VAR>h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝<VAR>S : WSeq α → WSeq β → Prop := fun s t => ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h✝ : S s t<VAR>c1 : Computation (WSeq α)<VAR>c2 : Computation (WSeq β)<VAR>h : Computation.LiftRel (LiftRel R) c1 c2<GOAL>∀ {a : WSeq α} {b : WSeq β}, LiftRel R a b → Computation.LiftRel (LiftRelO R S) a.destruct b.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>c1✝ : Computation (WSeq α)<VAR>c2✝ : Computation (WSeq β)<VAR>h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝<VAR>S : WSeq α → WSeq β → Prop := fun s t => ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h✝ : S s t<VAR>c1 : Computation (WSeq α)<VAR>c2 : Computation (WSeq β)<VAR>h : Computation.LiftRel (LiftRel R) c1 c2<VAR>a : WSeq α<VAR>b : WSeq β<VAR>ab : LiftRel R a b<GOAL>Computation.LiftRel (LiftRelO R S) a.destruct b.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>c1✝ : Computation (WSeq α)<VAR>c2✝ : Computation (WSeq β)<VAR>h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝<VAR>S : WSeq α → WSeq β → Prop := fun s t => ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h✝ : S s t<VAR>c1 : Computation (WSeq α)<VAR>c2 : Computation (WSeq β)<VAR>h : Computation.LiftRel (LiftRel R) c1 c2<VAR>a : WSeq α<VAR>b : WSeq β<VAR>ab : LiftRel R a b<GOAL>∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R (LiftRel R) a b → LiftRelO R S a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>c1✝ : Computation (WSeq α)<VAR>c2✝ : Computation (WSeq β)<VAR>h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝<VAR>S : WSeq α → WSeq β → Prop := fun s t => ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h✝ : S s t<VAR>c1 : Computation (WSeq α)<VAR>c2 : Computation (WSeq β)<VAR>h : Computation.LiftRel (LiftRel R) c1 c2<VAR>a✝ : WSeq α<VAR>b✝ : WSeq β<VAR>ab : LiftRel R a✝ b✝<VAR>a : Option (α × WSeq α)<VAR>b : Option (β × WSeq β)<GOAL>LiftRelO R (LiftRel R) a b → LiftRelO R S a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>c1✝ : Computation (WSeq α)<VAR>c2✝ : Computation (WSeq β)<VAR>h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝<VAR>S : WSeq α → WSeq β → Prop := fun s t => ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h✝ : S s t<VAR>c1 : Computation (WSeq α)<VAR>c2 : Computation (WSeq β)<VAR>h : Computation.LiftRel (LiftRel R) c1 c2<VAR>a✝ : WSeq α<VAR>b✝ : WSeq β<VAR>ab : LiftRel R a✝ b✝<VAR>a : Option (α × WSeq α)<VAR>b : Option (β × WSeq β)<GOAL>∀ (s : WSeq α) (t : WSeq β), LiftRel R s t → S s t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>c1✝ : Computation (WSeq α)<VAR>c2✝ : Computation (WSeq β)<VAR>h✝² : Computation.LiftRel (LiftRel R) c1✝ c2✝<VAR>S : WSeq α → WSeq β → Prop := fun s t => ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2<VAR>s✝ : WSeq α<VAR>t✝ : WSeq β<VAR>h✝¹ : S s✝ t✝<VAR>c1 : Computation (WSeq α)<VAR>c2 : Computation (WSeq β)<VAR>h✝ : Computation.LiftRel (LiftRel R) c1 c2<VAR>a✝ : WSeq α<VAR>b✝ : WSeq β<VAR>ab : LiftRel R a✝ b✝<VAR>a : Option (α × WSeq α)<VAR>b : Option (β × WSeq β)<VAR>s : WSeq α<VAR>t : WSeq β<VAR>h : LiftRel R s t<GOAL>S s t
<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') (-γ) = -γ.rightShift a n' hn'
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : HasOuterApproxClosed Ω<VAR>inst✝¹ : BorelSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν<GOAL>μ = ν
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : HasOuterApproxClosed Ω<VAR>inst✝¹ : BorelSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν<VAR>key : ∀ {F : Set Ω}, IsClosed F → μ F = ν F<GOAL>μ = ν
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : HasOuterApproxClosed Ω<VAR>inst✝¹ : BorelSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν<VAR>key : ∀ {F : Set Ω}, IsClosed F → μ F = ν F<GOAL>∀ s ∈ {s | IsClosed s}, μ s = ν s
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : HasOuterApproxClosed Ω<VAR>inst✝¹ : BorelSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν<VAR>key : ∀ {F : Set Ω}, IsClosed F → μ F = ν F<GOAL>μ univ = ν univ
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : HasOuterApproxClosed Ω<VAR>inst✝¹ : BorelSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν<VAR>key : ∀ {F : Set Ω}, IsClosed F → μ F = ν F<GOAL>inst✝⁴ = MeasurableSpace.generateFrom {s | IsClosed s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁷ : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁶ : DecidableEq m<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : LinearOrder α<VAR>h : M.BlockTriangular b<GOAL>M.det = ∏ k : α, (M.toSquareBlock b k).det
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁷ : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁶ : DecidableEq m<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : LinearOrder α<VAR>h : M.BlockTriangular b<VAR>a : α<VAR>x✝ : a ∈ univ<VAR>ha : a ∉ image b univ<GOAL>(M.toSquareBlock b a).det = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁷ : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁶ : DecidableEq m<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>inst✝ : LinearOrder α<VAR>h : M.BlockTriangular b<VAR>a : α<VAR>x✝ : a ∈ univ<VAR>ha : a ∉ image b univ<VAR>this : IsEmpty { i // b i = a }<GOAL>(M.toSquareBlock b a).det = 1
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Fintype K<VAR>p✝ : ℕ<VAR>inst✝³ : Fact (Nat.Prime p✝)<VAR>inst✝² : Algebra (ZMod p✝) K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>n : ℕ<VAR>hcard : q = p ^ n<VAR>x : K<GOAL>(frobenius K p ^ n) x = 1 x
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Fintype K<VAR>p✝ : ℕ<VAR>inst✝³ : Fact (Nat.Prime p✝)<VAR>inst✝² : Algebra (ZMod p✝) K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>n : ℕ<VAR>hcard : q = p ^ n<VAR>x : K<GOAL>(frobenius K p ^ n) x = x ^ p ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PolishSpace β<VAR>f : α → β<VAR>hf : ClosedEmbedding f<VAR>this✝ : UpgradedPolishSpace β := upgradePolishSpace β<VAR>this : MetricSpace α := Embedding.comapMetricSpace f ⋯<GOAL>PolishSpace α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PolishSpace β<VAR>f : α → β<VAR>hf : ClosedEmbedding f<VAR>this✝¹ : UpgradedPolishSpace β := upgradePolishSpace β<VAR>this✝ : MetricSpace α := Embedding.comapMetricSpace f ⋯<VAR>this : SecondCountableTopology α<GOAL>PolishSpace α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PolishSpace β<VAR>f : α → β<VAR>hf : ClosedEmbedding f<VAR>this✝² : UpgradedPolishSpace β := upgradePolishSpace β<VAR>this✝¹ : MetricSpace α := Embedding.comapMetricSpace f ⋯<VAR>this✝ : SecondCountableTopology α<VAR>this : CompleteSpace α<GOAL>PolishSpace α
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s s₁ s₂ t t₁ t₂ u : Finset α<VAR>a b c a✝ : α<GOAL>a✝ ∈ s ○ t ↔ a✝ ∈ t ○ s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s s₁ s₂ t t₁ t₂ u : Finset α<VAR>a b c a✝ : α<GOAL>(∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = a✝) ↔ ∃ a ∈ t, ∃ b ∈ s, Disjoint a b ∧ a ⊔ b = a✝
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g✝ : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<VAR>g : D ⟶ E<VAR>n : ι<GOAL>(nullHomotopicMap' hom ≫ g).f n = (nullHomotopicMap' fun i j hij => hom i j hij ≫ g.f j).f n
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g✝ : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)<VAR>g : D ⟶ E<VAR>n : ι<GOAL>(nullHomotopicMap fun i j => (dite (c.Rel j i) (hom i j) fun x => 0) ≫ g.f j).f n = (nullHomotopicMap' fun i j hij => hom i j hij ≫ g.f j).f n
<VAR>α₁ : Type u_2<VAR>β₁ : Type u_1<VAR>inst✝ : DecidableEq α₁<VAR>a✝ : α₁<VAR>e✝ e : Perm β₁<VAR>a a' : α₁<VAR>b : β₁<VAR>h : (prodExtendRight a e) (a', b) ≠ (a', b)<GOAL>a' = a
<VAR>α₁ : Type u_2<VAR>β₁ : Type u_1<VAR>inst✝ : DecidableEq α₁<VAR>a✝ : α₁<VAR>e✝ e : Perm β₁<VAR>a a' : α₁<VAR>b : β₁<VAR>h : a' ≠ a<GOAL>(prodExtendRight a e) (a', b) = (a', b)
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (A i)<VAR>inst✝² : (i : ι) → Module R (A i)<VAR>inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>r s : R<VAR>x y : (i : ι) → A i<GOAL>r • (tprod R) x * s • (tprod R) y = (r * s) • (tprod R) (x * y)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>x : M ∗ N<GOAL>(toProd x).1 = fst x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>x : M ∗ N<GOAL>(toProd x).1 = ((MonoidHom.fst M N).comp toProd) x
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>x y z : M₀<VAR>h : IsUnit x<VAR>h1 : inverse x * y = z<GOAL>y = x * z
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>x y z : M₀<VAR>h : IsUnit x<VAR>h1 : y = x * z<GOAL>inverse x * y = z
<VAR>n : ℕ<VAR>c : ℝ<GOAL>(iteratedDeriv n fun s => rexp (c * s)) = fun s => c ^ n * rexp (c * s)
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCommMonoid μ<VAR>inst✝² : HasAntidiagonal μ<VAR>inst✝¹ : DecidableEq μ<VAR>s✝ : Finset ι<VAR>n✝ : μ<VAR>f✝ : ι →₀ μ<VAR>inst✝ : DecidableEq μ<VAR>a : ι<VAR>s : Finset ι<VAR>h : a ∉ s<VAR>n : μ<VAR>p : μ × μ<VAR>x✝¹ x✝ : { x // x ∈ s.finsuppAntidiag p.2 }<VAR>f : ι →₀ μ<VAR>hf : f ∈ s.finsuppAntidiag p.2<VAR>g : ι →₀ μ<VAR>hg : g ∈ s.finsuppAntidiag p.2<VAR>hfg : (fun f => (↑f).update a p.1) ⟨f, hf⟩ = (fun f => (↑f).update a p.1) ⟨g, hg⟩<GOAL>↑⟨f, hf⟩ = ↑⟨g, hg⟩
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCommMonoid μ<VAR>inst✝² : HasAntidiagonal μ<VAR>inst✝¹ : DecidableEq μ<VAR>s✝ : Finset ι<VAR>n✝ : μ<VAR>f✝ : ι →₀ μ<VAR>inst✝ : DecidableEq μ<VAR>a : ι<VAR>s : Finset ι<VAR>h : a ∉ s<VAR>n : μ<VAR>p : μ × μ<VAR>x✝¹ x✝ : { x // x ∈ s.finsuppAntidiag p.2 }<VAR>f : ι →₀ μ<VAR>hf✝ : f ∈ s.finsuppAntidiag p.2<VAR>g : ι →₀ μ<VAR>hg✝ : g ∈ s.finsuppAntidiag p.2<VAR>hfg : (fun f => (↑f).update a p.1) ⟨f, hf✝⟩ = (fun f => (↑f).update a p.1) ⟨g, hg✝⟩<VAR>hf : s.sum ⇑f = p.2 ∧ f.support ⊆ s<VAR>hg : s.sum ⇑g = p.2 ∧ g.support ⊆ s<GOAL>↑⟨f, hf✝⟩ = ↑⟨g, hg✝⟩
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCommMonoid μ<VAR>inst✝² : HasAntidiagonal μ<VAR>inst✝¹ : DecidableEq μ<VAR>s✝ : Finset ι<VAR>n✝ : μ<VAR>f✝ : ι →₀ μ<VAR>inst✝ : DecidableEq μ<VAR>a : ι<VAR>s : Finset ι<VAR>h : a ∉ s<VAR>n : μ<VAR>p : μ × μ<VAR>x✝¹ x✝ : { x // x ∈ s.finsuppAntidiag p.2 }<VAR>f : ι →₀ μ<VAR>hf✝ : f ∈ s.finsuppAntidiag p.2<VAR>g : ι →₀ μ<VAR>hg✝ : g ∈ s.finsuppAntidiag p.2<VAR>hf : s.sum ⇑f = p.2 ∧ f.support ⊆ s<VAR>hg : s.sum ⇑g = p.2 ∧ g.support ⊆ s<VAR>hfg : ∀ (x : ι), (f.update a p.1) x = (g.update a p.1) x<GOAL>∀ (x : ι), f x = g x
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCommMonoid μ<VAR>inst✝² : HasAntidiagonal μ<VAR>inst✝¹ : DecidableEq μ<VAR>s✝ : Finset ι<VAR>n✝ : μ<VAR>f✝ : ι →₀ μ<VAR>inst✝ : DecidableEq μ<VAR>a : ι<VAR>s : Finset ι<VAR>h : a ∉ s<VAR>n : μ<VAR>p : μ × μ<VAR>x✝¹ x✝ : { x // x ∈ s.finsuppAntidiag p.2 }<VAR>f : ι →₀ μ<VAR>hf✝ : f ∈ s.finsuppAntidiag p.2<VAR>g : ι →₀ μ<VAR>hg✝ : g ∈ s.finsuppAntidiag p.2<VAR>hf : s.sum ⇑f = p.2 ∧ f.support ⊆ s<VAR>hg : s.sum ⇑g = p.2 ∧ g.support ⊆ s<VAR>hfg : ∀ (x : ι), (f.update a p.1) x = (g.update a p.1) x<VAR>x : ι<GOAL>f x = g x
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCommMonoid μ<VAR>inst✝² : HasAntidiagonal μ<VAR>inst✝¹ : DecidableEq μ<VAR>s✝ : Finset ι<VAR>n✝ : μ<VAR>f✝ : ι →₀ μ<VAR>inst✝ : DecidableEq μ<VAR>s : Finset ι<VAR>n : μ<VAR>p : μ × μ<VAR>x✝¹ x✝ : { x // x ∈ s.finsuppAntidiag p.2 }<VAR>f : ι →₀ μ<VAR>hf✝ : f ∈ s.finsuppAntidiag p.2<VAR>g : ι →₀ μ<VAR>hg✝ : g ∈ s.finsuppAntidiag p.2<VAR>hf : s.sum ⇑f = p.2 ∧ f.support ⊆ s<VAR>hg : s.sum ⇑g = p.2 ∧ g.support ⊆ s<VAR>x : ι<VAR>h : x ∉ s<VAR>hfg : ∀ (x_1 : ι), (f.update x p.1) x_1 = (g.update x p.1) x_1<GOAL>f x = g x
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCommMonoid μ<VAR>inst✝² : HasAntidiagonal μ<VAR>inst✝¹ : DecidableEq μ<VAR>s✝ : Finset ι<VAR>n✝ : μ<VAR>f✝ : ι →₀ μ<VAR>inst✝ : DecidableEq μ<VAR>a : ι<VAR>s : Finset ι<VAR>h : a ∉ s<VAR>n : μ<VAR>p : μ × μ<VAR>x✝¹ x✝ : { x // x ∈ s.finsuppAntidiag p.2 }<VAR>f : ι →₀ μ<VAR>hf✝ : f ∈ s.finsuppAntidiag p.2<VAR>g : ι →₀ μ<VAR>hg✝ : g ∈ s.finsuppAntidiag p.2<VAR>hf : s.sum ⇑f = p.2 ∧ f.support ⊆ s<VAR>hg : s.sum ⇑g = p.2 ∧ g.support ⊆ s<VAR>hfg : ∀ (x : ι), (f.update a p.1) x = (g.update a p.1) x<VAR>x : ι<VAR>hx : x ≠ a<GOAL>f x = g x
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCommMonoid μ<VAR>inst✝² : HasAntidiagonal μ<VAR>inst✝¹ : DecidableEq μ<VAR>s✝ : Finset ι<VAR>n✝ : μ<VAR>f✝ : ι →₀ μ<VAR>inst✝ : DecidableEq μ<VAR>a : ι<VAR>s : Finset ι<VAR>h : a ∉ s<VAR>n : μ<VAR>f : ι →₀ μ<GOAL>f ∈ (insert a s).finsuppAntidiag n ↔ f ∈ (antidiagonal n).biUnion fun p => map { toFun := fun f => (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCommMonoid μ<VAR>inst✝² : HasAntidiagonal μ<VAR>inst✝¹ : DecidableEq μ<VAR>s✝ : Finset ι<VAR>n✝ : μ<VAR>f✝ : ι →₀ μ<VAR>inst✝ : DecidableEq μ<VAR>a : ι<VAR>s : Finset ι<VAR>h : a ∉ s<VAR>n : μ<VAR>f : ι →₀ μ<GOAL>(∃ m ∈ antidiagonal n, ∃ g, f = g.update a m.1 ∧ g ∈ s.finsuppAntidiag m.2) ↔ ∃ a_1 ∈ antidiagonal n, f ∈ map { toFun := fun f => (↑f).update a a_1.1, inj' := ⋯ } (s.finsuppAntidiag a_1.2).attach
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>b : β<VAR>hu : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h : b < limsup u f<GOAL>∃ᶠ (x : α) in f, b < u x
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>b : β<VAR>hu : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h : ¬∃ᶠ (x : α) in f, b < u x<GOAL>limsup u f ≤ b
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u : α → β<VAR>b : β<VAR>hu : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h : ¬∃ᶠ (x : α) in f, b < u x<GOAL>∀ᶠ (n : β) in map u f, n ≤ b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<GOAL>TendstoLocallyUniformlyOn F f p s ↔ TendstoLocallyUniformly (fun i x => F i ↑x) (f ∘ Subtype.val) p
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<GOAL>(∀ (x : { a // a ∈ s }), Tendsto ((fun y => (f y.2, F y.1 y.2)) ∘ Prod.map id Subtype.val) (p ×ˢ 𝓝 x) (𝓤 β)) ↔ ∀ (x : ↑s), Tendsto (fun y => ((f ∘ Subtype.val) y.2, F y.1 ↑y.2)) (p ×ˢ 𝓝 x) (𝓤 β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>f✝ g✝ : α → β<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : TopologicalAddGroup β<VAR>f g f' : α → β<VAR>hf'_meas : StronglyMeasurable f'<VAR>hf_ae : f =ᶠ[ae μ] f'<VAR>g' : α → β<VAR>hg'_meas : StronglyMeasurable g'<VAR>hg_ae : g =ᶠ[ae μ] g'<GOAL>AEStronglyMeasurable' m (f - g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>f✝ g✝ : α → β<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : TopologicalAddGroup β<VAR>f g f' : α → β<VAR>hf'_meas : StronglyMeasurable f'<VAR>hf_ae : f =ᶠ[ae μ] f'<VAR>g' : α → β<VAR>hg'_meas : StronglyMeasurable g'<VAR>hg_ae : g =ᶠ[ae μ] g'<VAR>x : α<VAR>hx1 : g x = g' x<VAR>hx2 : f x = f' x<GOAL>(f - g) x = (f' - g') x